kings-crown/FVELER_Isabelle huggingface dataset:
theory TcbAcc_R

lemma prioL2Index_bit_set:
  fixes p :: priority
  shows "((2::32 word) ^ unat (p && mask wordRadix)) !! unat (p && mask wordRadix)" apply (simp add: nth_w2p wordRadix_def ucast_and_mask[symmetric] unat_ucast_upcast is_up) apply (rule unat_less_helper) apply (insert and_mask_less'[where w=p and n=wordRadix], simp add: wordRadix_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (2 ^ unat (p && mask wordRadix)) !! unat (p && mask wordRadix) proof (prove)
goal (1 subgoal):
 1. unat (p && mask 5) < 32 proof (prove)
goal (1 subgoal):
 1. p && mask 5 < word_of_nat 32 proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma addToBitmap_bitmapQ:
  "\<lbrace> \<lambda>s. True \<rbrace> addToBitmap d p \<lbrace>\<lambda>_. bitmapQ d p \<rbrace>" unfolding addToBitmap_def
             modifyReadyQueuesL1Bitmap_def modifyReadyQueuesL2Bitmap_def
             getReadyQueuesL1Bitmap_def getReadyQueuesL2Bitmap_def by (wpsimp simp: bitmap_fun_defs bitmapQ_def prioToL1Index_bit_set prioL2Index_bit_set
             simp_del: bit_exp_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. True\<rbrace> addToBitmap d p \<lbrace>\<lambda>_. bitmapQ d p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. True\<rbrace> do l1index <- return (prioToL1Index p);
l1indexInverted <- return (invertL1Index l1index);
l2bit <- return (fromIntegral (fromIntegral p && mask wordRadix));
do l1 <- gets (\<lambda>ks. ksReadyQueuesL1Bitmap ks d);
modify (\<lambda>ks. ks\<lparr>ksReadyQueuesL1Bitmap := ksReadyQueuesL1Bitmap ks aLU [(d, l1 || HaskellLib_H.bit l1index)]\<rparr>)
od;
l2 <- gets (\<lambda>ks. ksReadyQueuesL2Bitmap ks (d, l1indexInverted));
modify (\<lambda>ks. ks\<lparr>ksReadyQueuesL2Bitmap := ksReadyQueuesL2Bitmap ks aLU [((d, l1indexInverted), l2 || HaskellLib_H.bit l2bit)]\<rparr>)
od \<lbrace>\<lambda>_. bitmapQ d p\<rbrace>
theory TcbAcc_R

lemma addToBitmap_valid_queues_no_bitmap_except:
" \<lbrace> valid_queues_no_bitmap_except t \<rbrace>
     addToBitmap d p
  \<lbrace>\<lambda>_. valid_queues_no_bitmap_except t \<rbrace>" unfolding addToBitmap_def modifyReadyQueuesL1Bitmap_def modifyReadyQueuesL2Bitmap_def
             getReadyQueuesL1Bitmap_def getReadyQueuesL2Bitmap_def valid_queues_no_bitmap_except_def by (wp, clarsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues_no_bitmap_except t\<rbrace> addToBitmap d p \<lbrace>\<lambda>_. valid_queues_no_bitmap_except t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>d p. (\<forall>ta\<in>set (ksReadyQueues s (d, p)). ta \<noteq> t \<longrightarrow> obj_at' (inQ d p and runnable' \<circ> tcbState) ta s) \<and> distinct (ksReadyQueues s (d, p)) \<and> (maxDomain < d \<or> maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = [])\<rbrace> do l1index <- return (prioToL1Index p);
l1indexInverted <- return (invertL1Index l1index);
l2bit <- return (fromIntegral (fromIntegral p && mask wordRadix));
do l1 <- gets (\<lambda>ks. ksReadyQueuesL1Bitmap ks d);
modify (\<lambda>ks. ks\<lparr>ksReadyQueuesL1Bitmap := ksReadyQueuesL1Bitmap ks aLU [(d, l1 || HaskellLib_H.bit l1index)]\<rparr>)
od;
l2 <- gets (\<lambda>ks. ksReadyQueuesL2Bitmap ks (d, l1indexInverted));
modify (\<lambda>ks. ks\<lparr>ksReadyQueuesL2Bitmap := ksReadyQueuesL2Bitmap ks aLU [((d, l1indexInverted), l2 || HaskellLib_H.bit l2bit)]\<rparr>)
od \<lbrace>\<lambda>_ s. \<forall>d p. (\<forall>ta\<in>set (ksReadyQueues s (d, p)). ta \<noteq> t \<longrightarrow> obj_at' (inQ d p and runnable' \<circ> tcbState) ta s) \<and> distinct (ksReadyQueues s (d, p)) \<and> (maxDomain < d \<or> maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = [])\<rbrace>
theory TcbAcc_R

lemma prioToL1Index_lt:
  "2 ^ wordRadix \<le> x \<Longrightarrow> prioToL1Index p < x" unfolding prioToL1Index_def wordRadix_def by (insert unat_lt2p[where x=p], simp add: shiftr_div_2n')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 2 ^ wordRadix \<le> x \<Longrightarrow> prioToL1Index p < x proof (prove)
goal (1 subgoal):
 1. 2 ^ wordSizeCase 5 6 \<le> x \<Longrightarrow> (fromIntegral $ p `~shiftR~` wordSizeCase 5 6) < x
theory TcbAcc_R

lemma prioToL1Index_bits_low_high_eq:
  "\<lbrakk> pa \<noteq> p; prioToL1Index pa = prioToL1Index (p::priority) \<rbrakk>
   \<Longrightarrow>  unat (pa && mask wordRadix) \<noteq> unat (p && mask wordRadix)" unfolding prioToL1Index_def by (fastforce simp: nth_w2p wordRadix_def is_up bits_low_high_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pa \<noteq> p; prioToL1Index pa = prioToL1Index p\<rbrakk> \<Longrightarrow> unat (pa && mask wordRadix) \<noteq> unat (p && mask wordRadix) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pa \<noteq> p; (fromIntegral $ pa `~shiftR~` wordRadix) = (fromIntegral $ p `~shiftR~` wordRadix)\<rbrakk> \<Longrightarrow> unat (pa && mask wordRadix) \<noteq> unat (p && mask wordRadix)
theory TcbAcc_R

lemma prioToL1Index_bit_not_set:
  "\<not> (~~ ((2 :: machine_word) ^ prioToL1Index p)) !! prioToL1Index p" apply (subst word_ops_nth_size, simp_all add: prioToL1Index_bit_set del: bit_exp_iff) apply (fastforce simp: prioToL1Index_def wordRadix_def word_size
                  intro: order_less_le_trans[OF word_shiftr_lt]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> (~~ 2 ^ prioToL1Index p) !! prioToL1Index p proof (prove)
goal (1 subgoal):
 1. prioToL1Index p < size (2 ^ prioToL1Index p) proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma prioToL1Index_complement_nth_w2p:
  fixes p pa :: priority
  shows "(~~ ((2 :: machine_word) ^ prioToL1Index p)) !! prioToL1Index p'
          = (prioToL1Index p \<noteq> prioToL1Index p')" by (fastforce simp: complement_nth_w2p prioToL1Index_lt wordRadix_def word_size)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (~~ 2 ^ prioToL1Index p) !! prioToL1Index p' = (prioToL1Index p \<noteq> prioToL1Index p')
theory TcbAcc_R

lemma valid_bitmapQ_exceptE:
  "\<lbrakk> valid_bitmapQ_except d' p' s ; d \<noteq> d' \<or> p \<noteq> p' \<rbrakk>
   \<Longrightarrow> bitmapQ d p s = (ksReadyQueues s (d, p) \<noteq> [])" unfolding valid_bitmapQ_except_def by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_bitmapQ_except d' p' s; d \<noteq> d' \<or> p \<noteq> p'\<rbrakk> \<Longrightarrow> bitmapQ d p s = (ksReadyQueues s (d, p) \<noteq> []) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>d p. d \<noteq> d' \<or> p \<noteq> p' \<longrightarrow> bitmapQ d p s = (ksReadyQueues s (d, p) \<noteq> []); d \<noteq> d' \<or> p \<noteq> p'\<rbrakk> \<Longrightarrow> bitmapQ d p s = (ksReadyQueues s (d, p) \<noteq> [])
theory TcbAcc_R

lemma invertL1Index_eq_cancelD:
  "\<lbrakk>  invertL1Index i = invertL1Index j ; i < l2BitmapSize ; j < l2BitmapSize \<rbrakk>
   \<Longrightarrow> i = j" by (simp add: invertL1Index_def l2BitmapSize_def')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invertL1Index i = invertL1Index j; i < l2BitmapSize; j < l2BitmapSize\<rbrakk> \<Longrightarrow> i = j
theory TcbAcc_R

lemma invertL1Index_eq_cancel:
  "\<lbrakk> i < l2BitmapSize ; j < l2BitmapSize \<rbrakk>
   \<Longrightarrow> (invertL1Index i = invertL1Index j) = (i = j)" by (rule iffI, simp_all add: invertL1Index_eq_cancelD)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i < l2BitmapSize; j < l2BitmapSize\<rbrakk> \<Longrightarrow> (invertL1Index i = invertL1Index j) = (i = j)
theory TcbAcc_R

lemma removeFromBitmap_bitmapQ_no_L1_orphans[wp]:
  "\<lbrace> bitmapQ_no_L1_orphans \<rbrace> removeFromBitmap d p \<lbrace>\<lambda>_. bitmapQ_no_L1_orphans \<rbrace>" unfolding bitmap_fun_defs apply (wp | simp add: bitmap_fun_defs bitmapQ_no_L1_orphans_def)+ apply (fastforce simp: invertL1Index_eq_cancel prioToL1Index_bit_not_set
                         prioToL1Index_complement_nth_w2p) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>bitmapQ_no_L1_orphans\<rbrace> removeFromBitmap d p \<lbrace>\<lambda>_. bitmapQ_no_L1_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>bitmapQ_no_L1_orphans\<rbrace> do l1index <- return (prioToL1Index p);
l1indexInverted <- return (invertL1Index l1index);
l2bit <- return (fromIntegral (fromIntegral p && mask wordRadix));
(\<lambda>f. do l2 <- gets (\<lambda>ks. ksReadyQueuesL2Bitmap ks (d, l1indexInverted));
modify (\<lambda>ks. ks\<lparr>ksReadyQueuesL2Bitmap := ksReadyQueuesL2Bitmap ks aLU [((d, l1indexInverted), f l2)]\<rparr>)
od) $ (\<lambda>w. w && (wordNOT $ HaskellLib_H.bit l2bit));
l2 <- gets (\<lambda>ks. ksReadyQueuesL2Bitmap ks (d, l1indexInverted));
when (l2 = 0) $ (\<lambda>f. do l1 <- gets (\<lambda>ks. ksReadyQueuesL1Bitmap ks d);
modify (\<lambda>ks. ks\<lparr>ksReadyQueuesL1Bitmap := ksReadyQueuesL1Bitmap ks aLU [(d, f l1)]\<rparr>)
od) $ (\<lambda>w. w && (wordNOT $ HaskellLib_H.bit l1index))
od \<lbrace>\<lambda>_. bitmapQ_no_L1_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<forall>d i. ksReadyQueuesL1Bitmap s d !! i \<longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index i) \<noteq> 0 \<and> i < l2BitmapSize \<Longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) = 0 \<longrightarrow> (\<forall>i. (invertL1Index i = invertL1Index (prioToL1Index p) \<longrightarrow> i < 32 \<longrightarrow> ksReadyQueuesL1Bitmap s d !! i \<longrightarrow> prioToL1Index p = i) \<and> (invertL1Index i \<noteq> invertL1Index (prioToL1Index p) \<longrightarrow> ksReadyQueuesL1Bitmap s d !! i \<and> i < 32 \<and> (i < 32 \<longrightarrow> prioToL1Index p \<noteq> i) \<longrightarrow> i < l2BitmapSize)) proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma addToBitmap_bitmapQ_no_L2_orphans[wp]:
  "\<lbrace> bitmapQ_no_L2_orphans \<rbrace> addToBitmap d p \<lbrace>\<lambda>_. bitmapQ_no_L2_orphans \<rbrace>" unfolding bitmap_fun_defs bitmapQ_defs supply bit_exp_iff[simp del] apply wpsimp apply (fastforce simp: invertL1Index_eq_cancel prioToL1Index_bit_set) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>bitmapQ_no_L2_orphans\<rbrace> addToBitmap d p \<lbrace>\<lambda>_. bitmapQ_no_L2_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>d i j. ksReadyQueuesL2Bitmap s (d, invertL1Index i) !! j \<and> i < l2BitmapSize \<longrightarrow> ksReadyQueuesL1Bitmap s d !! i\<rbrace> do l1index <- return (prioToL1Index p);
l1indexInverted <- return (invertL1Index l1index);
l2bit <- return (fromIntegral (fromIntegral p && mask wordRadix));
do l1 <- gets (\<lambda>ks. ksReadyQueuesL1Bitmap ks d);
modify (\<lambda>ks. ks\<lparr>ksReadyQueuesL1Bitmap := ksReadyQueuesL1Bitmap ks aLU [(d, l1 || HaskellLib_H.bit l1index)]\<rparr>)
od;
l2 <- gets (\<lambda>ks. ksReadyQueuesL2Bitmap ks (d, l1indexInverted));
modify (\<lambda>ks. ks\<lparr>ksReadyQueuesL2Bitmap := ksReadyQueuesL2Bitmap ks aLU [((d, l1indexInverted), l2 || HaskellLib_H.bit l2bit)]\<rparr>)
od \<lbrace>\<lambda>_ s. \<forall>d i j. ksReadyQueuesL2Bitmap s (d, invertL1Index i) !! j \<and> i < l2BitmapSize \<longrightarrow> ksReadyQueuesL1Bitmap s d !! i\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>d i j. ksReadyQueuesL2Bitmap s (d, invertL1Index i) !! j \<and> i < l2BitmapSize \<longrightarrow> ksReadyQueuesL1Bitmap s d !! i\<rbrace> do l1index <- return (prioToL1Index p);
l1indexInverted <- return (invertL1Index l1index);
l2bit <- return (fromIntegral (fromIntegral p && mask wordRadix));
do l1 <- gets (\<lambda>ks. ksReadyQueuesL1Bitmap ks d);
modify (\<lambda>ks. ks\<lparr>ksReadyQueuesL1Bitmap := ksReadyQueuesL1Bitmap ks aLU [(d, l1 || HaskellLib_H.bit l1index)]\<rparr>)
od;
l2 <- gets (\<lambda>ks. ksReadyQueuesL2Bitmap ks (d, l1indexInverted));
modify (\<lambda>ks. ks\<lparr>ksReadyQueuesL2Bitmap := ksReadyQueuesL2Bitmap ks aLU [((d, l1indexInverted), l2 || HaskellLib_H.bit l2bit)]\<rparr>)
od \<lbrace>\<lambda>_ s. \<forall>d i j. ksReadyQueuesL2Bitmap s (d, invertL1Index i) !! j \<and> i < l2BitmapSize \<longrightarrow> ksReadyQueuesL1Bitmap s d !! i\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s i j. \<lbrakk>\<forall>d i. Ex ((!!) (ksReadyQueuesL2Bitmap s (d, invertL1Index i))) \<and> i < l2BitmapSize \<longrightarrow> ksReadyQueuesL1Bitmap s d !! i; invertL1Index i = invertL1Index (prioToL1Index p); i < l2BitmapSize; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) !! j \<or> (2 ^ unat (p && mask wordRadix)) !! j; \<not> (2 ^ prioToL1Index p) !! i\<rbrakk> \<Longrightarrow> ksReadyQueuesL1Bitmap s d !! i proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma addToBitmap_valid_bitmapQ:
" \<lbrace> valid_bitmapQ_except d p and bitmapQ_no_L2_orphans and
    (\<lambda>s. ksReadyQueues s (d,p) \<noteq> []) \<rbrace>
     addToBitmap d p
  \<lbrace>\<lambda>_. valid_bitmapQ \<rbrace>" proof - have "\<lbrace> valid_bitmapQ_except d p and bitmapQ_no_L2_orphans and
            (\<lambda>s. ksReadyQueues s (d,p) \<noteq> []) \<rbrace>
         addToBitmap d p
         \<lbrace>\<lambda>_. valid_bitmapQ_except d p and
              bitmapQ_no_L2_orphans and (\<lambda>s. bitmapQ d p s \<and> ksReadyQueues s (d,p) \<noteq> []) \<rbrace>" by (wp addToBitmap_valid_queues_no_bitmap_except addToBitmap_valid_bitmapQ_except
            addToBitmap_bitmapQ_no_L2_orphans addToBitmap_bitmapQ; simp) thus ?thesis by - (erule hoare_strengthen_post; fastforce elim: valid_bitmap_valid_bitmapQ_exceptE) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_bitmapQ_except d p and bitmapQ_no_L2_orphans and (\<lambda>s. ksReadyQueues s (d, p) \<noteq> [])\<rbrace> addToBitmap d p \<lbrace>\<lambda>_. valid_bitmapQ\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrace>valid_bitmapQ_except d p and bitmapQ_no_L2_orphans and (\<lambda>s. ksReadyQueues s (d, p) \<noteq> [])\<rbrace> addToBitmap d p \<lbrace>\<lambda>_. valid_bitmapQ\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_bitmapQ_except d p and bitmapQ_no_L2_orphans and (\<lambda>s. ksReadyQueues s (d, p) \<noteq> [])\<rbrace> addToBitmap d p \<lbrace>\<lambda>_. valid_bitmapQ_except d p and bitmapQ_no_L2_orphans and (\<lambda>s. bitmapQ d p s \<and> ksReadyQueues s (d, p) \<noteq> [])\<rbrace> proof (state)
this:
\<lbrace>valid_bitmapQ_except d p and bitmapQ_no_L2_orphans and (\<lambda>s. ksReadyQueues s (d, p) \<noteq> [])\<rbrace> addToBitmap d p \<lbrace>\<lambda>_. valid_bitmapQ_except d p and bitmapQ_no_L2_orphans and (\<lambda>s. bitmapQ d p s \<and> ksReadyQueues s (d, p) \<noteq> [])\<rbrace>

goal (1 subgoal):
 1. \<lbrace>valid_bitmapQ_except d p and bitmapQ_no_L2_orphans and (\<lambda>s. ksReadyQueues s (d, p) \<noteq> [])\<rbrace> addToBitmap d p \<lbrace>\<lambda>_. valid_bitmapQ\<rbrace> proof (prove)
using this:
\<lbrace>valid_bitmapQ_except d p and bitmapQ_no_L2_orphans and (\<lambda>s. ksReadyQueues s (d, p) \<noteq> [])\<rbrace> addToBitmap d p \<lbrace>\<lambda>_. valid_bitmapQ_except d p and bitmapQ_no_L2_orphans and (\<lambda>s. bitmapQ d p s \<and> ksReadyQueues s (d, p) \<noteq> [])\<rbrace>

goal (1 subgoal):
 1. \<lbrace>valid_bitmapQ_except d p and bitmapQ_no_L2_orphans and (\<lambda>s. ksReadyQueues s (d, p) \<noteq> [])\<rbrace> addToBitmap d p \<lbrace>\<lambda>_. valid_bitmapQ\<rbrace> proof (state)
this:
\<lbrace>valid_bitmapQ_except d p and bitmapQ_no_L2_orphans and (\<lambda>s. ksReadyQueues s (d, p) \<noteq> [])\<rbrace> addToBitmap d p \<lbrace>\<lambda>_. valid_bitmapQ\<rbrace>

goal:
No subgoals!
theory TcbAcc_R

lemma threadGet_const_tcb_at:
  "\<lbrace>\<lambda>s. tcb_at' t s \<and> obj_at' (P s \<circ> f) t s\<rbrace> threadGet f t \<lbrace>\<lambda>rv s. P s rv \<rbrace>" apply (simp add: threadGet_def liftM_def) apply (wp getObject_tcb_wp) apply (clarsimp simp: obj_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. tcb_at' t s \<and> obj_at' (P s \<circ> f) t s\<rbrace> threadGet f t \<lbrace>\<lambda>rv s. P s rv\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. tcb_at' t s \<and> obj_at' (P s \<circ> f) t s\<rbrace> do x <- getObject t;
return (f x)
od \<lbrace>\<lambda>rv s. P s rv\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. tcb_at' t s \<and> obj_at' (P s \<circ> f) t s \<Longrightarrow> tcb_at' t s \<longrightarrow> (\<exists>ta. ko_at' ta t s \<and> P s (f ta)) proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma threadGet_const_tcb_at_imp_lift:
  "\<lbrace>\<lambda>s. tcb_at' t s \<and> obj_at' (P s \<circ> f) t s \<longrightarrow>  obj_at' (Q s \<circ> f) t s \<rbrace>
   threadGet f t
   \<lbrace>\<lambda>rv s. P s rv \<longrightarrow> Q s rv \<rbrace>" apply (simp add: threadGet_def liftM_def) apply (wp getObject_tcb_wp) apply (clarsimp simp: obj_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. tcb_at' t s \<and> obj_at' (P s \<circ> f) t s \<longrightarrow> obj_at' (Q s \<circ> f) t s\<rbrace> threadGet f t \<lbrace>\<lambda>rv s. P s rv \<longrightarrow> Q s rv\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. tcb_at' t s \<and> obj_at' (P s \<circ> f) t s \<longrightarrow> obj_at' (Q s \<circ> f) t s\<rbrace> do x <- getObject t;
return (f x)
od \<lbrace>\<lambda>rv s. P s rv \<longrightarrow> Q s rv\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. tcb_at' t s \<and> obj_at' (P s \<circ> f) t s \<longrightarrow> obj_at' (Q s \<circ> f) t s \<Longrightarrow> tcb_at' t s \<longrightarrow> (\<exists>ta. ko_at' ta t s \<and> (P s (f ta) \<longrightarrow> Q s (f ta))) proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma valid_queues_no_bitmap_objD:
  "\<lbrakk> valid_queues_no_bitmap s; t \<in> set (ksReadyQueues s (d, p))\<rbrakk>
   \<Longrightarrow> obj_at' (inQ d p and runnable' \<circ> tcbState) t s" unfolding valid_queues_no_bitmap_def by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_queues_no_bitmap s; t \<in> set (ksReadyQueues s (d, p))\<rbrakk> \<Longrightarrow> obj_at' (inQ d p and runnable' \<circ> tcbState) t s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>d p. (\<forall>t\<in>set (ksReadyQueues s (d, p)). obj_at' (inQ d p and runnable' \<circ> tcbState) t s) \<and> distinct (ksReadyQueues s (d, p)) \<and> (maxDomain < d \<or> maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = []); t \<in> set (ksReadyQueues s (d, p))\<rbrakk> \<Longrightarrow> obj_at' (inQ d p and runnable' \<circ> tcbState) t s
theory TcbAcc_R

lemma setQueue_bitmapQ_no_L1_orphans[wp]:
  "\<lbrace> bitmapQ_no_L1_orphans \<rbrace>
       setQueue d p ts
   \<lbrace>\<lambda>rv. bitmapQ_no_L1_orphans \<rbrace>" unfolding setQueue_def bitmapQ_no_L1_orphans_def null_def by (wp, auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>bitmapQ_no_L1_orphans\<rbrace> setQueue d p ts \<lbrace>\<lambda>rv. bitmapQ_no_L1_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>d i. ksReadyQueuesL1Bitmap s d !! i \<longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index i) \<noteq> 0 \<and> i < l2BitmapSize\<rbrace> modify (\<lambda>ks. ks\<lparr>ksReadyQueues := ksReadyQueues ks aLU [((d, p), ts)]\<rparr>) \<lbrace>\<lambda>rv s. \<forall>d i. ksReadyQueuesL1Bitmap s d !! i \<longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index i) \<noteq> 0 \<and> i < l2BitmapSize\<rbrace>
theory TcbAcc_R

lemma setQueue_bitmapQ_no_L2_orphans[wp]:
  "\<lbrace> bitmapQ_no_L2_orphans \<rbrace>
       setQueue d p ts
   \<lbrace>\<lambda>rv. bitmapQ_no_L2_orphans \<rbrace>" unfolding setQueue_def bitmapQ_no_L2_orphans_def null_def by (wp, auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>bitmapQ_no_L2_orphans\<rbrace> setQueue d p ts \<lbrace>\<lambda>rv. bitmapQ_no_L2_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>d i j. ksReadyQueuesL2Bitmap s (d, invertL1Index i) !! j \<and> i < l2BitmapSize \<longrightarrow> ksReadyQueuesL1Bitmap s d !! i\<rbrace> modify (\<lambda>ks. ks\<lparr>ksReadyQueues := ksReadyQueues ks aLU [((d, p), ts)]\<rparr>) \<lbrace>\<lambda>rv s. \<forall>d i j. ksReadyQueuesL2Bitmap s (d, invertL1Index i) !! j \<and> i < l2BitmapSize \<longrightarrow> ksReadyQueuesL1Bitmap s d !! i\<rbrace>
theory TcbAcc_R

lemma setQueue_sets_queue[wp]:
  "\<And>d p ts P. \<lbrace> \<lambda>s. P ts \<rbrace> setQueue d p ts \<lbrace>\<lambda>rv s. P (ksReadyQueues s (d, p)) \<rbrace>" unfolding setQueue_def by (wp, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>d p ts P. \<lbrace>\<lambda>s. P ts\<rbrace> setQueue d p ts \<lbrace>\<lambda>rv s. P (ksReadyQueues s (d, p))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>d p ts P. \<lbrace>\<lambda>s. P ts\<rbrace> modify (\<lambda>ks. ks\<lparr>ksReadyQueues := ksReadyQueues ks aLU [((d, p), ts)]\<rparr>) \<lbrace>\<lambda>rv s. P (ksReadyQueues s (d, p))\<rbrace>
theory TcbAcc_R

lemma tcbSchedEnqueue_valid_queues[wp]:
  "\<lbrace>Invariants_H.valid_queues
    and st_tcb_at' runnable' t
    and valid_objs' \<rbrace>
     tcbSchedEnqueue t
   \<lbrace>\<lambda>_. Invariants_H.valid_queues\<rbrace>" unfolding tcbSchedEnqueue_def by (fastforce intro:  tcbSchedEnqueueOrAppend_valid_queues)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>Invariants_H.valid_queues and st_tcb_at' runnable' t and valid_objs'\<rbrace> tcbSchedEnqueue t \<lbrace>\<lambda>_. Invariants_H.valid_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>Invariants_H.valid_queues and st_tcb_at' runnable' t and valid_objs'\<rbrace> do queued <- threadGet tcbQueued t;
unless queued $ do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
setQueue tdom prio $ t # queue;
when (null queue) $ addToBitmap tdom prio;
threadSet (tcbQueued_update (\<lambda>_. True)) t
od
od \<lbrace>\<lambda>_. Invariants_H.valid_queues\<rbrace>
theory TcbAcc_R

lemma tcbSchedAppend_valid_queues[wp]:
  "\<lbrace>Invariants_H.valid_queues
    and st_tcb_at' runnable' t
    and valid_objs' \<rbrace>
     tcbSchedAppend t
   \<lbrace>\<lambda>_. Invariants_H.valid_queues\<rbrace>" unfolding tcbSchedAppend_def by (fastforce intro:  tcbSchedEnqueueOrAppend_valid_queues)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>Invariants_H.valid_queues and st_tcb_at' runnable' t and valid_objs'\<rbrace> tcbSchedAppend t \<lbrace>\<lambda>_. Invariants_H.valid_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>Invariants_H.valid_queues and st_tcb_at' runnable' t and valid_objs'\<rbrace> do queued <- threadGet tcbQueued t;
unless queued $ do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
setQueue tdom prio $ queue @ [t];
when (null queue) $ addToBitmap tdom prio;
threadSet (tcbQueued_update (\<lambda>_. True)) t
od
od \<lbrace>\<lambda>_. Invariants_H.valid_queues\<rbrace>
theory TcbAcc_R

lemma rescheduleRequired_valid_queues[wp]:
  "\<lbrace>\<lambda>s. Invariants_H.valid_queues s \<and> valid_objs' s \<and>
        weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>
    rescheduleRequired
   \<lbrace>\<lambda>_. Invariants_H.valid_queues\<rbrace>" apply (simp add: rescheduleRequired_def) apply (wp | wpc | simp)+ apply (fastforce simp: weak_sch_act_wf_def elim: valid_objs'_maxDomain valid_objs'_maxPriority) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. Invariants_H.valid_queues s \<and> valid_objs' s \<and> weak_sch_act_wf (ksSchedulerAction s) s\<rbrace> rescheduleRequired \<lbrace>\<lambda>_. Invariants_H.valid_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. Invariants_H.valid_queues s \<and> valid_objs' s \<and> weak_sch_act_wf (ksSchedulerAction s) s\<rbrace> do action <- getSchedulerAction;
y <- case action of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return ();
setSchedulerAction ChooseNewThread
od \<lbrace>\<lambda>_. Invariants_H.valid_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. Invariants_H.valid_queues s \<and> valid_objs' s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<Longrightarrow> \<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s proof (prove)
goal:
No subgoals!