theory Syscall_AC

lemma schedule_integrity_pasMayEditReadyQueues:
  "\<lbrace>einvs and integrity aag X st and pas_refined aag
          and guarded_pas_domain aag and K (pasMayEditReadyQueues aag)\<rbrace>
   schedule
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" supply ethread_get_wp[wp del] supply schedule_choose_new_thread_integrity[wp] supply if_split[split del] apply (simp add: schedule_def wrap_is_highest_prio_def[symmetric]) apply (wp, wpc) 
        (* resume current thread *)
         apply wp prefer 2 
       (* choose thread *)
        apply wp 
      (* switch_to *)
       apply (wpsimp wp: set_scheduler_action_cnt_valid_sched enqueue_thread_queued
                        append_thread_queued tcb_sched_action_append_integrity_pasMayEditReadyQueues
                        guarded_switch_to_lift switch_to_thread_respects_pasMayEditReadyQueues)+ 
            (* is_highest_prio *)
             apply (simp add: wrap_is_highest_prio_def) apply ((wp (once) hoare_drop_imp)+)[1] apply (wpsimp wp: tcb_sched_action_enqueue_valid_blocked_except hoare_vcg_imp_lift' gts_wp)+ apply (clarsimp simp: if_apply_def2 cong: imp_cong conj_cong) apply (safe; ((solves \<open>clarsimp simp: valid_sched_def not_cur_thread_def
                                        valid_sched_action_def weak_valid_sched_action_def\<close>)?)) apply (clarsimp simp: obj_at_def pred_tcb_at_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>einvs and integrity aag X st and pas_refined aag and guarded_pas_domain aag and K (pasMayEditReadyQueues aag)\<rbrace> schedule \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>einvs and integrity aag X st and pas_refined aag and guarded_pas_domain aag and K (pasMayEditReadyQueues aag)\<rbrace> schedule \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>einvs and integrity aag X st and pas_refined aag and guarded_pas_domain aag and K (pasMayEditReadyQueues aag)\<rbrace> schedule \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>einvs and integrity aag X st and pas_refined aag and guarded_pas_domain aag and K (pasMayEditReadyQueues aag)\<rbrace> schedule \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>einvs and integrity aag X st and pas_refined aag and guarded_pas_domain aag and (\<lambda>y. pasMayEditReadyQueues aag)\<rbrace> do ct <- gets cur_thread;
ct_st <- get_thread_state ct;
gets scheduler_action >>= case_scheduler_action (do id <- gets idle_thread;
assert (runnable ct_st \<or> ct = id)
od) (\<lambda>candidate. do y <- when (runnable ct_st) (tcb_sched_action tcb_sched_enqueue ct);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority candidate;
ct_prio <- ethread_get_when (ct \<noteq> it) tcb_priority ct;
fastfail <- schedule_switch_thread_fastfail ct it ct_prio target_prio;
cur_dom <- gets cur_domain;
highest <- wrap_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>_. integrity aag X st\<rbrace> 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>_. integrity aag X st\<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 <- wrap_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>_. integrity aag X st\<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>_. integrity aag X st\<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. (einvs and integrity aag X st and pas_refined aag and guarded_pas_domain aag and (\<lambda>y. pasMayEditReadyQueues aag)) 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>_. integrity aag X st\<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 <- wrap_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>_. integrity aag X st\<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>_. integrity aag X st\<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. (einvs and integrity aag X st and pas_refined aag and guarded_pas_domain aag and (\<lambda>y. pasMayEditReadyQueues aag)) 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 <- wrap_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>_. integrity aag X st\<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>_. integrity aag X st\<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> integrity aag X st 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. (einvs and integrity aag X st and pas_refined aag and guarded_pas_domain aag and (\<lambda>y. pasMayEditReadyQueues aag)) 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>_. integrity aag X st\<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 <- wrap_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>_. integrity aag X st\<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> integrity aag X st 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. (einvs and integrity aag X st and pas_refined aag and guarded_pas_domain aag and (\<lambda>y. pasMayEditReadyQueues aag)) 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>_. integrity aag X st\<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 <- wrap_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>_. integrity aag X st\<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> integrity aag X st 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. (einvs and integrity aag X st and pas_refined aag and guarded_pas_domain aag and (\<lambda>y. pasMayEditReadyQueues aag)) 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 <- wrap_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>_. integrity aag X st\<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> integrity aag X st 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 \<lambda>s. invs s \<and> (valid_sched_except_blocked and st_tcb_at runnable ct and not_cur_thread ct and valid_blocked_except ct) s \<and> valid_list s \<and> integrity aag X st s \<and> pas_refined aag s \<and> K (pasMayEditReadyQueues aag) s \<and> scheduler_action s = choose_new_thread else (\<lambda>s. invs s \<and> valid_sched s \<and> valid_list s \<and> integrity aag X st s \<and> pas_refined aag s \<and> K (pasMayEditReadyQueues aag) s \<and> scheduler_action s = choose_new_thread)) 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. (einvs and integrity aag X st and pas_refined aag and guarded_pas_domain aag and (\<lambda>y. pasMayEditReadyQueues aag)) 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 <- wrap_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>_. integrity aag X st\<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> integrity aag X st 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 \<lambda>s. invs s \<and> (valid_sched_except_blocked and st_tcb_at runnable ct and not_cur_thread ct and valid_blocked_except ct) s \<and> valid_list s \<and> integrity aag X st s \<and> pas_refined aag s \<and> K (pasMayEditReadyQueues aag) s \<and> scheduler_action s = choose_new_thread else (\<lambda>s. invs s \<and> valid_sched s \<and> valid_list s \<and> integrity aag X st s \<and> pas_refined aag s \<and> K (pasMayEditReadyQueues aag) s \<and> scheduler_action s = choose_new_thread)) 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. (einvs and integrity aag X st and pas_refined aag and guarded_pas_domain aag and (\<lambda>y. pasMayEditReadyQueues aag)) s \<Longrightarrow> ?Q6 s proof (prove)
goal (11 subgoals):
 1. \<And>ct ct_st x2 it target_prio ct_prio fastfail cur_dom. \<lbrace>?B59 ct ct_st (switch_thread x2) x2 () it target_prio ct_prio fastfail cur_dom\<rbrace> wrap_is_highest_prio cur_dom target_prio \<lbrace>\<lambda>highest s. (fastfail \<and> \<not> highest \<longrightarrow> invs s \<and> valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> st_tcb_at runnable x2 s \<and> not_cur_thread x2 s \<and> valid_blocked_except x2 s \<and> scheduler_action s = switch_thread x2 \<and> valid_list s \<and> integrity aag X st s \<and> pas_refined aag s \<and> pasMayEditReadyQueues aag) \<and> ((fastfail \<longrightarrow> highest) \<longrightarrow> (runnable ct_st \<and> ct_prio = target_prio \<longrightarrow> invs s \<and> valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> st_tcb_at runnable x2 s \<and> not_cur_thread x2 s \<and> valid_blocked_except x2 s \<and> scheduler_action s = switch_thread x2 \<and> valid_list s \<and> integrity aag X st s \<and> pas_refined aag s \<and> pasMayEditReadyQueues aag) \<and> ((runnable ct_st \<longrightarrow> ct_prio \<noteq> target_prio) \<longrightarrow> integrity aag X st s \<and> pas_refined aag s \<and> pasMayEditReadyQueues aag))\<rbrace>
 2. \<And>ct ct_st x x2 y it target_prio ct_prio fastfail. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B58 ct ct_st x x2 y it target_prio ct_prio fastfail\<rbrace> gets cur_domain \<lbrace>?B59 ct ct_st x x2 y it target_prio ct_prio fastfail\<rbrace>
 3. \<And>ct ct_st x x2 y it target_prio ct_prio. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B57 ct ct_st x x2 y it target_prio ct_prio\<rbrace> schedule_switch_thread_fastfail ct it ct_prio target_prio \<lbrace>?B58 ct ct_st x x2 y it target_prio ct_prio\<rbrace>
 4. \<And>ct ct_st x x2 y it target_prio. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B56 ct ct_st x x2 y it target_prio\<rbrace> ethread_get_when (ct \<noteq> it) tcb_priority ct \<lbrace>?B57 ct ct_st x x2 y it target_prio\<rbrace>
 5. \<And>ct ct_st x x2 y it. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B55 ct ct_st x x2 y it\<rbrace> ethread_get tcb_priority x2 \<lbrace>?B56 ct ct_st x x2 y it\<rbrace>
 6. \<And>ct ct_st x x2 y. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B54 ct ct_st x x2 y\<rbrace> gets idle_thread \<lbrace>?B55 ct ct_st x x2 y\<rbrace>
 7. \<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>?B54 ct ct_st x x2\<rbrace>
 8. \<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> integrity aag X st 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 \<lambda>s. invs s \<and> (valid_sched_except_blocked and st_tcb_at runnable ct and not_cur_thread ct and valid_blocked_except ct) s \<and> valid_list s \<and> integrity aag X st s \<and> pas_refined aag s \<and> K (pasMayEditReadyQueues aag) s \<and> scheduler_action s = choose_new_thread else (\<lambda>s. invs s \<and> valid_sched s \<and> valid_list s \<and> integrity aag X st s \<and> pas_refined aag s \<and> K (pasMayEditReadyQueues aag) s \<and> scheduler_action s = choose_new_thread)) s)\<rbrace>
 9. \<And>ct. \<lbrace>?B7 ct\<rbrace> get_thread_state ct \<lbrace>?B8 ct\<rbrace>
 10. \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>?B7\<rbrace>
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>ct ct_st x2 it target_prio ct_prio fastfail cur_dom. \<lbrace>?B59 ct ct_st (switch_thread x2) x2 () it target_prio ct_prio fastfail cur_dom\<rbrace> wrap_is_highest_prio cur_dom target_prio \<lbrace>\<lambda>highest s. (fastfail \<and> \<not> highest \<longrightarrow> invs s \<and> valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> st_tcb_at runnable x2 s \<and> not_cur_thread x2 s \<and> valid_blocked_except x2 s \<and> scheduler_action s = switch_thread x2 \<and> valid_list s \<and> integrity aag X st s \<and> pas_refined aag s \<and> pasMayEditReadyQueues aag) \<and> ((fastfail \<longrightarrow> highest) \<longrightarrow> (runnable ct_st \<and> ct_prio = target_prio \<longrightarrow> invs s \<and> valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> st_tcb_at runnable x2 s \<and> not_cur_thread x2 s \<and> valid_blocked_except x2 s \<and> scheduler_action s = switch_thread x2 \<and> valid_list s \<and> integrity aag X st s \<and> pas_refined aag s \<and> pasMayEditReadyQueues aag) \<and> ((runnable ct_st \<longrightarrow> ct_prio \<noteq> target_prio) \<longrightarrow> integrity aag X st s \<and> pas_refined aag s \<and> pasMayEditReadyQueues aag))\<rbrace>
 2. \<And>ct ct_st x x2 y it target_prio ct_prio fastfail. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B58 ct ct_st x x2 y it target_prio ct_prio fastfail\<rbrace> gets cur_domain \<lbrace>?B59 ct ct_st x x2 y it target_prio ct_prio fastfail\<rbrace>
 3. \<And>ct ct_st x x2 y it target_prio ct_prio. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B57 ct ct_st x x2 y it target_prio ct_prio\<rbrace> schedule_switch_thread_fastfail ct it ct_prio target_prio \<lbrace>?B58 ct ct_st x x2 y it target_prio ct_prio\<rbrace>
 4. \<And>ct ct_st x x2 y it target_prio. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B56 ct ct_st x x2 y it target_prio\<rbrace> ethread_get_when (ct \<noteq> it) tcb_priority ct \<lbrace>?B57 ct ct_st x x2 y it target_prio\<rbrace>
 5. \<And>ct ct_st x x2 y it. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B55 ct ct_st x x2 y it\<rbrace> ethread_get tcb_priority x2 \<lbrace>?B56 ct ct_st x x2 y it\<rbrace>
 6. \<And>ct ct_st x x2 y. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B54 ct ct_st x x2 y\<rbrace> gets idle_thread \<lbrace>?B55 ct ct_st x x2 y\<rbrace>
 7. \<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>?B54 ct ct_st x x2\<rbrace>
 8. \<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> integrity aag X st 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 \<lambda>s. invs s \<and> (valid_sched_except_blocked and st_tcb_at runnable ct and not_cur_thread ct and valid_blocked_except ct) s \<and> valid_list s \<and> integrity aag X st s \<and> pas_refined aag s \<and> K (pasMayEditReadyQueues aag) s \<and> scheduler_action s = choose_new_thread else (\<lambda>s. invs s \<and> valid_sched s \<and> valid_list s \<and> integrity aag X st s \<and> pas_refined aag s \<and> K (pasMayEditReadyQueues aag) s \<and> scheduler_action s = choose_new_thread)) s)\<rbrace>
 9. \<And>ct. \<lbrace>?B7 ct\<rbrace> get_thread_state ct \<lbrace>?B8 ct\<rbrace>
 10. \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>?B7\<rbrace>
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>ct ct_st x2 it target_prio ct_prio fastfail cur_dom. \<lbrace>?B59 ct ct_st (switch_thread x2) x2 () 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> valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> st_tcb_at runnable x2 s \<and> not_cur_thread x2 s \<and> valid_blocked_except x2 s \<and> scheduler_action s = switch_thread x2 \<and> valid_list s \<and> integrity aag X st s \<and> pas_refined aag s \<and> pasMayEditReadyQueues aag) \<and> ((fastfail \<longrightarrow> highest) \<longrightarrow> (runnable ct_st \<and> ct_prio = target_prio \<longrightarrow> invs s \<and> valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> st_tcb_at runnable x2 s \<and> not_cur_thread x2 s \<and> valid_blocked_except x2 s \<and> scheduler_action s = switch_thread x2 \<and> valid_list s \<and> integrity aag X st s \<and> pas_refined aag s \<and> pasMayEditReadyQueues aag) \<and> ((runnable ct_st \<longrightarrow> ct_prio \<noteq> target_prio) \<longrightarrow> integrity aag X st s \<and> pas_refined aag s \<and> pasMayEditReadyQueues aag))\<rbrace>
 2. \<And>ct ct_st x x2 y it target_prio ct_prio fastfail. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B58 ct ct_st x x2 y it target_prio ct_prio fastfail\<rbrace> gets cur_domain \<lbrace>?B59 ct ct_st x x2 y it target_prio ct_prio fastfail\<rbrace>
 3. \<And>ct ct_st x x2 y it target_prio ct_prio. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B57 ct ct_st x x2 y it target_prio ct_prio\<rbrace> schedule_switch_thread_fastfail ct it ct_prio target_prio \<lbrace>?B58 ct ct_st x x2 y it target_prio ct_prio\<rbrace>
 4. \<And>ct ct_st x x2 y it target_prio. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B56 ct ct_st x x2 y it target_prio\<rbrace> ethread_get_when (ct \<noteq> it) tcb_priority ct \<lbrace>?B57 ct ct_st x x2 y it target_prio\<rbrace>
 5. \<And>ct ct_st x x2 y it. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B55 ct ct_st x x2 y it\<rbrace> ethread_get tcb_priority x2 \<lbrace>?B56 ct ct_st x x2 y it\<rbrace>
 6. \<And>ct ct_st x x2 y. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B54 ct ct_st x x2 y\<rbrace> gets idle_thread \<lbrace>?B55 ct ct_st x x2 y\<rbrace>
 7. \<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>?B54 ct ct_st x x2\<rbrace>
 8. \<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> integrity aag X st 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 \<lambda>s. invs s \<and> (valid_sched_except_blocked and st_tcb_at runnable ct and not_cur_thread ct and valid_blocked_except ct) s \<and> valid_list s \<and> integrity aag X st s \<and> pas_refined aag s \<and> K (pasMayEditReadyQueues aag) s \<and> scheduler_action s = choose_new_thread else (\<lambda>s. invs s \<and> valid_sched s \<and> valid_list s \<and> integrity aag X st s \<and> pas_refined aag s \<and> K (pasMayEditReadyQueues aag) s \<and> scheduler_action s = choose_new_thread)) s)\<rbrace>
 9. \<And>ct. \<lbrace>?B7 ct\<rbrace> get_thread_state ct \<lbrace>?B8 ct\<rbrace>
 10. \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>?B7\<rbrace>
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>ct ct_st x x2 y it target_prio ct_prio fastfail. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B58 ct ct_st x x2 y it target_prio ct_prio fastfail\<rbrace> gets cur_domain \<lbrace>\<lambda>a b. (invs b \<and> valid_etcbs b \<and> valid_queues b \<and> ct_not_in_q b \<and> valid_sched_action b \<and> ct_in_cur_domain b \<and> valid_idle_etcb b \<and> st_tcb_at runnable x2 b \<and> not_cur_thread x2 b \<and> valid_blocked_except x2 b \<and> scheduler_action b = x \<and> valid_list b \<and> integrity aag X st b \<and> pas_refined aag b \<and> pasMayEditReadyQueues aag) \<and> (invs b \<and> valid_etcbs b \<and> valid_queues b \<and> ct_not_in_q b \<and> valid_sched_action b \<and> ct_in_cur_domain b \<and> valid_idle_etcb b \<and> st_tcb_at runnable x2 b \<and> not_cur_thread x2 b \<and> valid_blocked_except x2 b \<and> scheduler_action b = x \<and> valid_list b \<and> integrity aag X st b \<and> pas_refined aag b \<and> pasMayEditReadyQueues aag) \<and> integrity aag X st b \<and> pas_refined aag b \<and> pasMayEditReadyQueues aag\<rbrace>
 2. \<And>ct ct_st x x2 y it target_prio ct_prio. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B57 ct ct_st x x2 y it target_prio ct_prio\<rbrace> schedule_switch_thread_fastfail ct it ct_prio target_prio \<lbrace>?B58 ct ct_st x x2 y it target_prio ct_prio\<rbrace>
 3. \<And>ct ct_st x x2 y it target_prio. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B56 ct ct_st x x2 y it target_prio\<rbrace> ethread_get_when (ct \<noteq> it) tcb_priority ct \<lbrace>?B57 ct ct_st x x2 y it target_prio\<rbrace>
 4. \<And>ct ct_st x x2 y it. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B55 ct ct_st x x2 y it\<rbrace> ethread_get tcb_priority x2 \<lbrace>?B56 ct ct_st x x2 y it\<rbrace>
 5. \<And>ct ct_st x x2 y. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B54 ct ct_st x x2 y\<rbrace> gets idle_thread \<lbrace>?B55 ct ct_st x x2 y\<rbrace>
 6. \<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>?B54 ct ct_st x x2\<rbrace>
 7. \<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> integrity aag X st 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 \<lambda>s. invs s \<and> (valid_sched_except_blocked and st_tcb_at runnable ct and not_cur_thread ct and valid_blocked_except ct) s \<and> valid_list s \<and> integrity aag X st s \<and> pas_refined aag s \<and> K (pasMayEditReadyQueues aag) s \<and> scheduler_action s = choose_new_thread else (\<lambda>s. invs s \<and> valid_sched s \<and> valid_list s \<and> integrity aag X st s \<and> pas_refined aag s \<and> K (pasMayEditReadyQueues aag) s \<and> scheduler_action s = choose_new_thread)) s)\<rbrace>
 8. \<And>ct. \<lbrace>?B7 ct\<rbrace> get_thread_state ct \<lbrace>?B8 ct\<rbrace>
 9. \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>?B7\<rbrace>
 10. \<And>s. (einvs and integrity aag X st and pas_refined aag and guarded_pas_domain aag and (\<lambda>y. pasMayEditReadyQueues aag)) s \<Longrightarrow> ?Q6 s proof (prove)
goal (1 subgoal):
 1. \<And>s sta. \<lbrakk>invs s; valid_list s; valid_sched s; integrity aag X st s; pas_refined aag s; guarded_pas_domain aag s; pasMayEditReadyQueues aag; st_tcb_at ((=) sta) (cur_thread s) s\<rbrakk> \<Longrightarrow> (\<forall>x. scheduler_action s = switch_thread x \<longrightarrow> (if runnable sta then \<lambda>sa. invs sa \<and> valid_etcbs sa \<and> valid_queues sa \<and> st_tcb_at runnable (cur_thread s) sa \<and> ct_not_in_q sa \<and> not_cur_thread (cur_thread s) sa \<and> valid_sched_action sa \<and> ct_in_cur_domain sa \<and> valid_idle_etcb sa \<and> st_tcb_at runnable x sa \<and> not_cur_thread x sa \<and> valid_blocked_except x sa \<and> scheduler_action sa = switch_thread x \<and> valid_list sa \<and> integrity aag X st sa \<and> pas_refined aag sa \<and> invs sa \<and> valid_etcbs sa \<and> valid_queues sa \<and> st_tcb_at runnable (cur_thread s) sa \<and> ct_not_in_q sa \<and> not_cur_thread (cur_thread s) sa \<and> valid_sched_action sa \<and> ct_in_cur_domain sa \<and> valid_idle_etcb sa \<and> st_tcb_at runnable x sa \<and> not_cur_thread x sa \<and> valid_blocked_except x sa \<and> scheduler_action sa = switch_thread x \<and> valid_list sa \<and> integrity aag X st sa \<and> pas_refined aag sa \<and> integrity aag X st sa \<and> pas_refined aag sa else (\<lambda>s. invs s \<and> valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> st_tcb_at runnable x s \<and> not_cur_thread x s \<and> valid_blocked_except x s \<and> scheduler_action s = switch_thread x \<and> valid_list s \<and> integrity aag X st s \<and> pas_refined aag s \<and> invs s \<and> valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> st_tcb_at runnable x s \<and> not_cur_thread x s \<and> valid_blocked_except x s \<and> scheduler_action s = switch_thread x \<and> valid_list s \<and> integrity aag X st s \<and> pas_refined aag s)) s) \<and> (scheduler_action s = choose_new_thread \<longrightarrow> (if runnable sta then \<lambda>sa. invs sa \<and> valid_etcbs sa \<and> valid_queues sa \<and> ct_not_in_q sa \<and> valid_sched_action sa \<and> ct_in_cur_domain sa \<and> valid_idle_etcb sa \<and> st_tcb_at runnable (cur_thread s) sa \<and> not_cur_thread (cur_thread s) sa \<and> valid_blocked_except (cur_thread s) sa \<and> valid_list sa \<and> integrity aag X st sa \<and> pas_refined aag sa \<and> scheduler_action sa = choose_new_thread else (\<lambda>s. invs s \<and> valid_sched s \<and> valid_list s \<and> integrity aag X st s \<and> pas_refined aag s \<and> scheduler_action s = choose_new_thread)) s) proof (prove)
goal (1 subgoal):
 1. \<And>s sta. \<lbrakk>invs s; valid_list s; valid_sched s; integrity aag X st s; pas_refined aag s; guarded_pas_domain aag s; pasMayEditReadyQueues aag; st_tcb_at ((=) sta) (cur_thread s) s\<rbrakk> \<Longrightarrow> (\<forall>x. scheduler_action s = switch_thread x \<longrightarrow> (runnable sta \<longrightarrow> valid_etcbs s \<and> valid_queues s \<and> st_tcb_at runnable (cur_thread s) s \<and> ct_not_in_q_2 (ready_queues s) (switch_thread x) (cur_thread s) \<and> not_cur_thread_2 (cur_thread s) (switch_thread x) (cur_thread s) \<and> valid_sched_action_2 (switch_thread x) (ekheap s) (kheap s) (cur_thread s) (cur_domain s) \<and> valid_idle_etcb s \<and> st_tcb_at runnable x s \<and> not_cur_thread_2 x (switch_thread x) (cur_thread s) \<and> valid_blocked_except_2 x (ready_queues s) (kheap s) (switch_thread x) (cur_thread s)) \<and> (\<not> runnable sta \<longrightarrow> valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q_2 (ready_queues s) (switch_thread x) (cur_thread s) \<and> valid_sched_action_2 (switch_thread x) (ekheap s) (kheap s) (cur_thread s) (cur_domain s) \<and> valid_idle_etcb s \<and> st_tcb_at runnable x s \<and> not_cur_thread_2 x (switch_thread x) (cur_thread s) \<and> valid_blocked_except_2 x (ready_queues s) (kheap s) (switch_thread x) (cur_thread s))) \<and> (scheduler_action s = choose_new_thread \<longrightarrow> (runnable sta \<longrightarrow> valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q_2 (ready_queues s) choose_new_thread (cur_thread s) \<and> valid_idle_etcb s \<and> st_tcb_at runnable (cur_thread s) s \<and> not_cur_thread_2 (cur_thread s) choose_new_thread (cur_thread s) \<and> valid_blocked_except_2 (cur_thread s) (ready_queues s) (kheap s) choose_new_thread (cur_thread s)) \<and> (\<not> runnable sta \<longrightarrow> valid_sched_2 (ready_queues s) (ekheap s) choose_new_thread (cur_domain s) (kheap s) (cur_thread s) (idle_thread s))) proof (prove)
goal (2 subgoals):
 1. \<And>s sta x. \<lbrakk>invs s; valid_list s; valid_sched s; integrity aag X st s; pas_refined aag s; guarded_pas_domain aag s; pasMayEditReadyQueues aag; st_tcb_at ((=) sta) (cur_thread s) s; scheduler_action s = switch_thread x; runnable sta\<rbrakk> \<Longrightarrow> st_tcb_at runnable (cur_thread s) s
 2. \<And>s sta. \<lbrakk>invs s; valid_list s; valid_sched s; integrity aag X st s; pas_refined aag s; guarded_pas_domain aag s; pasMayEditReadyQueues aag; st_tcb_at ((=) sta) (cur_thread s) s; scheduler_action s = choose_new_thread; runnable sta\<rbrakk> \<Longrightarrow> st_tcb_at runnable (cur_thread s) s proof (prove)
goal:
No subgoals!