theory TcbAcc_R

lemma addToBitmap_valid_bitmapQ_except:
  "\<lbrace> valid_bitmapQ_except d p and bitmapQ_no_L2_orphans \<rbrace>
     addToBitmap d p
   \<lbrace>\<lambda>_. valid_bitmapQ_except d p \<rbrace>" unfolding bitmap_fun_defs bitmapQ_defs apply wp apply (clarsimp simp: bitmapQ_def invertL1Index_eq_cancel
                        ucast_and_mask[symmetric] unat_ucast_upcast is_up nth_w2p) apply (fastforce simp: priority_mask_wordRadix_size[simplified wordBits_def']
                   dest: prioToL1Index_bits_low_high_eq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_bitmapQ_except d p and bitmapQ_no_L2_orphans\<rbrace> addToBitmap d p \<lbrace>\<lambda>_. valid_bitmapQ_except d p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<forall>da pa. da \<noteq> d \<or> pa \<noteq> p \<longrightarrow> (ksReadyQueuesL1Bitmap s da !! prioToL1Index pa \<and> ksReadyQueuesL2Bitmap s (da, invertL1Index (prioToL1Index pa)) !! unat (pa && mask wordRadix)) = (ksReadyQueues s (da, pa) \<noteq> [])) and (\<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>da pa. da \<noteq> d \<or> pa \<noteq> p \<longrightarrow> (ksReadyQueuesL1Bitmap s da !! prioToL1Index pa \<and> ksReadyQueuesL2Bitmap s (da, invertL1Index (prioToL1Index pa)) !! unat (pa && mask wordRadix)) = (ksReadyQueues s (da, pa) \<noteq> [])\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. \<forall>da pa. da \<noteq> d \<or> pa \<noteq> p \<longrightarrow> (ksReadyQueuesL1Bitmap s da !! prioToL1Index pa \<and> ksReadyQueuesL2Bitmap s (da, invertL1Index (prioToL1Index pa)) !! unat (pa && mask wordRadix)) = (ksReadyQueues s (da, pa) \<noteq> [])) and (\<lambda>s. \<forall>d i j. ksReadyQueuesL2Bitmap s (d, invertL1Index i) !! j \<and> i < l2BitmapSize \<longrightarrow> ksReadyQueuesL1Bitmap s d !! i)) s \<Longrightarrow> \<forall>da pa. da \<noteq> d \<or> pa \<noteq> p \<longrightarrow> (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 !! prioToL1Index pa \<and> 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 (prioToL1Index pa)) !! unat (pa && mask wordRadix)) = (ksReadyQueues (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, pa) \<noteq> []) proof (prove)
goal (1 subgoal):
 1. \<And>s pa. \<lbrakk>\<forall>da pa. (da = d \<longrightarrow> pa \<noteq> p) \<longrightarrow> (ksReadyQueuesL1Bitmap s da !! prioToL1Index pa \<and> ksReadyQueuesL2Bitmap s (da, invertL1Index (prioToL1Index pa)) !! unat (pa && mask wordRadix)) = (ksReadyQueues s (da, pa) \<noteq> []); \<forall>d i. Ex ((!!) (ksReadyQueuesL2Bitmap s (d, invertL1Index i))) \<and> i < l2BitmapSize \<longrightarrow> ksReadyQueuesL1Bitmap s d !! i; prioToL1Index pa = prioToL1Index p; pa \<noteq> p\<rbrakk> \<Longrightarrow> ((ksReadyQueuesL1Bitmap s d !! prioToL1Index p \<or> prioToL1Index p < 32) \<and> (ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) !! unat (pa && mask wordRadix) \<or> unat (pa && mask wordRadix) < 32 \<and> p && mask wordRadix = pa && mask wordRadix)) = (ksReadyQueues s (d, pa) \<noteq> []) proof (prove)
goal:
No subgoals!