theory Fastpath_Equiv

lemma schedule_rewrite_ct_not_runnable':
  "monadic_rewrite True True
            (\<lambda>s. ksSchedulerAction s = SwitchToThread t \<and> ct_in_state' (Not \<circ> runnable') s
                 \<and> (ksCurThread s \<noteq> ksIdleThread s)
                 \<and> fastpathBestSwitchCandidate t s)
            (schedule)
            (do setSchedulerAction ResumeCurrentThread; switchToThread t od)" supply subst_all [simp del] apply (simp add: schedule_def) 
  (* switching to t *)
   apply (monadic_rewrite_l sched_act_SwitchToThread_rewrite[where t=t]) 
   (* not wasRunnable, skip enqueue *)
    apply (simp add: when_def) apply (monadic_rewrite_l monadic_rewrite_if_l_False) 
   (* fastpath: \<not> (fastfail \<and> \<not> highest) *)
    apply (monadic_rewrite_l monadic_rewrite_if_l_False
            \<open>wpsimp simp: isHighestPrio_def'
                    wp: hoare_vcg_imp_lift hoare_vcg_disj_lift threadGet_wp''
                        scheduleSwitchThreadFastfail_False_wp\<close>) 
   (* fastpath: no scheduleChooseNewThread *)
    apply (monadic_rewrite_l monadic_rewrite_if_l_False
            \<open>wpsimp simp: isHighestPrio_def'
                    wp: hoare_vcg_imp_lift hoare_vcg_disj_lift threadGet_wp''
                        scheduleSwitchThreadFastfail_False_wp\<close>) 
   (* remove no-ops *)
    apply (repeat 10 monadic_rewrite_symb_exec_l)  (* until switchToThread *)
               apply (simp add: setSchedulerAction_def) apply (subst oblivious_modify_swap[symmetric],
                     rule oblivious_switchToThread_schact) apply (rule monadic_rewrite_refl) apply (wpsimp wp: empty_fail_isRunnable simp: isHighestPrio_def')+ apply (clarsimp simp: ct_in_state'_def not_pred_tcb_at'_strengthen
                        fastpathBestSwitchCandidate_def) apply normalise_obj_at' done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite True True (\<lambda>s. ksSchedulerAction s = SwitchToThread t \<and> ct_in_state' (Not \<circ> runnable') s \<and> ksCurThread s \<noteq> ksIdleThread s \<and> fastpathBestSwitchCandidate t s) ThreadDecls_H.schedule (do setSchedulerAction ResumeCurrentThread;
global.switchToThread t
od) proof (prove)
goal (1 subgoal):
 1. monadic_rewrite True True (\<lambda>s. ksSchedulerAction s = SwitchToThread t \<and> ct_in_state' (Not \<circ> runnable') s \<and> ksCurThread s \<noteq> ksIdleThread s \<and> fastpathBestSwitchCandidate t s) ThreadDecls_H.schedule (do setSchedulerAction ResumeCurrentThread;
global.switchToThread t
od) proof (prove)
goal (1 subgoal):
 1. monadic_rewrite True True (\<lambda>s. ksSchedulerAction s = SwitchToThread t \<and> ct_in_state' (Not \<circ> runnable') s \<and> ksCurThread s \<noteq> ksIdleThread s \<and> fastpathBestSwitchCandidate t s) (do curThread <- getCurThread;
action <- getSchedulerAction;
case action of ResumeCurrentThread \<Rightarrow> return () | ChooseNewThread \<Rightarrow> do curRunnable <- isRunnable curThread;
when curRunnable $ tcbSchedEnqueue curThread;
scheduleChooseNewThread
od | SwitchToThread candidate \<Rightarrow> do wasRunnable <- isRunnable curThread;
when wasRunnable (tcbSchedEnqueue curThread);
idleThread <- getIdleThread;
targetPrio <- threadGet tcbPriority candidate;
curPrio <- threadGet tcbPriority curThread;
fastfail <- scheduleSwitchThreadFastfail curThread idleThread curPrio targetPrio;
curDom <- curDomain;
highest <- isHighestPrio curDom targetPrio;
if fastfail \<and> \<not> highest then do tcbSchedEnqueue candidate;
setSchedulerAction ChooseNewThread;
scheduleChooseNewThread
od else if wasRunnable \<and> curPrio = targetPrio then do tcbSchedAppend candidate;
setSchedulerAction ChooseNewThread;
scheduleChooseNewThread
od else do global.switchToThread candidate;
setSchedulerAction ResumeCurrentThread
od
od
od) (do y <- setSchedulerAction ResumeCurrentThread;
global.switchToThread t
od) proof (prove)
goal (1 subgoal):
 1. monadic_rewrite True True (\<lambda>s. ksSchedulerAction s = SwitchToThread t \<and> ct_in_state' (Not \<circ> runnable') s \<and> ksCurThread s \<noteq> ksIdleThread s \<and> fastpathBestSwitchCandidate t s) (do curThread <- getCurThread;
action <- getSchedulerAction;
case action of ResumeCurrentThread \<Rightarrow> return () | ChooseNewThread \<Rightarrow> do curRunnable <- isRunnable curThread;
when curRunnable $ tcbSchedEnqueue curThread;
scheduleChooseNewThread
od | SwitchToThread candidate \<Rightarrow> do wasRunnable <- isRunnable curThread;
when wasRunnable (tcbSchedEnqueue curThread);
idleThread <- getIdleThread;
targetPrio <- threadGet tcbPriority candidate;
curPrio <- threadGet tcbPriority curThread;
fastfail <- scheduleSwitchThreadFastfail curThread idleThread curPrio targetPrio;
curDom <- curDomain;
highest <- isHighestPrio curDom targetPrio;
if fastfail \<and> \<not> highest then do tcbSchedEnqueue candidate;
setSchedulerAction ChooseNewThread;
scheduleChooseNewThread
od else if wasRunnable \<and> curPrio = targetPrio then do tcbSchedAppend candidate;
setSchedulerAction ChooseNewThread;
scheduleChooseNewThread
od else do global.switchToThread candidate;
setSchedulerAction ResumeCurrentThread
od
od
od) (do y <- setSchedulerAction ResumeCurrentThread;
global.switchToThread t
od) proof (prove)
goal (2 subgoals):
 1. monadic_rewrite True True ?Q1 (do curThread <- getCurThread;
action <- getSchedulerAction;
wasRunnable <- isRunnable curThread;
when wasRunnable (tcbSchedEnqueue curThread);
idleThread <- getIdleThread;
targetPrio <- threadGet tcbPriority t;
curPrio <- threadGet tcbPriority curThread;
fastfail <- scheduleSwitchThreadFastfail curThread idleThread curPrio targetPrio;
curDom <- curDomain;
highest <- isHighestPrio curDom targetPrio;
if fastfail \<and> \<not> highest then do tcbSchedEnqueue t;
setSchedulerAction ChooseNewThread;
scheduleChooseNewThread
od else if wasRunnable \<and> curPrio = targetPrio then do tcbSchedAppend t;
setSchedulerAction ChooseNewThread;
scheduleChooseNewThread
od else do global.switchToThread t;
setSchedulerAction ResumeCurrentThread
od
od) (do y <- setSchedulerAction ResumeCurrentThread;
global.switchToThread t
od)
 2. \<And>s. ksSchedulerAction s = SwitchToThread t \<and> ct_in_state' (Not \<circ> runnable') s \<and> ksCurThread s \<noteq> ksIdleThread s \<and> fastpathBestSwitchCandidate t s \<Longrightarrow> ((\<lambda>s. ((\<lambda>_. ksSchedulerAction s = SwitchToThread t) and (\<lambda>_. True)) s) and ?Q1) s proof (prove)
goal (2 subgoals):
 1. monadic_rewrite True True ?Q1 (do curThread <- getCurThread;
action <- getSchedulerAction;
wasRunnable <- isRunnable curThread;
when wasRunnable (tcbSchedEnqueue curThread);
idleThread <- getIdleThread;
targetPrio <- threadGet tcbPriority t;
curPrio <- threadGet tcbPriority curThread;
fastfail <- scheduleSwitchThreadFastfail curThread idleThread curPrio targetPrio;
curDom <- curDomain;
highest <- isHighestPrio curDom targetPrio;
if fastfail \<and> \<not> highest then do tcbSchedEnqueue t;
setSchedulerAction ChooseNewThread;
scheduleChooseNewThread
od else if wasRunnable \<and> curPrio = targetPrio then do tcbSchedAppend t;
setSchedulerAction ChooseNewThread;
scheduleChooseNewThread
od else do global.switchToThread t;
setSchedulerAction ResumeCurrentThread
od
od) (do y <- setSchedulerAction ResumeCurrentThread;
global.switchToThread t
od)
 2. \<And>s. ksSchedulerAction s = SwitchToThread t \<and> ct_in_state' (Not \<circ> runnable') s \<and> ksCurThread s \<noteq> ksIdleThread s \<and> fastpathBestSwitchCandidate t s \<Longrightarrow> ((\<lambda>s. ((\<lambda>_. ksSchedulerAction s = SwitchToThread t) and (\<lambda>_. True)) s) and ?Q1) s proof (prove)
goal (2 subgoals):
 1. monadic_rewrite True True ?Q1 (do curThread <- getCurThread;
action <- getSchedulerAction;
wasRunnable <- isRunnable curThread;
y <- if wasRunnable then tcbSchedEnqueue curThread else return ();
idleThread <- getIdleThread;
targetPrio <- threadGet tcbPriority t;
curPrio <- threadGet tcbPriority curThread;
fastfail <- scheduleSwitchThreadFastfail curThread idleThread curPrio targetPrio;
curDom <- curDomain;
highest <- isHighestPrio curDom targetPrio;
if fastfail \<and> \<not> highest then do y <- tcbSchedEnqueue t;
y <- setSchedulerAction ChooseNewThread;
scheduleChooseNewThread
od else if wasRunnable \<and> curPrio = targetPrio then do y <- tcbSchedAppend t;
y <- setSchedulerAction ChooseNewThread;
scheduleChooseNewThread
od else do y <- global.switchToThread t;
setSchedulerAction ResumeCurrentThread
od
od) (do y <- setSchedulerAction ResumeCurrentThread;
global.switchToThread t
od)
 2. \<And>s. ksSchedulerAction s = SwitchToThread t \<and> ct_in_state' (Not \<circ> runnable') s \<and> ksCurThread s \<noteq> ksIdleThread s \<and> fastpathBestSwitchCandidate t s \<Longrightarrow> ((\<lambda>s. ((\<lambda>_. ksSchedulerAction s = SwitchToThread t) and (\<lambda>_. True)) s) and ?Q1) s proof (prove)
goal (2 subgoals):
 1. monadic_rewrite True True ?Q37 (do curThread <- getCurThread;
action <- getSchedulerAction;
wasRunnable <- isRunnable curThread;
y <- return ();
idleThread <- getIdleThread;
targetPrio <- threadGet tcbPriority t;
curPrio <- threadGet tcbPriority curThread;
fastfail <- scheduleSwitchThreadFastfail curThread idleThread curPrio targetPrio;
curDom <- curDomain;
highest <- isHighestPrio curDom targetPrio;
if fastfail \<and> \<not> highest then do y <- tcbSchedEnqueue t;
y <- setSchedulerAction ChooseNewThread;
scheduleChooseNewThread
od else if wasRunnable \<and> curPrio = targetPrio then do y <- tcbSchedAppend t;
y <- setSchedulerAction ChooseNewThread;
scheduleChooseNewThread
od else do y <- global.switchToThread t;
setSchedulerAction ResumeCurrentThread
od
od) (do y <- setSchedulerAction ResumeCurrentThread;
global.switchToThread t
od)
 2. \<And>s. ksSchedulerAction s = SwitchToThread t \<and> ct_in_state' (Not \<circ> runnable') s \<and> ksCurThread s \<noteq> ksIdleThread s \<and> fastpathBestSwitchCandidate t s \<Longrightarrow> ((\<lambda>s. ((\<lambda>_. ksSchedulerAction s = SwitchToThread t) and (\<lambda>_. True)) s) and ((\<lambda>s. ((\<lambda>_. \<not> st_tcb_at' runnable' (ksCurThread s) s) and (\<lambda>_. True)) s) and ?Q37)) s proof (prove)
goal (2 subgoals):
 1. monadic_rewrite True True ?Q37 (do curThread <- getCurThread;
action <- getSchedulerAction;
wasRunnable <- isRunnable curThread;
y <- return ();
idleThread <- getIdleThread;
targetPrio <- threadGet tcbPriority t;
curPrio <- threadGet tcbPriority curThread;
fastfail <- scheduleSwitchThreadFastfail curThread idleThread curPrio targetPrio;
curDom <- curDomain;
highest <- isHighestPrio curDom targetPrio;
if fastfail \<and> \<not> highest then do y <- tcbSchedEnqueue t;
y <- setSchedulerAction ChooseNewThread;
scheduleChooseNewThread
od else if wasRunnable \<and> curPrio = targetPrio then do y <- tcbSchedAppend t;
y <- setSchedulerAction ChooseNewThread;
scheduleChooseNewThread
od else do y <- global.switchToThread t;
setSchedulerAction ResumeCurrentThread
od
od) (do y <- setSchedulerAction ResumeCurrentThread;
global.switchToThread t
od)
 2. \<And>s. ksSchedulerAction s = SwitchToThread t \<and> ct_in_state' (Not \<circ> runnable') s \<and> ksCurThread s \<noteq> ksIdleThread s \<and> fastpathBestSwitchCandidate t s \<Longrightarrow> ((\<lambda>s. ((\<lambda>_. ksSchedulerAction s = SwitchToThread t) and (\<lambda>_. True)) s) and ((\<lambda>s. ((\<lambda>_. \<not> st_tcb_at' runnable' (ksCurThread s) s) and (\<lambda>_. True)) s) and ?Q37)) s proof (prove)
goal (2 subgoals):
 1. monadic_rewrite True True ?Q87 (do curThread <- getCurThread;
action <- getSchedulerAction;
wasRunnable <- isRunnable curThread;
y <- return ();
idleThread <- getIdleThread;
targetPrio <- threadGet tcbPriority t;
curPrio <- threadGet tcbPriority curThread;
fastfail <- scheduleSwitchThreadFastfail curThread idleThread curPrio targetPrio;
curDom <- curDomain;
highest <- isHighestPrio curDom targetPrio;
if wasRunnable \<and> curPrio = targetPrio then do y <- tcbSchedAppend t;
y <- setSchedulerAction ChooseNewThread;
scheduleChooseNewThread
od else do y <- global.switchToThread t;
setSchedulerAction ResumeCurrentThread
od
od) (do y <- setSchedulerAction ResumeCurrentThread;
global.switchToThread t
od)
 2. \<And>s. ksSchedulerAction s = SwitchToThread t \<and> ct_in_state' (Not \<circ> runnable') s \<and> ksCurThread s \<noteq> ksIdleThread s \<and> fastpathBestSwitchCandidate t s \<Longrightarrow> ((\<lambda>s. ((\<lambda>_. ksSchedulerAction s = SwitchToThread t) and (\<lambda>_. True)) s) and ((\<lambda>s. ((\<lambda>_. \<not> st_tcb_at' runnable' (ksCurThread s) s) and (\<lambda>_. True)) s) and ((\<lambda>s. (\<forall>v. obj_at' (\<lambda>tcb. tcbPriority tcb = v) t s \<longrightarrow> (\<forall>va. obj_at' (\<lambda>tcb. tcbPriority tcb = va) (ksCurThread s) s \<longrightarrow> ksCurThread s \<noteq> ksIdleThread s \<and> va \<le> v)) \<or> (\<forall>v. obj_at' (\<lambda>tcb. tcbPriority tcb = v) t s \<longrightarrow> (\<forall>v. obj_at' (\<lambda>tcb. tcbPriority tcb = v) (ksCurThread s) s \<longrightarrow> ksReadyQueuesL1Bitmap s (ksCurDomain s) = 0)) \<or> (\<forall>v. obj_at' (\<lambda>tcb. tcbPriority tcb = v) t s \<longrightarrow> (\<forall>va. obj_at' (\<lambda>tcb. tcbPriority tcb = va) (ksCurThread s) s \<longrightarrow> lookupBitmapPriority (ksCurDomain s) s \<le> v))) and ?Q87))) s proof (prove)
goal (2 subgoals):
 1. monadic_rewrite True True ?Q87 (do curThread <- getCurThread;
action <- getSchedulerAction;
wasRunnable <- isRunnable curThread;
y <- return ();
idleThread <- getIdleThread;
targetPrio <- threadGet tcbPriority t;
curPrio <- threadGet tcbPriority curThread;
fastfail <- scheduleSwitchThreadFastfail curThread idleThread curPrio targetPrio;
curDom <- curDomain;
highest <- isHighestPrio curDom targetPrio;
if wasRunnable \<and> curPrio = targetPrio then do y <- tcbSchedAppend t;
y <- setSchedulerAction ChooseNewThread;
scheduleChooseNewThread
od else do y <- global.switchToThread t;
setSchedulerAction ResumeCurrentThread
od
od) (do y <- setSchedulerAction ResumeCurrentThread;
global.switchToThread t
od)
 2. \<And>s. ksSchedulerAction s = SwitchToThread t \<and> ct_in_state' (Not \<circ> runnable') s \<and> ksCurThread s \<noteq> ksIdleThread s \<and> fastpathBestSwitchCandidate t s \<Longrightarrow> ((\<lambda>s. ((\<lambda>_. ksSchedulerAction s = SwitchToThread t) and (\<lambda>_. True)) s) and ((\<lambda>s. ((\<lambda>_. \<not> st_tcb_at' runnable' (ksCurThread s) s) and (\<lambda>_. True)) s) and ((\<lambda>s. (\<forall>v. obj_at' (\<lambda>tcb. tcbPriority tcb = v) t s \<longrightarrow> (\<forall>va. obj_at' (\<lambda>tcb. tcbPriority tcb = va) (ksCurThread s) s \<longrightarrow> ksCurThread s \<noteq> ksIdleThread s \<and> va \<le> v)) \<or> (\<forall>v. obj_at' (\<lambda>tcb. tcbPriority tcb = v) t s \<longrightarrow> (\<forall>v. obj_at' (\<lambda>tcb. tcbPriority tcb = v) (ksCurThread s) s \<longrightarrow> ksReadyQueuesL1Bitmap s (ksCurDomain s) = 0)) \<or> (\<forall>v. obj_at' (\<lambda>tcb. tcbPriority tcb = v) t s \<longrightarrow> (\<forall>va. obj_at' (\<lambda>tcb. tcbPriority tcb = va) (ksCurThread s) s \<longrightarrow> lookupBitmapPriority (ksCurDomain s) s \<le> v))) and ?Q87))) s proof (prove)
goal (2 subgoals):
 1. monadic_rewrite True True ?Q240 (do curThread <- getCurThread;
action <- getSchedulerAction;
wasRunnable <- isRunnable curThread;
y <- return ();
idleThread <- getIdleThread;
targetPrio <- threadGet tcbPriority t;
curPrio <- threadGet tcbPriority curThread;
fastfail <- scheduleSwitchThreadFastfail curThread idleThread curPrio targetPrio;
curDom <- curDomain;
highest <- isHighestPrio curDom targetPrio;
y <- global.switchToThread t;
setSchedulerAction ResumeCurrentThread
od) (do y <- setSchedulerAction ResumeCurrentThread;
global.switchToThread t
od)
 2. \<And>s. ksSchedulerAction s = SwitchToThread t \<and> ct_in_state' (Not \<circ> runnable') s \<and> ksCurThread s \<noteq> ksIdleThread s \<and> fastpathBestSwitchCandidate t s \<Longrightarrow> ((\<lambda>s. ((\<lambda>_. ksSchedulerAction s = SwitchToThread t) and (\<lambda>_. True)) s) and ((\<lambda>s. ((\<lambda>_. \<not> st_tcb_at' runnable' (ksCurThread s) s) and (\<lambda>_. True)) s) and ((\<lambda>s. (\<forall>v. obj_at' (\<lambda>tcb. tcbPriority tcb = v) t s \<longrightarrow> (\<forall>va. obj_at' (\<lambda>tcb. tcbPriority tcb = va) (ksCurThread s) s \<longrightarrow> ksCurThread s \<noteq> ksIdleThread s \<and> va \<le> v)) \<or> (\<forall>v. obj_at' (\<lambda>tcb. tcbPriority tcb = v) t s \<longrightarrow> (\<forall>v. obj_at' (\<lambda>tcb. tcbPriority tcb = v) (ksCurThread s) s \<longrightarrow> ksReadyQueuesL1Bitmap s (ksCurDomain s) = 0)) \<or> (\<forall>v. obj_at' (\<lambda>tcb. tcbPriority tcb = v) t s \<longrightarrow> (\<forall>va. obj_at' (\<lambda>tcb. tcbPriority tcb = va) (ksCurThread s) s \<longrightarrow> lookupBitmapPriority (ksCurDomain s) s \<le> v))) and ((\<lambda>s. \<forall>v. obj_at' (\<lambda>tcb. tcbPriority tcb = v) t s \<longrightarrow> (\<forall>va. obj_at' (\<lambda>tcb. tcbPriority tcb = va) (ksCurThread s) s \<longrightarrow> ((\<lambda>_. \<not> (st_tcb_at' runnable' (ksCurThread s) s \<and> va = v)) and (\<lambda>_. True)) s)) and ?Q240)))) s proof (prove)
goal (2 subgoals):
 1. monadic_rewrite True True ?Q240 (do curThread <- getCurThread;
action <- getSchedulerAction;
wasRunnable <- isRunnable curThread;
y <- return ();
idleThread <- getIdleThread;
targetPrio <- threadGet tcbPriority t;
curPrio <- threadGet tcbPriority curThread;
fastfail <- scheduleSwitchThreadFastfail curThread idleThread curPrio targetPrio;
curDom <- curDomain;
highest <- isHighestPrio curDom targetPrio;
y <- global.switchToThread t;
setSchedulerAction ResumeCurrentThread
od) (do y <- setSchedulerAction ResumeCurrentThread;
global.switchToThread t
od)
 2. \<And>s. ksSchedulerAction s = SwitchToThread t \<and> ct_in_state' (Not \<circ> runnable') s \<and> ksCurThread s \<noteq> ksIdleThread s \<and> fastpathBestSwitchCandidate t s \<Longrightarrow> ((\<lambda>s. ((\<lambda>_. ksSchedulerAction s = SwitchToThread t) and (\<lambda>_. True)) s) and ((\<lambda>s. ((\<lambda>_. \<not> st_tcb_at' runnable' (ksCurThread s) s) and (\<lambda>_. True)) s) and ((\<lambda>s. (\<forall>v. obj_at' (\<lambda>tcb. tcbPriority tcb = v) t s \<longrightarrow> (\<forall>va. obj_at' (\<lambda>tcb. tcbPriority tcb = va) (ksCurThread s) s \<longrightarrow> ksCurThread s \<noteq> ksIdleThread s \<and> va \<le> v)) \<or> (\<forall>v. obj_at' (\<lambda>tcb. tcbPriority tcb = v) t s \<longrightarrow> (\<forall>v. obj_at' (\<lambda>tcb. tcbPriority tcb = v) (ksCurThread s) s \<longrightarrow> ksReadyQueuesL1Bitmap s (ksCurDomain s) = 0)) \<or> (\<forall>v. obj_at' (\<lambda>tcb. tcbPriority tcb = v) t s \<longrightarrow> (\<forall>va. obj_at' (\<lambda>tcb. tcbPriority tcb = va) (ksCurThread s) s \<longrightarrow> lookupBitmapPriority (ksCurDomain s) s \<le> v))) and ((\<lambda>s. \<forall>v. obj_at' (\<lambda>tcb. tcbPriority tcb = v) t s \<longrightarrow> (\<forall>va. obj_at' (\<lambda>tcb. tcbPriority tcb = va) (ksCurThread s) s \<longrightarrow> ((\<lambda>_. \<not> (st_tcb_at' runnable' (ksCurThread s) s \<and> va = v)) and (\<lambda>_. True)) s)) and ?Q240)))) s proof (prove)
goal (13 subgoals):
 1. \<And>curThread action wasRunnable y idleThread targetPrio curPrio fastfail curDom highest. monadic_rewrite True True (?Q584 curThread action wasRunnable y idleThread targetPrio curPrio fastfail curDom highest) (do y <- global.switchToThread t;
setSchedulerAction ResumeCurrentThread
od) (do y <- setSchedulerAction ResumeCurrentThread;
global.switchToThread t
od)
 2. \<And>curThread action wasRunnable y idleThread targetPrio curPrio fastfail curDom. empty_fail (isHighestPrio curDom targetPrio)
 3. \<And>curThread action wasRunnable y idleThread targetPrio curPrio fastfail curDom. \<lbrace>?Q559 curThread action wasRunnable y idleThread targetPrio curPrio fastfail curDom\<rbrace> isHighestPrio curDom targetPrio \<lbrace>?Q584 curThread action wasRunnable y idleThread targetPrio curPrio fastfail curDom\<rbrace>
 4. \<And>curThread action wasRunnable y idleThread targetPrio curPrio fastfail. \<lbrace>?Q533 curThread action wasRunnable y idleThread targetPrio curPrio fastfail\<rbrace> curDomain \<lbrace>?Q559 curThread action wasRunnable y idleThread targetPrio curPrio fastfail\<rbrace>
 5. \<And>curThread action wasRunnable y idleThread targetPrio curPrio. \<lbrace>?Q507 curThread action wasRunnable y idleThread targetPrio curPrio\<rbrace> scheduleSwitchThreadFastfail curThread idleThread curPrio targetPrio \<lbrace>?Q533 curThread action wasRunnable y idleThread targetPrio curPrio\<rbrace>
 6. \<And>curThread action wasRunnable y idleThread targetPrio. \<lbrace>?Q481 curThread action wasRunnable y idleThread targetPrio\<rbrace> threadGet tcbPriority curThread \<lbrace>?Q507 curThread action wasRunnable y idleThread targetPrio\<rbrace>
 7. \<And>curThread action wasRunnable y idleThread. \<lbrace>?Q456 curThread action wasRunnable y idleThread\<rbrace> threadGet tcbPriority t \<lbrace>?Q481 curThread action wasRunnable y idleThread\<rbrace>
 8. \<And>curThread action wasRunnable y. \<lbrace>?Q430 curThread action wasRunnable y\<rbrace> getIdleThread \<lbrace>?Q456 curThread action wasRunnable y\<rbrace>
 9. \<And>curThread action wasRunnable. \<lbrace>?Q404 curThread action wasRunnable\<rbrace> return () \<lbrace>?Q430 curThread action wasRunnable\<rbrace>
 10. \<And>curThread action. \<lbrace>?Q379 curThread action\<rbrace> isRunnable curThread \<lbrace>?Q404 curThread action\<rbrace>
A total of 13 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>curThread action wasRunnable y idleThread targetPrio curPrio fastfail curDom highest. monadic_rewrite True True (?Q584 curThread action wasRunnable y idleThread targetPrio curPrio fastfail curDom highest) (do y <- global.switchToThread t;
setSchedulerAction ResumeCurrentThread
od) (do y <- setSchedulerAction ResumeCurrentThread;
global.switchToThread t
od)
 2. \<And>curThread action wasRunnable y idleThread targetPrio curPrio fastfail curDom. empty_fail (isHighestPrio curDom targetPrio)
 3. \<And>curThread action wasRunnable y idleThread targetPrio curPrio fastfail curDom. \<lbrace>?Q559 curThread action wasRunnable y idleThread targetPrio curPrio fastfail curDom\<rbrace> isHighestPrio curDom targetPrio \<lbrace>?Q584 curThread action wasRunnable y idleThread targetPrio curPrio fastfail curDom\<rbrace>
 4. \<And>curThread action wasRunnable y idleThread targetPrio curPrio fastfail. \<lbrace>?Q533 curThread action wasRunnable y idleThread targetPrio curPrio fastfail\<rbrace> curDomain \<lbrace>?Q559 curThread action wasRunnable y idleThread targetPrio curPrio fastfail\<rbrace>
 5. \<And>curThread action wasRunnable y idleThread targetPrio curPrio. \<lbrace>?Q507 curThread action wasRunnable y idleThread targetPrio curPrio\<rbrace> scheduleSwitchThreadFastfail curThread idleThread curPrio targetPrio \<lbrace>?Q533 curThread action wasRunnable y idleThread targetPrio curPrio\<rbrace>
 6. \<And>curThread action wasRunnable y idleThread targetPrio. \<lbrace>?Q481 curThread action wasRunnable y idleThread targetPrio\<rbrace> threadGet tcbPriority curThread \<lbrace>?Q507 curThread action wasRunnable y idleThread targetPrio\<rbrace>
 7. \<And>curThread action wasRunnable y idleThread. \<lbrace>?Q456 curThread action wasRunnable y idleThread\<rbrace> threadGet tcbPriority t \<lbrace>?Q481 curThread action wasRunnable y idleThread\<rbrace>
 8. \<And>curThread action wasRunnable y. \<lbrace>?Q430 curThread action wasRunnable y\<rbrace> getIdleThread \<lbrace>?Q456 curThread action wasRunnable y\<rbrace>
 9. \<And>curThread action wasRunnable. \<lbrace>?Q404 curThread action wasRunnable\<rbrace> return () \<lbrace>?Q430 curThread action wasRunnable\<rbrace>
 10. \<And>curThread action. \<lbrace>?Q379 curThread action\<rbrace> isRunnable curThread \<lbrace>?Q404 curThread action\<rbrace>
A total of 13 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>curThread action wasRunnable idleThread targetPrio curPrio fastfail curDom highest. monadic_rewrite True True (?Q584 curThread action wasRunnable () idleThread targetPrio curPrio fastfail curDom highest) (do y <- global.switchToThread t;
modify (ksSchedulerAction_update (\<lambda>_. ResumeCurrentThread))
od) (do y <- modify (ksSchedulerAction_update (\<lambda>_. ResumeCurrentThread));
global.switchToThread t
od)
 2. \<And>curThread action wasRunnable y idleThread targetPrio curPrio fastfail curDom. empty_fail (isHighestPrio curDom targetPrio)
 3. \<And>curThread action wasRunnable y idleThread targetPrio curPrio fastfail curDom. \<lbrace>?Q559 curThread action wasRunnable y idleThread targetPrio curPrio fastfail curDom\<rbrace> isHighestPrio curDom targetPrio \<lbrace>?Q584 curThread action wasRunnable y idleThread targetPrio curPrio fastfail curDom\<rbrace>
 4. \<And>curThread action wasRunnable y idleThread targetPrio curPrio fastfail. \<lbrace>?Q533 curThread action wasRunnable y idleThread targetPrio curPrio fastfail\<rbrace> curDomain \<lbrace>?Q559 curThread action wasRunnable y idleThread targetPrio curPrio fastfail\<rbrace>
 5. \<And>curThread action wasRunnable y idleThread targetPrio curPrio. \<lbrace>?Q507 curThread action wasRunnable y idleThread targetPrio curPrio\<rbrace> scheduleSwitchThreadFastfail curThread idleThread curPrio targetPrio \<lbrace>?Q533 curThread action wasRunnable y idleThread targetPrio curPrio\<rbrace>
 6. \<And>curThread action wasRunnable y idleThread targetPrio. \<lbrace>?Q481 curThread action wasRunnable y idleThread targetPrio\<rbrace> threadGet tcbPriority curThread \<lbrace>?Q507 curThread action wasRunnable y idleThread targetPrio\<rbrace>
 7. \<And>curThread action wasRunnable y idleThread. \<lbrace>?Q456 curThread action wasRunnable y idleThread\<rbrace> threadGet tcbPriority t \<lbrace>?Q481 curThread action wasRunnable y idleThread\<rbrace>
 8. \<And>curThread action wasRunnable y. \<lbrace>?Q430 curThread action wasRunnable y\<rbrace> getIdleThread \<lbrace>?Q456 curThread action wasRunnable y\<rbrace>
 9. \<And>curThread action wasRunnable. \<lbrace>?Q404 curThread action wasRunnable\<rbrace> return () \<lbrace>?Q430 curThread action wasRunnable\<rbrace>
 10. \<And>curThread action. \<lbrace>?Q379 curThread action\<rbrace> isRunnable curThread \<lbrace>?Q404 curThread action\<rbrace>
A total of 13 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>curThread action wasRunnable idleThread targetPrio curPrio fastfail curDom highest. monadic_rewrite True True (?Q605 curThread action wasRunnable idleThread targetPrio curPrio fastfail curDom highest (?curThread605 curThread action wasRunnable idleThread targetPrio curPrio fastfail curDom highest) (?action605 curThread action wasRunnable idleThread targetPrio curPrio fastfail curDom highest) (?wasRunnable605 curThread action wasRunnable idleThread targetPrio curPrio fastfail curDom highest) () (?idleThread605 curThread action wasRunnable idleThread targetPrio curPrio fastfail curDom highest) (?targetPrio605 curThread action wasRunnable idleThread targetPrio curPrio fastfail curDom highest) (?curPrio605 curThread action wasRunnable idleThread targetPrio curPrio fastfail curDom highest) (?fastfail605 curThread action wasRunnable idleThread targetPrio curPrio fastfail curDom highest) (?curDom605 curThread action wasRunnable idleThread targetPrio curPrio fastfail curDom highest) (?highest605 curThread action wasRunnable idleThread targetPrio curPrio fastfail curDom highest)) (do rv <- modify (ksSchedulerAction_update (\<lambda>_. ResumeCurrentThread));
global.switchToThread t
od) (do y <- modify (ksSchedulerAction_update (\<lambda>_. ResumeCurrentThread));
global.switchToThread t
od)
 2. \<And>curThread action wasRunnable y idleThread targetPrio curPrio fastfail curDom. empty_fail (isHighestPrio curDom targetPrio)
 3. \<And>curThread action wasRunnable y idleThread targetPrio curPrio fastfail curDom. \<lbrace>?Q559 curThread action wasRunnable y idleThread targetPrio curPrio fastfail curDom\<rbrace> isHighestPrio curDom targetPrio \<lbrace>?Q584 curThread action wasRunnable y idleThread targetPrio curPrio fastfail curDom\<rbrace>
 4. \<And>curThread action wasRunnable y idleThread targetPrio curPrio fastfail. \<lbrace>?Q533 curThread action wasRunnable y idleThread targetPrio curPrio fastfail\<rbrace> curDomain \<lbrace>?Q559 curThread action wasRunnable y idleThread targetPrio curPrio fastfail\<rbrace>
 5. \<And>curThread action wasRunnable y idleThread targetPrio curPrio. \<lbrace>?Q507 curThread action wasRunnable y idleThread targetPrio curPrio\<rbrace> scheduleSwitchThreadFastfail curThread idleThread curPrio targetPrio \<lbrace>?Q533 curThread action wasRunnable y idleThread targetPrio curPrio\<rbrace>
 6. \<And>curThread action wasRunnable y idleThread targetPrio. \<lbrace>?Q481 curThread action wasRunnable y idleThread targetPrio\<rbrace> threadGet tcbPriority curThread \<lbrace>?Q507 curThread action wasRunnable y idleThread targetPrio\<rbrace>
 7. \<And>curThread action wasRunnable y idleThread. \<lbrace>?Q456 curThread action wasRunnable y idleThread\<rbrace> threadGet tcbPriority t \<lbrace>?Q481 curThread action wasRunnable y idleThread\<rbrace>
 8. \<And>curThread action wasRunnable y. \<lbrace>?Q430 curThread action wasRunnable y\<rbrace> getIdleThread \<lbrace>?Q456 curThread action wasRunnable y\<rbrace>
 9. \<And>curThread action wasRunnable. \<lbrace>?Q404 curThread action wasRunnable\<rbrace> return () \<lbrace>?Q430 curThread action wasRunnable\<rbrace>
 10. \<And>curThread action. \<lbrace>?Q379 curThread action\<rbrace> isRunnable curThread \<lbrace>?Q404 curThread action\<rbrace>
A total of 13 subgoals...
flex-flex pairs:
\<lambda>curThread action wasRunnable idleThread targetPrio curPrio fastfail curDom highest. ?Q605 curThread action wasRunnable idleThread targetPrio curPrio fastfail curDom highest (?curThread605 curThread action wasRunnable idleThread targetPrio curPrio fastfail curDom highest) (?action605 curThread action wasRunnable idleThread targetPrio curPrio fastfail curDom highest) (?wasRunnable605 curThread action wasRunnable idleThread targetPrio curPrio fastfail curDom highest) () (?idleThread605 curThread action wasRunnable idleThread targetPrio curPrio fastfail curDom highest) (?targetPrio605 curThread action wasRunnable idleThread targetPrio curPrio fastfail curDom highest) (?curPrio605 curThread action wasRunnable idleThread targetPrio curPrio fastfail curDom highest) (?fastfail605 curThread action wasRunnable idleThread targetPrio curPrio fastfail curDom highest) (?curDom605 curThread action wasRunnable idleThread targetPrio curPrio fastfail curDom highest) (?highest605 curThread action wasRunnable idleThread targetPrio curPrio fastfail curDom highest) \<equiv>\<^sup>? \<lambda>curThread action wasRunnable. ?Q584 curThread action wasRunnable () proof (prove)
goal (12 subgoals):
 1. \<And>curThread action wasRunnable y idleThread targetPrio curPrio fastfail curDom. empty_fail (isHighestPrio curDom targetPrio)
 2. \<And>curThread action wasRunnable y idleThread targetPrio curPrio fastfail curDom. \<lbrace>?Q559 curThread action wasRunnable y idleThread targetPrio curPrio fastfail curDom\<rbrace> isHighestPrio curDom targetPrio \<lbrace>\<lambda>a b. True\<rbrace>
 3. \<And>curThread action wasRunnable y idleThread targetPrio curPrio fastfail. \<lbrace>?Q533 curThread action wasRunnable y idleThread targetPrio curPrio fastfail\<rbrace> curDomain \<lbrace>?Q559 curThread action wasRunnable y idleThread targetPrio curPrio fastfail\<rbrace>
 4. \<And>curThread action wasRunnable y idleThread targetPrio curPrio. \<lbrace>?Q507 curThread action wasRunnable y idleThread targetPrio curPrio\<rbrace> scheduleSwitchThreadFastfail curThread idleThread curPrio targetPrio \<lbrace>?Q533 curThread action wasRunnable y idleThread targetPrio curPrio\<rbrace>
 5. \<And>curThread action wasRunnable y idleThread targetPrio. \<lbrace>?Q481 curThread action wasRunnable y idleThread targetPrio\<rbrace> threadGet tcbPriority curThread \<lbrace>?Q507 curThread action wasRunnable y idleThread targetPrio\<rbrace>
 6. \<And>curThread action wasRunnable y idleThread. \<lbrace>?Q456 curThread action wasRunnable y idleThread\<rbrace> threadGet tcbPriority t \<lbrace>?Q481 curThread action wasRunnable y idleThread\<rbrace>
 7. \<And>curThread action wasRunnable y. \<lbrace>?Q430 curThread action wasRunnable y\<rbrace> getIdleThread \<lbrace>?Q456 curThread action wasRunnable y\<rbrace>
 8. \<And>curThread action wasRunnable. \<lbrace>?Q404 curThread action wasRunnable\<rbrace> return () \<lbrace>?Q430 curThread action wasRunnable\<rbrace>
 9. \<And>curThread action. \<lbrace>?Q379 curThread action\<rbrace> isRunnable curThread \<lbrace>?Q404 curThread action\<rbrace>
 10. \<And>curThread. \<lbrace>?Q353 curThread\<rbrace> getSchedulerAction \<lbrace>?Q379 curThread\<rbrace>
A total of 12 subgoals... proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>ksSchedulerAction s = SwitchToThread t; ct_in_state' (Not \<circ> runnable') s; ksCurThread s \<noteq> ksIdleThread s; fastpathBestSwitchCandidate t s\<rbrakk> \<Longrightarrow> \<not> st_tcb_at' runnable' (ksCurThread s) s \<and> ((\<exists>v. obj_at' (\<lambda>tcb. tcbPriority tcb = v) t s) \<longrightarrow> (\<exists>v. obj_at' (\<lambda>tcb. tcbPriority tcb = v) (ksCurThread s) s) \<longrightarrow> (\<forall>v. obj_at' (\<lambda>tcb. tcbPriority tcb = v) t s \<longrightarrow> (\<forall>va. obj_at' (\<lambda>tcb. tcbPriority tcb = va) (ksCurThread s) s \<longrightarrow> va \<le> v)) \<or> ksReadyQueuesL1Bitmap s (ksCurDomain s) = 0 \<or> (\<forall>v. obj_at' (\<lambda>tcb. tcbPriority tcb = v) t s \<longrightarrow> lookupBitmapPriority (ksCurDomain s) s \<le> v)) \<and> (\<forall>v. obj_at' (\<lambda>tcb. tcbPriority tcb = v) t s \<longrightarrow> (\<forall>va. obj_at' (\<lambda>tcb. tcbPriority tcb = va) (ksCurThread s) s \<longrightarrow> st_tcb_at' runnable' (ksCurThread s) s \<longrightarrow> va \<noteq> v)) proof (prove)
goal (1 subgoal):
 1. \<And>s v va vb vc vd. \<lbrakk>ksSchedulerAction s = SwitchToThread t; st_tcb_at' (Not \<circ> runnable') (ksCurThread s) s; ksCurThread s \<noteq> ksIdleThread s; obj_at' (\<lambda>tcb. tcbPriority tcb = v) t s; obj_at' (\<lambda>tcb. tcbPriority tcb = va) (ksCurThread s) s; ksReadyQueuesL1Bitmap s (ksCurDomain s) \<noteq> 0; obj_at' (\<lambda>tcb. tcbPriority tcb = vb) t s; obj_at' (\<lambda>tcb. tcbPriority tcb = vc) t s; \<not> lookupBitmapPriority (ksCurDomain s) s \<le> vc; obj_at' (\<lambda>tcb. tcbPriority tcb = vd) (ksCurThread s) s; \<forall>tprio. obj_at' (\<lambda>tcb. tcbPriority tcb = tprio) t s \<longrightarrow> obj_at' (\<lambda>tcb. tcbPriority tcb \<le> tprio) (ksCurThread s) s \<or> lookupBitmapPriority (ksCurDomain s) s \<le> tprio\<rbrakk> \<Longrightarrow> vd \<le> vb proof (prove)
goal:
No subgoals!