theory Fastpath_Equiv

lemma fastpathBestSwitchCandidate_lift:
  assumes ct[wp]: "\<And>P. \<lbrace>\<lambda>s. P (ksCurThread s) \<rbrace> f \<lbrace> \<lambda>_ s. P (ksCurThread s) \<rbrace>"
  assumes cd[wp]: "\<And>P. \<lbrace>\<lambda>s. P (ksCurDomain s) \<rbrace> f \<lbrace> \<lambda>_ s. P (ksCurDomain s) \<rbrace>"
  assumes l1[wp]: "\<And>P. \<lbrace>\<lambda>s. P (ksReadyQueuesL1Bitmap s) \<rbrace> f \<lbrace> \<lambda>_ s. P (ksReadyQueuesL1Bitmap s) \<rbrace>"
  assumes l2[wp]: "\<And>P. \<lbrace>\<lambda>s. P (ksReadyQueuesL2Bitmap s) \<rbrace> f \<lbrace> \<lambda>_ s. P (ksReadyQueuesL2Bitmap s) \<rbrace>"
  assumes p[wp]: "\<And>P t. \<lbrace> obj_at' (\<lambda>tcb. P (tcbPriority tcb)) t \<rbrace> f \<lbrace> \<lambda>_.  obj_at' (\<lambda>tcb. P (tcbPriority tcb)) t \<rbrace>"
  shows "\<lbrace> tcb_at' t and fastpathBestSwitchCandidate t \<rbrace> f \<lbrace>\<lambda>rv. fastpathBestSwitchCandidate t \<rbrace>" unfolding fastpathBestSwitchCandidate_def lookupBitmapPriority_def l1IndexToPrio_def apply (rule hoare_pre) apply (rule hoare_lift_Pf2[where f=ksCurDomain]) apply (wp hoare_vcg_disj_lift hoare_vcg_all_lift) apply (rule hoare_lift_Pf2[where f=ksCurThread]) apply (rule hoare_lift_Pf2[where f=ksReadyQueuesL1Bitmap]) apply (rule hoare_lift_Pf2[where f=ksReadyQueuesL2Bitmap]) apply (wp hoare_vcg_imp_lift') apply (strengthen not_obj_at'_strengthen) apply (wpsimp simp: comp_def wp: l1 l2 hoare_vcg_disj_lift)+ apply (drule (1) tcb_at_not_obj_at_elim'[rotated]) apply (rename_tac tprio, erule_tac x=tprio in allE) apply clarsimp apply (drule (1) tcb_at_not_obj_at_elim'[rotated]) apply (clarsimp simp: obj_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at' t and fastpathBestSwitchCandidate t\<rbrace> f \<lbrace>\<lambda>rv. fastpathBestSwitchCandidate t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at' t and (\<lambda>s. ksReadyQueuesL1Bitmap s (ksCurDomain s) = 0 \<or> (\<forall>tprio. obj_at' (\<lambda>tcb. tcbPriority tcb = tprio) t s \<longrightarrow> obj_at' (\<lambda>tcb. tcbPriority tcb \<le> tprio) (ksCurThread s) s \<or> fromIntegral (word_log2 (ksReadyQueuesL1Bitmap s (ksCurDomain s))) `~shiftL~` wordRadix || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (ksCurDomain s, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s (ksCurDomain s)))))) \<le> tprio))\<rbrace> f \<lbrace>\<lambda>rv s. ksReadyQueuesL1Bitmap s (ksCurDomain s) = 0 \<or> (\<forall>tprio. obj_at' (\<lambda>tcb. tcbPriority tcb = tprio) t s \<longrightarrow> obj_at' (\<lambda>tcb. tcbPriority tcb \<le> tprio) (ksCurThread s) s \<or> fromIntegral (word_log2 (ksReadyQueuesL1Bitmap s (ksCurDomain s))) `~shiftL~` wordRadix || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (ksCurDomain s, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s (ksCurDomain s)))))) \<le> tprio)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> f \<lbrace>\<lambda>rv s. ksReadyQueuesL1Bitmap s (ksCurDomain s) = 0 \<or> (\<forall>tprio. obj_at' (\<lambda>tcb. tcbPriority tcb = tprio) t s \<longrightarrow> obj_at' (\<lambda>tcb. tcbPriority tcb \<le> tprio) (ksCurThread s) s \<or> fromIntegral (word_log2 (ksReadyQueuesL1Bitmap s (ksCurDomain s))) `~shiftL~` wordRadix || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (ksCurDomain s, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s (ksCurDomain s)))))) \<le> tprio)\<rbrace>
 2. \<And>s. (tcb_at' t and (\<lambda>s. ksReadyQueuesL1Bitmap s (ksCurDomain s) = 0 \<or> (\<forall>tprio. obj_at' (\<lambda>tcb. tcbPriority tcb = tprio) t s \<longrightarrow> obj_at' (\<lambda>tcb. tcbPriority tcb \<le> tprio) (ksCurThread s) s \<or> fromIntegral (word_log2 (ksReadyQueuesL1Bitmap s (ksCurDomain s))) `~shiftL~` wordRadix || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (ksCurDomain s, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s (ksCurDomain s)))))) \<le> tprio))) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrace>?Q3 x\<rbrace> f \<lbrace>\<lambda>_ a. ksReadyQueuesL1Bitmap a x = 0 \<or> (\<forall>tprio. obj_at' (\<lambda>tcb. tcbPriority tcb = tprio) t a \<longrightarrow> obj_at' (\<lambda>tcb. tcbPriority tcb \<le> tprio) (ksCurThread a) a \<or> fromIntegral (word_log2 (ksReadyQueuesL1Bitmap a x)) `~shiftL~` wordRadix || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap a (x, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap a x))))) \<le> tprio)\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksCurDomain s)\<rbrace>
 3. \<And>s. (tcb_at' t and (\<lambda>s. ksReadyQueuesL1Bitmap s (ksCurDomain s) = 0 \<or> (\<forall>tprio. obj_at' (\<lambda>tcb. tcbPriority tcb = tprio) t s \<longrightarrow> obj_at' (\<lambda>tcb. tcbPriority tcb \<le> tprio) (ksCurThread s) s \<or> fromIntegral (word_log2 (ksReadyQueuesL1Bitmap s (ksCurDomain s))) `~shiftL~` wordRadix || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (ksCurDomain s, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s (ksCurDomain s)))))) \<le> tprio))) s \<Longrightarrow> ?Q3 (ksCurDomain s) s proof (prove)
goal (3 subgoals):
 1. \<And>x tprio. \<lbrace>?P11 x tprio\<rbrace> f \<lbrace>\<lambda>rv s. obj_at' (\<lambda>tcb. tcbPriority tcb = tprio) t s \<longrightarrow> obj_at' (\<lambda>tcb. tcbPriority tcb \<le> tprio) (ksCurThread s) s \<or> fromIntegral (word_log2 (ksReadyQueuesL1Bitmap s x)) `~shiftL~` wordRadix || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (x, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s x))))) \<le> tprio\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksCurDomain s)\<rbrace>
 3. \<And>s. (tcb_at' t and (\<lambda>s. ksReadyQueuesL1Bitmap s (ksCurDomain s) = 0 \<or> (\<forall>tprio. obj_at' (\<lambda>tcb. tcbPriority tcb = tprio) t s \<longrightarrow> obj_at' (\<lambda>tcb. tcbPriority tcb \<le> tprio) (ksCurThread s) s \<or> fromIntegral (word_log2 (ksReadyQueuesL1Bitmap s (ksCurDomain s))) `~shiftL~` wordRadix || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (ksCurDomain s, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s (ksCurDomain s)))))) \<le> tprio))) s \<Longrightarrow> ksReadyQueuesL1Bitmap s (ksCurDomain s) = 0 \<or> (\<forall>x. ?P11 (ksCurDomain s) x s) proof (prove)
goal (4 subgoals):
 1. \<And>x tprio xa. \<lbrace>?Q13 x tprio xa\<rbrace> f \<lbrace>\<lambda>_ a. obj_at' (\<lambda>tcb. tcbPriority tcb = tprio) t a \<longrightarrow> obj_at' (\<lambda>tcb. tcbPriority tcb \<le> tprio) xa a \<or> fromIntegral (word_log2 (ksReadyQueuesL1Bitmap a x)) `~shiftL~` wordRadix || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap a (x, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap a x))))) \<le> tprio\<rbrace>
 2. \<And>x tprio P. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace>
 3. \<And>P. \<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksCurDomain s)\<rbrace>
 4. \<And>s. (tcb_at' t and (\<lambda>s. ksReadyQueuesL1Bitmap s (ksCurDomain s) = 0 \<or> (\<forall>tprio. obj_at' (\<lambda>tcb. tcbPriority tcb = tprio) t s \<longrightarrow> obj_at' (\<lambda>tcb. tcbPriority tcb \<le> tprio) (ksCurThread s) s \<or> fromIntegral (word_log2 (ksReadyQueuesL1Bitmap s (ksCurDomain s))) `~shiftL~` wordRadix || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (ksCurDomain s, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s (ksCurDomain s)))))) \<le> tprio))) s \<Longrightarrow> ksReadyQueuesL1Bitmap s (ksCurDomain s) = 0 \<or> (\<forall>x. ?Q13 (ksCurDomain s) x (ksCurThread s) s) proof (prove)
goal (5 subgoals):
 1. \<And>x tprio xa xb. \<lbrace>?Q17 x tprio xa xb\<rbrace> f \<lbrace>\<lambda>_ a. obj_at' (\<lambda>tcb. tcbPriority tcb = tprio) t a \<longrightarrow> obj_at' (\<lambda>tcb. tcbPriority tcb \<le> tprio) xa a \<or> fromIntegral (word_log2 (xb x)) `~shiftL~` wordRadix || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap a (x, invertL1Index (word_log2 (xb x))))) \<le> tprio\<rbrace>
 2. \<And>x tprio xa P. \<lbrace>\<lambda>s. P (ksReadyQueuesL1Bitmap s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksReadyQueuesL1Bitmap s)\<rbrace>
 3. \<And>x tprio P. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace>
 4. \<And>P. \<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksCurDomain s)\<rbrace>
 5. \<And>s. (tcb_at' t and (\<lambda>s. ksReadyQueuesL1Bitmap s (ksCurDomain s) = 0 \<or> (\<forall>tprio. obj_at' (\<lambda>tcb. tcbPriority tcb = tprio) t s \<longrightarrow> obj_at' (\<lambda>tcb. tcbPriority tcb \<le> tprio) (ksCurThread s) s \<or> fromIntegral (word_log2 (ksReadyQueuesL1Bitmap s (ksCurDomain s))) `~shiftL~` wordRadix || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (ksCurDomain s, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s (ksCurDomain s)))))) \<le> tprio))) s \<Longrightarrow> ksReadyQueuesL1Bitmap s (ksCurDomain s) = 0 \<or> (\<forall>x. ?Q17 (ksCurDomain s) x (ksCurThread s) (ksReadyQueuesL1Bitmap s) s) proof (prove)
goal (6 subgoals):
 1. \<And>x tprio xa xb xc. \<lbrace>?Q23 x tprio xa xb xc\<rbrace> f \<lbrace>\<lambda>_ a. obj_at' (\<lambda>tcb. tcbPriority tcb = tprio) t a \<longrightarrow> obj_at' (\<lambda>tcb. tcbPriority tcb \<le> tprio) xa a \<or> fromIntegral (word_log2 (xb x)) `~shiftL~` wordRadix || word_of_nat (word_log2 (xc (x, invertL1Index (word_log2 (xb x))))) \<le> tprio\<rbrace>
 2. \<And>x tprio xa xb P. \<lbrace>\<lambda>s. P (ksReadyQueuesL2Bitmap s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksReadyQueuesL2Bitmap s)\<rbrace>
 3. \<And>x tprio xa P. \<lbrace>\<lambda>s. P (ksReadyQueuesL1Bitmap s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksReadyQueuesL1Bitmap s)\<rbrace>
 4. \<And>x tprio P. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace>
 5. \<And>P. \<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksCurDomain s)\<rbrace>
 6. \<And>s. (tcb_at' t and (\<lambda>s. ksReadyQueuesL1Bitmap s (ksCurDomain s) = 0 \<or> (\<forall>tprio. obj_at' (\<lambda>tcb. tcbPriority tcb = tprio) t s \<longrightarrow> obj_at' (\<lambda>tcb. tcbPriority tcb \<le> tprio) (ksCurThread s) s \<or> fromIntegral (word_log2 (ksReadyQueuesL1Bitmap s (ksCurDomain s))) `~shiftL~` wordRadix || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (ksCurDomain s, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s (ksCurDomain s)))))) \<le> tprio))) s \<Longrightarrow> ksReadyQueuesL1Bitmap s (ksCurDomain s) = 0 \<or> (\<forall>x. ?Q23 (ksCurDomain s) x (ksCurThread s) (ksReadyQueuesL1Bitmap s) (ksReadyQueuesL2Bitmap s) s) proof (prove)
goal (7 subgoals):
 1. \<And>x tprio xa xb xc. \<lbrace>?P'31 x tprio xa xb xc\<rbrace> f \<lbrace>\<lambda>_ s. \<not> obj_at' (\<lambda>tcb. tcbPriority tcb = tprio) t s\<rbrace>
 2. \<And>x tprio xa xb xc. \<lbrace>?Q'31 x tprio xa xb xc\<rbrace> f \<lbrace>\<lambda>rv s. obj_at' (\<lambda>tcb. tcbPriority tcb \<le> tprio) xa s \<or> fromIntegral (word_log2 (xb x)) `~shiftL~` wordRadix || word_of_nat (word_log2 (xc (x, invertL1Index (word_log2 (xb x))))) \<le> tprio\<rbrace>
 3. \<And>x tprio xa xb P. \<lbrace>\<lambda>s. P (ksReadyQueuesL2Bitmap s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksReadyQueuesL2Bitmap s)\<rbrace>
 4. \<And>x tprio xa P. \<lbrace>\<lambda>s. P (ksReadyQueuesL1Bitmap s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksReadyQueuesL1Bitmap s)\<rbrace>
 5. \<And>x tprio P. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace>
 6. \<And>P. \<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksCurDomain s)\<rbrace>
 7. \<And>s. (tcb_at' t and (\<lambda>s. ksReadyQueuesL1Bitmap s (ksCurDomain s) = 0 \<or> (\<forall>tprio. obj_at' (\<lambda>tcb. tcbPriority tcb = tprio) t s \<longrightarrow> obj_at' (\<lambda>tcb. tcbPriority tcb \<le> tprio) (ksCurThread s) s \<or> fromIntegral (word_log2 (ksReadyQueuesL1Bitmap s (ksCurDomain s))) `~shiftL~` wordRadix || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (ksCurDomain s, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s (ksCurDomain s)))))) \<le> tprio))) s \<Longrightarrow> ksReadyQueuesL1Bitmap s (ksCurDomain s) = 0 \<or> (\<forall>x. \<not> ?P'31 (ksCurDomain s) x (ksCurThread s) (ksReadyQueuesL1Bitmap s) (ksReadyQueuesL2Bitmap s) s \<longrightarrow> ?Q'31 (ksCurDomain s) x (ksCurThread s) (ksReadyQueuesL1Bitmap s) (ksReadyQueuesL2Bitmap s) s) proof (prove)
goal (7 subgoals):
 1. \<And>x tprio xa xb xc. \<lbrace>?P'31 x tprio xa xb xc\<rbrace> f \<lbrace>\<lambda>r. obj_at' (Not \<circ> (\<lambda>tcb. tcbPriority tcb = tprio)) t\<rbrace>
 2. \<And>x tprio xa xb xc. \<lbrace>?Q'31 x tprio xa xb xc\<rbrace> f \<lbrace>\<lambda>rv s. obj_at' (\<lambda>tcb. tcbPriority tcb \<le> tprio) xa s \<or> fromIntegral (word_log2 (xb x)) `~shiftL~` wordRadix || word_of_nat (word_log2 (xc (x, invertL1Index (word_log2 (xb x))))) \<le> tprio\<rbrace>
 3. \<And>x tprio xa xb P. \<lbrace>\<lambda>s. P (ksReadyQueuesL2Bitmap s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksReadyQueuesL2Bitmap s)\<rbrace>
 4. \<And>x tprio xa P. \<lbrace>\<lambda>s. P (ksReadyQueuesL1Bitmap s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksReadyQueuesL1Bitmap s)\<rbrace>
 5. \<And>x tprio P. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace>
 6. \<And>P. \<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksCurDomain s)\<rbrace>
 7. \<And>s. (tcb_at' t and (\<lambda>s. ksReadyQueuesL1Bitmap s (ksCurDomain s) = 0 \<or> (\<forall>tprio. obj_at' (\<lambda>tcb. tcbPriority tcb = tprio) t s \<longrightarrow> obj_at' (\<lambda>tcb. tcbPriority tcb \<le> tprio) (ksCurThread s) s \<or> fromIntegral (word_log2 (ksReadyQueuesL1Bitmap s (ksCurDomain s))) `~shiftL~` wordRadix || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (ksCurDomain s, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s (ksCurDomain s)))))) \<le> tprio))) s \<Longrightarrow> ksReadyQueuesL1Bitmap s (ksCurDomain s) = 0 \<or> (\<forall>x. \<not> ?P'31 (ksCurDomain s) x (ksCurThread s) (ksReadyQueuesL1Bitmap s) (ksReadyQueuesL2Bitmap s) s \<longrightarrow> ?Q'31 (ksCurDomain s) x (ksCurThread s) (ksReadyQueuesL1Bitmap s) (ksReadyQueuesL2Bitmap s) s) proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>tcb_at' t s; ksReadyQueuesL1Bitmap s (ksCurDomain s) \<noteq> 0; \<not> obj_at' (\<lambda>tcb. tcbPriority tcb \<noteq> x) t s; \<not> (word_of_nat (word_log2 (ksReadyQueuesL1Bitmap s (ksCurDomain s))) << wordRadix) || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (ksCurDomain s, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s (ksCurDomain s)))))) \<le> x; \<forall>tprio. obj_at' (\<lambda>tcb. tcbPriority tcb = tprio) t s \<longrightarrow> obj_at' (\<lambda>tcb. tcbPriority tcb \<le> tprio) (ksCurThread s) s \<or> (word_of_nat (word_log2 (ksReadyQueuesL1Bitmap s (ksCurDomain s))) << wordRadix) || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (ksCurDomain s, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s (ksCurDomain s)))))) \<le> tprio\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>tcb. tcbPriority tcb \<le> x) (ksCurThread s) s proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>tcb_at' t s; ksReadyQueuesL1Bitmap s (ksCurDomain s) \<noteq> 0; \<not> (word_of_nat (word_log2 (ksReadyQueuesL1Bitmap s (ksCurDomain s))) << wordRadix) || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (ksCurDomain s, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s (ksCurDomain s)))))) \<le> x; \<forall>tprio. obj_at' (\<lambda>tcb. tcbPriority tcb = tprio) t s \<longrightarrow> obj_at' (\<lambda>tcb. tcbPriority tcb \<le> tprio) (ksCurThread s) s \<or> (word_of_nat (word_log2 (ksReadyQueuesL1Bitmap s (ksCurDomain s))) << wordRadix) || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (ksCurDomain s, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s (ksCurDomain s)))))) \<le> tprio; obj_at' (Not \<circ> (\<lambda>tcb. tcbPriority tcb \<noteq> x)) t s\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>tcb. tcbPriority tcb \<le> x) (ksCurThread s) s proof (prove)
goal (1 subgoal):
 1. \<And>s tprio. \<lbrakk>tcb_at' t s; ksReadyQueuesL1Bitmap s (ksCurDomain s) \<noteq> 0; \<not> (word_of_nat (word_log2 (ksReadyQueuesL1Bitmap s (ksCurDomain s))) << wordRadix) || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (ksCurDomain s, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s (ksCurDomain s)))))) \<le> tprio; obj_at' (Not \<circ> (\<lambda>tcb. tcbPriority tcb \<noteq> tprio)) t s; obj_at' (\<lambda>tcb. tcbPriority tcb = tprio) t s \<longrightarrow> obj_at' (\<lambda>tcb. tcbPriority tcb \<le> tprio) (ksCurThread s) s \<or> (word_of_nat (word_log2 (ksReadyQueuesL1Bitmap s (ksCurDomain s))) << wordRadix) || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (ksCurDomain s, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s (ksCurDomain s)))))) \<le> tprio\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>tcb. tcbPriority tcb \<le> tprio) (ksCurThread s) s proof (prove)
goal (1 subgoal):
 1. \<And>s tprio. \<lbrakk>tcb_at' t s; ksReadyQueuesL1Bitmap s (ksCurDomain s) \<noteq> 0; \<not> (word_of_nat (word_log2 (ksReadyQueuesL1Bitmap s (ksCurDomain s))) << wordRadix) || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (ksCurDomain s, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s (ksCurDomain s)))))) \<le> tprio; obj_at' (Not \<circ> (\<lambda>tcb. tcbPriority tcb \<noteq> tprio)) t s; \<not> obj_at' (\<lambda>tcb. tcbPriority tcb = tprio) t s\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>tcb. tcbPriority tcb \<le> tprio) (ksCurThread s) s proof (prove)
goal (1 subgoal):
 1. \<And>s tprio. \<lbrakk>tcb_at' t s; ksReadyQueuesL1Bitmap s (ksCurDomain s) \<noteq> 0; \<not> (word_of_nat (word_log2 (ksReadyQueuesL1Bitmap s (ksCurDomain s))) << wordRadix) || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (ksCurDomain s, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s (ksCurDomain s)))))) \<le> tprio; obj_at' (Not \<circ> (\<lambda>tcb. tcbPriority tcb \<noteq> tprio)) t s; obj_at' (Not \<circ> (\<lambda>tcb. tcbPriority tcb = tprio)) t s\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>tcb. tcbPriority tcb \<le> tprio) (ksCurThread s) s proof (prove)
goal:
No subgoals!