theory Fastpath_Equiv

lemma schedule_known_rewrite:
  "monadic_rewrite True False
      (\<lambda>s. ksSchedulerAction s = SwitchToThread t
               \<and> tcb_at' t s
               \<and> obj_at' (Not \<circ> tcbQueued) t s
               \<and> ksCurThread s = t'
               \<and> st_tcb_at' (Not \<circ> runnable') t' s
               \<and> (ksCurThread s \<noteq> ksIdleThread s)
               \<and> fastpathBestSwitchCandidate t s)
      (schedule)
      (do Arch.switchToThread t;
          setCurThread t;
          setSchedulerAction ResumeCurrentThread od)" supply subst_all[simp del] if_split[split del] apply (simp add: schedule_def) apply (simp only: Thread_H.switchToThread_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>) apply (simp add: bind_assoc) apply (monadic_rewrite_l tcbSchedDequeue_rewrite_not_queued
                            \<open>wpsimp wp: Arch_switchToThread_obj_at_pre\<close>) 
   (* remove no-ops *)
    apply simp apply (repeat 9 \<open>rule monadic_rewrite_symb_exec_l\<close>)  (* until switchToThread *)
                               apply (rule monadic_rewrite_refl) apply (wpsimp 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 False (\<lambda>s. ksSchedulerAction s = SwitchToThread t \<and> tcb_at' t s \<and> obj_at' (Not \<circ> tcbQueued) t s \<and> ksCurThread s = t' \<and> st_tcb_at' (Not \<circ> runnable') t' s \<and> ksCurThread s \<noteq> ksIdleThread s \<and> fastpathBestSwitchCandidate t s) ThreadDecls_H.schedule (do Arch.switchToThread t;
setCurThread t;
setSchedulerAction ResumeCurrentThread
od) proof (prove)
goal (1 subgoal):
 1. monadic_rewrite True False (\<lambda>s. ksSchedulerAction s = SwitchToThread t \<and> tcb_at' t s \<and> obj_at' (Not \<circ> tcbQueued) t s \<and> ksCurThread s = t' \<and> st_tcb_at' (Not \<circ> runnable') t' s \<and> ksCurThread s \<noteq> ksIdleThread s \<and> fastpathBestSwitchCandidate t s) ThreadDecls_H.schedule (do Arch.switchToThread t;
setCurThread t;
setSchedulerAction ResumeCurrentThread
od) proof (prove)
goal (1 subgoal):
 1. monadic_rewrite True False (\<lambda>s. ksSchedulerAction s = SwitchToThread t \<and> tcb_at' t s \<and> obj_at' (Not \<circ> tcbQueued) t s \<and> ksCurThread s = t' \<and> st_tcb_at' (Not \<circ> runnable') t' 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 <- Arch.switchToThread t;
y <- setCurThread t;
setSchedulerAction ResumeCurrentThread
od) proof (prove)
goal (1 subgoal):
 1. monadic_rewrite True False (\<lambda>s. ksSchedulerAction s = SwitchToThread t \<and> tcb_at' t s \<and> obj_at' (Not \<circ> tcbQueued) t s \<and> ksCurThread s = t' \<and> st_tcb_at' (Not \<circ> runnable') t' 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 do Arch.switchToThread candidate;
tcbSchedDequeue candidate;
setCurThread candidate
od;
setSchedulerAction ResumeCurrentThread
od
od
od) (do y <- Arch.switchToThread t;
y <- setCurThread t;
setSchedulerAction ResumeCurrentThread
od) proof (prove)
goal (1 subgoal):
 1. monadic_rewrite True False (\<lambda>s. ksSchedulerAction s = SwitchToThread t \<and> tcb_at' t s \<and> obj_at' (Not \<circ> tcbQueued) t s \<and> ksCurThread s = t' \<and> st_tcb_at' (Not \<circ> runnable') t' 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 do Arch.switchToThread candidate;
tcbSchedDequeue candidate;
setCurThread candidate
od;
setSchedulerAction ResumeCurrentThread
od
od
od) (do y <- Arch.switchToThread t;
y <- setCurThread t;
setSchedulerAction ResumeCurrentThread
od) proof (prove)
goal (2 subgoals):
 1. monadic_rewrite True False ?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 do Arch.switchToThread t;
tcbSchedDequeue t;
setCurThread t
od;
setSchedulerAction ResumeCurrentThread
od
od) (do y <- Arch.switchToThread t;
y <- setCurThread t;
setSchedulerAction ResumeCurrentThread
od)
 2. \<And>s. ksSchedulerAction s = SwitchToThread t \<and> tcb_at' t s \<and> obj_at' (Not \<circ> tcbQueued) t s \<and> ksCurThread s = t' \<and> st_tcb_at' (Not \<circ> runnable') t' 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 False ?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 do Arch.switchToThread t;
tcbSchedDequeue t;
setCurThread t
od;
setSchedulerAction ResumeCurrentThread
od
od) (do y <- Arch.switchToThread t;
y <- setCurThread t;
setSchedulerAction ResumeCurrentThread
od)
 2. \<And>s. ksSchedulerAction s = SwitchToThread t \<and> tcb_at' t s \<and> obj_at' (Not \<circ> tcbQueued) t s \<and> ksCurThread s = t' \<and> st_tcb_at' (Not \<circ> runnable') t' 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 False ?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 <- do y <- Arch.switchToThread t;
y <- tcbSchedDequeue t;
setCurThread t
od;
setSchedulerAction ResumeCurrentThread
od
od) (do y <- Arch.switchToThread t;
y <- setCurThread t;
setSchedulerAction ResumeCurrentThread
od)
 2. \<And>s. ksSchedulerAction s = SwitchToThread t \<and> tcb_at' t s \<and> obj_at' (Not \<circ> tcbQueued) t s \<and> ksCurThread s = t' \<and> st_tcb_at' (Not \<circ> runnable') t' 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 False ?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 <- do y <- Arch.switchToThread t;
y <- tcbSchedDequeue t;
setCurThread t
od;
setSchedulerAction ResumeCurrentThread
od
od) (do y <- Arch.switchToThread t;
y <- setCurThread t;
setSchedulerAction ResumeCurrentThread
od)
 2. \<And>s. ksSchedulerAction s = SwitchToThread t \<and> tcb_at' t s \<and> obj_at' (Not \<circ> tcbQueued) t s \<and> ksCurThread s = t' \<and> st_tcb_at' (Not \<circ> runnable') t' 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 False ?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 <- do y <- Arch.switchToThread t;
y <- tcbSchedDequeue t;
setCurThread t
od;
setSchedulerAction ResumeCurrentThread
od
od) (do y <- Arch.switchToThread t;
y <- setCurThread t;
setSchedulerAction ResumeCurrentThread
od)
 2. \<And>s. ksSchedulerAction s = SwitchToThread t \<and> tcb_at' t s \<and> obj_at' (Not \<circ> tcbQueued) t s \<and> ksCurThread s = t' \<and> st_tcb_at' (Not \<circ> runnable') t' 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 False ?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 <- do y <- Arch.switchToThread t;
y <- tcbSchedDequeue t;
setCurThread t
od;
setSchedulerAction ResumeCurrentThread
od
od) (do y <- Arch.switchToThread t;
y <- setCurThread t;
setSchedulerAction ResumeCurrentThread
od)
 2. \<And>s. ksSchedulerAction s = SwitchToThread t \<and> tcb_at' t s \<and> obj_at' (Not \<circ> tcbQueued) t s \<and> ksCurThread s = t' \<and> st_tcb_at' (Not \<circ> runnable') t' 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 False ?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 <- do y <- Arch.switchToThread t;
y <- tcbSchedDequeue t;
setCurThread t
od;
setSchedulerAction ResumeCurrentThread
od
od) (do y <- Arch.switchToThread t;
y <- setCurThread t;
setSchedulerAction ResumeCurrentThread
od)
 2. \<And>s. ksSchedulerAction s = SwitchToThread t \<and> tcb_at' t s \<and> obj_at' (Not \<circ> tcbQueued) t s \<and> ksCurThread s = t' \<and> st_tcb_at' (Not \<circ> runnable') t' 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 False ?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 <- do y <- Arch.switchToThread t;
y <- tcbSchedDequeue t;
setCurThread t
od;
setSchedulerAction ResumeCurrentThread
od) (do y <- Arch.switchToThread t;
y <- setCurThread t;
setSchedulerAction ResumeCurrentThread
od)
 2. \<And>s. ksSchedulerAction s = SwitchToThread t \<and> tcb_at' t s \<and> obj_at' (Not \<circ> tcbQueued) t s \<and> ksCurThread s = t' \<and> st_tcb_at' (Not \<circ> runnable') t' 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 False ?Q240 (do curThread <- getCurThread;
action <- getSchedulerAction;
wasRunnable <- isRunnable curThread;
idleThread <- getIdleThread;
targetPrio <- threadGet tcbPriority t;
curPrio <- threadGet tcbPriority curThread;
fastfail <- scheduleSwitchThreadFastfail curThread idleThread curPrio targetPrio;
curDom <- curDomain;
highest <- isHighestPrio curDom targetPrio;
y <- Arch.switchToThread t;
y <- tcbSchedDequeue t;
y <- setCurThread t;
setSchedulerAction ResumeCurrentThread
od) (do y <- Arch.switchToThread t;
y <- setCurThread t;
setSchedulerAction ResumeCurrentThread
od)
 2. \<And>s. ksSchedulerAction s = SwitchToThread t \<and> tcb_at' t s \<and> obj_at' (Not \<circ> tcbQueued) t s \<and> ksCurThread s = t' \<and> st_tcb_at' (Not \<circ> runnable') t' 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 False ?Q352 (do curThread <- getCurThread;
action <- getSchedulerAction;
wasRunnable <- isRunnable curThread;
x <- getIdleThread;
targetPrio <- threadGet tcbPriority t;
curPrio <- threadGet tcbPriority curThread;
fastfail <- scheduleSwitchThreadFastfail curThread x curPrio targetPrio;
curDom <- curDomain;
highest <- isHighestPrio curDom targetPrio;
y <- Arch.switchToThread t;
y <- return ();
y <- setCurThread t;
setSchedulerAction ResumeCurrentThread
od) (do y <- Arch.switchToThread t;
y <- setCurThread t;
setSchedulerAction ResumeCurrentThread
od)
 2. \<And>s. ksSchedulerAction s = SwitchToThread t \<and> tcb_at' t s \<and> obj_at' (Not \<circ> tcbQueued) t s \<and> ksCurThread s = t' \<and> st_tcb_at' (Not \<circ> runnable') t' 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 ((\<lambda>s. tcb_at' t s \<and> obj_at' (Not \<circ> tcbQueued) t s) and ?Q352))))) s proof (prove)
goal (2 subgoals):
 1. monadic_rewrite True False ?Q352 (do curThread <- getCurThread;
action <- getSchedulerAction;
wasRunnable <- isRunnable curThread;
x <- getIdleThread;
targetPrio <- threadGet tcbPriority t;
curPrio <- threadGet tcbPriority curThread;
fastfail <- scheduleSwitchThreadFastfail curThread x curPrio targetPrio;
curDom <- curDomain;
highest <- isHighestPrio curDom targetPrio;
y <- Arch.switchToThread t;
y <- return ();
y <- setCurThread t;
setSchedulerAction ResumeCurrentThread
od) (do y <- Arch.switchToThread t;
y <- setCurThread t;
setSchedulerAction ResumeCurrentThread
od)
 2. \<And>s. ksSchedulerAction s = SwitchToThread t \<and> tcb_at' t s \<and> obj_at' (Not \<circ> tcbQueued) t s \<and> ksCurThread s = t' \<and> st_tcb_at' (Not \<circ> runnable') t' 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 ((\<lambda>s. tcb_at' t s \<and> obj_at' (Not \<circ> tcbQueued) t s) and ?Q352))))) s proof (prove)
goal (2 subgoals):
 1. monadic_rewrite True False ?Q352 (do curThread <- getCurThread;
action <- getSchedulerAction;
wasRunnable <- isRunnable curThread;
x <- getIdleThread;
targetPrio <- threadGet tcbPriority t;
curPrio <- threadGet tcbPriority curThread;
fastfail <- scheduleSwitchThreadFastfail curThread x curPrio targetPrio;
curDom <- curDomain;
highest <- isHighestPrio curDom targetPrio;
y <- Arch.switchToThread t;
y <- setCurThread t;
setSchedulerAction ResumeCurrentThread
od) (do y <- Arch.switchToThread t;
y <- setCurThread t;
setSchedulerAction ResumeCurrentThread
od)
 2. \<And>s. ksSchedulerAction s = SwitchToThread t \<and> tcb_at' t s \<and> obj_at' (Not \<circ> tcbQueued) t s \<and> ksCurThread s = t' \<and> st_tcb_at' (Not \<circ> runnable') t' 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 ((\<lambda>s. tcb_at' t s \<and> obj_at' (Not \<circ> tcbQueued) t s) and ?Q352))))) s proof (prove)
goal (29 subgoals):
 1. \<And>curThread action wasRunnable x targetPrio curPrio fastfail curDom highest. monadic_rewrite True False (?Q507 curThread action wasRunnable x targetPrio curPrio fastfail curDom highest) (do y <- Arch.switchToThread t;
y <- setCurThread t;
setSchedulerAction ResumeCurrentThread
od) (do y <- Arch.switchToThread t;
y <- setCurThread t;
setSchedulerAction ResumeCurrentThread
od)
 2. \<And>curThread action wasRunnable x targetPrio curPrio fastfail curDom P. \<lbrace>P\<rbrace> isHighestPrio curDom targetPrio \<lbrace>\<lambda>_. P\<rbrace>
 3. \<And>curThread action wasRunnable x targetPrio curPrio fastfail curDom. empty_fail (isHighestPrio curDom targetPrio)
 4. \<And>curThread action wasRunnable x targetPrio curPrio fastfail curDom. \<lbrace>?Q502 curThread action wasRunnable x targetPrio curPrio fastfail curDom\<rbrace> isHighestPrio curDom targetPrio \<lbrace>?Q507 curThread action wasRunnable x targetPrio curPrio fastfail curDom\<rbrace>
 5. \<And>curThread action wasRunnable x targetPrio curPrio fastfail P. \<lbrace>P\<rbrace> curDomain \<lbrace>\<lambda>_. P\<rbrace>
 6. \<And>curThread action wasRunnable x targetPrio curPrio fastfail. empty_fail curDomain
 7. \<And>curThread action wasRunnable x targetPrio curPrio fastfail. \<lbrace>?Q497 curThread action wasRunnable x targetPrio curPrio fastfail\<rbrace> curDomain \<lbrace>?Q502 curThread action wasRunnable x targetPrio curPrio fastfail\<rbrace>
 8. \<And>curThread action wasRunnable x targetPrio curPrio P. \<lbrace>P\<rbrace> scheduleSwitchThreadFastfail curThread x curPrio targetPrio \<lbrace>\<lambda>_. P\<rbrace>
 9. \<And>curThread action wasRunnable x targetPrio curPrio. empty_fail (scheduleSwitchThreadFastfail curThread x curPrio targetPrio)
 10. \<And>curThread action wasRunnable x targetPrio curPrio. \<lbrace>?Q492 curThread action wasRunnable x targetPrio curPrio\<rbrace> scheduleSwitchThreadFastfail curThread x curPrio targetPrio \<lbrace>?Q497 curThread action wasRunnable x targetPrio curPrio\<rbrace>
A total of 29 subgoals... proof (prove)
goal (29 subgoals):
 1. \<And>curThread action wasRunnable x targetPrio curPrio fastfail curDom highest. monadic_rewrite True False (?Q507 curThread action wasRunnable x targetPrio curPrio fastfail curDom highest) (do y <- Arch.switchToThread t;
y <- setCurThread t;
setSchedulerAction ResumeCurrentThread
od) (do y <- Arch.switchToThread t;
y <- setCurThread t;
setSchedulerAction ResumeCurrentThread
od)
 2. \<And>curThread action wasRunnable x targetPrio curPrio fastfail curDom P. \<lbrace>P\<rbrace> isHighestPrio curDom targetPrio \<lbrace>\<lambda>_. P\<rbrace>
 3. \<And>curThread action wasRunnable x targetPrio curPrio fastfail curDom. empty_fail (isHighestPrio curDom targetPrio)
 4. \<And>curThread action wasRunnable x targetPrio curPrio fastfail curDom. \<lbrace>?Q502 curThread action wasRunnable x targetPrio curPrio fastfail curDom\<rbrace> isHighestPrio curDom targetPrio \<lbrace>?Q507 curThread action wasRunnable x targetPrio curPrio fastfail curDom\<rbrace>
 5. \<And>curThread action wasRunnable x targetPrio curPrio fastfail P. \<lbrace>P\<rbrace> curDomain \<lbrace>\<lambda>_. P\<rbrace>
 6. \<And>curThread action wasRunnable x targetPrio curPrio fastfail. empty_fail curDomain
 7. \<And>curThread action wasRunnable x targetPrio curPrio fastfail. \<lbrace>?Q497 curThread action wasRunnable x targetPrio curPrio fastfail\<rbrace> curDomain \<lbrace>?Q502 curThread action wasRunnable x targetPrio curPrio fastfail\<rbrace>
 8. \<And>curThread action wasRunnable x targetPrio curPrio P. \<lbrace>P\<rbrace> scheduleSwitchThreadFastfail curThread x curPrio targetPrio \<lbrace>\<lambda>_. P\<rbrace>
 9. \<And>curThread action wasRunnable x targetPrio curPrio. empty_fail (scheduleSwitchThreadFastfail curThread x curPrio targetPrio)
 10. \<And>curThread action wasRunnable x targetPrio curPrio. \<lbrace>?Q492 curThread action wasRunnable x targetPrio curPrio\<rbrace> scheduleSwitchThreadFastfail curThread x curPrio targetPrio \<lbrace>?Q497 curThread action wasRunnable x targetPrio curPrio\<rbrace>
A total of 29 subgoals... proof (prove)
goal (28 subgoals):
 1. \<And>curThread action wasRunnable x targetPrio curPrio fastfail curDom P. \<lbrace>P\<rbrace> isHighestPrio curDom targetPrio \<lbrace>\<lambda>_. P\<rbrace>
 2. \<And>curThread action wasRunnable x targetPrio curPrio fastfail curDom. empty_fail (isHighestPrio curDom targetPrio)
 3. \<And>curThread action wasRunnable x targetPrio curPrio fastfail curDom. \<lbrace>?Q502 curThread action wasRunnable x targetPrio curPrio fastfail curDom\<rbrace> isHighestPrio curDom targetPrio \<lbrace>\<lambda>highest _. True\<rbrace>
 4. \<And>curThread action wasRunnable x targetPrio curPrio fastfail P. \<lbrace>P\<rbrace> curDomain \<lbrace>\<lambda>_. P\<rbrace>
 5. \<And>curThread action wasRunnable x targetPrio curPrio fastfail. empty_fail curDomain
 6. \<And>curThread action wasRunnable x targetPrio curPrio fastfail. \<lbrace>?Q497 curThread action wasRunnable x targetPrio curPrio fastfail\<rbrace> curDomain \<lbrace>?Q502 curThread action wasRunnable x targetPrio curPrio fastfail\<rbrace>
 7. \<And>curThread action wasRunnable x targetPrio curPrio P. \<lbrace>P\<rbrace> scheduleSwitchThreadFastfail curThread x curPrio targetPrio \<lbrace>\<lambda>_. P\<rbrace>
 8. \<And>curThread action wasRunnable x targetPrio curPrio. empty_fail (scheduleSwitchThreadFastfail curThread x curPrio targetPrio)
 9. \<And>curThread action wasRunnable x targetPrio curPrio. \<lbrace>?Q492 curThread action wasRunnable x targetPrio curPrio\<rbrace> scheduleSwitchThreadFastfail curThread x curPrio targetPrio \<lbrace>?Q497 curThread action wasRunnable x targetPrio curPrio\<rbrace>
 10. \<And>curThread action wasRunnable x targetPrio P. \<lbrace>P\<rbrace> threadGet tcbPriority curThread \<lbrace>\<lambda>_. P\<rbrace>
A total of 28 subgoals... proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>ksSchedulerAction s = SwitchToThread t; tcb_at' t s; obj_at' (Not \<circ> tcbQueued) t s; t' = ksCurThread s; st_tcb_at' (Not \<circ> runnable') (ksCurThread s) 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; tcb_at' t s; obj_at' (Not \<circ> tcbQueued) t s; t' = ksCurThread s; 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!