theory TcbAcc_R

lemma addToBitmap_bitmapQ_no_L1_orphans[wp]:
  "\<lbrace> bitmapQ_no_L1_orphans \<rbrace> addToBitmap d p \<lbrace>\<lambda>_. bitmapQ_no_L1_orphans \<rbrace>" unfolding bitmap_fun_defs bitmapQ_defs using word_unat_mask_lt[where w=p and m=wordRadix] apply wp apply (clarsimp simp: word_or_zero prioToL1Index_bit_set ucast_and_mask[symmetric]
                        unat_ucast_upcast is_up wordRadix_def' word_size nth_w2p
                        wordBits_def numPriorities_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>bitmapQ_no_L1_orphans\<rbrace> addToBitmap d p \<lbrace>\<lambda>_. 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> 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. ksReadyQueuesL1Bitmap s d !! i \<longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index i) \<noteq> 0 \<and> i < l2BitmapSize\<rbrace> proof (prove)
using this:
wordRadix \<le> size p \<Longrightarrow> unat (p && mask wordRadix) < 2 ^ wordRadix

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> 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. ksReadyQueuesL1Bitmap s d !! i \<longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index i) \<noteq> 0 \<and> i < l2BitmapSize\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>wordRadix \<le> size p \<Longrightarrow> unat (p && mask wordRadix) < 2 ^ wordRadix; \<forall>d i. ksReadyQueuesL1Bitmap s d !! i \<longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index i) \<noteq> 0 \<and> i < l2BitmapSize\<rbrakk> \<Longrightarrow> \<forall>da i. ksReadyQueuesL1Bitmap (s\<lparr>ksReadyQueuesL1Bitmap := ksReadyQueuesL1Bitmap s aLU [(d, ksReadyQueuesL1Bitmap s d || HaskellLib_H.bit (prioToL1Index p))], ksReadyQueuesL2Bitmap := ksReadyQueuesL2Bitmap (s\<lparr>ksReadyQueuesL1Bitmap := ksReadyQueuesL1Bitmap s aLU [(d, ksReadyQueuesL1Bitmap s d || HaskellLib_H.bit (prioToL1Index p))]\<rparr>) aLU [((d, invertL1Index (prioToL1Index p)), ksReadyQueuesL2Bitmap (s\<lparr>ksReadyQueuesL1Bitmap := ksReadyQueuesL1Bitmap s aLU [(d, ksReadyQueuesL1Bitmap s d || HaskellLib_H.bit (prioToL1Index p))]\<rparr>) (d, invertL1Index (prioToL1Index p)) || HaskellLib_H.bit (fromIntegral (fromIntegral p && mask wordRadix)))]\<rparr>) da !! i \<longrightarrow> ksReadyQueuesL2Bitmap (s\<lparr>ksReadyQueuesL1Bitmap := ksReadyQueuesL1Bitmap s aLU [(d, ksReadyQueuesL1Bitmap s d || HaskellLib_H.bit (prioToL1Index p))], ksReadyQueuesL2Bitmap := ksReadyQueuesL2Bitmap (s\<lparr>ksReadyQueuesL1Bitmap := ksReadyQueuesL1Bitmap s aLU [(d, ksReadyQueuesL1Bitmap s d || HaskellLib_H.bit (prioToL1Index p))]\<rparr>) aLU [((d, invertL1Index (prioToL1Index p)), ksReadyQueuesL2Bitmap (s\<lparr>ksReadyQueuesL1Bitmap := ksReadyQueuesL1Bitmap s aLU [(d, ksReadyQueuesL1Bitmap s d || HaskellLib_H.bit (prioToL1Index p))]\<rparr>) (d, invertL1Index (prioToL1Index p)) || HaskellLib_H.bit (fromIntegral (fromIntegral p && mask wordRadix)))]\<rparr>) (da, invertL1Index i) \<noteq> 0 \<and> i < l2BitmapSize proof (prove)
goal:
No subgoals!