theory TcbAcc_R

lemma removeFromBitmap_bitmapQ_no_L2_orphans[wp]:
  "\<lbrace> bitmapQ_no_L2_orphans and bitmapQ_no_L1_orphans \<rbrace>
   removeFromBitmap d p
   \<lbrace>\<lambda>_. bitmapQ_no_L2_orphans \<rbrace>" unfolding bitmap_fun_defs apply (wp, clarsimp simp: bitmap_fun_defs bitmapQ_no_L2_orphans_def)+ apply (rule conjI, clarsimp) apply (clarsimp simp: complement_nth_w2p l2BitmapSize_def') apply clarsimp apply metis done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>bitmapQ_no_L2_orphans and bitmapQ_no_L1_orphans\<rbrace> removeFromBitmap d p \<lbrace>\<lambda>_. bitmapQ_no_L2_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>bitmapQ_no_L2_orphans and 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_L2_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>d i. Ex ((!!) (ksReadyQueuesL2Bitmap s (d, invertL1Index i))) \<and> i < l2BitmapSize \<longrightarrow> ksReadyQueuesL1Bitmap s d !! i; bitmapQ_no_L1_orphans s\<rbrakk> \<Longrightarrow> (ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) = 0 \<longrightarrow> (\<forall>i. invertL1Index i \<noteq> invertL1Index (prioToL1Index p) \<longrightarrow> Ex ((!!) (ksReadyQueuesL2Bitmap s (d, invertL1Index i))) \<and> i < l2BitmapSize \<longrightarrow> i < 32 \<and> (i < 32 \<longrightarrow> prioToL1Index p \<noteq> i))) \<and> (ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) \<noteq> 0 \<longrightarrow> (\<forall>i. invertL1Index i = invertL1Index (prioToL1Index p) \<longrightarrow> Ex ((!!) (ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix))) \<and> i < l2BitmapSize \<longrightarrow> ksReadyQueuesL1Bitmap s d !! i)) proof (prove)
goal (2 subgoals):
 1. \<And>s i x. \<lbrakk>\<forall>d i. Ex ((!!) (ksReadyQueuesL2Bitmap s (d, invertL1Index i))) \<and> i < l2BitmapSize \<longrightarrow> ksReadyQueuesL1Bitmap s d !! i; bitmapQ_no_L1_orphans s; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) = 0; invertL1Index i \<noteq> invertL1Index (prioToL1Index p); i < l2BitmapSize; ksReadyQueuesL2Bitmap s (d, invertL1Index i) !! x\<rbrakk> \<Longrightarrow> i < 32 \<and> (i < 32 \<longrightarrow> prioToL1Index p \<noteq> i)
 2. \<And>s. \<lbrakk>\<forall>d i. Ex ((!!) (ksReadyQueuesL2Bitmap s (d, invertL1Index i))) \<and> i < l2BitmapSize \<longrightarrow> ksReadyQueuesL1Bitmap s d !! i; bitmapQ_no_L1_orphans s\<rbrakk> \<Longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) \<noteq> 0 \<longrightarrow> (\<forall>i. invertL1Index i = invertL1Index (prioToL1Index p) \<longrightarrow> Ex ((!!) (ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix))) \<and> i < l2BitmapSize \<longrightarrow> ksReadyQueuesL1Bitmap s d !! i) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>d i. Ex ((!!) (ksReadyQueuesL2Bitmap s (d, invertL1Index i))) \<and> i < l2BitmapSize \<longrightarrow> ksReadyQueuesL1Bitmap s d !! i; bitmapQ_no_L1_orphans s\<rbrakk> \<Longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) \<noteq> 0 \<longrightarrow> (\<forall>i. invertL1Index i = invertL1Index (prioToL1Index p) \<longrightarrow> Ex ((!!) (ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix))) \<and> i < l2BitmapSize \<longrightarrow> ksReadyQueuesL1Bitmap s d !! i) proof (prove)
goal (1 subgoal):
 1. \<And>s i x. \<lbrakk>\<forall>d i. Ex ((!!) (ksReadyQueuesL2Bitmap s (d, invertL1Index i))) \<and> i < l2BitmapSize \<longrightarrow> ksReadyQueuesL1Bitmap s d !! i; bitmapQ_no_L1_orphans s; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) \<noteq> 0; invertL1Index i = invertL1Index (prioToL1Index p); i < l2BitmapSize; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) !! x; x < 32; unat (p && mask wordRadix) \<noteq> x\<rbrakk> \<Longrightarrow> ksReadyQueuesL1Bitmap s d !! i proof (prove)
goal:
No subgoals!