theory DetSchedSchedule_AI

lemma schedule_valid_sched:
  "\<lbrace>valid_sched and valid_idle\<rbrace> schedule \<lbrace>\<lambda>_. valid_sched\<rbrace>" unfolding schedule_def supply ethread_get_wp[wp del] apply (wp, wpc) 
         (* resume_cur_thread *)
          apply wp prefer 2 
        (* choose new thread *)
         apply (wp schedule_choose_new_thread_valid_sched tcb_sched_action_enqueue_valid_blocked
                   tcb_sched_enqueue_cur_ct_in_q) 
       (* switch_thread candidate *)
        apply (rename_tac candidate) apply (wp del: when_wp
                  add: set_scheduler_action_rct_valid_sched schedule_choose_new_thread_valid_sched) apply (rule hoare_vcg_conj_lift) apply (rule_tac t=candidate in set_scheduler_action_cnt_valid_blocked') apply (wp tcb_sched_action_enqueue_valid_blocked tcb_sched_enqueue_ct_in_q enqueue_thread_queued)+ apply (wp schedule_choose_new_thread_valid_sched)+ apply (rule hoare_vcg_conj_lift) apply (rule_tac t=candidate in set_scheduler_action_cnt_valid_blocked') apply (wp tcb_sched_action_append_valid_blocked tcb_sched_append_ct_in_q
                         append_thread_queued set_scheduler_action_rct_switch_thread_valid_sched
                         guarded_switch_to_lift switch_to_thread_valid_sched
                         stt_activatable[simplified ct_in_state_def]
                         hoare_disjI1[OF switch_to_thread_cur_in_cur_domain]
                         switch_to_thread_sched_act_is_cur)+ 
           (* discard result of fastfail calculation *)
            apply (wpsimp wp: hoare_drop_imp)+ apply (strengthen valid_blocked_valid_blocked_except) apply (wp tcb_sched_action_enqueue_valid_blocked tcb_sched_enqueue_cur_ct_in_q gts_wp)+ apply (clarsimp simp: valid_sched_def valid_sched_action_def weak_valid_sched_action_def
                        switch_in_cur_domain_def) apply (safe ; (fastforce elim: st_tcb_at_opeqI
                 | fastforce simp: valid_sched_def valid_blocked_def valid_blocked_except_def
                                   valid_sched_action_def weak_valid_sched_action_def
                                   switch_in_cur_domain_def ct_in_q_def ct_not_in_q_def
                                   st_tcb_at_def obj_at_def)?) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched and valid_idle\<rbrace> schedule \<lbrace>\<lambda>_. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched and valid_idle\<rbrace> do ct <- gets cur_thread;
ct_st <- get_thread_state ct;
ct_runnable <- return $ runnable ct_st;
action <- gets scheduler_action;
case action of resume_cur_thread \<Rightarrow> do id <- gets idle_thread;
assert (ct_runnable \<or> ct = id);
return ()
od | switch_thread candidate \<Rightarrow> do when ct_runnable (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 ct_runnable \<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 | choose_new_thread \<Rightarrow> do when ct_runnable (tcb_sched_action tcb_sched_enqueue ct);
schedule_choose_new_thread
od
od \<lbrace>\<lambda>_. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched and valid_idle\<rbrace> do ct <- gets cur_thread;
ct_st <- get_thread_state ct;
ct_runnable <- return $ runnable ct_st;
action <- gets scheduler_action;
case action of resume_cur_thread \<Rightarrow> do id <- gets idle_thread;
assert (ct_runnable \<or> ct = id);
return ()
od | switch_thread candidate \<Rightarrow> do when ct_runnable (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 ct_runnable \<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 | choose_new_thread \<Rightarrow> do when ct_runnable (tcb_sched_action tcb_sched_enqueue ct);
schedule_choose_new_thread
od
od \<lbrace>\<lambda>_. valid_sched\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>ct ct_st ct_runnable action. action = resume_cur_thread \<Longrightarrow> \<lbrace>?R13 ct ct_st ct_runnable action\<rbrace> do id <- gets idle_thread;
assert (ct_runnable \<or> ct = id);
return ()
od \<lbrace>\<lambda>_. valid_sched\<rbrace>
 2. \<And>ct ct_st ct_runnable action x2. action = switch_thread x2 \<Longrightarrow> \<lbrace>?R12 ct ct_st ct_runnable action x2\<rbrace> do when ct_runnable (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 tcb_sched_action tcb_sched_enqueue x2;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if ct_runnable \<and> ct_prio = target_prio then do tcb_sched_action tcb_sched_append x2;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do guarded_switch_to x2;
set_scheduler_action resume_cur_thread
od
od \<lbrace>\<lambda>_. valid_sched\<rbrace>
 3. \<And>ct ct_st ct_runnable action. action = choose_new_thread \<Longrightarrow> \<lbrace>?R10 ct ct_st ct_runnable action\<rbrace> do when ct_runnable (tcb_sched_action tcb_sched_enqueue ct);
schedule_choose_new_thread
od \<lbrace>\<lambda>_. valid_sched\<rbrace>
 4. \<And>ct ct_st ct_runnable. \<lbrace>?B3 ct ct_st ct_runnable\<rbrace> gets scheduler_action \<lbrace>\<lambda>action s. (action = resume_cur_thread \<longrightarrow> ?R13 ct ct_st ct_runnable action s) \<and> (\<forall>x. action = switch_thread x \<longrightarrow> ?R12 ct ct_st ct_runnable action x s) \<and> (action = choose_new_thread \<longrightarrow> ?R10 ct ct_st ct_runnable action s)\<rbrace>
 5. \<And>ct ct_st. \<lbrace>?B2 ct ct_st\<rbrace> return $ runnable ct_st \<lbrace>?B3 ct ct_st\<rbrace>
 6. \<And>ct. \<lbrace>?B1 ct\<rbrace> get_thread_state ct \<lbrace>?B2 ct\<rbrace>
 7. \<lbrace>?Q\<rbrace> gets cur_thread \<lbrace>?B1\<rbrace>
 8. \<And>s. (valid_sched and valid_idle) s \<Longrightarrow> ?Q s proof (prove)
goal (8 subgoals):
 1. \<And>ct ct_st ct_runnable action. action = resume_cur_thread \<Longrightarrow> \<lbrace>?R13 ct ct_st ct_runnable action\<rbrace> do id <- gets idle_thread;
assert (ct_runnable \<or> ct = id);
return ()
od \<lbrace>\<lambda>_. valid_sched\<rbrace>
 2. \<And>ct ct_st ct_runnable action x2. action = switch_thread x2 \<Longrightarrow> \<lbrace>?R12 ct ct_st ct_runnable action x2\<rbrace> do when ct_runnable (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 tcb_sched_action tcb_sched_enqueue x2;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if ct_runnable \<and> ct_prio = target_prio then do tcb_sched_action tcb_sched_append x2;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do guarded_switch_to x2;
set_scheduler_action resume_cur_thread
od
od \<lbrace>\<lambda>_. valid_sched\<rbrace>
 3. \<And>ct ct_st ct_runnable action. action = choose_new_thread \<Longrightarrow> \<lbrace>?R10 ct ct_st ct_runnable action\<rbrace> do when ct_runnable (tcb_sched_action tcb_sched_enqueue ct);
schedule_choose_new_thread
od \<lbrace>\<lambda>_. valid_sched\<rbrace>
 4. \<And>ct ct_st ct_runnable. \<lbrace>?B3 ct ct_st ct_runnable\<rbrace> gets scheduler_action \<lbrace>\<lambda>action s. (action = resume_cur_thread \<longrightarrow> ?R13 ct ct_st ct_runnable action s) \<and> (\<forall>x. action = switch_thread x \<longrightarrow> ?R12 ct ct_st ct_runnable action x s) \<and> (action = choose_new_thread \<longrightarrow> ?R10 ct ct_st ct_runnable action s)\<rbrace>
 5. \<And>ct ct_st. \<lbrace>?B2 ct ct_st\<rbrace> return $ runnable ct_st \<lbrace>?B3 ct ct_st\<rbrace>
 6. \<And>ct. \<lbrace>?B1 ct\<rbrace> get_thread_state ct \<lbrace>?B2 ct\<rbrace>
 7. \<lbrace>?Q\<rbrace> gets cur_thread \<lbrace>?B1\<rbrace>
 8. \<And>s. (valid_sched and valid_idle) s \<Longrightarrow> ?Q s proof (prove)
goal (7 subgoals):
 1. \<And>ct ct_st ct_runnable action x2. action = switch_thread x2 \<Longrightarrow> \<lbrace>?R12 ct ct_st ct_runnable action x2\<rbrace> do when ct_runnable (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 tcb_sched_action tcb_sched_enqueue x2;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if ct_runnable \<and> ct_prio = target_prio then do tcb_sched_action tcb_sched_append x2;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do guarded_switch_to x2;
set_scheduler_action resume_cur_thread
od
od \<lbrace>\<lambda>_. valid_sched\<rbrace>
 2. \<And>ct ct_st ct_runnable action. action = choose_new_thread \<Longrightarrow> \<lbrace>?R10 ct ct_st ct_runnable action\<rbrace> do when ct_runnable (tcb_sched_action tcb_sched_enqueue ct);
schedule_choose_new_thread
od \<lbrace>\<lambda>_. valid_sched\<rbrace>
 3. \<And>ct ct_st ct_runnable. \<lbrace>?B3 ct ct_st ct_runnable\<rbrace> gets scheduler_action \<lbrace>\<lambda>action s. (action = resume_cur_thread \<longrightarrow> ct_runnable \<or> ct = idle_thread s \<longrightarrow> valid_sched s) \<and> (\<forall>x. action = switch_thread x \<longrightarrow> ?R12 ct ct_st ct_runnable action x s) \<and> (action = choose_new_thread \<longrightarrow> ?R10 ct ct_st ct_runnable action s)\<rbrace>
 4. \<And>ct ct_st. \<lbrace>?B2 ct ct_st\<rbrace> return $ runnable ct_st \<lbrace>?B3 ct ct_st\<rbrace>
 5. \<And>ct. \<lbrace>?B1 ct\<rbrace> get_thread_state ct \<lbrace>?B2 ct\<rbrace>
 6. \<lbrace>?Q\<rbrace> gets cur_thread \<lbrace>?B1\<rbrace>
 7. \<And>s. (valid_sched and valid_idle) s \<Longrightarrow> ?Q s proof (prove)
goal (7 subgoals):
 1. \<And>ct ct_st ct_runnable action. action = choose_new_thread \<Longrightarrow> \<lbrace>?R10 ct ct_st ct_runnable action\<rbrace> do when ct_runnable (tcb_sched_action tcb_sched_enqueue ct);
schedule_choose_new_thread
od \<lbrace>\<lambda>_. valid_sched\<rbrace>
 2. \<And>ct ct_st ct_runnable action x2. action = switch_thread x2 \<Longrightarrow> \<lbrace>?R12 ct ct_st ct_runnable action x2\<rbrace> do when ct_runnable (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 tcb_sched_action tcb_sched_enqueue x2;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if ct_runnable \<and> ct_prio = target_prio then do tcb_sched_action tcb_sched_append x2;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do guarded_switch_to x2;
set_scheduler_action resume_cur_thread
od
od \<lbrace>\<lambda>_. valid_sched\<rbrace>
 3. \<And>ct ct_st ct_runnable. \<lbrace>?B3 ct ct_st ct_runnable\<rbrace> gets scheduler_action \<lbrace>\<lambda>action s. (action = resume_cur_thread \<longrightarrow> ct_runnable \<or> ct = idle_thread s \<longrightarrow> valid_sched s) \<and> (\<forall>x. action = switch_thread x \<longrightarrow> ?R12 ct ct_st ct_runnable action x s) \<and> (action = choose_new_thread \<longrightarrow> ?R10 ct ct_st ct_runnable action s)\<rbrace>
 4. \<And>ct ct_st. \<lbrace>?B2 ct ct_st\<rbrace> return $ runnable ct_st \<lbrace>?B3 ct ct_st\<rbrace>
 5. \<And>ct. \<lbrace>?B1 ct\<rbrace> get_thread_state ct \<lbrace>?B2 ct\<rbrace>
 6. \<lbrace>?Q\<rbrace> gets cur_thread \<lbrace>?B1\<rbrace>
 7. \<And>s. (valid_sched and valid_idle) s \<Longrightarrow> ?Q s proof (prove)
goal (7 subgoals):
 1. \<And>ct ct_st ct_runnable action. action = choose_new_thread \<Longrightarrow> \<lbrace>?R10 ct ct_st ct_runnable action\<rbrace> do when ct_runnable (tcb_sched_action tcb_sched_enqueue ct);
schedule_choose_new_thread
od \<lbrace>\<lambda>_. valid_sched\<rbrace>
 2. \<And>ct ct_st ct_runnable action x2. action = switch_thread x2 \<Longrightarrow> \<lbrace>?R12 ct ct_st ct_runnable action x2\<rbrace> do when ct_runnable (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 tcb_sched_action tcb_sched_enqueue x2;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if ct_runnable \<and> ct_prio = target_prio then do tcb_sched_action tcb_sched_append x2;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do guarded_switch_to x2;
set_scheduler_action resume_cur_thread
od
od \<lbrace>\<lambda>_. valid_sched\<rbrace>
 3. \<And>ct ct_st ct_runnable. \<lbrace>?B3 ct ct_st ct_runnable\<rbrace> gets scheduler_action \<lbrace>\<lambda>action s. (action = resume_cur_thread \<longrightarrow> ct_runnable \<or> ct = idle_thread s \<longrightarrow> valid_sched s) \<and> (\<forall>x. action = switch_thread x \<longrightarrow> ?R12 ct ct_st ct_runnable action x s) \<and> (action = choose_new_thread \<longrightarrow> ?R10 ct ct_st ct_runnable action s)\<rbrace>
 4. \<And>ct ct_st. \<lbrace>?B2 ct ct_st\<rbrace> return $ runnable ct_st \<lbrace>?B3 ct ct_st\<rbrace>
 5. \<And>ct. \<lbrace>?B1 ct\<rbrace> get_thread_state ct \<lbrace>?B2 ct\<rbrace>
 6. \<lbrace>?Q\<rbrace> gets cur_thread \<lbrace>?B1\<rbrace>
 7. \<And>s. (valid_sched and valid_idle) s \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>ct ct_st ct_runnable action x2. action = switch_thread x2 \<Longrightarrow> \<lbrace>?R12 ct ct_st ct_runnable action x2\<rbrace> do when ct_runnable (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 tcb_sched_action tcb_sched_enqueue x2;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if ct_runnable \<and> ct_prio = target_prio then do tcb_sched_action tcb_sched_append x2;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do guarded_switch_to x2;
set_scheduler_action resume_cur_thread
od
od \<lbrace>\<lambda>_. valid_sched\<rbrace>
 2. \<And>ct ct_st ct_runnable. \<lbrace>?B3 ct ct_st ct_runnable\<rbrace> gets scheduler_action \<lbrace>\<lambda>action s. (action = resume_cur_thread \<longrightarrow> ct_runnable \<or> ct = idle_thread s \<longrightarrow> valid_sched s) \<and> (\<forall>x. action = switch_thread x \<longrightarrow> ?R12 ct ct_st ct_runnable action x s) \<and> (action = choose_new_thread \<longrightarrow> (if ct_runnable then \<lambda>s. valid_idle s \<and> valid_etcbs s \<and> valid_idle_etcb s \<and> (valid_queues and st_tcb_at runnable ct) s \<and> valid_blocked_except ct s \<and> scheduler_action s = choose_new_thread \<and> ct = cur_thread s else (\<lambda>s. valid_idle s \<and> valid_etcbs s \<and> valid_idle_etcb s \<and> valid_queues s \<and> valid_blocked s \<and> scheduler_action s = choose_new_thread \<and> ct_in_q s)) s)\<rbrace>
 3. \<And>ct ct_st. \<lbrace>?B2 ct ct_st\<rbrace> return $ runnable ct_st \<lbrace>?B3 ct ct_st\<rbrace>
 4. \<And>ct. \<lbrace>?B1 ct\<rbrace> get_thread_state ct \<lbrace>?B2 ct\<rbrace>
 5. \<lbrace>?Q\<rbrace> gets cur_thread \<lbrace>?B1\<rbrace>
 6. \<And>s. (valid_sched and valid_idle) s \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>ct ct_st ct_runnable action x2. action = switch_thread x2 \<Longrightarrow> \<lbrace>?R12 ct ct_st ct_runnable action x2\<rbrace> do when ct_runnable (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 tcb_sched_action tcb_sched_enqueue x2;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if ct_runnable \<and> ct_prio = target_prio then do tcb_sched_action tcb_sched_append x2;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do guarded_switch_to x2;
set_scheduler_action resume_cur_thread
od
od \<lbrace>\<lambda>_. valid_sched\<rbrace>
 2. \<And>ct ct_st ct_runnable. \<lbrace>?B3 ct ct_st ct_runnable\<rbrace> gets scheduler_action \<lbrace>\<lambda>action s. (action = resume_cur_thread \<longrightarrow> ct_runnable \<or> ct = idle_thread s \<longrightarrow> valid_sched s) \<and> (\<forall>x. action = switch_thread x \<longrightarrow> ?R12 ct ct_st ct_runnable action x s) \<and> (action = choose_new_thread \<longrightarrow> (if ct_runnable then \<lambda>s. valid_idle s \<and> valid_etcbs s \<and> valid_idle_etcb s \<and> (valid_queues and st_tcb_at runnable ct) s \<and> valid_blocked_except ct s \<and> scheduler_action s = choose_new_thread \<and> ct = cur_thread s else (\<lambda>s. valid_idle s \<and> valid_etcbs s \<and> valid_idle_etcb s \<and> valid_queues s \<and> valid_blocked s \<and> scheduler_action s = choose_new_thread \<and> ct_in_q s)) s)\<rbrace>
 3. \<And>ct ct_st. \<lbrace>?B2 ct ct_st\<rbrace> return $ runnable ct_st \<lbrace>?B3 ct ct_st\<rbrace>
 4. \<And>ct. \<lbrace>?B1 ct\<rbrace> get_thread_state ct \<lbrace>?B2 ct\<rbrace>
 5. \<lbrace>?Q\<rbrace> gets cur_thread \<lbrace>?B1\<rbrace>
 6. \<And>s. (valid_sched and valid_idle) s \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>ct ct_st ct_runnable action candidate. action = switch_thread candidate \<Longrightarrow> \<lbrace>?R12 ct ct_st ct_runnable action candidate\<rbrace> do when ct_runnable (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 ct_runnable \<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 \<lbrace>\<lambda>_. valid_sched\<rbrace>
 2. \<And>ct ct_st ct_runnable. \<lbrace>?B3 ct ct_st ct_runnable\<rbrace> gets scheduler_action \<lbrace>\<lambda>action s. (action = resume_cur_thread \<longrightarrow> ct_runnable \<or> ct = idle_thread s \<longrightarrow> valid_sched s) \<and> (\<forall>x. action = switch_thread x \<longrightarrow> ?R12 ct ct_st ct_runnable action x s) \<and> (action = choose_new_thread \<longrightarrow> (if ct_runnable then \<lambda>s. valid_idle s \<and> valid_etcbs s \<and> valid_idle_etcb s \<and> (valid_queues and st_tcb_at runnable ct) s \<and> valid_blocked_except ct s \<and> scheduler_action s = choose_new_thread \<and> ct = cur_thread s else (\<lambda>s. valid_idle s \<and> valid_etcbs s \<and> valid_idle_etcb s \<and> valid_queues s \<and> valid_blocked s \<and> scheduler_action s = choose_new_thread \<and> ct_in_q s)) s)\<rbrace>
 3. \<And>ct ct_st. \<lbrace>?B2 ct ct_st\<rbrace> return $ runnable ct_st \<lbrace>?B3 ct ct_st\<rbrace>
 4. \<And>ct. \<lbrace>?B1 ct\<rbrace> get_thread_state ct \<lbrace>?B2 ct\<rbrace>
 5. \<lbrace>?Q\<rbrace> gets cur_thread \<lbrace>?B1\<rbrace>
 6. \<And>s. (valid_sched and valid_idle) s \<Longrightarrow> ?Q s proof (prove)
goal (15 subgoals):
 1. \<And>ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest xa. \<lbrakk>action = switch_thread candidate; fastfail \<and> \<not> highest\<rbrakk> \<Longrightarrow> \<lbrace>?P'77 ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest xa\<rbrace> set_scheduler_action choose_new_thread \<lbrace>\<lambda>rv s. valid_blocked s \<and> scheduler_action s = choose_new_thread \<and> ct_in_q s\<rbrace>
 2. \<And>ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest. \<lbrakk>action = switch_thread candidate; fastfail \<and> \<not> highest\<rbrakk> \<Longrightarrow> \<lbrace>?Q59 ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest\<rbrace> tcb_sched_action tcb_sched_enqueue candidate \<lbrace>\<lambda>xa s. valid_idle s \<and> valid_etcbs s \<and> valid_idle_etcb s \<and> valid_queues s \<and> ?P'77 ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest xa s\<rbrace>
 3. \<And>ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest. \<lbrakk>action = switch_thread candidate; \<not> (fastfail \<and> \<not> highest)\<rbrakk> \<Longrightarrow> \<lbrace>?R59 ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest\<rbrace> if ct_runnable \<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 \<lbrace>\<lambda>_. valid_sched\<rbrace>
 4. \<And>ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom. action = switch_thread candidate \<Longrightarrow> \<lbrace>?B57 ct ct_st ct_runnable action candidate x 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> ?Q59 ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest s) \<and> (\<not> (fastfail \<and> \<not> highest) \<longrightarrow> ?R59 ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest s)\<rbrace>
 5. \<And>ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail. action = switch_thread candidate \<Longrightarrow> \<lbrace>?B56 ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail\<rbrace> gets cur_domain \<lbrace>?B57 ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail\<rbrace>
 6. \<And>ct ct_st ct_runnable action candidate x it target_prio ct_prio. action = switch_thread candidate \<Longrightarrow> \<lbrace>?B55 ct ct_st ct_runnable action candidate x it target_prio ct_prio\<rbrace> schedule_switch_thread_fastfail ct it ct_prio target_prio \<lbrace>?B56 ct ct_st ct_runnable action candidate x it target_prio ct_prio\<rbrace>
 7. \<And>ct ct_st ct_runnable action candidate x it target_prio. action = switch_thread candidate \<Longrightarrow> \<lbrace>?B54 ct ct_st ct_runnable action candidate x it target_prio\<rbrace> ethread_get_when (ct \<noteq> it) tcb_priority ct \<lbrace>?B55 ct ct_st ct_runnable action candidate x it target_prio\<rbrace>
 8. \<And>ct ct_st ct_runnable action candidate x it. action = switch_thread candidate \<Longrightarrow> \<lbrace>?B53 ct ct_st ct_runnable action candidate x it\<rbrace> ethread_get tcb_priority candidate \<lbrace>?B54 ct ct_st ct_runnable action candidate x it\<rbrace>
 9. \<And>ct ct_st ct_runnable action candidate x. action = switch_thread candidate \<Longrightarrow> \<lbrace>?B51 ct ct_st ct_runnable action candidate x\<rbrace> gets idle_thread \<lbrace>?B53 ct ct_st ct_runnable action candidate x\<rbrace>
 10. \<And>ct ct_st ct_runnable action candidate. action = switch_thread candidate \<Longrightarrow> \<lbrace>?R12 ct ct_st ct_runnable action candidate\<rbrace> when ct_runnable (tcb_sched_action tcb_sched_enqueue ct) \<lbrace>?B51 ct ct_st ct_runnable action candidate\<rbrace>
A total of 15 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest xa. \<lbrakk>action = switch_thread candidate; fastfail \<and> \<not> highest\<rbrakk> \<Longrightarrow> \<lbrace>?P80 ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest xa\<rbrace> set_scheduler_action choose_new_thread \<lbrace>\<lambda>rv. valid_blocked\<rbrace>
 2. \<And>ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest xa. \<lbrakk>action = switch_thread candidate; fastfail \<and> \<not> highest\<rbrakk> \<Longrightarrow> \<lbrace>?P'80 ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest xa\<rbrace> set_scheduler_action choose_new_thread \<lbrace>\<lambda>rv s. scheduler_action s = choose_new_thread \<and> ct_in_q s\<rbrace>
 3. \<And>ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest. \<lbrakk>action = switch_thread candidate; fastfail \<and> \<not> highest\<rbrakk> \<Longrightarrow> \<lbrace>?Q59 ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest\<rbrace> tcb_sched_action tcb_sched_enqueue candidate \<lbrace>\<lambda>xa s. valid_idle s \<and> valid_etcbs s \<and> valid_idle_etcb s \<and> valid_queues s \<and> ?P80 ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest xa s \<and> ?P'80 ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest xa s\<rbrace>
 4. \<And>ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest. \<lbrakk>action = switch_thread candidate; \<not> (fastfail \<and> \<not> highest)\<rbrakk> \<Longrightarrow> \<lbrace>?R59 ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest\<rbrace> if ct_runnable \<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 \<lbrace>\<lambda>_. valid_sched\<rbrace>
 5. \<And>ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom. action = switch_thread candidate \<Longrightarrow> \<lbrace>?B57 ct ct_st ct_runnable action candidate x 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> ?Q59 ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest s) \<and> (\<not> (fastfail \<and> \<not> highest) \<longrightarrow> ?R59 ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest s)\<rbrace>
 6. \<And>ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail. action = switch_thread candidate \<Longrightarrow> \<lbrace>?B56 ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail\<rbrace> gets cur_domain \<lbrace>?B57 ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail\<rbrace>
 7. \<And>ct ct_st ct_runnable action candidate x it target_prio ct_prio. action = switch_thread candidate \<Longrightarrow> \<lbrace>?B55 ct ct_st ct_runnable action candidate x it target_prio ct_prio\<rbrace> schedule_switch_thread_fastfail ct it ct_prio target_prio \<lbrace>?B56 ct ct_st ct_runnable action candidate x it target_prio ct_prio\<rbrace>
 8. \<And>ct ct_st ct_runnable action candidate x it target_prio. action = switch_thread candidate \<Longrightarrow> \<lbrace>?B54 ct ct_st ct_runnable action candidate x it target_prio\<rbrace> ethread_get_when (ct \<noteq> it) tcb_priority ct \<lbrace>?B55 ct ct_st ct_runnable action candidate x it target_prio\<rbrace>
 9. \<And>ct ct_st ct_runnable action candidate x it. action = switch_thread candidate \<Longrightarrow> \<lbrace>?B53 ct ct_st ct_runnable action candidate x it\<rbrace> ethread_get tcb_priority candidate \<lbrace>?B54 ct ct_st ct_runnable action candidate x it\<rbrace>
 10. \<And>ct ct_st ct_runnable action candidate x. action = switch_thread candidate \<Longrightarrow> \<lbrace>?B51 ct ct_st ct_runnable action candidate x\<rbrace> gets idle_thread \<lbrace>?B53 ct ct_st ct_runnable action candidate x\<rbrace>
A total of 16 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest xa. \<lbrakk>action = switch_thread candidate; fastfail \<and> \<not> highest\<rbrakk> \<Longrightarrow> \<lbrace>?P'80 ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest xa\<rbrace> set_scheduler_action choose_new_thread \<lbrace>\<lambda>rv s. scheduler_action s = choose_new_thread \<and> ct_in_q s\<rbrace>
 2. \<And>ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest. \<lbrakk>action = switch_thread candidate; fastfail \<and> \<not> highest\<rbrakk> \<Longrightarrow> \<lbrace>?Q59 ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest\<rbrace> tcb_sched_action tcb_sched_enqueue candidate \<lbrace>\<lambda>xa s. valid_idle s \<and> valid_etcbs s \<and> valid_idle_etcb s \<and> valid_queues s \<and> (valid_blocked and (\<lambda>s. scheduler_action s = switch_thread candidate \<and> (\<exists>d p. candidate \<in> set (ready_queues s d p)))) s \<and> ?P'80 ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest xa s\<rbrace>
 3. \<And>ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest. \<lbrakk>action = switch_thread candidate; \<not> (fastfail \<and> \<not> highest)\<rbrakk> \<Longrightarrow> \<lbrace>?R59 ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest\<rbrace> if ct_runnable \<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 \<lbrace>\<lambda>_. valid_sched\<rbrace>
 4. \<And>ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom. action = switch_thread candidate \<Longrightarrow> \<lbrace>?B57 ct ct_st ct_runnable action candidate x 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> ?Q59 ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest s) \<and> (\<not> (fastfail \<and> \<not> highest) \<longrightarrow> ?R59 ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest s)\<rbrace>
 5. \<And>ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail. action = switch_thread candidate \<Longrightarrow> \<lbrace>?B56 ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail\<rbrace> gets cur_domain \<lbrace>?B57 ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail\<rbrace>
 6. \<And>ct ct_st ct_runnable action candidate x it target_prio ct_prio. action = switch_thread candidate \<Longrightarrow> \<lbrace>?B55 ct ct_st ct_runnable action candidate x it target_prio ct_prio\<rbrace> schedule_switch_thread_fastfail ct it ct_prio target_prio \<lbrace>?B56 ct ct_st ct_runnable action candidate x it target_prio ct_prio\<rbrace>
 7. \<And>ct ct_st ct_runnable action candidate x it target_prio. action = switch_thread candidate \<Longrightarrow> \<lbrace>?B54 ct ct_st ct_runnable action candidate x it target_prio\<rbrace> ethread_get_when (ct \<noteq> it) tcb_priority ct \<lbrace>?B55 ct ct_st ct_runnable action candidate x it target_prio\<rbrace>
 8. \<And>ct ct_st ct_runnable action candidate x it. action = switch_thread candidate \<Longrightarrow> \<lbrace>?B53 ct ct_st ct_runnable action candidate x it\<rbrace> ethread_get tcb_priority candidate \<lbrace>?B54 ct ct_st ct_runnable action candidate x it\<rbrace>
 9. \<And>ct ct_st ct_runnable action candidate x. action = switch_thread candidate \<Longrightarrow> \<lbrace>?B51 ct ct_st ct_runnable action candidate x\<rbrace> gets idle_thread \<lbrace>?B53 ct ct_st ct_runnable action candidate x\<rbrace>
 10. \<And>ct ct_st ct_runnable action candidate. action = switch_thread candidate \<Longrightarrow> \<lbrace>?R12 ct ct_st ct_runnable action candidate\<rbrace> when ct_runnable (tcb_sched_action tcb_sched_enqueue ct) \<lbrace>?B51 ct ct_st ct_runnable action candidate\<rbrace>
A total of 15 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest xa xb. \<lbrakk>action = switch_thread candidate; \<not> (fastfail \<and> \<not> highest); ct_runnable \<and> ct_prio = target_prio\<rbrakk> \<Longrightarrow> \<lbrace>?B114 ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest xa xb\<rbrace> schedule_choose_new_thread \<lbrace>\<lambda>_. valid_sched\<rbrace>
 2. \<And>ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest xa. \<lbrakk>action = switch_thread candidate; \<not> (fastfail \<and> \<not> highest); ct_runnable \<and> ct_prio = target_prio\<rbrakk> \<Longrightarrow> \<lbrace>?B112 ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest xa\<rbrace> set_scheduler_action choose_new_thread \<lbrace>?B114 ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest xa\<rbrace>
 3. \<And>ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest. \<lbrakk>action = switch_thread candidate; \<not> (fastfail \<and> \<not> highest); ct_runnable \<and> ct_prio = target_prio\<rbrakk> \<Longrightarrow> \<lbrace>?Q111 ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest\<rbrace> tcb_sched_action tcb_sched_append candidate \<lbrace>?B112 ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest\<rbrace>
 4. \<And>ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest. \<lbrakk>action = switch_thread candidate; \<not> (fastfail \<and> \<not> highest); \<not> (ct_runnable \<and> ct_prio = target_prio)\<rbrakk> \<Longrightarrow> \<lbrace>?R111 ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest\<rbrace> do guarded_switch_to candidate;
set_scheduler_action resume_cur_thread
od \<lbrace>\<lambda>_. valid_sched\<rbrace>
 5. \<And>ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom. action = switch_thread candidate \<Longrightarrow> \<lbrace>?B57 ct ct_st ct_runnable action candidate x 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> valid_idle s \<and> valid_etcbs s \<and> valid_idle_etcb s \<and> (valid_queues and st_tcb_at runnable candidate) s \<and> valid_blocked_except candidate s \<and> scheduler_action s = switch_thread candidate \<and> True \<and> True \<and> ct_in_q s) \<and> (\<not> (fastfail \<and> \<not> highest) \<longrightarrow> (ct_runnable \<and> ct_prio = target_prio \<longrightarrow> ?Q111 ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest s) \<and> (\<not> (ct_runnable \<and> ct_prio = target_prio) \<longrightarrow> ?R111 ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest s))\<rbrace>
 6. \<And>ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail. action = switch_thread candidate \<Longrightarrow> \<lbrace>?B56 ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail\<rbrace> gets cur_domain \<lbrace>?B57 ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail\<rbrace>
 7. \<And>ct ct_st ct_runnable action candidate x it target_prio ct_prio. action = switch_thread candidate \<Longrightarrow> \<lbrace>?B55 ct ct_st ct_runnable action candidate x it target_prio ct_prio\<rbrace> schedule_switch_thread_fastfail ct it ct_prio target_prio \<lbrace>?B56 ct ct_st ct_runnable action candidate x it target_prio ct_prio\<rbrace>
 8. \<And>ct ct_st ct_runnable action candidate x it target_prio. action = switch_thread candidate \<Longrightarrow> \<lbrace>?B54 ct ct_st ct_runnable action candidate x it target_prio\<rbrace> ethread_get_when (ct \<noteq> it) tcb_priority ct \<lbrace>?B55 ct ct_st ct_runnable action candidate x it target_prio\<rbrace>
 9. \<And>ct ct_st ct_runnable action candidate x it. action = switch_thread candidate \<Longrightarrow> \<lbrace>?B53 ct ct_st ct_runnable action candidate x it\<rbrace> ethread_get tcb_priority candidate \<lbrace>?B54 ct ct_st ct_runnable action candidate x it\<rbrace>
 10. \<And>ct ct_st ct_runnable action candidate x. action = switch_thread candidate \<Longrightarrow> \<lbrace>?B51 ct ct_st ct_runnable action candidate x\<rbrace> gets idle_thread \<lbrace>?B53 ct ct_st ct_runnable action candidate x\<rbrace>
A total of 16 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest xa. \<lbrakk>action = switch_thread candidate; \<not> (fastfail \<and> \<not> highest); ct_runnable \<and> ct_prio = target_prio\<rbrakk> \<Longrightarrow> \<lbrace>?P'133 ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest xa\<rbrace> set_scheduler_action choose_new_thread \<lbrace>\<lambda>rv s. valid_blocked s \<and> scheduler_action s = choose_new_thread \<and> ct_in_q s\<rbrace>
 2. \<And>ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest. \<lbrakk>action = switch_thread candidate; \<not> (fastfail \<and> \<not> highest); ct_runnable \<and> ct_prio = target_prio\<rbrakk> \<Longrightarrow> \<lbrace>?Q111 ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest\<rbrace> tcb_sched_action tcb_sched_append candidate \<lbrace>\<lambda>xa s. valid_idle s \<and> valid_etcbs s \<and> valid_idle_etcb s \<and> valid_queues s \<and> ?P'133 ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest xa s\<rbrace>
 3. \<And>ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest. \<lbrakk>action = switch_thread candidate; \<not> (fastfail \<and> \<not> highest); \<not> (ct_runnable \<and> ct_prio = target_prio)\<rbrakk> \<Longrightarrow> \<lbrace>?R111 ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest\<rbrace> do guarded_switch_to candidate;
set_scheduler_action resume_cur_thread
od \<lbrace>\<lambda>_. valid_sched\<rbrace>
 4. \<And>ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom. action = switch_thread candidate \<Longrightarrow> \<lbrace>?B57 ct ct_st ct_runnable action candidate x 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> valid_idle s \<and> valid_etcbs s \<and> valid_idle_etcb s \<and> (valid_queues and st_tcb_at runnable candidate) s \<and> valid_blocked_except candidate s \<and> scheduler_action s = switch_thread candidate \<and> True \<and> True \<and> ct_in_q s) \<and> (\<not> (fastfail \<and> \<not> highest) \<longrightarrow> (ct_runnable \<and> ct_prio = target_prio \<longrightarrow> ?Q111 ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest s) \<and> (\<not> (ct_runnable \<and> ct_prio = target_prio) \<longrightarrow> ?R111 ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest s))\<rbrace>
 5. \<And>ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail. action = switch_thread candidate \<Longrightarrow> \<lbrace>?B56 ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail\<rbrace> gets cur_domain \<lbrace>?B57 ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail\<rbrace>
 6. \<And>ct ct_st ct_runnable action candidate x it target_prio ct_prio. action = switch_thread candidate \<Longrightarrow> \<lbrace>?B55 ct ct_st ct_runnable action candidate x it target_prio ct_prio\<rbrace> schedule_switch_thread_fastfail ct it ct_prio target_prio \<lbrace>?B56 ct ct_st ct_runnable action candidate x it target_prio ct_prio\<rbrace>
 7. \<And>ct ct_st ct_runnable action candidate x it target_prio. action = switch_thread candidate \<Longrightarrow> \<lbrace>?B54 ct ct_st ct_runnable action candidate x it target_prio\<rbrace> ethread_get_when (ct \<noteq> it) tcb_priority ct \<lbrace>?B55 ct ct_st ct_runnable action candidate x it target_prio\<rbrace>
 8. \<And>ct ct_st ct_runnable action candidate x it. action = switch_thread candidate \<Longrightarrow> \<lbrace>?B53 ct ct_st ct_runnable action candidate x it\<rbrace> ethread_get tcb_priority candidate \<lbrace>?B54 ct ct_st ct_runnable action candidate x it\<rbrace>
 9. \<And>ct ct_st ct_runnable action candidate x. action = switch_thread candidate \<Longrightarrow> \<lbrace>?B51 ct ct_st ct_runnable action candidate x\<rbrace> gets idle_thread \<lbrace>?B53 ct ct_st ct_runnable action candidate x\<rbrace>
 10. \<And>ct ct_st ct_runnable action candidate. action = switch_thread candidate \<Longrightarrow> \<lbrace>?R12 ct ct_st ct_runnable action candidate\<rbrace> when ct_runnable (tcb_sched_action tcb_sched_enqueue ct) \<lbrace>?B51 ct ct_st ct_runnable action candidate\<rbrace>
A total of 15 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest xa. \<lbrakk>action = switch_thread candidate; \<not> (fastfail \<and> \<not> highest); ct_runnable \<and> ct_prio = target_prio\<rbrakk> \<Longrightarrow> \<lbrace>?P136 ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest xa\<rbrace> set_scheduler_action choose_new_thread \<lbrace>\<lambda>rv. valid_blocked\<rbrace>
 2. \<And>ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest xa. \<lbrakk>action = switch_thread candidate; \<not> (fastfail \<and> \<not> highest); ct_runnable \<and> ct_prio = target_prio\<rbrakk> \<Longrightarrow> \<lbrace>?P'136 ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest xa\<rbrace> set_scheduler_action choose_new_thread \<lbrace>\<lambda>rv s. scheduler_action s = choose_new_thread \<and> ct_in_q s\<rbrace>
 3. \<And>ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest. \<lbrakk>action = switch_thread candidate; \<not> (fastfail \<and> \<not> highest); ct_runnable \<and> ct_prio = target_prio\<rbrakk> \<Longrightarrow> \<lbrace>?Q111 ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest\<rbrace> tcb_sched_action tcb_sched_append candidate \<lbrace>\<lambda>xa s. valid_idle s \<and> valid_etcbs s \<and> valid_idle_etcb s \<and> valid_queues s \<and> ?P136 ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest xa s \<and> ?P'136 ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest xa s\<rbrace>
 4. \<And>ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest. \<lbrakk>action = switch_thread candidate; \<not> (fastfail \<and> \<not> highest); \<not> (ct_runnable \<and> ct_prio = target_prio)\<rbrakk> \<Longrightarrow> \<lbrace>?R111 ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest\<rbrace> do guarded_switch_to candidate;
set_scheduler_action resume_cur_thread
od \<lbrace>\<lambda>_. valid_sched\<rbrace>
 5. \<And>ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom. action = switch_thread candidate \<Longrightarrow> \<lbrace>?B57 ct ct_st ct_runnable action candidate x 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> valid_idle s \<and> valid_etcbs s \<and> valid_idle_etcb s \<and> (valid_queues and st_tcb_at runnable candidate) s \<and> valid_blocked_except candidate s \<and> scheduler_action s = switch_thread candidate \<and> True \<and> True \<and> ct_in_q s) \<and> (\<not> (fastfail \<and> \<not> highest) \<longrightarrow> (ct_runnable \<and> ct_prio = target_prio \<longrightarrow> ?Q111 ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest s) \<and> (\<not> (ct_runnable \<and> ct_prio = target_prio) \<longrightarrow> ?R111 ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest s))\<rbrace>
 6. \<And>ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail. action = switch_thread candidate \<Longrightarrow> \<lbrace>?B56 ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail\<rbrace> gets cur_domain \<lbrace>?B57 ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail\<rbrace>
 7. \<And>ct ct_st ct_runnable action candidate x it target_prio ct_prio. action = switch_thread candidate \<Longrightarrow> \<lbrace>?B55 ct ct_st ct_runnable action candidate x it target_prio ct_prio\<rbrace> schedule_switch_thread_fastfail ct it ct_prio target_prio \<lbrace>?B56 ct ct_st ct_runnable action candidate x it target_prio ct_prio\<rbrace>
 8. \<And>ct ct_st ct_runnable action candidate x it target_prio. action = switch_thread candidate \<Longrightarrow> \<lbrace>?B54 ct ct_st ct_runnable action candidate x it target_prio\<rbrace> ethread_get_when (ct \<noteq> it) tcb_priority ct \<lbrace>?B55 ct ct_st ct_runnable action candidate x it target_prio\<rbrace>
 9. \<And>ct ct_st ct_runnable action candidate x it. action = switch_thread candidate \<Longrightarrow> \<lbrace>?B53 ct ct_st ct_runnable action candidate x it\<rbrace> ethread_get tcb_priority candidate \<lbrace>?B54 ct ct_st ct_runnable action candidate x it\<rbrace>
 10. \<And>ct ct_st ct_runnable action candidate x. action = switch_thread candidate \<Longrightarrow> \<lbrace>?B51 ct ct_st ct_runnable action candidate x\<rbrace> gets idle_thread \<lbrace>?B53 ct ct_st ct_runnable action candidate x\<rbrace>
A total of 16 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest xa. \<lbrakk>action = switch_thread candidate; \<not> (fastfail \<and> \<not> highest); ct_runnable \<and> ct_prio = target_prio\<rbrakk> \<Longrightarrow> \<lbrace>?P'136 ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest xa\<rbrace> set_scheduler_action choose_new_thread \<lbrace>\<lambda>rv s. scheduler_action s = choose_new_thread \<and> ct_in_q s\<rbrace>
 2. \<And>ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest. \<lbrakk>action = switch_thread candidate; \<not> (fastfail \<and> \<not> highest); ct_runnable \<and> ct_prio = target_prio\<rbrakk> \<Longrightarrow> \<lbrace>?Q111 ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest\<rbrace> tcb_sched_action tcb_sched_append candidate \<lbrace>\<lambda>xa s. valid_idle s \<and> valid_etcbs s \<and> valid_idle_etcb s \<and> valid_queues s \<and> (valid_blocked and (\<lambda>s. scheduler_action s = switch_thread candidate \<and> (\<exists>d p. candidate \<in> set (ready_queues s d p)))) s \<and> ?P'136 ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest xa s\<rbrace>
 3. \<And>ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest. \<lbrakk>action = switch_thread candidate; \<not> (fastfail \<and> \<not> highest); \<not> (ct_runnable \<and> ct_prio = target_prio)\<rbrakk> \<Longrightarrow> \<lbrace>?R111 ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest\<rbrace> do guarded_switch_to candidate;
set_scheduler_action resume_cur_thread
od \<lbrace>\<lambda>_. valid_sched\<rbrace>
 4. \<And>ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom. action = switch_thread candidate \<Longrightarrow> \<lbrace>?B57 ct ct_st ct_runnable action candidate x 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> valid_idle s \<and> valid_etcbs s \<and> valid_idle_etcb s \<and> (valid_queues and st_tcb_at runnable candidate) s \<and> valid_blocked_except candidate s \<and> scheduler_action s = switch_thread candidate \<and> True \<and> True \<and> ct_in_q s) \<and> (\<not> (fastfail \<and> \<not> highest) \<longrightarrow> (ct_runnable \<and> ct_prio = target_prio \<longrightarrow> ?Q111 ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest s) \<and> (\<not> (ct_runnable \<and> ct_prio = target_prio) \<longrightarrow> ?R111 ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail cur_dom highest s))\<rbrace>
 5. \<And>ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail. action = switch_thread candidate \<Longrightarrow> \<lbrace>?B56 ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail\<rbrace> gets cur_domain \<lbrace>?B57 ct ct_st ct_runnable action candidate x it target_prio ct_prio fastfail\<rbrace>
 6. \<And>ct ct_st ct_runnable action candidate x it target_prio ct_prio. action = switch_thread candidate \<Longrightarrow> \<lbrace>?B55 ct ct_st ct_runnable action candidate x it target_prio ct_prio\<rbrace> schedule_switch_thread_fastfail ct it ct_prio target_prio \<lbrace>?B56 ct ct_st ct_runnable action candidate x it target_prio ct_prio\<rbrace>
 7. \<And>ct ct_st ct_runnable action candidate x it target_prio. action = switch_thread candidate \<Longrightarrow> \<lbrace>?B54 ct ct_st ct_runnable action candidate x it target_prio\<rbrace> ethread_get_when (ct \<noteq> it) tcb_priority ct \<lbrace>?B55 ct ct_st ct_runnable action candidate x it target_prio\<rbrace>
 8. \<And>ct ct_st ct_runnable action candidate x it. action = switch_thread candidate \<Longrightarrow> \<lbrace>?B53 ct ct_st ct_runnable action candidate x it\<rbrace> ethread_get tcb_priority candidate \<lbrace>?B54 ct ct_st ct_runnable action candidate x it\<rbrace>
 9. \<And>ct ct_st ct_runnable action candidate x. action = switch_thread candidate \<Longrightarrow> \<lbrace>?B51 ct ct_st ct_runnable action candidate x\<rbrace> gets idle_thread \<lbrace>?B53 ct ct_st ct_runnable action candidate x\<rbrace>
 10. \<And>ct ct_st ct_runnable action candidate. action = switch_thread candidate \<Longrightarrow> \<lbrace>?R12 ct ct_st ct_runnable action candidate\<rbrace> when ct_runnable (tcb_sched_action tcb_sched_enqueue ct) \<lbrace>?B51 ct ct_st ct_runnable action candidate\<rbrace>
A total of 15 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>ct ct_st ct_runnable action candidate x it target_prio ct_prio. action = switch_thread candidate \<Longrightarrow> \<lbrace>?B55 ct ct_st ct_runnable action candidate x 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> valid_idle s \<and> valid_etcbs s \<and> valid_idle_etcb s \<and> (valid_queues and st_tcb_at runnable candidate) s \<and> valid_blocked_except candidate s \<and> scheduler_action s = switch_thread candidate \<and> True \<and> True \<and> ct_in_q s) \<and> (\<not> (fastfail \<and> \<not> is_highest_prio (cur_domain s) target_prio s) \<longrightarrow> (ct_runnable \<and> ct_prio = target_prio \<longrightarrow> valid_idle s \<and> valid_etcbs s \<and> valid_idle_etcb s \<and> (valid_queues and st_tcb_at runnable candidate) s \<and> valid_blocked_except candidate s \<and> scheduler_action s = switch_thread candidate \<and> True \<and> True \<and> ct_in_q s) \<and> (\<not> (ct_runnable \<and> ct_prio = target_prio) \<longrightarrow> (is_activatable candidate and in_cur_domain candidate and valid_sched_action and valid_etcbs and valid_queues and valid_blocked and ct_in_q and valid_idle_etcb) s \<and> valid_queues s \<and> st_tcb_at runnable candidate s \<and> in_cur_domain candidate s \<and> scheduler_action s = switch_thread candidate))\<rbrace>
 2. \<And>ct ct_st ct_runnable action candidate x it target_prio. action = switch_thread candidate \<Longrightarrow> \<lbrace>?B54 ct ct_st ct_runnable action candidate x it target_prio\<rbrace> ethread_get_when (ct \<noteq> it) tcb_priority ct \<lbrace>?B55 ct ct_st ct_runnable action candidate x it target_prio\<rbrace>
 3. \<And>ct ct_st ct_runnable action candidate x it. action = switch_thread candidate \<Longrightarrow> \<lbrace>?B53 ct ct_st ct_runnable action candidate x it\<rbrace> ethread_get tcb_priority candidate \<lbrace>?B54 ct ct_st ct_runnable action candidate x it\<rbrace>
 4. \<And>ct ct_st ct_runnable action candidate x. action = switch_thread candidate \<Longrightarrow> \<lbrace>?B51 ct ct_st ct_runnable action candidate x\<rbrace> gets idle_thread \<lbrace>?B53 ct ct_st ct_runnable action candidate x\<rbrace>
 5. \<And>ct ct_st ct_runnable action candidate. action = switch_thread candidate \<Longrightarrow> \<lbrace>?R12 ct ct_st ct_runnable action candidate\<rbrace> when ct_runnable (tcb_sched_action tcb_sched_enqueue ct) \<lbrace>?B51 ct ct_st ct_runnable action candidate\<rbrace>
 6. \<And>ct ct_st ct_runnable. \<lbrace>?B3 ct ct_st ct_runnable\<rbrace> gets scheduler_action \<lbrace>\<lambda>action s. (action = resume_cur_thread \<longrightarrow> ct_runnable \<or> ct = idle_thread s \<longrightarrow> valid_sched s) \<and> (\<forall>x. action = switch_thread x \<longrightarrow> ?R12 ct ct_st ct_runnable action x s) \<and> (action = choose_new_thread \<longrightarrow> (if ct_runnable then \<lambda>s. valid_idle s \<and> valid_etcbs s \<and> valid_idle_etcb s \<and> (valid_queues and st_tcb_at runnable ct) s \<and> valid_blocked_except ct s \<and> scheduler_action s = choose_new_thread \<and> ct = cur_thread s else (\<lambda>s. valid_idle s \<and> valid_etcbs s \<and> valid_idle_etcb s \<and> valid_queues s \<and> valid_blocked s \<and> scheduler_action s = choose_new_thread \<and> ct_in_q s)) s)\<rbrace>
 7. \<And>ct ct_st. \<lbrace>?B2 ct ct_st\<rbrace> return $ runnable ct_st \<lbrace>?B3 ct ct_st\<rbrace>
 8. \<And>ct. \<lbrace>?B1 ct\<rbrace> get_thread_state ct \<lbrace>?B2 ct\<rbrace>
 9. \<lbrace>?Q\<rbrace> gets cur_thread \<lbrace>?B1\<rbrace>
 10. \<And>s. (valid_sched and valid_idle) s \<Longrightarrow> ?Q s proof (prove)
goal (10 subgoals):
 1. \<And>ct ct_st ct_runnable action candidate x it target_prio ct_prio. action = switch_thread candidate \<Longrightarrow> \<lbrace>?B55 ct ct_st ct_runnable action candidate x 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> valid_idle s \<and> valid_etcbs s \<and> valid_idle_etcb s \<and> (valid_queues and st_tcb_at runnable candidate) s \<and> valid_blocked_except candidate s \<and> scheduler_action s = switch_thread candidate \<and> True \<and> True \<and> ct_in_q s) \<and> (\<not> (fastfail \<and> \<not> is_highest_prio (cur_domain s) target_prio s) \<longrightarrow> (ct_runnable \<and> ct_prio = target_prio \<longrightarrow> valid_idle s \<and> valid_etcbs s \<and> valid_idle_etcb s \<and> (valid_queues and st_tcb_at runnable candidate) s \<and> valid_blocked_except candidate s \<and> scheduler_action s = switch_thread candidate \<and> True \<and> True \<and> ct_in_q s) \<and> (\<not> (ct_runnable \<and> ct_prio = target_prio) \<longrightarrow> (is_activatable candidate and in_cur_domain candidate and valid_sched_action and valid_etcbs and valid_queues and valid_blocked and ct_in_q and valid_idle_etcb) s \<and> valid_queues s \<and> st_tcb_at runnable candidate s \<and> in_cur_domain candidate s \<and> scheduler_action s = switch_thread candidate))\<rbrace>
 2. \<And>ct ct_st ct_runnable action candidate x it target_prio. action = switch_thread candidate \<Longrightarrow> \<lbrace>?B54 ct ct_st ct_runnable action candidate x it target_prio\<rbrace> ethread_get_when (ct \<noteq> it) tcb_priority ct \<lbrace>?B55 ct ct_st ct_runnable action candidate x it target_prio\<rbrace>
 3. \<And>ct ct_st ct_runnable action candidate x it. action = switch_thread candidate \<Longrightarrow> \<lbrace>?B53 ct ct_st ct_runnable action candidate x it\<rbrace> ethread_get tcb_priority candidate \<lbrace>?B54 ct ct_st ct_runnable action candidate x it\<rbrace>
 4. \<And>ct ct_st ct_runnable action candidate x. action = switch_thread candidate \<Longrightarrow> \<lbrace>?B51 ct ct_st ct_runnable action candidate x\<rbrace> gets idle_thread \<lbrace>?B53 ct ct_st ct_runnable action candidate x\<rbrace>
 5. \<And>ct ct_st ct_runnable action candidate. action = switch_thread candidate \<Longrightarrow> \<lbrace>?R12 ct ct_st ct_runnable action candidate\<rbrace> when ct_runnable (tcb_sched_action tcb_sched_enqueue ct) \<lbrace>?B51 ct ct_st ct_runnable action candidate\<rbrace>
 6. \<And>ct ct_st ct_runnable. \<lbrace>?B3 ct ct_st ct_runnable\<rbrace> gets scheduler_action \<lbrace>\<lambda>action s. (action = resume_cur_thread \<longrightarrow> ct_runnable \<or> ct = idle_thread s \<longrightarrow> valid_sched s) \<and> (\<forall>x. action = switch_thread x \<longrightarrow> ?R12 ct ct_st ct_runnable action x s) \<and> (action = choose_new_thread \<longrightarrow> (if ct_runnable then \<lambda>s. valid_idle s \<and> valid_etcbs s \<and> valid_idle_etcb s \<and> (valid_queues and st_tcb_at runnable ct) s \<and> valid_blocked_except ct s \<and> scheduler_action s = choose_new_thread \<and> ct = cur_thread s else (\<lambda>s. valid_idle s \<and> valid_etcbs s \<and> valid_idle_etcb s \<and> valid_queues s \<and> valid_blocked s \<and> scheduler_action s = choose_new_thread \<and> ct_in_q s)) s)\<rbrace>
 7. \<And>ct ct_st. \<lbrace>?B2 ct ct_st\<rbrace> return $ runnable ct_st \<lbrace>?B3 ct ct_st\<rbrace>
 8. \<And>ct. \<lbrace>?B1 ct\<rbrace> get_thread_state ct \<lbrace>?B2 ct\<rbrace>
 9. \<lbrace>?Q\<rbrace> gets cur_thread \<lbrace>?B1\<rbrace>
 10. \<And>s. (valid_sched and valid_idle) s \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>ct ct_st ct_runnable candidate. ct_runnable \<Longrightarrow> \<lbrace>?P'227 ct ct_st (ds_id True) (switch_thread candidate) candidate\<rbrace> tcb_sched_action tcb_sched_enqueue ct \<lbrace>\<lambda>rv s. valid_blocked_except candidate s \<and> scheduler_action s = switch_thread candidate \<and> ct_in_q s \<and> valid_idle s \<and> valid_etcbs s \<and> valid_idle_etcb s \<and> valid_queues s \<and> st_tcb_at runnable candidate s \<and> valid_blocked_except candidate s \<and> scheduler_action s = switch_thread candidate \<and> ct_in_q s \<and> is_activatable candidate s \<and> in_cur_domain candidate s \<and> valid_sched_action s \<and> valid_etcbs s \<and> valid_queues s \<and> valid_blocked s \<and> ct_in_q s \<and> valid_idle_etcb s \<and> valid_queues s \<and> st_tcb_at runnable candidate s \<and> in_cur_domain candidate s \<and> scheduler_action s = switch_thread candidate\<rbrace>
 2. \<And>ct ct_st ct_runnable. \<lbrace>?B3 ct ct_st ct_runnable\<rbrace> gets scheduler_action \<lbrace>\<lambda>action s. (action = resume_cur_thread \<longrightarrow> ct_runnable \<or> ct = idle_thread s \<longrightarrow> valid_sched s) \<and> (\<forall>x. action = switch_thread x \<longrightarrow> (if ct_runnable then \<lambda>s. valid_idle s \<and> valid_etcbs s \<and> valid_idle_etcb s \<and> (valid_queues and st_tcb_at runnable ct) s \<and> st_tcb_at runnable x s \<and> ?P'227 ct ct_st ct_runnable action x s else (\<lambda>s. valid_idle s \<and> (valid_etcbs s \<and> valid_idle_etcb s \<and> (valid_queues and st_tcb_at runnable x) s \<and> valid_blocked_except x s \<and> scheduler_action s = switch_thread x \<and> True \<and> True \<and> ct_in_q s) \<and> (valid_idle s \<and> valid_etcbs s \<and> valid_idle_etcb s \<and> (valid_queues and st_tcb_at runnable x) s \<and> valid_blocked_except x s \<and> scheduler_action s = switch_thread x \<and> True \<and> True \<and> ct_in_q s) \<and> (is_activatable x and in_cur_domain x and valid_sched_action and valid_etcbs and valid_queues and valid_blocked and ct_in_q and valid_idle_etcb) s \<and> valid_queues s \<and> st_tcb_at runnable x s \<and> in_cur_domain x s \<and> scheduler_action s = switch_thread x)) s) \<and> (action = choose_new_thread \<longrightarrow> (if ct_runnable then \<lambda>s. valid_idle s \<and> valid_etcbs s \<and> valid_idle_etcb s \<and> (valid_queues and st_tcb_at runnable ct) s \<and> valid_blocked_except ct s \<and> scheduler_action s = choose_new_thread \<and> ct = cur_thread s else (\<lambda>s. valid_idle s \<and> valid_etcbs s \<and> valid_idle_etcb s \<and> valid_queues s \<and> valid_blocked s \<and> scheduler_action s = choose_new_thread \<and> ct_in_q s)) s)\<rbrace>
 3. \<And>ct ct_st. \<lbrace>?B2 ct ct_st\<rbrace> return $ runnable ct_st \<lbrace>?B3 ct ct_st\<rbrace>
 4. \<And>ct. \<lbrace>?B1 ct\<rbrace> get_thread_state ct \<lbrace>?B2 ct\<rbrace>
 5. \<lbrace>?Q\<rbrace> gets cur_thread \<lbrace>?B1\<rbrace>
 6. \<And>s. (valid_sched and valid_idle) s \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>ct ct_st ct_runnable candidate. ct_runnable \<Longrightarrow> \<lbrace>?P'227 ct ct_st (ds_id True) (switch_thread candidate) candidate\<rbrace> tcb_sched_action tcb_sched_enqueue ct \<lbrace>\<lambda>r s. valid_blocked s \<and> scheduler_action s = switch_thread candidate \<and> ct_in_q s \<and> valid_idle s \<and> valid_etcbs s \<and> valid_idle_etcb s \<and> valid_queues s \<and> st_tcb_at runnable candidate s \<and> valid_blocked s \<and> scheduler_action s = switch_thread candidate \<and> ct_in_q s \<and> is_activatable candidate s \<and> in_cur_domain candidate s \<and> valid_sched_action s \<and> valid_etcbs s \<and> valid_queues s \<and> valid_blocked s \<and> ct_in_q s \<and> valid_idle_etcb s \<and> valid_queues s \<and> st_tcb_at runnable candidate s \<and> in_cur_domain candidate s \<and> scheduler_action s = switch_thread candidate\<rbrace>
 2. \<And>ct ct_st ct_runnable. \<lbrace>?B3 ct ct_st ct_runnable\<rbrace> gets scheduler_action \<lbrace>\<lambda>action s. (action = resume_cur_thread \<longrightarrow> ct_runnable \<or> ct = idle_thread s \<longrightarrow> valid_sched s) \<and> (\<forall>x. action = switch_thread x \<longrightarrow> (if ct_runnable then \<lambda>s. valid_idle s \<and> valid_etcbs s \<and> valid_idle_etcb s \<and> (valid_queues and st_tcb_at runnable ct) s \<and> st_tcb_at runnable x s \<and> ?P'227 ct ct_st ct_runnable action x s else (\<lambda>s. valid_idle s \<and> (valid_etcbs s \<and> valid_idle_etcb s \<and> (valid_queues and st_tcb_at runnable x) s \<and> valid_blocked_except x s \<and> scheduler_action s = switch_thread x \<and> True \<and> True \<and> ct_in_q s) \<and> (valid_idle s \<and> valid_etcbs s \<and> valid_idle_etcb s \<and> (valid_queues and st_tcb_at runnable x) s \<and> valid_blocked_except x s \<and> scheduler_action s = switch_thread x \<and> True \<and> True \<and> ct_in_q s) \<and> (is_activatable x and in_cur_domain x and valid_sched_action and valid_etcbs and valid_queues and valid_blocked and ct_in_q and valid_idle_etcb) s \<and> valid_queues s \<and> st_tcb_at runnable x s \<and> in_cur_domain x s \<and> scheduler_action s = switch_thread x)) s) \<and> (action = choose_new_thread \<longrightarrow> (if ct_runnable then \<lambda>s. valid_idle s \<and> valid_etcbs s \<and> valid_idle_etcb s \<and> (valid_queues and st_tcb_at runnable ct) s \<and> valid_blocked_except ct s \<and> scheduler_action s = choose_new_thread \<and> ct = cur_thread s else (\<lambda>s. valid_idle s \<and> valid_etcbs s \<and> valid_idle_etcb s \<and> valid_queues s \<and> valid_blocked s \<and> scheduler_action s = choose_new_thread \<and> ct_in_q s)) s)\<rbrace>
 3. \<And>ct ct_st. \<lbrace>?B2 ct ct_st\<rbrace> return $ runnable ct_st \<lbrace>?B3 ct ct_st\<rbrace>
 4. \<And>ct. \<lbrace>?B1 ct\<rbrace> get_thread_state ct \<lbrace>?B2 ct\<rbrace>
 5. \<lbrace>?Q\<rbrace> gets cur_thread \<lbrace>?B1\<rbrace>
 6. \<And>s. (valid_sched and valid_idle) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_sched and valid_idle) s \<Longrightarrow> \<forall>st. st_tcb_at ((=) st) (cur_thread s) s \<longrightarrow> (scheduler_action s = resume_cur_thread \<longrightarrow> runnable st \<or> cur_thread s = idle_thread s \<longrightarrow> valid_sched s) \<and> (\<forall>x. scheduler_action s = switch_thread x \<longrightarrow> (if runnable st then \<lambda>sa. valid_idle sa \<and> valid_etcbs sa \<and> valid_idle_etcb sa \<and> (valid_queues and st_tcb_at runnable (cur_thread s)) sa \<and> st_tcb_at runnable x sa \<and> valid_blocked_except (cur_thread s) sa \<and> scheduler_action sa = scheduler_action s \<and> cur_thread s = cur_thread sa \<and> valid_idle sa \<and> valid_etcbs sa \<and> valid_idle_etcb sa \<and> (valid_queues and st_tcb_at runnable (cur_thread s)) sa \<and> st_tcb_at runnable x sa \<and> valid_blocked_except (cur_thread s) sa \<and> scheduler_action sa = scheduler_action s \<and> cur_thread s = cur_thread sa \<and> is_activatable x sa \<and> in_cur_domain x sa \<and> valid_sched_action sa \<and> valid_etcbs sa \<and> (valid_queues and st_tcb_at runnable (cur_thread s)) sa \<and> valid_blocked_except (cur_thread s) sa \<and> cur_thread s = cur_thread sa \<and> valid_idle_etcb sa \<and> (valid_queues and st_tcb_at runnable (cur_thread s)) sa \<and> st_tcb_at runnable x sa \<and> in_cur_domain x sa \<and> scheduler_action sa = scheduler_action s else (\<lambda>s. valid_idle s \<and> (valid_etcbs s \<and> valid_idle_etcb s \<and> (valid_queues and st_tcb_at runnable x) s \<and> valid_blocked_except x s \<and> scheduler_action s = switch_thread x \<and> True \<and> True \<and> ct_in_q s) \<and> (valid_idle s \<and> valid_etcbs s \<and> valid_idle_etcb s \<and> (valid_queues and st_tcb_at runnable x) s \<and> valid_blocked_except x s \<and> scheduler_action s = switch_thread x \<and> True \<and> True \<and> ct_in_q s) \<and> (is_activatable x and in_cur_domain x and valid_sched_action and valid_etcbs and valid_queues and valid_blocked and ct_in_q and valid_idle_etcb) s \<and> valid_queues s \<and> st_tcb_at runnable x s \<and> in_cur_domain x s \<and> scheduler_action s = switch_thread x)) s) \<and> (scheduler_action s = choose_new_thread \<longrightarrow> (if runnable st then \<lambda>sa. valid_idle sa \<and> valid_etcbs sa \<and> valid_idle_etcb sa \<and> (valid_queues and st_tcb_at runnable (cur_thread s)) sa \<and> valid_blocked_except (cur_thread s) sa \<and> scheduler_action sa = choose_new_thread \<and> cur_thread s = cur_thread sa else (\<lambda>s. valid_idle s \<and> valid_etcbs s \<and> valid_idle_etcb s \<and> valid_queues s \<and> valid_blocked s \<and> scheduler_action s = choose_new_thread \<and> ct_in_q s)) s) proof (prove)
goal (1 subgoal):
 1. \<And>s st. \<lbrakk>valid_etcbs s; valid_queues s; ct_not_in_q s; is_activatable (cur_thread s) s; \<forall>t. scheduler_action s = switch_thread t \<longrightarrow> st_tcb_at runnable t s; \<forall>t. scheduler_action s = switch_thread t \<longrightarrow> in_cur_domain t s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s\<rbrakk> \<Longrightarrow> (runnable st \<longrightarrow> st_tcb_at ((=) st) (cur_thread s) s \<longrightarrow> (scheduler_action s = resume_cur_thread \<longrightarrow> ct_not_in_q_2 (ready_queues s) resume_cur_thread (cur_thread s) \<and> is_activatable_2 (cur_thread s) resume_cur_thread (kheap s) \<and> ct_in_cur_domain_2 (cur_thread s) (idle_thread s) resume_cur_thread (cur_domain s) (ekheap s) \<and> valid_blocked_2 (ready_queues s) (kheap s) resume_cur_thread (cur_thread s) \<and> (cur_thread s = idle_thread s \<longrightarrow> ct_not_in_q_2 (ready_queues s) resume_cur_thread (idle_thread s) \<and> is_activatable_2 (idle_thread s) resume_cur_thread (kheap s) \<and> ct_in_cur_domain_2 (idle_thread s) (idle_thread s) resume_cur_thread (cur_domain s) (ekheap s) \<and> valid_blocked_2 (ready_queues s) (kheap s) resume_cur_thread (idle_thread s))) \<and> (\<forall>x. scheduler_action s = switch_thread x \<longrightarrow> st_tcb_at runnable (cur_thread s) s \<and> valid_blocked_except_2 (cur_thread s) (ready_queues s) (kheap s) (switch_thread x) (cur_thread s) \<and> st_tcb_at runnable (cur_thread s) s \<and> valid_blocked_except_2 (cur_thread s) (ready_queues s) (kheap s) (switch_thread x) (cur_thread s) \<and> st_tcb_at runnable (cur_thread s) s \<and> valid_blocked_except_2 (cur_thread s) (ready_queues s) (kheap s) (switch_thread x) (cur_thread s) \<and> st_tcb_at runnable (cur_thread s) s) \<and> (scheduler_action s = choose_new_thread \<longrightarrow> st_tcb_at runnable (cur_thread s) s \<and> valid_blocked_except_2 (cur_thread s) (ready_queues s) (kheap s) choose_new_thread (cur_thread s))) \<and> (\<not> runnable st \<longrightarrow> st_tcb_at ((=) st) (cur_thread s) s \<longrightarrow> (scheduler_action s = resume_cur_thread \<longrightarrow> cur_thread s = idle_thread s \<longrightarrow> ct_not_in_q_2 (ready_queues s) resume_cur_thread (idle_thread s) \<and> is_activatable_2 (idle_thread s) resume_cur_thread (kheap s) \<and> ct_in_cur_domain_2 (idle_thread s) (idle_thread s) resume_cur_thread (cur_domain s) (ekheap s) \<and> valid_blocked_2 (ready_queues s) (kheap s) resume_cur_thread (idle_thread s)) \<and> (\<forall>x. scheduler_action s = switch_thread x \<longrightarrow> valid_blocked_except_2 x (ready_queues s) (kheap s) (switch_thread x) (cur_thread s) \<and> ct_in_q s \<and> valid_blocked_except_2 x (ready_queues s) (kheap s) (switch_thread x) (cur_thread s) \<and> ct_in_q s \<and> valid_blocked_2 (ready_queues s) (kheap s) (switch_thread x) (cur_thread s) \<and> ct_in_q s) \<and> (scheduler_action s = choose_new_thread \<longrightarrow> valid_blocked_2 (ready_queues s) (kheap s) choose_new_thread (cur_thread s) \<and> ct_in_q s)) proof (prove)
goal:
No subgoals!