theory IpcCancel_C

lemma getHighestPrio_ccorres:
  "ccorres (\<lambda>rv rv'. rv' = ucast rv) ret__unsigned_long_'
    (\<lambda>s. d \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s d \<noteq> 0 \<and> bitmapQ_no_L1_orphans s)
    (UNIV \<inter> {s. dom_' s = ucast d}) hs
    (getHighestPrio d) (Call getHighestPrio_'proc)" proof - note prio_and_dom_limit_helpers [simp] note Collect_const_mem [simp] have signed_word_log2:
  "\<And>w. w \<noteq> 0 \<Longrightarrow> (0x1F::32 signed word) - of_nat (word_clz (w::machine_word)) = (of_nat (word_log2 w))" unfolding word_log2_def by (clarsimp dest!: word_clz_nonzero_max simp: word_size) have word_log2_def32:
    "\<And>w. word_log2 (w::machine_word) = 31 - word_clz w" unfolding word_log2_def by (simp add: word_size) 

  (* FIXME generalise *)
   have word_clz_sint_upper[simp]:
    "\<And>(w::machine_word). sint (of_nat (word_clz w) :: 32 signed word) \<le> 2147483679" apply (subst sint_eq_uint) apply (rule not_msb_from_less) apply simp apply (rule word_of_nat_less) apply simp apply (rule order_le_less_trans[OF word_clz_max]) apply (simp add: word_size) apply (subst uint_nat) apply (simp add: unat_of_nat) apply (subst Divides.mod_less) apply simp apply (rule order_le_less_trans[OF word_clz_max]) apply (simp add: word_size) apply (rule iffD2 [OF le_nat_iff[symmetric]]) apply simp apply (rule order_trans[OF word_clz_max]) apply (simp add: word_size) done have word_clz_sint_lower[simp]:
    "\<And>(w::machine_word). - sint (of_nat (word_clz w) :: 32 signed word) \<le> 2147483616" apply (subst sint_eq_uint) apply (rule not_msb_from_less) apply simp apply (rule word_of_nat_less) apply simp apply (rule order_le_less_trans[OF word_clz_max]) apply (simp add: word_size) apply (subst uint_nat) apply (simp add: unat_of_nat) done have invertL1Index_unat_fold:
    "\<And>(w::32 word). \<lbrakk> w \<noteq> 0 ; word_log2 w < l2BitmapSize \<rbrakk> \<Longrightarrow>
       unat (of_nat l2BitmapSize - (1::32 word) - of_nat (word_log2 w))
     = invertL1Index (word_log2 w)" apply (subst unat_sub) apply (clarsimp simp: l2BitmapSize_def') apply (rule word_of_nat_le) apply (drule word_log2_nth_same) apply (clarsimp simp: l2BitmapSize_def') apply (clarsimp simp: invertL1Index_def l2BitmapSize_def') apply (simp add: unat_of_nat_eq) done 

  (* when numDomains = 1, array bounds checks would become _ = 0 rather than _ < 1, changing the
     shape of the proof compared to when numDomains > 1 *)
   include no_less_1_simps show ?thesis apply (cinit lift: dom_') apply (clarsimp split del: if_split) apply (rule ccorres_pre_getReadyQueuesL1Bitmap) apply (rule ccorres_pre_getReadyQueuesL2Bitmap) apply (rename_tac l2) apply (rule ccorres_Guard_Seq|csymbr)+ apply (rule ccorres_abstract_cleanup) apply (rule ccorres_Guard_Seq|csymbr)+ apply (rule ccorres_abstract_cleanup) apply (rule ccorres_Guard_Seq|csymbr)+ apply (clarsimp simp: word_log2_def word_size) apply (rename_tac clz_l1index clz_l2index) apply (rule_tac P="\<lambda>s. l1 \<noteq> 0 \<and> l2 \<noteq> 0 \<and> word_log2 l1 < l2BitmapSize"
            and P'="{s. clz_l1index = of_nat (word_clz l1) \<and>
                        clz_l2index = of_nat (word_clz l2) }"
            in ccorres_from_vcg_throws) apply (rule allI, rule conseqPre, vcg) subgoal apply (clarsimp simp: return_def l1IndexToPrio_def) apply (simp add: signed_word_log2 word_log2_def32[symmetric] ucast_or_distrib) apply (rule_tac f="(||)" in arg_cong2) apply (subst of_nat_shiftl)+ apply (subst ucast_of_nat_small, simp add: wordRadix_def l2BitmapSize_def') apply (rule refl) apply (subst ucast_of_nat_small, simp add: wordRadix_def) apply (rule word_log2_max_word32[THEN order_less_le_trans], simp) apply (rule refl) done apply (clarsimp simp: word_sle_def) apply (frule rf_sr_cbitmap_L1_relation) apply (subgoal_tac "ksReadyQueuesL1Bitmap_' (globals s').[unat d] \<noteq> 0") prefer 2 subgoal by (fastforce simp: cbitmap_L1_relation_def) apply (clarsimp simp: signed_word_log2 cbitmap_L1_relation_def maxDomain_le_unat_ucast_explicit) apply (frule bitmapQ_no_L1_orphansD, erule word_log2_nth_same) apply (rule conjI, fastforce simp: invertL1Index_def l2BitmapSize_def') apply (rule conjI, fastforce) apply (rule conjI, fastforce) apply (rule conjI, fastforce simp: invertL1Index_unat_fold) apply (rule conjI) apply (subst invertL1Index_unat_fold, assumption, fastforce) apply (frule rf_sr_cbitmap_L2_relation) apply (fastforce simp: cbitmap_L2_relation_def) apply (clarsimp simp: l2BitmapSize_def') apply (fastforce simp: word_less_nat_alt word_le_nat_alt unat_sub unat_of_nat) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) ret__unsigned_long_' (\<lambda>s. d \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s d \<noteq> 0 \<and> bitmapQ_no_L1_orphans s) (UNIV \<inter> \<lbrace>\<acute>dom = UCAST(8 \<rightarrow> 32) d\<rbrace>) hs (getHighestPrio d) (Call getHighestPrio_'proc) proof (state)
goal (1 subgoal):
 1. ccorres (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) ret__unsigned_long_' (\<lambda>s. d \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s d \<noteq> 0 \<and> bitmapQ_no_L1_orphans s) (UNIV \<inter> \<lbrace>\<acute>dom = UCAST(8 \<rightarrow> 32) d\<rbrace>) hs (getHighestPrio d) (Call getHighestPrio_'proc) proof (state)
this:
UCAST(8 \<rightarrow> 32) ?p >> wordRadix < 8
UCAST(8 \<rightarrow> 32) ?p >> wordRadix \<le> 7
UCAST(8 \<rightarrow> 32) ?p >> wordRadix < 0x20
unat (?p >> wordRadix) \<le> 7
unat (UCAST(8 \<rightarrow> 32) ?d * 0x100 + UCAST(8 \<rightarrow> 32) ?p) = unat ?d * 256 + unat ?p
unat (UCAST(8 \<rightarrow> 32) ?p && 0x1F) = unat (?p && 0x1F)
?w && 0x1F < 0x20

goal (1 subgoal):
 1. ccorres (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) ret__unsigned_long_' (\<lambda>s. d \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s d \<noteq> 0 \<and> bitmapQ_no_L1_orphans s) (UNIV \<inter> \<lbrace>\<acute>dom = UCAST(8 \<rightarrow> 32) d\<rbrace>) hs (getHighestPrio d) (Call getHighestPrio_'proc) proof (state)
this:
(?x \<in> (if ?P then UNIV else {})) = ?P

goal (1 subgoal):
 1. ccorres (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) ret__unsigned_long_' (\<lambda>s. d \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s d \<noteq> 0 \<and> bitmapQ_no_L1_orphans s) (UNIV \<inter> \<lbrace>\<acute>dom = UCAST(8 \<rightarrow> 32) d\<rbrace>) hs (getHighestPrio d) (Call getHighestPrio_'proc) proof (prove)
goal (1 subgoal):
 1. \<And>w. w \<noteq> 0 \<Longrightarrow> 0x1F - word_of_nat (word_clz w) = word_of_nat (word_log2 w) proof (prove)
goal (1 subgoal):
 1. \<And>w. w \<noteq> 0 \<Longrightarrow> 0x1F - word_of_nat (word_clz w) = word_of_nat (size w - 1 - word_clz w) proof (state)
this:
?w1 \<noteq> 0 \<Longrightarrow> 0x1F - word_of_nat (word_clz ?w1) = word_of_nat (word_log2 ?w1)

goal (1 subgoal):
 1. ccorres (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) ret__unsigned_long_' (\<lambda>s. d \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s d \<noteq> 0 \<and> bitmapQ_no_L1_orphans s) (UNIV \<inter> \<lbrace>\<acute>dom = UCAST(8 \<rightarrow> 32) d\<rbrace>) hs (getHighestPrio d) (Call getHighestPrio_'proc) proof (prove)
goal (1 subgoal):
 1. \<And>w. word_log2 w = 31 - word_clz w proof (prove)
goal (1 subgoal):
 1. \<And>w. size w - 1 - word_clz w = 31 - word_clz w proof (state)
this:
word_log2 ?w1 = 31 - word_clz ?w1

goal (1 subgoal):
 1. ccorres (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) ret__unsigned_long_' (\<lambda>s. d \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s d \<noteq> 0 \<and> bitmapQ_no_L1_orphans s) (UNIV \<inter> \<lbrace>\<acute>dom = UCAST(8 \<rightarrow> 32) d\<rbrace>) hs (getHighestPrio d) (Call getHighestPrio_'proc) proof (state)
this:
word_log2 ?w1 = 31 - word_clz ?w1

goal (1 subgoal):
 1. ccorres (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) ret__unsigned_long_' (\<lambda>s. d \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s d \<noteq> 0 \<and> bitmapQ_no_L1_orphans s) (UNIV \<inter> \<lbrace>\<acute>dom = UCAST(8 \<rightarrow> 32) d\<rbrace>) hs (getHighestPrio d) (Call getHighestPrio_'proc) proof (prove)
goal (1 subgoal):
 1. \<And>w. sint (word_of_nat (word_clz w)) \<le> 2147483679 proof (prove)
goal (2 subgoals):
 1. \<And>w. \<not> msb (word_of_nat (word_clz w))
 2. \<And>w. uint (word_of_nat (word_clz w)) \<le> 2147483679 proof (prove)
goal (2 subgoals):
 1. \<And>w. word_of_nat (word_clz w) < 2 ^ (LENGTH(32 signed) - 1)
 2. \<And>w. uint (word_of_nat (word_clz w)) \<le> 2147483679 proof (prove)
goal (2 subgoals):
 1. \<And>w. word_of_nat (word_clz w) < 0x80000000
 2. \<And>w. uint (word_of_nat (word_clz w)) \<le> 2147483679 proof (prove)
goal (2 subgoals):
 1. \<And>w. word_clz w < unat 0x80000000
 2. \<And>w. uint (word_of_nat (word_clz w)) \<le> 2147483679 proof (prove)
goal (2 subgoals):
 1. \<And>w. word_clz w < 2147483648
 2. \<And>w. uint (word_of_nat (word_clz w)) \<le> 2147483679 proof (prove)
goal (2 subgoals):
 1. \<And>w. size w < 2147483648
 2. \<And>w. uint (word_of_nat (word_clz w)) \<le> 2147483679 proof (prove)
goal (1 subgoal):
 1. \<And>w. uint (word_of_nat (word_clz w)) \<le> 2147483679 proof (prove)
goal (1 subgoal):
 1. \<And>w. int (unat (word_of_nat (word_clz w))) \<le> 2147483679 proof (prove)
goal (1 subgoal):
 1. \<And>w. int (word_clz w mod 4294967296) \<le> 2147483679 proof (prove)
goal (3 subgoals):
 1. \<And>w. 0 \<le> word_clz w
 2. \<And>w. word_clz w < 4294967296
 3. \<And>w. int (word_clz w) \<le> 2147483679 proof (prove)
goal (2 subgoals):
 1. \<And>w. word_clz w < 4294967296
 2. \<And>w. int (word_clz w) \<le> 2147483679 proof (prove)
goal (2 subgoals):
 1. \<And>w. size w < 4294967296
 2. \<And>w. int (word_clz w) \<le> 2147483679 proof (prove)
goal (1 subgoal):
 1. \<And>w. int (word_clz w) \<le> 2147483679 proof (prove)
goal (2 subgoals):
 1. \<And>w. 0 \<le> 2147483679
 2. \<And>w. word_clz w \<le> nat 2147483679 proof (prove)
goal (1 subgoal):
 1. \<And>w. word_clz w \<le> nat 2147483679 proof (prove)
goal (1 subgoal):
 1. \<And>w. size w \<le> nat 2147483679 proof (prove)
goal:
No subgoals! proof (state)
this:
sint (word_of_nat (word_clz ?w1)) \<le> 2147483679

goal (1 subgoal):
 1. ccorres (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) ret__unsigned_long_' (\<lambda>s. d \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s d \<noteq> 0 \<and> bitmapQ_no_L1_orphans s) (UNIV \<inter> \<lbrace>\<acute>dom = UCAST(8 \<rightarrow> 32) d\<rbrace>) hs (getHighestPrio d) (Call getHighestPrio_'proc) proof (prove)
goal (1 subgoal):
 1. \<And>w. - sint (word_of_nat (word_clz w)) \<le> 2147483616 proof (prove)
goal (2 subgoals):
 1. \<And>w. \<not> msb (word_of_nat (word_clz w))
 2. \<And>w. - uint (word_of_nat (word_clz w)) \<le> 2147483616 proof (prove)
goal (2 subgoals):
 1. \<And>w. word_of_nat (word_clz w) < 2 ^ (LENGTH(32 signed) - 1)
 2. \<And>w. - uint (word_of_nat (word_clz w)) \<le> 2147483616 proof (prove)
goal (2 subgoals):
 1. \<And>w. word_of_nat (word_clz w) < 0x80000000
 2. \<And>w. - uint (word_of_nat (word_clz w)) \<le> 2147483616 proof (prove)
goal (2 subgoals):
 1. \<And>w. word_clz w < unat 0x80000000
 2. \<And>w. - uint (word_of_nat (word_clz w)) \<le> 2147483616 proof (prove)
goal (2 subgoals):
 1. \<And>w. word_clz w < 2147483648
 2. \<And>w. - uint (word_of_nat (word_clz w)) \<le> 2147483616 proof (prove)
goal (2 subgoals):
 1. \<And>w. size w < 2147483648
 2. \<And>w. - uint (word_of_nat (word_clz w)) \<le> 2147483616 proof (prove)
goal (1 subgoal):
 1. \<And>w. - uint (word_of_nat (word_clz w)) \<le> 2147483616 proof (prove)
goal (1 subgoal):
 1. \<And>w. - int (unat (word_of_nat (word_clz w))) \<le> 2147483616 proof (prove)
goal:
No subgoals! proof (state)
this:
- sint (word_of_nat (word_clz ?w1)) \<le> 2147483616

goal (1 subgoal):
 1. ccorres (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) ret__unsigned_long_' (\<lambda>s. d \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s d \<noteq> 0 \<and> bitmapQ_no_L1_orphans s) (UNIV \<inter> \<lbrace>\<acute>dom = UCAST(8 \<rightarrow> 32) d\<rbrace>) hs (getHighestPrio d) (Call getHighestPrio_'proc) proof (prove)
goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<noteq> 0; word_log2 w < l2BitmapSize\<rbrakk> \<Longrightarrow> unat (word_of_nat l2BitmapSize - 1 - word_of_nat (word_log2 w)) = invertL1Index (word_log2 w) proof (prove)
goal (2 subgoals):
 1. \<And>w. \<lbrakk>w \<noteq> 0; word_log2 w < l2BitmapSize\<rbrakk> \<Longrightarrow> word_of_nat (word_log2 w) \<le> word_of_nat l2BitmapSize - 1
 2. \<And>w. \<lbrakk>w \<noteq> 0; word_log2 w < l2BitmapSize\<rbrakk> \<Longrightarrow> unat (word_of_nat l2BitmapSize - 1) - unat (word_of_nat (word_log2 w)) = invertL1Index (word_log2 w) proof (prove)
goal (2 subgoals):
 1. \<And>w. \<lbrakk>w \<noteq> 0; word_log2 w < 8\<rbrakk> \<Longrightarrow> word_of_nat (word_log2 w) \<le> 7
 2. \<And>w. \<lbrakk>w \<noteq> 0; word_log2 w < l2BitmapSize\<rbrakk> \<Longrightarrow> unat (word_of_nat l2BitmapSize - 1) - unat (word_of_nat (word_log2 w)) = invertL1Index (word_log2 w) proof (prove)
goal (2 subgoals):
 1. \<And>w. \<lbrakk>w \<noteq> 0; word_log2 w < 8\<rbrakk> \<Longrightarrow> word_log2 w \<le> unat 7
 2. \<And>w. \<lbrakk>w \<noteq> 0; word_log2 w < l2BitmapSize\<rbrakk> \<Longrightarrow> unat (word_of_nat l2BitmapSize - 1) - unat (word_of_nat (word_log2 w)) = invertL1Index (word_log2 w) proof (prove)
goal (2 subgoals):
 1. \<And>w. \<lbrakk>word_log2 w < 8; w !! word_log2 w\<rbrakk> \<Longrightarrow> word_log2 w \<le> unat 7
 2. \<And>w. \<lbrakk>w \<noteq> 0; word_log2 w < l2BitmapSize\<rbrakk> \<Longrightarrow> unat (word_of_nat l2BitmapSize - 1) - unat (word_of_nat (word_log2 w)) = invertL1Index (word_log2 w) proof (prove)
goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<noteq> 0; word_log2 w < l2BitmapSize\<rbrakk> \<Longrightarrow> unat (word_of_nat l2BitmapSize - 1) - unat (word_of_nat (word_log2 w)) = invertL1Index (word_log2 w) proof (prove)
goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<noteq> 0; word_log2 w < 8\<rbrakk> \<Longrightarrow> 7 - unat (word_of_nat (word_log2 w)) = 7 - word_log2 w proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrakk>?w1 \<noteq> 0; word_log2 ?w1 < l2BitmapSize\<rbrakk> \<Longrightarrow> unat (word_of_nat l2BitmapSize - 1 - word_of_nat (word_log2 ?w1)) = invertL1Index (word_log2 ?w1)

goal (1 subgoal):
 1. ccorres (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) ret__unsigned_long_' (\<lambda>s. d \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s d \<noteq> 0 \<and> bitmapQ_no_L1_orphans s) (UNIV \<inter> \<lbrace>\<acute>dom = UCAST(8 \<rightarrow> 32) d\<rbrace>) hs (getHighestPrio d) (Call getHighestPrio_'proc) proof (state)
this:
\<lbrakk>?w1 \<noteq> 0; word_log2 ?w1 < l2BitmapSize\<rbrakk> \<Longrightarrow> unat (word_of_nat l2BitmapSize - 1 - word_of_nat (word_log2 ?w1)) = invertL1Index (word_log2 ?w1)

goal (1 subgoal):
 1. ccorres (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) ret__unsigned_long_' (\<lambda>s. d \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s d \<noteq> 0 \<and> bitmapQ_no_L1_orphans s) (UNIV \<inter> \<lbrace>\<acute>dom = UCAST(8 \<rightarrow> 32) d\<rbrace>) hs (getHighestPrio d) (Call getHighestPrio_'proc) proof (state)
goal (1 subgoal):
 1. ccorres (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) ret__unsigned_long_' (\<lambda>s. d \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s d \<noteq> 0 \<and> bitmapQ_no_L1_orphans s) (UNIV \<inter> \<lbrace>\<acute>dom = UCAST(8 \<rightarrow> 32) d\<rbrace>) hs (getHighestPrio d) (Call getHighestPrio_'proc) proof (prove)
goal (1 subgoal):
 1. ccorres (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) ret__unsigned_long_' (\<lambda>s. d \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s d \<noteq> 0 \<and> bitmapQ_no_L1_orphans s) (UNIV \<inter> \<lbrace>\<acute>dom = UCAST(8 \<rightarrow> 32) d\<rbrace>) hs (getHighestPrio d) (Call getHighestPrio_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>dom. dom = UCAST(8 \<rightarrow> 32) d \<Longrightarrow> ccorres (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) ret__unsigned_long_' (?Q623 dom) (?Q'623 dom) (SKIP # hs) (do l1 <- getReadyQueuesL1Bitmap d;
l2 <- getReadyQueuesL2Bitmap d (invertL1Index (word_log2 l1));
return (l1IndexToPrio (word_log2 l1) || word_of_nat (word_log2 l2))
od) (Guard ArrayBounds \<lbrace>dom < 0x10\<rbrace> (\<acute>ret__long :== CALL clzl_'proc(\<acute>ksReadyQueuesL1Bitmap.[unat dom]));;
(Guard SignedArithmetic \<lbrace>sint \<acute>ret__long \<le> 2147483679 \<and> - sint \<acute>ret__long \<le> 2147483616\<rbrace> (\<acute>l1index :== SCAST(32 signed \<rightarrow> 32) (0x1F - \<acute>ret__long));;
(\<acute>l1index_inverted :== CALL invert_l1index_'proc(\<acute>l1index);;
(Guard ArrayBounds \<lbrace>\<acute>l1index_inverted < 8\<rbrace> (Guard ArrayBounds \<lbrace>dom < 0x10\<rbrace> (\<acute>ret__long :== CALL clzl_'proc(\<acute>ksReadyQueuesL2Bitmap.[unat dom].[unat \<acute>l1index_inverted])));;
(Guard SignedArithmetic \<lbrace>sint \<acute>ret__long \<le> 2147483679 \<and> - sint \<acute>ret__long \<le> 2147483616\<rbrace> (\<acute>l2index :== SCAST(32 signed \<rightarrow> 32) (0x1F - \<acute>ret__long));;
(\<acute>ret__unsigned_long :== CALL l1index_to_prio_'proc(\<acute>l1index);;
return_C ret__unsigned_long_'_update (\<lambda>s. ret__unsigned_long_' s || l2index_' s)))))))
 2. \<And>dom s s'. \<lbrakk>dom = UCAST(8 \<rightarrow> 32) d; (s, s') \<in> rf_sr; d \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s d \<noteq> 0 \<and> bitmapQ_no_L1_orphans s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q623 dom s \<and> s' \<in> ?Q'623 dom proof (prove)
goal (2 subgoals):
 1. ccorres (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) ret__unsigned_long_' (?Q623 (UCAST(8 \<rightarrow> 32) d)) (?Q'623 (UCAST(8 \<rightarrow> 32) d)) (SKIP # hs) (do l1 <- getReadyQueuesL1Bitmap d;
l2 <- getReadyQueuesL2Bitmap d (invertL1Index (word_log2 l1));
return (l1IndexToPrio (word_log2 l1) || word_of_nat (word_log2 l2))
od) (Guard ArrayBounds (if UCAST(8 \<rightarrow> 32) d < 0x10 then UNIV else {}) (\<acute>ret__long :== CALL clzl_'proc(\<acute>ksReadyQueuesL1Bitmap.[unat d]));;
(Guard SignedArithmetic \<lbrace>sint \<acute>ret__long \<le> 2147483679 \<and> - sint \<acute>ret__long \<le> 2147483616\<rbrace> (\<acute>l1index :== SCAST(32 signed \<rightarrow> 32) (0x1F - \<acute>ret__long));;
(\<acute>l1index_inverted :== CALL invert_l1index_'proc();;
(Guard ArrayBounds \<lbrace>\<acute>l1index_inverted < 8\<rbrace> (Guard ArrayBounds (if UCAST(8 \<rightarrow> 32) d < 0x10 then UNIV else {}) (\<acute>ret__long :== CALL clzl_'proc(\<acute>ksReadyQueuesL2Bitmap.[unat d].[unat \<acute>l1index_inverted])));;
(Guard SignedArithmetic \<lbrace>sint \<acute>ret__long \<le> 2147483679 \<and> - sint \<acute>ret__long \<le> 2147483616\<rbrace> (\<acute>l2index :== SCAST(32 signed \<rightarrow> 32) (0x1F - \<acute>ret__long));;
(\<acute>ret__unsigned_long :== CALL l1index_to_prio_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. ret__unsigned_long_' s || l2index_' s)))))))
 2. \<And>dom s s'. \<lbrakk>dom = UCAST(8 \<rightarrow> 32) d; (s, s') \<in> rf_sr; d \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s d \<noteq> 0 \<and> bitmapQ_no_L1_orphans s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q623 dom s \<and> s' \<in> ?Q'623 dom proof (prove)
goal (2 subgoals):
 1. \<And>l1. ccorres (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) ret__unsigned_long_' (\<lambda>a. ?P639 (UCAST(8 \<rightarrow> 32) d) a l1) (?P'640 (UCAST(8 \<rightarrow> 32) d) l1) (SKIP # hs) (do l2 <- getReadyQueuesL2Bitmap d (invertL1Index (word_log2 l1));
return (l1IndexToPrio (word_log2 l1) || word_of_nat (word_log2 l2))
od) (Guard ArrayBounds (if UCAST(8 \<rightarrow> 32) d < 0x10 then UNIV else {}) (\<acute>ret__long :== CALL clzl_'proc(\<acute>ksReadyQueuesL1Bitmap.[unat d]));;
(Guard SignedArithmetic \<lbrace>sint \<acute>ret__long \<le> 2147483679 \<and> - sint \<acute>ret__long \<le> 2147483616\<rbrace> (\<acute>l1index :== SCAST(32 signed \<rightarrow> 32) (0x1F - \<acute>ret__long));;
(\<acute>l1index_inverted :== CALL invert_l1index_'proc();;
(Guard ArrayBounds \<lbrace>\<acute>l1index_inverted < 8\<rbrace> (Guard ArrayBounds (if UCAST(8 \<rightarrow> 32) d < 0x10 then UNIV else {}) (\<acute>ret__long :== CALL clzl_'proc(\<acute>ksReadyQueuesL2Bitmap.[unat d].[unat \<acute>l1index_inverted])));;
(Guard SignedArithmetic \<lbrace>sint \<acute>ret__long \<le> 2147483679 \<and> - sint \<acute>ret__long \<le> 2147483616\<rbrace> (\<acute>l2index :== SCAST(32 signed \<rightarrow> 32) (0x1F - \<acute>ret__long));;
(\<acute>ret__unsigned_long :== CALL l1index_to_prio_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. ret__unsigned_long_' s || l2index_' s)))))))
 2. \<And>dom s s'. \<lbrakk>dom = UCAST(8 \<rightarrow> 32) d; (s, s') \<in> rf_sr; d \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s d \<noteq> 0 \<and> bitmapQ_no_L1_orphans s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (d \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s d = rv \<longrightarrow> ?P639 dom s rv)) \<and> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat d] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> ?P'640 dom rv} proof (prove)
goal (2 subgoals):
 1. \<And>l1 rv. ccorres (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) ret__unsigned_long_' (\<lambda>a. ?P647 (UCAST(8 \<rightarrow> 32) d) l1 a rv) (?P'646 (UCAST(8 \<rightarrow> 32) d) l1 rv) (SKIP # hs) (return (l1IndexToPrio (word_log2 l1) || word_of_nat (word_log2 rv))) (Guard ArrayBounds (if UCAST(8 \<rightarrow> 32) d < 0x10 then UNIV else {}) (\<acute>ret__long :== CALL clzl_'proc(\<acute>ksReadyQueuesL1Bitmap.[unat d]));;
(Guard SignedArithmetic \<lbrace>sint \<acute>ret__long \<le> 2147483679 \<and> - sint \<acute>ret__long \<le> 2147483616\<rbrace> (\<acute>l1index :== SCAST(32 signed \<rightarrow> 32) (0x1F - \<acute>ret__long));;
(\<acute>l1index_inverted :== CALL invert_l1index_'proc();;
(Guard ArrayBounds \<lbrace>\<acute>l1index_inverted < 8\<rbrace> (Guard ArrayBounds (if UCAST(8 \<rightarrow> 32) d < 0x10 then UNIV else {}) (\<acute>ret__long :== CALL clzl_'proc(\<acute>ksReadyQueuesL2Bitmap.[unat d].[unat \<acute>l1index_inverted])));;
(Guard SignedArithmetic \<lbrace>sint \<acute>ret__long \<le> 2147483679 \<and> - sint \<acute>ret__long \<le> 2147483616\<rbrace> (\<acute>l2index :== SCAST(32 signed \<rightarrow> 32) (0x1F - \<acute>ret__long));;
(\<acute>ret__unsigned_long :== CALL l1index_to_prio_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. ret__unsigned_long_' s || l2index_' s)))))))
 2. \<And>dom s s'. \<lbrakk>dom = UCAST(8 \<rightarrow> 32) d; (s, s') \<in> rf_sr; d \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s d \<noteq> 0 \<and> bitmapQ_no_L1_orphans s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (d \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s d = rv \<longrightarrow> d \<le> maxDomain \<and> invertL1Index (word_log2 rv) < l2BitmapSize \<and> (\<forall>rva. ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 rv)) = rva \<longrightarrow> ?P647 dom rv s rva))) \<and> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat d] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> {s. \<forall>rva. ksReadyQueuesL2Bitmap_' (globals s).[unat d].[invertL1Index (word_log2 rv)] = UCAST(32 \<rightarrow> 32) rva \<longrightarrow> s \<in> ?P'646 dom rv rva}} proof (prove)
goal (2 subgoals):
 1. \<And>l1 l2. ccorres (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) ret__unsigned_long_' (\<lambda>a. ?P647 (UCAST(8 \<rightarrow> 32) d) l1 a l2) (?P'646 (UCAST(8 \<rightarrow> 32) d) l1 l2) (SKIP # hs) (return (l1IndexToPrio (word_log2 l1) || word_of_nat (word_log2 l2))) (Guard ArrayBounds (if UCAST(8 \<rightarrow> 32) d < 0x10 then UNIV else {}) (\<acute>ret__long :== CALL clzl_'proc(\<acute>ksReadyQueuesL1Bitmap.[unat d]));;
(Guard SignedArithmetic \<lbrace>sint \<acute>ret__long \<le> 2147483679 \<and> - sint \<acute>ret__long \<le> 2147483616\<rbrace> (\<acute>l1index :== SCAST(32 signed \<rightarrow> 32) (0x1F - \<acute>ret__long));;
(\<acute>l1index_inverted :== CALL invert_l1index_'proc();;
(Guard ArrayBounds \<lbrace>\<acute>l1index_inverted < 8\<rbrace> (Guard ArrayBounds (if UCAST(8 \<rightarrow> 32) d < 0x10 then UNIV else {}) (\<acute>ret__long :== CALL clzl_'proc(\<acute>ksReadyQueuesL2Bitmap.[unat d].[unat \<acute>l1index_inverted])));;
(Guard SignedArithmetic \<lbrace>sint \<acute>ret__long \<le> 2147483679 \<and> - sint \<acute>ret__long \<le> 2147483616\<rbrace> (\<acute>l2index :== SCAST(32 signed \<rightarrow> 32) (0x1F - \<acute>ret__long));;
(\<acute>ret__unsigned_long :== CALL l1index_to_prio_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. ret__unsigned_long_' s || l2index_' s)))))))
 2. \<And>dom s s'. \<lbrakk>dom = UCAST(8 \<rightarrow> 32) d; (s, s') \<in> rf_sr; d \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s d \<noteq> 0 \<and> bitmapQ_no_L1_orphans s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (d \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s d = rv \<longrightarrow> d \<le> maxDomain \<and> invertL1Index (word_log2 rv) < l2BitmapSize \<and> (\<forall>rva. ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 rv)) = rva \<longrightarrow> ?P647 dom rv s rva))) \<and> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat d] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> {s. \<forall>rva. ksReadyQueuesL2Bitmap_' (globals s).[unat d].[invertL1Index (word_log2 rv)] = UCAST(32 \<rightarrow> 32) rva \<longrightarrow> s \<in> ?P'646 dom rv rva}} proof (prove)
goal (2 subgoals):
 1. \<And>l1 l2 ret__long. ccorres (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) ret__unsigned_long_' (?P652 (UCAST(8 \<rightarrow> 32) d) l1 l2) (?G'660 (UCAST(8 \<rightarrow> 32) d) l1 l2 ret__long \<inter> \<lbrace>ret__long = word_of_nat (word_clz (\<acute>ksReadyQueuesL1Bitmap.[unat d]))\<rbrace>) (SKIP # hs) (return (l1IndexToPrio (word_log2 l1) || word_of_nat (word_log2 l2))) (Guard SignedArithmetic \<lbrace>sint ret__long \<le> 2147483679 \<and> - sint ret__long \<le> 2147483616\<rbrace> (\<acute>l1index :== SCAST(32 signed \<rightarrow> 32) (0x1F - ret__long));;
(\<acute>l1index_inverted :== CALL invert_l1index_'proc(\<acute>l1index);;
(Guard ArrayBounds \<lbrace>\<acute>l1index_inverted < 8\<rbrace> (Guard ArrayBounds (if UCAST(8 \<rightarrow> 32) d < 0x10 then UNIV else {}) (\<acute>ret__long :== CALL clzl_'proc(\<acute>ksReadyQueuesL2Bitmap.[unat d].[unat \<acute>l1index_inverted])));;
(Guard SignedArithmetic \<lbrace>sint \<acute>ret__long \<le> 2147483679 \<and> - sint \<acute>ret__long \<le> 2147483616\<rbrace> (\<acute>l2index :== SCAST(32 signed \<rightarrow> 32) (0x1F - \<acute>ret__long));;
(\<acute>ret__unsigned_long :== CALL l1index_to_prio_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. ret__unsigned_long_' s || l2index_' s))))))
 2. \<And>dom s s'. \<lbrakk>dom = UCAST(8 \<rightarrow> 32) d; (s, s') \<in> rf_sr; d \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s d \<noteq> 0 \<and> bitmapQ_no_L1_orphans s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (d \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s d = rv \<longrightarrow> d \<le> maxDomain \<and> invertL1Index (word_log2 rv) < l2BitmapSize \<and> (\<forall>rva. ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 rv)) = rva \<longrightarrow> ?P652 dom rv rva s))) \<and> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat d] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> {s. \<forall>rva. ksReadyQueuesL2Bitmap_' (globals s).[unat d].[invertL1Index (word_log2 rv)] = UCAST(32 \<rightarrow> 32) rva \<longrightarrow> s \<in> {s. \<forall>v v'. v = word_of_nat (word_clz (x___unsigned_long_' (s\<lparr>x___unsigned_long_' := ksReadyQueuesL1Bitmap_' (globals s).[unat d]\<rparr>))) \<longrightarrow> s\<lparr>ret__long_' := v\<rparr> \<in> {s. s \<in> ?G'660 dom rv rva v}} \<inter> {s. x___unsigned_long_' (s\<lparr>x___unsigned_long_' := ksReadyQueuesL1Bitmap_' (globals s).[unat d]\<rparr>) \<noteq> 0} \<inter> (if dom < 0x10 then UNIV else {})}} proof (prove)
goal (2 subgoals):
 1. \<And>l1 l2 ret__long. ccorres (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) ret__unsigned_long_' (?P652 (UCAST(8 \<rightarrow> 32) d) l1 l2) (?G'784 (UCAST(8 \<rightarrow> 32) d) l1 l2 ret__long) (SKIP # hs) (return (l1IndexToPrio (word_log2 l1) || word_of_nat (word_log2 l2))) (Guard SignedArithmetic \<lbrace>sint ret__long \<le> 2147483679 \<and> - sint ret__long \<le> 2147483616\<rbrace> (\<acute>l1index :== SCAST(32 signed \<rightarrow> 32) (0x1F - ret__long));;
(\<acute>l1index_inverted :== CALL invert_l1index_'proc(\<acute>l1index);;
(Guard ArrayBounds \<lbrace>\<acute>l1index_inverted < 8\<rbrace> (Guard ArrayBounds (if UCAST(8 \<rightarrow> 32) d < 0x10 then UNIV else {}) (\<acute>ret__long :== CALL clzl_'proc(\<acute>ksReadyQueuesL2Bitmap.[unat d].[unat \<acute>l1index_inverted])));;
(Guard SignedArithmetic \<lbrace>sint \<acute>ret__long \<le> 2147483679 \<and> - sint \<acute>ret__long \<le> 2147483616\<rbrace> (\<acute>l2index :== SCAST(32 signed \<rightarrow> 32) (0x1F - \<acute>ret__long));;
(\<acute>ret__unsigned_long :== CALL l1index_to_prio_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. ret__unsigned_long_' s || l2index_' s))))))
 2. \<And>dom s s'. \<lbrakk>dom = UCAST(8 \<rightarrow> 32) d; (s, s') \<in> rf_sr; d \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s d \<noteq> 0 \<and> bitmapQ_no_L1_orphans s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (d \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s d = rv \<longrightarrow> d \<le> maxDomain \<and> invertL1Index (word_log2 rv) < l2BitmapSize \<and> (\<forall>rva. ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 rv)) = rva \<longrightarrow> ?P652 dom rv rva s))) \<and> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat d] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> {s. \<forall>rva. ksReadyQueuesL2Bitmap_' (globals s).[unat d].[invertL1Index (word_log2 rv)] = UCAST(32 \<rightarrow> 32) rva \<longrightarrow> s \<in> {s. \<forall>v v'. v = word_of_nat (word_clz (x___unsigned_long_' (s\<lparr>x___unsigned_long_' := ksReadyQueuesL1Bitmap_' (globals s).[unat d]\<rparr>))) \<longrightarrow> s\<lparr>ret__long_' := v\<rparr> \<in> {s. s \<in> {s. s \<in> \<lbrace>v = word_of_nat (word_clz (\<acute>ksReadyQueuesL1Bitmap.[unat d]))\<rbrace> \<longrightarrow> s \<in> ?G'784 dom rv rva v}}} \<inter> {s. x___unsigned_long_' (s\<lparr>x___unsigned_long_' := ksReadyQueuesL1Bitmap_' (globals s).[unat d]\<rparr>) \<noteq> 0} \<inter> (if dom < 0x10 then UNIV else {})}} proof (prove)
goal (2 subgoals):
 1. \<And>l1 l2 ret__longa l1index_inverted ret__long. l1index_inverted = word_of_nat l2BitmapSize - 1 - SCAST(32 signed \<rightarrow> 32) (0x1F - ret__longa) \<Longrightarrow> ccorres (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) ret__unsigned_long_' (?P652 (UCAST(8 \<rightarrow> 32) d) l1 l2) (?G'1082 (UCAST(8 \<rightarrow> 32) d) l1 l2 ret__longa l1index_inverted ret__long \<inter> \<lbrace>ret__long = word_of_nat (word_clz (\<acute>ksReadyQueuesL2Bitmap.[unat d].[unat l1index_inverted]))\<rbrace>) (SKIP # hs) (return (l1IndexToPrio (word_log2 l1) || word_of_nat (word_log2 l2))) (Guard SignedArithmetic \<lbrace>sint ret__long \<le> 2147483679 \<and> - sint ret__long \<le> 2147483616\<rbrace> (\<acute>l2index :== SCAST(32 signed \<rightarrow> 32) (0x1F - ret__long));;
(\<acute>ret__unsigned_long :== CALL l1index_to_prio_'proc(SCAST(32 signed \<rightarrow> 32) (0x1F - ret__longa));;
return_C ret__unsigned_long_'_update (\<lambda>s. ret__unsigned_long_' s || l2index_' s)))
 2. \<And>dom s s'. \<lbrakk>dom = UCAST(8 \<rightarrow> 32) d; (s, s') \<in> rf_sr; d \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s d \<noteq> 0 \<and> bitmapQ_no_L1_orphans s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (d \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s d = rv \<longrightarrow> d \<le> maxDomain \<and> invertL1Index (word_log2 rv) < l2BitmapSize \<and> (\<forall>rva. ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 rv)) = rva \<longrightarrow> ?P652 dom rv rva s))) \<and> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat d] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> {s. \<forall>rva. ksReadyQueuesL2Bitmap_' (globals s).[unat d].[invertL1Index (word_log2 rv)] = UCAST(32 \<rightarrow> 32) rva \<longrightarrow> s \<in> {s. \<forall>v v'. v = word_of_nat (word_clz (x___unsigned_long_' (s\<lparr>x___unsigned_long_' := ksReadyQueuesL1Bitmap_' (globals s).[unat d]\<rparr>))) \<longrightarrow> s\<lparr>ret__long_' := v\<rparr> \<in> {s. s \<in> {s. s \<in> \<lbrace>v = word_of_nat (word_clz (\<acute>ksReadyQueuesL1Bitmap.[unat d]))\<rbrace> \<longrightarrow> s \<in> {s. l1index_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) (0x1F - v)) s \<in> {s. \<forall>va. va = word_of_nat l2BitmapSize - 1 - l1index_' (l1index_'_update (\<lambda>x. SCAST(32 signed \<rightarrow> 32) (0x1F - v)) s) \<longrightarrow> l1index_inverted_'_update (\<lambda>_. va) s \<in> {s. \<forall>vb v'. vb = word_of_nat (word_clz (x___unsigned_long_' (s\<lparr>x___unsigned_long_' := ksReadyQueuesL2Bitmap_' (globals s).[unat d].[unat va]\<rparr>))) \<longrightarrow> s\<lparr>ret__long_' := vb\<rparr> \<in> {s. s \<in> ?G'1082 dom rv rva v va vb}} \<inter> {s. x___unsigned_long_' (s\<lparr>x___unsigned_long_' := ksReadyQueuesL2Bitmap_' (globals s).[unat d].[unat va]\<rparr>) \<noteq> 0} \<inter> (if dom < 0x10 then UNIV else {}) \<inter> \<lbrace>va < 8\<rbrace>}} \<inter> \<lbrace>sint v \<le> 2147483679 \<and> - sint v \<le> 2147483616\<rbrace>}}} \<inter> {s. x___unsigned_long_' (s\<lparr>x___unsigned_long_' := ksReadyQueuesL1Bitmap_' (globals s).[unat d]\<rparr>) \<noteq> 0} \<inter> (if dom < 0x10 then UNIV else {})}} proof (prove)
goal (2 subgoals):
 1. \<And>l1 l2 ret__longa l1index_inverted ret__long. l1index_inverted = word_of_nat l2BitmapSize - 1 - SCAST(32 signed \<rightarrow> 32) (0x1F - ret__longa) \<Longrightarrow> ccorres (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) ret__unsigned_long_' (?P652 (UCAST(8 \<rightarrow> 32) d) l1 l2) (?G'1166 (UCAST(8 \<rightarrow> 32) d) l1 l2 ret__longa l1index_inverted ret__long) (SKIP # hs) (return (l1IndexToPrio (word_log2 l1) || word_of_nat (word_log2 l2))) (Guard SignedArithmetic \<lbrace>sint ret__long \<le> 2147483679 \<and> - sint ret__long \<le> 2147483616\<rbrace> (\<acute>l2index :== SCAST(32 signed \<rightarrow> 32) (0x1F - ret__long));;
(\<acute>ret__unsigned_long :== CALL l1index_to_prio_'proc(SCAST(32 signed \<rightarrow> 32) (0x1F - ret__longa));;
return_C ret__unsigned_long_'_update (\<lambda>s. ret__unsigned_long_' s || l2index_' s)))
 2. \<And>dom s s'. \<lbrakk>dom = UCAST(8 \<rightarrow> 32) d; (s, s') \<in> rf_sr; d \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s d \<noteq> 0 \<and> bitmapQ_no_L1_orphans s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (d \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s d = rv \<longrightarrow> d \<le> maxDomain \<and> invertL1Index (word_log2 rv) < l2BitmapSize \<and> (\<forall>rva. ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 rv)) = rva \<longrightarrow> ?P652 dom rv rva s))) \<and> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat d] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> {s. \<forall>rva. ksReadyQueuesL2Bitmap_' (globals s).[unat d].[invertL1Index (word_log2 rv)] = UCAST(32 \<rightarrow> 32) rva \<longrightarrow> s \<in> {s. \<forall>v v'. v = word_of_nat (word_clz (x___unsigned_long_' (s\<lparr>x___unsigned_long_' := ksReadyQueuesL1Bitmap_' (globals s).[unat d]\<rparr>))) \<longrightarrow> s\<lparr>ret__long_' := v\<rparr> \<in> {s. s \<in> {s. s \<in> \<lbrace>v = word_of_nat (word_clz (\<acute>ksReadyQueuesL1Bitmap.[unat d]))\<rbrace> \<longrightarrow> s \<in> {s. l1index_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) (0x1F - v)) s \<in> {s. \<forall>va. va = word_of_nat l2BitmapSize - 1 - l1index_' (l1index_'_update (\<lambda>x. SCAST(32 signed \<rightarrow> 32) (0x1F - v)) s) \<longrightarrow> l1index_inverted_'_update (\<lambda>_. va) s \<in> {s. \<forall>vb v'. vb = word_of_nat (word_clz (x___unsigned_long_' (s\<lparr>x___unsigned_long_' := ksReadyQueuesL2Bitmap_' (globals s).[unat d].[unat va]\<rparr>))) \<longrightarrow> s\<lparr>ret__long_' := vb\<rparr> \<in> {s. s \<in> {s. s \<in> \<lbrace>vb = word_of_nat (word_clz (\<acute>ksReadyQueuesL2Bitmap.[unat d].[unat va]))\<rbrace> \<longrightarrow> s \<in> ?G'1166 dom rv rva v va vb}}} \<inter> {s. x___unsigned_long_' (s\<lparr>x___unsigned_long_' := ksReadyQueuesL2Bitmap_' (globals s).[unat d].[unat va]\<rparr>) \<noteq> 0} \<inter> (if dom < 0x10 then UNIV else {}) \<inter> \<lbrace>va < 8\<rbrace>}} \<inter> \<lbrace>sint v \<le> 2147483679 \<and> - sint v \<le> 2147483616\<rbrace>}}} \<inter> {s. x___unsigned_long_' (s\<lparr>x___unsigned_long_' := ksReadyQueuesL1Bitmap_' (globals s).[unat d]\<rparr>) \<noteq> 0} \<inter> (if dom < 0x10 then UNIV else {})}} proof (prove)
goal (2 subgoals):
 1. \<And>l1 l2 ret__longa l1index_inverted ret__long ret__unsigned_long. \<lbrakk>l1index_inverted = word_of_nat l2BitmapSize - 1 - SCAST(32 signed \<rightarrow> 32) (0x1F - ret__longa); ret__unsigned_long = SCAST(32 signed \<rightarrow> 32) (0x1F - ret__longa) << wordRadix\<rbrakk> \<Longrightarrow> ccorres (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) ret__unsigned_long_' (?P652 (UCAST(8 \<rightarrow> 32) d) l1 l2) (?G'1241 (UCAST(8 \<rightarrow> 32) d) l1 l2 ret__longa l1index_inverted ret__long ret__unsigned_long) (SKIP # hs) (return (l1IndexToPrio (word_log2 l1) || word_of_nat (word_log2 l2))) (return_C ret__unsigned_long_'_update (\<lambda>s. ret__unsigned_long || SCAST(32 signed \<rightarrow> 32) (0x1F - ret__long)))
 2. \<And>dom s s'. \<lbrakk>dom = UCAST(8 \<rightarrow> 32) d; (s, s') \<in> rf_sr; d \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s d \<noteq> 0 \<and> bitmapQ_no_L1_orphans s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (d \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s d = rv \<longrightarrow> d \<le> maxDomain \<and> invertL1Index (word_log2 rv) < l2BitmapSize \<and> (\<forall>rva. ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 rv)) = rva \<longrightarrow> ?P652 dom rv rva s))) \<and> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat d] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> {s. \<forall>rva. ksReadyQueuesL2Bitmap_' (globals s).[unat d].[invertL1Index (word_log2 rv)] = UCAST(32 \<rightarrow> 32) rva \<longrightarrow> s \<in> {s. \<forall>v v'. v = word_of_nat (word_clz (x___unsigned_long_' (s\<lparr>x___unsigned_long_' := ksReadyQueuesL1Bitmap_' (globals s).[unat d]\<rparr>))) \<longrightarrow> s\<lparr>ret__long_' := v\<rparr> \<in> {s. s \<in> {s. s \<in> \<lbrace>v = word_of_nat (word_clz (\<acute>ksReadyQueuesL1Bitmap.[unat d]))\<rbrace> \<longrightarrow> s \<in> {s. l1index_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) (0x1F - v)) s \<in> {s. \<forall>va. va = word_of_nat l2BitmapSize - 1 - l1index_' (l1index_'_update (\<lambda>x. SCAST(32 signed \<rightarrow> 32) (0x1F - v)) s) \<longrightarrow> l1index_inverted_'_update (\<lambda>_. va) s \<in> {s. \<forall>vb v'. vb = word_of_nat (word_clz (x___unsigned_long_' (s\<lparr>x___unsigned_long_' := ksReadyQueuesL2Bitmap_' (globals s).[unat d].[unat va]\<rparr>))) \<longrightarrow> s\<lparr>ret__long_' := vb\<rparr> \<in> {s. s \<in> {s. s \<in> \<lbrace>vb = word_of_nat (word_clz (\<acute>ksReadyQueuesL2Bitmap.[unat d].[unat va]))\<rbrace> \<longrightarrow> s \<in> {s. l2index_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) (0x1F - vb)) s \<in> {s. \<forall>vc. vc = l1index_' (l1index_'_update (\<lambda>x. SCAST(32 signed \<rightarrow> 32) (0x1F - v)) s) << wordRadix \<longrightarrow> s\<lparr>ret__unsigned_long_' := vc\<rparr> \<in> ?G'1241 dom rv rva v va vb vc}} \<inter> \<lbrace>sint vb \<le> 2147483679 \<and> - sint vb \<le> 2147483616\<rbrace>}}} \<inter> {s. x___unsigned_long_' (s\<lparr>x___unsigned_long_' := ksReadyQueuesL2Bitmap_' (globals s).[unat d].[unat va]\<rparr>) \<noteq> 0} \<inter> (if dom < 0x10 then UNIV else {}) \<inter> \<lbrace>va < 8\<rbrace>}} \<inter> \<lbrace>sint v \<le> 2147483679 \<and> - sint v \<le> 2147483616\<rbrace>}}} \<inter> {s. x___unsigned_long_' (s\<lparr>x___unsigned_long_' := ksReadyQueuesL1Bitmap_' (globals s).[unat d]\<rparr>) \<noteq> 0} \<inter> (if dom < 0x10 then UNIV else {})}} proof (prove)
goal (2 subgoals):
 1. \<And>l1 l2 ret__longa ret__long. ccorres (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) ret__unsigned_long_' (?P652 (UCAST(8 \<rightarrow> 32) d) l1 l2) (?G'1241 (UCAST(8 \<rightarrow> 32) d) l1 l2 ret__longa (word_of_nat l2BitmapSize - 1 - SCAST(32 signed \<rightarrow> 32) (0x1F - ret__longa)) ret__long (SCAST(32 signed \<rightarrow> 32) (0x1F - ret__longa) << wordRadix)) (SKIP # hs) (return (l1IndexToPrio (31 - word_clz l1) || word_of_nat (31 - word_clz l2))) (return_C ret__unsigned_long_'_update (\<lambda>s. (SCAST(32 signed \<rightarrow> 32) (0x1F - ret__longa) << wordRadix) || SCAST(32 signed \<rightarrow> 32) (0x1F - ret__long)))
 2. \<And>dom s s'. \<lbrakk>dom = UCAST(8 \<rightarrow> 32) d; (s, s') \<in> rf_sr; d \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s d \<noteq> 0 \<and> bitmapQ_no_L1_orphans s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (d \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s d = rv \<longrightarrow> d \<le> maxDomain \<and> invertL1Index (word_log2 rv) < l2BitmapSize \<and> (\<forall>rva. ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 rv)) = rva \<longrightarrow> ?P652 dom rv rva s))) \<and> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat d] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> {s. \<forall>rva. ksReadyQueuesL2Bitmap_' (globals s).[unat d].[invertL1Index (word_log2 rv)] = UCAST(32 \<rightarrow> 32) rva \<longrightarrow> s \<in> {s. \<forall>v v'. v = word_of_nat (word_clz (x___unsigned_long_' (s\<lparr>x___unsigned_long_' := ksReadyQueuesL1Bitmap_' (globals s).[unat d]\<rparr>))) \<longrightarrow> s\<lparr>ret__long_' := v\<rparr> \<in> {s. s \<in> {s. s \<in> \<lbrace>v = word_of_nat (word_clz (\<acute>ksReadyQueuesL1Bitmap.[unat d]))\<rbrace> \<longrightarrow> s \<in> {s. l1index_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) (0x1F - v)) s \<in> {s. \<forall>va. va = word_of_nat l2BitmapSize - 1 - l1index_' (l1index_'_update (\<lambda>x. SCAST(32 signed \<rightarrow> 32) (0x1F - v)) s) \<longrightarrow> l1index_inverted_'_update (\<lambda>_. va) s \<in> {s. \<forall>vb v'. vb = word_of_nat (word_clz (x___unsigned_long_' (s\<lparr>x___unsigned_long_' := ksReadyQueuesL2Bitmap_' (globals s).[unat d].[unat va]\<rparr>))) \<longrightarrow> s\<lparr>ret__long_' := vb\<rparr> \<in> {s. s \<in> {s. s \<in> \<lbrace>vb = word_of_nat (word_clz (\<acute>ksReadyQueuesL2Bitmap.[unat d].[unat va]))\<rbrace> \<longrightarrow> s \<in> {s. l2index_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) (0x1F - vb)) s \<in> {s. \<forall>vc. vc = l1index_' (l1index_'_update (\<lambda>x. SCAST(32 signed \<rightarrow> 32) (0x1F - v)) s) << wordRadix \<longrightarrow> s\<lparr>ret__unsigned_long_' := vc\<rparr> \<in> ?G'1241 dom rv rva v va vb vc}} \<inter> \<lbrace>sint vb \<le> 2147483679 \<and> - sint vb \<le> 2147483616\<rbrace>}}} \<inter> {s. x___unsigned_long_' (s\<lparr>x___unsigned_long_' := ksReadyQueuesL2Bitmap_' (globals s).[unat d].[unat va]\<rparr>) \<noteq> 0} \<inter> (if dom < 0x10 then UNIV else {}) \<inter> \<lbrace>va < 8\<rbrace>}} \<inter> \<lbrace>sint v \<le> 2147483679 \<and> - sint v \<le> 2147483616\<rbrace>}}} \<inter> {s. x___unsigned_long_' (s\<lparr>x___unsigned_long_' := ksReadyQueuesL1Bitmap_' (globals s).[unat d]\<rparr>) \<noteq> 0} \<inter> (if dom < 0x10 then UNIV else {})}} proof (prove)
goal (2 subgoals):
 1. \<And>l1 l2 clz_l1index clz_l2index. ccorres (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) ret__unsigned_long_' (?P652 (UCAST(8 \<rightarrow> 32) d) l1 l2) (?G'1241 (UCAST(8 \<rightarrow> 32) d) l1 l2 clz_l1index (word_of_nat l2BitmapSize - 1 - SCAST(32 signed \<rightarrow> 32) (0x1F - clz_l1index)) clz_l2index (SCAST(32 signed \<rightarrow> 32) (0x1F - clz_l1index) << wordRadix)) (SKIP # hs) (return (l1IndexToPrio (31 - word_clz l1) || word_of_nat (31 - word_clz l2))) (return_C ret__unsigned_long_'_update (\<lambda>s. (SCAST(32 signed \<rightarrow> 32) (0x1F - clz_l1index) << wordRadix) || SCAST(32 signed \<rightarrow> 32) (0x1F - clz_l2index)))
 2. \<And>dom s s'. \<lbrakk>dom = UCAST(8 \<rightarrow> 32) d; (s, s') \<in> rf_sr; d \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s d \<noteq> 0 \<and> bitmapQ_no_L1_orphans s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (d \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s d = rv \<longrightarrow> d \<le> maxDomain \<and> invertL1Index (word_log2 rv) < l2BitmapSize \<and> (\<forall>rva. ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 rv)) = rva \<longrightarrow> ?P652 dom rv rva s))) \<and> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat d] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> {s. \<forall>rva. ksReadyQueuesL2Bitmap_' (globals s).[unat d].[invertL1Index (word_log2 rv)] = UCAST(32 \<rightarrow> 32) rva \<longrightarrow> s \<in> {s. \<forall>v v'. v = word_of_nat (word_clz (x___unsigned_long_' (s\<lparr>x___unsigned_long_' := ksReadyQueuesL1Bitmap_' (globals s).[unat d]\<rparr>))) \<longrightarrow> s\<lparr>ret__long_' := v\<rparr> \<in> {s. s \<in> {s. s \<in> \<lbrace>v = word_of_nat (word_clz (\<acute>ksReadyQueuesL1Bitmap.[unat d]))\<rbrace> \<longrightarrow> s \<in> {s. l1index_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) (0x1F - v)) s \<in> {s. \<forall>va. va = word_of_nat l2BitmapSize - 1 - l1index_' (l1index_'_update (\<lambda>x. SCAST(32 signed \<rightarrow> 32) (0x1F - v)) s) \<longrightarrow> l1index_inverted_'_update (\<lambda>_. va) s \<in> {s. \<forall>vb v'. vb = word_of_nat (word_clz (x___unsigned_long_' (s\<lparr>x___unsigned_long_' := ksReadyQueuesL2Bitmap_' (globals s).[unat d].[unat va]\<rparr>))) \<longrightarrow> s\<lparr>ret__long_' := vb\<rparr> \<in> {s. s \<in> {s. s \<in> \<lbrace>vb = word_of_nat (word_clz (\<acute>ksReadyQueuesL2Bitmap.[unat d].[unat va]))\<rbrace> \<longrightarrow> s \<in> {s. l2index_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) (0x1F - vb)) s \<in> {s. \<forall>vc. vc = l1index_' (l1index_'_update (\<lambda>x. SCAST(32 signed \<rightarrow> 32) (0x1F - v)) s) << wordRadix \<longrightarrow> s\<lparr>ret__unsigned_long_' := vc\<rparr> \<in> ?G'1241 dom rv rva v va vb vc}} \<inter> \<lbrace>sint vb \<le> 2147483679 \<and> - sint vb \<le> 2147483616\<rbrace>}}} \<inter> {s. x___unsigned_long_' (s\<lparr>x___unsigned_long_' := ksReadyQueuesL2Bitmap_' (globals s).[unat d].[unat va]\<rparr>) \<noteq> 0} \<inter> (if dom < 0x10 then UNIV else {}) \<inter> \<lbrace>va < 8\<rbrace>}} \<inter> \<lbrace>sint v \<le> 2147483679 \<and> - sint v \<le> 2147483616\<rbrace>}}} \<inter> {s. x___unsigned_long_' (s\<lparr>x___unsigned_long_' := ksReadyQueuesL1Bitmap_' (globals s).[unat d]\<rparr>) \<noteq> 0} \<inter> (if dom < 0x10 then UNIV else {})}} proof (prove)
goal (2 subgoals):
 1. \<And>l1 l2 clz_l1index clz_l2index. \<forall>\<sigma>. \<Gamma>\<turnstile> {s. (l1 \<noteq> 0 \<and> l2 \<noteq> 0 \<and> word_log2 l1 < l2BitmapSize) \<and> s \<in> \<lbrace>clz_l1index = word_of_nat (word_clz l1) \<and> clz_l2index = word_of_nat (word_clz l2)\<rbrace> \<and> (\<sigma>, s) \<in> rf_sr} return_C ret__unsigned_long_'_update (\<lambda>s. (SCAST(32 signed \<rightarrow> 32) (0x1F - clz_l1index) << wordRadix) || SCAST(32 signed \<rightarrow> 32) (0x1F - clz_l2index)) {},{s. \<exists>(rv, \<sigma>')\<in>fst (return (l1IndexToPrio (31 - word_clz l1) || word_of_nat (31 - word_clz l2)) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> ret__unsigned_long_' s = UCAST(8 \<rightarrow> 32) rv}
 2. \<And>dom s s'. \<lbrakk>dom = UCAST(8 \<rightarrow> 32) d; (s, s') \<in> rf_sr; d \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s d \<noteq> 0 \<and> bitmapQ_no_L1_orphans s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (d \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s d = rv \<longrightarrow> d \<le> maxDomain \<and> invertL1Index (word_log2 rv) < l2BitmapSize \<and> (\<forall>rva. ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 rv)) = rva \<longrightarrow> rv \<noteq> 0 \<and> rva \<noteq> 0 \<and> word_log2 rv < l2BitmapSize))) \<and> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat d] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> {s. \<forall>rva. ksReadyQueuesL2Bitmap_' (globals s).[unat d].[invertL1Index (word_log2 rv)] = UCAST(32 \<rightarrow> 32) rva \<longrightarrow> s \<in> {s. \<forall>v v'. v = word_of_nat (word_clz (x___unsigned_long_' (s\<lparr>x___unsigned_long_' := ksReadyQueuesL1Bitmap_' (globals s).[unat d]\<rparr>))) \<longrightarrow> s\<lparr>ret__long_' := v\<rparr> \<in> {s. s \<in> {s. s \<in> \<lbrace>v = word_of_nat (word_clz (\<acute>ksReadyQueuesL1Bitmap.[unat d]))\<rbrace> \<longrightarrow> s \<in> {s. l1index_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) (0x1F - v)) s \<in> {s. \<forall>va. va = word_of_nat l2BitmapSize - 1 - l1index_' (l1index_'_update (\<lambda>x. SCAST(32 signed \<rightarrow> 32) (0x1F - v)) s) \<longrightarrow> l1index_inverted_'_update (\<lambda>_. va) s \<in> {s. \<forall>vb v'. vb = word_of_nat (word_clz (x___unsigned_long_' (s\<lparr>x___unsigned_long_' := ksReadyQueuesL2Bitmap_' (globals s).[unat d].[unat va]\<rparr>))) \<longrightarrow> s\<lparr>ret__long_' := vb\<rparr> \<in> {s. s \<in> {s. s \<in> \<lbrace>vb = word_of_nat (word_clz (\<acute>ksReadyQueuesL2Bitmap.[unat d].[unat va]))\<rbrace> \<longrightarrow> s \<in> {s. l2index_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) (0x1F - vb)) s \<in> {s. \<forall>va. va = l1index_' (l1index_'_update (\<lambda>x. SCAST(32 signed \<rightarrow> 32) (0x1F - v)) s) << wordRadix \<longrightarrow> s\<lparr>ret__unsigned_long_' := va\<rparr> \<in> \<lbrace>v = word_of_nat (word_clz rv) \<and> vb = word_of_nat (word_clz rva)\<rbrace>}} \<inter> \<lbrace>sint vb \<le> 2147483679 \<and> - sint vb \<le> 2147483616\<rbrace>}}} \<inter> {s. x___unsigned_long_' (s\<lparr>x___unsigned_long_' := ksReadyQueuesL2Bitmap_' (globals s).[unat d].[unat va]\<rparr>) \<noteq> 0} \<inter> (if dom < 0x10 then UNIV else {}) \<inter> \<lbrace>va < 8\<rbrace>}} \<inter> \<lbrace>sint v \<le> 2147483679 \<and> - sint v \<le> 2147483616\<rbrace>}}} \<inter> {s. x___unsigned_long_' (s\<lparr>x___unsigned_long_' := ksReadyQueuesL1Bitmap_' (globals s).[unat d]\<rparr>) \<noteq> 0} \<inter> (if dom < 0x10 then UNIV else {})}} proof (prove)
goal (2 subgoals):
 1. \<And>l1 l2 clz_l1index clz_l2index \<sigma>. {s. (l1 \<noteq> 0 \<and> l2 \<noteq> 0 \<and> word_log2 l1 < l2BitmapSize) \<and> s \<in> \<lbrace>clz_l1index = word_of_nat (word_clz l1) \<and> clz_l2index = word_of_nat (word_clz l2)\<rbrace> \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst (return (l1IndexToPrio (31 - word_clz l1) || word_of_nat (31 - word_clz l2)) \<sigma>). (\<sigma>', s\<lparr>ret__unsigned_long_' := (SCAST(32 signed \<rightarrow> 32) (0x1F - clz_l1index) << wordRadix) || SCAST(32 signed \<rightarrow> 32) (0x1F - clz_l2index), global_exn_var_' := Return\<rparr>) \<in> rf_sr \<and> (SCAST(32 signed \<rightarrow> 32) (0x1F - clz_l1index) << wordRadix) || SCAST(32 signed \<rightarrow> 32) (0x1F - clz_l2index) = UCAST(8 \<rightarrow> 32) rv}
 2. \<And>dom s s'. \<lbrakk>dom = UCAST(8 \<rightarrow> 32) d; (s, s') \<in> rf_sr; d \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s d \<noteq> 0 \<and> bitmapQ_no_L1_orphans s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (d \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s d = rv \<longrightarrow> d \<le> maxDomain \<and> invertL1Index (word_log2 rv) < l2BitmapSize \<and> (\<forall>rva. ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 rv)) = rva \<longrightarrow> rv \<noteq> 0 \<and> rva \<noteq> 0 \<and> word_log2 rv < l2BitmapSize))) \<and> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat d] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> {s. \<forall>rva. ksReadyQueuesL2Bitmap_' (globals s).[unat d].[invertL1Index (word_log2 rv)] = UCAST(32 \<rightarrow> 32) rva \<longrightarrow> s \<in> {s. \<forall>v v'. v = word_of_nat (word_clz (x___unsigned_long_' (s\<lparr>x___unsigned_long_' := ksReadyQueuesL1Bitmap_' (globals s).[unat d]\<rparr>))) \<longrightarrow> s\<lparr>ret__long_' := v\<rparr> \<in> {s. s \<in> {s. s \<in> \<lbrace>v = word_of_nat (word_clz (\<acute>ksReadyQueuesL1Bitmap.[unat d]))\<rbrace> \<longrightarrow> s \<in> {s. l1index_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) (0x1F - v)) s \<in> {s. \<forall>va. va = word_of_nat l2BitmapSize - 1 - l1index_' (l1index_'_update (\<lambda>x. SCAST(32 signed \<rightarrow> 32) (0x1F - v)) s) \<longrightarrow> l1index_inverted_'_update (\<lambda>_. va) s \<in> {s. \<forall>vb v'. vb = word_of_nat (word_clz (x___unsigned_long_' (s\<lparr>x___unsigned_long_' := ksReadyQueuesL2Bitmap_' (globals s).[unat d].[unat va]\<rparr>))) \<longrightarrow> s\<lparr>ret__long_' := vb\<rparr> \<in> {s. s \<in> {s. s \<in> \<lbrace>vb = word_of_nat (word_clz (\<acute>ksReadyQueuesL2Bitmap.[unat d].[unat va]))\<rbrace> \<longrightarrow> s \<in> {s. l2index_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) (0x1F - vb)) s \<in> {s. \<forall>va. va = l1index_' (l1index_'_update (\<lambda>x. SCAST(32 signed \<rightarrow> 32) (0x1F - v)) s) << wordRadix \<longrightarrow> s\<lparr>ret__unsigned_long_' := va\<rparr> \<in> \<lbrace>v = word_of_nat (word_clz rv) \<and> vb = word_of_nat (word_clz rva)\<rbrace>}} \<inter> \<lbrace>sint vb \<le> 2147483679 \<and> - sint vb \<le> 2147483616\<rbrace>}}} \<inter> {s. x___unsigned_long_' (s\<lparr>x___unsigned_long_' := ksReadyQueuesL2Bitmap_' (globals s).[unat d].[unat va]\<rparr>) \<noteq> 0} \<inter> (if dom < 0x10 then UNIV else {}) \<inter> \<lbrace>va < 8\<rbrace>}} \<inter> \<lbrace>sint v \<le> 2147483679 \<and> - sint v \<le> 2147483616\<rbrace>}}} \<inter> {s. x___unsigned_long_' (s\<lparr>x___unsigned_long_' := ksReadyQueuesL1Bitmap_' (globals s).[unat d]\<rparr>) \<noteq> 0} \<inter> (if dom < 0x10 then UNIV else {})}} proof (prove)
goal (1 subgoal):
 1. {s. (l1_ \<noteq> 0 \<and> l2_ \<noteq> 0 \<and> word_log2 l1_ < l2BitmapSize) \<and> s \<in> \<lbrace>clz_l1index_ = word_of_nat (word_clz l1_) \<and> clz_l2index_ = word_of_nat (word_clz l2_)\<rbrace> \<and> (\<sigma>_, s) \<in> rf_sr} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst (return (l1IndexToPrio (31 - word_clz l1_) || word_of_nat (31 - word_clz l2_)) \<sigma>_). (\<sigma>', s\<lparr>ret__unsigned_long_' := (SCAST(32 signed \<rightarrow> 32) (0x1F - clz_l1index_) << wordRadix) || SCAST(32 signed \<rightarrow> 32) (0x1F - clz_l2index_), global_exn_var_' := Return\<rparr>) \<in> rf_sr \<and> (SCAST(32 signed \<rightarrow> 32) (0x1F - clz_l1index_) << wordRadix) || SCAST(32 signed \<rightarrow> 32) (0x1F - clz_l2index_) = UCAST(8 \<rightarrow> 32) rv} proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>l1_ \<noteq> 0; l2_ \<noteq> 0; word_log2 l1_ < l2BitmapSize; clz_l1index_ = word_of_nat (word_clz l1_); (\<sigma>_, x) \<in> rf_sr; clz_l2index_ = word_of_nat (word_clz l2_)\<rbrakk> \<Longrightarrow> (SCAST(32 signed \<rightarrow> 32) (0x1F - word_of_nat (word_clz l1_)) << wordRadix) || SCAST(32 signed \<rightarrow> 32) (0x1F - word_of_nat (word_clz l2_)) = UCAST(8 \<rightarrow> 32) ((word_of_nat (31 - word_clz l1_) << wordRadix) || word_of_nat (31 - word_clz l2_)) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>l1_ \<noteq> 0; l2_ \<noteq> 0; word_log2 l1_ < l2BitmapSize; clz_l1index_ = word_of_nat (word_clz l1_); (\<sigma>_, x) \<in> rf_sr; clz_l2index_ = word_of_nat (word_clz l2_)\<rbrakk> \<Longrightarrow> (word_of_nat (word_log2 l1_) << wordRadix) || word_of_nat (word_log2 l2_) = UCAST(8 \<rightarrow> 32) (word_of_nat (word_log2 l1_) << wordRadix) || UCAST(8 \<rightarrow> 32) (word_of_nat (word_log2 l2_)) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>l1_ \<noteq> 0; l2_ \<noteq> 0; word_log2 l1_ < l2BitmapSize; clz_l1index_ = word_of_nat (word_clz l1_); (\<sigma>_, x) \<in> rf_sr; clz_l2index_ = word_of_nat (word_clz l2_)\<rbrakk> \<Longrightarrow> word_of_nat (word_log2 l1_) << wordRadix = UCAST(8 \<rightarrow> 32) (word_of_nat (word_log2 l1_) << wordRadix)
 2. \<And>x. \<lbrakk>l1_ \<noteq> 0; l2_ \<noteq> 0; word_log2 l1_ < l2BitmapSize; clz_l1index_ = word_of_nat (word_clz l1_); (\<sigma>_, x) \<in> rf_sr; clz_l2index_ = word_of_nat (word_clz l2_)\<rbrakk> \<Longrightarrow> word_of_nat (word_log2 l2_) = UCAST(8 \<rightarrow> 32) (word_of_nat (word_log2 l2_)) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>l1_ \<noteq> 0; l2_ \<noteq> 0; word_log2 l1_ < l2BitmapSize; clz_l1index_ = word_of_nat (word_clz l1_); (\<sigma>_, x) \<in> rf_sr; clz_l2index_ = word_of_nat (word_clz l2_)\<rbrakk> \<Longrightarrow> word_of_nat (word_log2 l1_ * 2 ^ wordRadix) = UCAST(8 \<rightarrow> 32) (word_of_nat (word_log2 l1_ * 2 ^ wordRadix))
 2. \<And>x. \<lbrakk>l1_ \<noteq> 0; l2_ \<noteq> 0; word_log2 l1_ < l2BitmapSize; clz_l1index_ = word_of_nat (word_clz l1_); (\<sigma>_, x) \<in> rf_sr; clz_l2index_ = word_of_nat (word_clz l2_)\<rbrakk> \<Longrightarrow> word_of_nat (word_log2 l2_) = UCAST(8 \<rightarrow> 32) (word_of_nat (word_log2 l2_)) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>l1_ \<noteq> 0; l2_ \<noteq> 0; word_log2 l1_ < l2BitmapSize; clz_l1index_ = word_of_nat (word_clz l1_); (\<sigma>_, x) \<in> rf_sr; clz_l2index_ = word_of_nat (word_clz l2_)\<rbrakk> \<Longrightarrow> word_of_nat (word_log2 l1_ * 2 ^ wordRadix) = word_of_nat (word_log2 l1_ * 2 ^ wordRadix)
 2. \<And>x. \<lbrakk>l1_ \<noteq> 0; l2_ \<noteq> 0; word_log2 l1_ < l2BitmapSize; clz_l1index_ = word_of_nat (word_clz l1_); (\<sigma>_, x) \<in> rf_sr; clz_l2index_ = word_of_nat (word_clz l2_)\<rbrakk> \<Longrightarrow> word_of_nat (word_log2 l2_) = UCAST(8 \<rightarrow> 32) (word_of_nat (word_log2 l2_)) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>l1_ \<noteq> 0; l2_ \<noteq> 0; word_log2 l1_ < l2BitmapSize; clz_l1index_ = word_of_nat (word_clz l1_); (\<sigma>_, x) \<in> rf_sr; clz_l2index_ = word_of_nat (word_clz l2_)\<rbrakk> \<Longrightarrow> word_of_nat (word_log2 l2_) = UCAST(8 \<rightarrow> 32) (word_of_nat (word_log2 l2_)) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>l1_ \<noteq> 0; l2_ \<noteq> 0; word_log2 l1_ < l2BitmapSize; clz_l1index_ = word_of_nat (word_clz l1_); (\<sigma>_, x) \<in> rf_sr; clz_l2index_ = word_of_nat (word_clz l2_)\<rbrakk> \<Longrightarrow> word_log2 l2_ < 256
 2. \<And>x. \<lbrakk>l1_ \<noteq> 0; l2_ \<noteq> 0; word_log2 l1_ < l2BitmapSize; clz_l1index_ = word_of_nat (word_clz l1_); (\<sigma>_, x) \<in> rf_sr; clz_l2index_ = word_of_nat (word_clz l2_)\<rbrakk> \<Longrightarrow> word_of_nat (word_log2 l2_) = word_of_nat (word_log2 l2_) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>l1_ \<noteq> 0; l2_ \<noteq> 0; word_log2 l1_ < l2BitmapSize; clz_l1index_ = word_of_nat (word_clz l1_); (\<sigma>_, x) \<in> rf_sr; clz_l2index_ = word_of_nat (word_clz l2_)\<rbrakk> \<Longrightarrow> word_of_nat (word_log2 l2_) = word_of_nat (word_log2 l2_) proof (prove)
goal:
No subgoals! proof (prove)
goal (1 subgoal):
 1. \<And>dom s s'. \<lbrakk>dom = UCAST(8 \<rightarrow> 32) d; (s, s') \<in> rf_sr; d \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s d \<noteq> 0 \<and> bitmapQ_no_L1_orphans s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (d \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s d = rv \<longrightarrow> d \<le> maxDomain \<and> invertL1Index (word_log2 rv) < l2BitmapSize \<and> (\<forall>rva. ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 rv)) = rva \<longrightarrow> rv \<noteq> 0 \<and> rva \<noteq> 0 \<and> word_log2 rv < l2BitmapSize))) \<and> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat d] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> {s. \<forall>rva. ksReadyQueuesL2Bitmap_' (globals s).[unat d].[invertL1Index (word_log2 rv)] = UCAST(32 \<rightarrow> 32) rva \<longrightarrow> s \<in> {s. \<forall>v v'. v = word_of_nat (word_clz (x___unsigned_long_' (s\<lparr>x___unsigned_long_' := ksReadyQueuesL1Bitmap_' (globals s).[unat d]\<rparr>))) \<longrightarrow> s\<lparr>ret__long_' := v\<rparr> \<in> {s. s \<in> {s. s \<in> \<lbrace>v = word_of_nat (word_clz (\<acute>ksReadyQueuesL1Bitmap.[unat d]))\<rbrace> \<longrightarrow> s \<in> {s. l1index_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) (0x1F - v)) s \<in> {s. \<forall>va. va = word_of_nat l2BitmapSize - 1 - l1index_' (l1index_'_update (\<lambda>x. SCAST(32 signed \<rightarrow> 32) (0x1F - v)) s) \<longrightarrow> l1index_inverted_'_update (\<lambda>_. va) s \<in> {s. \<forall>vb v'. vb = word_of_nat (word_clz (x___unsigned_long_' (s\<lparr>x___unsigned_long_' := ksReadyQueuesL2Bitmap_' (globals s).[unat d].[unat va]\<rparr>))) \<longrightarrow> s\<lparr>ret__long_' := vb\<rparr> \<in> {s. s \<in> {s. s \<in> \<lbrace>vb = word_of_nat (word_clz (\<acute>ksReadyQueuesL2Bitmap.[unat d].[unat va]))\<rbrace> \<longrightarrow> s \<in> {s. l2index_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) (0x1F - vb)) s \<in> {s. \<forall>va. va = l1index_' (l1index_'_update (\<lambda>x. SCAST(32 signed \<rightarrow> 32) (0x1F - v)) s) << wordRadix \<longrightarrow> s\<lparr>ret__unsigned_long_' := va\<rparr> \<in> \<lbrace>v = word_of_nat (word_clz rv) \<and> vb = word_of_nat (word_clz rva)\<rbrace>}} \<inter> \<lbrace>sint vb \<le> 2147483679 \<and> - sint vb \<le> 2147483616\<rbrace>}}} \<inter> {s. x___unsigned_long_' (s\<lparr>x___unsigned_long_' := ksReadyQueuesL2Bitmap_' (globals s).[unat d].[unat va]\<rparr>) \<noteq> 0} \<inter> (if dom < 0x10 then UNIV else {}) \<inter> \<lbrace>va < 8\<rbrace>}} \<inter> \<lbrace>sint v \<le> 2147483679 \<and> - sint v \<le> 2147483616\<rbrace>}}} \<inter> {s. x___unsigned_long_' (s\<lparr>x___unsigned_long_' := ksReadyQueuesL1Bitmap_' (globals s).[unat d]\<rparr>) \<noteq> 0} \<inter> (if dom < 0x10 then UNIV else {})}} proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; d \<le> maxDomain; ksReadyQueuesL1Bitmap s d \<noteq> 0; bitmapQ_no_L1_orphans s\<rbrakk> \<Longrightarrow> invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)) < l2BitmapSize \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) \<noteq> 0 \<and> word_log2 (ksReadyQueuesL1Bitmap s d) < l2BitmapSize \<and> word_of_nat (word_clz (ksReadyQueuesL2Bitmap_' (globals s').[unat d].[unat (word_of_nat l2BitmapSize - 1 - SCAST(32 signed \<rightarrow> 32) (0x1F - word_of_nat (word_clz (ksReadyQueuesL1Bitmap_' (globals s').[unat d]))))])) = word_of_nat (word_clz (ksReadyQueuesL2Bitmap_' (globals s').[unat d].[invertL1Index (word_log2 (ksReadyQueuesL1Bitmap_' (globals s').[unat d]))])) \<and> ksReadyQueuesL2Bitmap_' (globals s').[unat d].[unat (word_of_nat l2BitmapSize - 1 - SCAST(32 signed \<rightarrow> 32) (0x1F - word_of_nat (word_clz (ksReadyQueuesL1Bitmap_' (globals s').[unat d]))))] \<noteq> 0 \<and> UCAST(8 \<rightarrow> 32) d < 0x10 \<and> word_of_nat l2BitmapSize - 1 - SCAST(32 signed \<rightarrow> 32) (0x1F - word_of_nat (word_clz (ksReadyQueuesL1Bitmap_' (globals s').[unat d]))) < 8 \<and> ksReadyQueuesL1Bitmap_' (globals s').[unat d] \<noteq> 0 \<and> UCAST(8 \<rightarrow> 32) d < 0x10 proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; d \<le> maxDomain; ksReadyQueuesL1Bitmap s d \<noteq> 0; bitmapQ_no_L1_orphans s; cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s)\<rbrakk> \<Longrightarrow> invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)) < l2BitmapSize \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) \<noteq> 0 \<and> word_log2 (ksReadyQueuesL1Bitmap s d) < l2BitmapSize \<and> word_of_nat (word_clz (ksReadyQueuesL2Bitmap_' (globals s').[unat d].[unat (word_of_nat l2BitmapSize - 1 - SCAST(32 signed \<rightarrow> 32) (0x1F - word_of_nat (word_clz (ksReadyQueuesL1Bitmap_' (globals s').[unat d]))))])) = word_of_nat (word_clz (ksReadyQueuesL2Bitmap_' (globals s').[unat d].[invertL1Index (word_log2 (ksReadyQueuesL1Bitmap_' (globals s').[unat d]))])) \<and> ksReadyQueuesL2Bitmap_' (globals s').[unat d].[unat (word_of_nat l2BitmapSize - 1 - SCAST(32 signed \<rightarrow> 32) (0x1F - word_of_nat (word_clz (ksReadyQueuesL1Bitmap_' (globals s').[unat d]))))] \<noteq> 0 \<and> UCAST(8 \<rightarrow> 32) d < 0x10 \<and> word_of_nat l2BitmapSize - 1 - SCAST(32 signed \<rightarrow> 32) (0x1F - word_of_nat (word_clz (ksReadyQueuesL1Bitmap_' (globals s').[unat d]))) < 8 \<and> ksReadyQueuesL1Bitmap_' (globals s').[unat d] \<noteq> 0 \<and> UCAST(8 \<rightarrow> 32) d < 0x10 proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; d \<le> maxDomain; ksReadyQueuesL1Bitmap s d \<noteq> 0; bitmapQ_no_L1_orphans s; cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s); ksReadyQueuesL1Bitmap_' (globals s').[unat d] \<noteq> 0\<rbrakk> \<Longrightarrow> invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)) < l2BitmapSize \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) \<noteq> 0 \<and> word_log2 (ksReadyQueuesL1Bitmap s d) < l2BitmapSize \<and> word_of_nat (word_clz (ksReadyQueuesL2Bitmap_' (globals s').[unat d].[unat (word_of_nat l2BitmapSize - 1 - SCAST(32 signed \<rightarrow> 32) (0x1F - word_of_nat (word_clz (ksReadyQueuesL1Bitmap_' (globals s').[unat d]))))])) = word_of_nat (word_clz (ksReadyQueuesL2Bitmap_' (globals s').[unat d].[invertL1Index (word_log2 (ksReadyQueuesL1Bitmap_' (globals s').[unat d]))])) \<and> ksReadyQueuesL2Bitmap_' (globals s').[unat d].[unat (word_of_nat l2BitmapSize - 1 - SCAST(32 signed \<rightarrow> 32) (0x1F - word_of_nat (word_clz (ksReadyQueuesL1Bitmap_' (globals s').[unat d]))))] \<noteq> 0 \<and> UCAST(8 \<rightarrow> 32) d < 0x10 \<and> word_of_nat l2BitmapSize - 1 - SCAST(32 signed \<rightarrow> 32) (0x1F - word_of_nat (word_clz (ksReadyQueuesL1Bitmap_' (globals s').[unat d]))) < 8 \<and> ksReadyQueuesL1Bitmap_' (globals s').[unat d] \<noteq> 0 \<and> UCAST(8 \<rightarrow> 32) d < 0x10
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; d \<le> maxDomain; ksReadyQueuesL1Bitmap s d \<noteq> 0; bitmapQ_no_L1_orphans s; cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s)\<rbrakk> \<Longrightarrow> ksReadyQueuesL1Bitmap_' (globals s').[unat d] \<noteq> 0 proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; d \<le> maxDomain; ksReadyQueuesL1Bitmap s d \<noteq> 0; bitmapQ_no_L1_orphans s; cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s)\<rbrakk> \<Longrightarrow> ksReadyQueuesL1Bitmap_' (globals s').[unat d] \<noteq> 0
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; d \<le> maxDomain; ksReadyQueuesL1Bitmap s d \<noteq> 0; bitmapQ_no_L1_orphans s; cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s); ksReadyQueuesL1Bitmap_' (globals s').[unat d] \<noteq> 0\<rbrakk> \<Longrightarrow> invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)) < l2BitmapSize \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) \<noteq> 0 \<and> word_log2 (ksReadyQueuesL1Bitmap s d) < l2BitmapSize \<and> word_of_nat (word_clz (ksReadyQueuesL2Bitmap_' (globals s').[unat d].[unat (word_of_nat l2BitmapSize - 1 - SCAST(32 signed \<rightarrow> 32) (0x1F - word_of_nat (word_clz (ksReadyQueuesL1Bitmap_' (globals s').[unat d]))))])) = word_of_nat (word_clz (ksReadyQueuesL2Bitmap_' (globals s').[unat d].[invertL1Index (word_log2 (ksReadyQueuesL1Bitmap_' (globals s').[unat d]))])) \<and> ksReadyQueuesL2Bitmap_' (globals s').[unat d].[unat (word_of_nat l2BitmapSize - 1 - SCAST(32 signed \<rightarrow> 32) (0x1F - word_of_nat (word_clz (ksReadyQueuesL1Bitmap_' (globals s').[unat d]))))] \<noteq> 0 \<and> UCAST(8 \<rightarrow> 32) d < 0x10 \<and> word_of_nat l2BitmapSize - 1 - SCAST(32 signed \<rightarrow> 32) (0x1F - word_of_nat (word_clz (ksReadyQueuesL1Bitmap_' (globals s').[unat d]))) < 8 \<and> ksReadyQueuesL1Bitmap_' (globals s').[unat d] \<noteq> 0 \<and> UCAST(8 \<rightarrow> 32) d < 0x10 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s_, s'_) \<in> rf_sr; d \<le> maxDomain; ksReadyQueuesL1Bitmap s_ d \<noteq> 0; bitmapQ_no_L1_orphans s_; cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s'_)) (ksReadyQueuesL1Bitmap s_)\<rbrakk> \<Longrightarrow> ksReadyQueuesL1Bitmap_' (globals s'_).[unat d] \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; d \<le> maxDomain; ksReadyQueuesL1Bitmap s d \<noteq> 0; bitmapQ_no_L1_orphans s; cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s); ksReadyQueuesL1Bitmap_' (globals s').[unat d] \<noteq> 0\<rbrakk> \<Longrightarrow> invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)) < l2BitmapSize \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) \<noteq> 0 \<and> word_log2 (ksReadyQueuesL1Bitmap s d) < l2BitmapSize \<and> word_of_nat (word_clz (ksReadyQueuesL2Bitmap_' (globals s').[unat d].[unat (word_of_nat l2BitmapSize - 1 - SCAST(32 signed \<rightarrow> 32) (0x1F - word_of_nat (word_clz (ksReadyQueuesL1Bitmap_' (globals s').[unat d]))))])) = word_of_nat (word_clz (ksReadyQueuesL2Bitmap_' (globals s').[unat d].[invertL1Index (word_log2 (ksReadyQueuesL1Bitmap_' (globals s').[unat d]))])) \<and> ksReadyQueuesL2Bitmap_' (globals s').[unat d].[unat (word_of_nat l2BitmapSize - 1 - SCAST(32 signed \<rightarrow> 32) (0x1F - word_of_nat (word_clz (ksReadyQueuesL1Bitmap_' (globals s').[unat d]))))] \<noteq> 0 \<and> UCAST(8 \<rightarrow> 32) d < 0x10 \<and> word_of_nat l2BitmapSize - 1 - SCAST(32 signed \<rightarrow> 32) (0x1F - word_of_nat (word_clz (ksReadyQueuesL1Bitmap_' (globals s').[unat d]))) < 8 \<and> ksReadyQueuesL1Bitmap_' (globals s').[unat d] \<noteq> 0 \<and> UCAST(8 \<rightarrow> 32) d < 0x10 proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; d \<le> maxDomain; ksReadyQueuesL1Bitmap s d \<noteq> 0; bitmapQ_no_L1_orphans s; \<forall>d. (d \<le> maxDomain \<longrightarrow> ksReadyQueuesL1Bitmap_' (globals s').[unat d] = ksReadyQueuesL1Bitmap s d) \<and> (\<not> d \<le> maxDomain \<longrightarrow> ksReadyQueuesL1Bitmap s d = 0)\<rbrakk> \<Longrightarrow> invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)) < l2BitmapSize \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) \<noteq> 0 \<and> word_log2 (ksReadyQueuesL1Bitmap s d) < l2BitmapSize \<and> word_of_nat (word_clz (ksReadyQueuesL2Bitmap_' (globals s').[unat d].[unat (word_of_nat l2BitmapSize - 1 - word_of_nat (word_log2 (ksReadyQueuesL1Bitmap s d)))])) = word_of_nat (word_clz (ksReadyQueuesL2Bitmap_' (globals s').[unat d].[invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))])) \<and> ksReadyQueuesL2Bitmap_' (globals s').[unat d].[unat (word_of_nat l2BitmapSize - 1 - word_of_nat (word_log2 (ksReadyQueuesL1Bitmap s d)))] \<noteq> 0 \<and> word_of_nat l2BitmapSize - 1 - word_of_nat (word_log2 (ksReadyQueuesL1Bitmap s d)) < 8 proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; d \<le> maxDomain; ksReadyQueuesL1Bitmap s d \<noteq> 0; bitmapQ_no_L1_orphans s; \<forall>d. (d \<le> maxDomain \<longrightarrow> ksReadyQueuesL1Bitmap_' (globals s').[unat d] = ksReadyQueuesL1Bitmap s d) \<and> (\<not> d \<le> maxDomain \<longrightarrow> ksReadyQueuesL1Bitmap s d = 0); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) \<noteq> 0 \<and> word_log2 (ksReadyQueuesL1Bitmap s d) < l2BitmapSize\<rbrakk> \<Longrightarrow> invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)) < l2BitmapSize \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) \<noteq> 0 \<and> word_log2 (ksReadyQueuesL1Bitmap s d) < l2BitmapSize \<and> word_of_nat (word_clz (ksReadyQueuesL2Bitmap_' (globals s').[unat d].[unat (word_of_nat l2BitmapSize - 1 - word_of_nat (word_log2 (ksReadyQueuesL1Bitmap s d)))])) = word_of_nat (word_clz (ksReadyQueuesL2Bitmap_' (globals s').[unat d].[invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))])) \<and> ksReadyQueuesL2Bitmap_' (globals s').[unat d].[unat (word_of_nat l2BitmapSize - 1 - word_of_nat (word_log2 (ksReadyQueuesL1Bitmap s d)))] \<noteq> 0 \<and> word_of_nat l2BitmapSize - 1 - word_of_nat (word_log2 (ksReadyQueuesL1Bitmap s d)) < 8 proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; d \<le> maxDomain; ksReadyQueuesL1Bitmap s d \<noteq> 0; bitmapQ_no_L1_orphans s; \<forall>d. (d \<le> maxDomain \<longrightarrow> ksReadyQueuesL1Bitmap_' (globals s').[unat d] = ksReadyQueuesL1Bitmap s d) \<and> (\<not> d \<le> maxDomain \<longrightarrow> ksReadyQueuesL1Bitmap s d = 0); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) \<noteq> 0 \<and> word_log2 (ksReadyQueuesL1Bitmap s d) < l2BitmapSize\<rbrakk> \<Longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) \<noteq> 0 \<and> word_log2 (ksReadyQueuesL1Bitmap s d) < l2BitmapSize \<and> word_of_nat (word_clz (ksReadyQueuesL2Bitmap_' (globals s').[unat d].[unat (word_of_nat l2BitmapSize - 1 - word_of_nat (word_log2 (ksReadyQueuesL1Bitmap s d)))])) = word_of_nat (word_clz (ksReadyQueuesL2Bitmap_' (globals s').[unat d].[invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))])) \<and> ksReadyQueuesL2Bitmap_' (globals s').[unat d].[unat (word_of_nat l2BitmapSize - 1 - word_of_nat (word_log2 (ksReadyQueuesL1Bitmap s d)))] \<noteq> 0 \<and> word_of_nat l2BitmapSize - 1 - word_of_nat (word_log2 (ksReadyQueuesL1Bitmap s d)) < 8 proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; d \<le> maxDomain; ksReadyQueuesL1Bitmap s d \<noteq> 0; bitmapQ_no_L1_orphans s; \<forall>d. (d \<le> maxDomain \<longrightarrow> ksReadyQueuesL1Bitmap_' (globals s').[unat d] = ksReadyQueuesL1Bitmap s d) \<and> (\<not> d \<le> maxDomain \<longrightarrow> ksReadyQueuesL1Bitmap s d = 0); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) \<noteq> 0 \<and> word_log2 (ksReadyQueuesL1Bitmap s d) < l2BitmapSize\<rbrakk> \<Longrightarrow> word_log2 (ksReadyQueuesL1Bitmap s d) < l2BitmapSize \<and> word_of_nat (word_clz (ksReadyQueuesL2Bitmap_' (globals s').[unat d].[unat (word_of_nat l2BitmapSize - 1 - word_of_nat (word_log2 (ksReadyQueuesL1Bitmap s d)))])) = word_of_nat (word_clz (ksReadyQueuesL2Bitmap_' (globals s').[unat d].[invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))])) \<and> ksReadyQueuesL2Bitmap_' (globals s').[unat d].[unat (word_of_nat l2BitmapSize - 1 - word_of_nat (word_log2 (ksReadyQueuesL1Bitmap s d)))] \<noteq> 0 \<and> word_of_nat l2BitmapSize - 1 - word_of_nat (word_log2 (ksReadyQueuesL1Bitmap s d)) < 8 proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; d \<le> maxDomain; ksReadyQueuesL1Bitmap s d \<noteq> 0; bitmapQ_no_L1_orphans s; \<forall>d. (d \<le> maxDomain \<longrightarrow> ksReadyQueuesL1Bitmap_' (globals s').[unat d] = ksReadyQueuesL1Bitmap s d) \<and> (\<not> d \<le> maxDomain \<longrightarrow> ksReadyQueuesL1Bitmap s d = 0); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) \<noteq> 0 \<and> word_log2 (ksReadyQueuesL1Bitmap s d) < l2BitmapSize\<rbrakk> \<Longrightarrow> word_of_nat (word_clz (ksReadyQueuesL2Bitmap_' (globals s').[unat d].[unat (word_of_nat l2BitmapSize - 1 - word_of_nat (word_log2 (ksReadyQueuesL1Bitmap s d)))])) = word_of_nat (word_clz (ksReadyQueuesL2Bitmap_' (globals s').[unat d].[invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))])) \<and> ksReadyQueuesL2Bitmap_' (globals s').[unat d].[unat (word_of_nat l2BitmapSize - 1 - word_of_nat (word_log2 (ksReadyQueuesL1Bitmap s d)))] \<noteq> 0 \<and> word_of_nat l2BitmapSize - 1 - word_of_nat (word_log2 (ksReadyQueuesL1Bitmap s d)) < 8 proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; d \<le> maxDomain; ksReadyQueuesL1Bitmap s d \<noteq> 0; bitmapQ_no_L1_orphans s; \<forall>d. (d \<le> maxDomain \<longrightarrow> ksReadyQueuesL1Bitmap_' (globals s').[unat d] = ksReadyQueuesL1Bitmap s d) \<and> (\<not> d \<le> maxDomain \<longrightarrow> ksReadyQueuesL1Bitmap s d = 0); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) \<noteq> 0 \<and> word_log2 (ksReadyQueuesL1Bitmap s d) < l2BitmapSize\<rbrakk> \<Longrightarrow> ksReadyQueuesL2Bitmap_' (globals s').[unat d].[unat (word_of_nat l2BitmapSize - 1 - word_of_nat (word_log2 (ksReadyQueuesL1Bitmap s d)))] \<noteq> 0 \<and> word_of_nat l2BitmapSize - 1 - word_of_nat (word_log2 (ksReadyQueuesL1Bitmap s d)) < 8 proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; d \<le> maxDomain; ksReadyQueuesL1Bitmap s d \<noteq> 0; bitmapQ_no_L1_orphans s; \<forall>d. (d \<le> maxDomain \<longrightarrow> ksReadyQueuesL1Bitmap_' (globals s').[unat d] = ksReadyQueuesL1Bitmap s d) \<and> (\<not> d \<le> maxDomain \<longrightarrow> ksReadyQueuesL1Bitmap s d = 0); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) \<noteq> 0 \<and> word_log2 (ksReadyQueuesL1Bitmap s d) < l2BitmapSize\<rbrakk> \<Longrightarrow> ksReadyQueuesL2Bitmap_' (globals s').[unat d].[unat (word_of_nat l2BitmapSize - 1 - word_of_nat (word_log2 (ksReadyQueuesL1Bitmap s d)))] \<noteq> 0
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; d \<le> maxDomain; ksReadyQueuesL1Bitmap s d \<noteq> 0; bitmapQ_no_L1_orphans s; \<forall>d. (d \<le> maxDomain \<longrightarrow> ksReadyQueuesL1Bitmap_' (globals s').[unat d] = ksReadyQueuesL1Bitmap s d) \<and> (\<not> d \<le> maxDomain \<longrightarrow> ksReadyQueuesL1Bitmap s d = 0); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) \<noteq> 0 \<and> word_log2 (ksReadyQueuesL1Bitmap s d) < l2BitmapSize\<rbrakk> \<Longrightarrow> word_of_nat l2BitmapSize - 1 - word_of_nat (word_log2 (ksReadyQueuesL1Bitmap s d)) < 8 proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; d \<le> maxDomain; ksReadyQueuesL1Bitmap s d \<noteq> 0; bitmapQ_no_L1_orphans s; \<forall>d. (d \<le> maxDomain \<longrightarrow> ksReadyQueuesL1Bitmap_' (globals s').[unat d] = ksReadyQueuesL1Bitmap s d) \<and> (\<not> d \<le> maxDomain \<longrightarrow> ksReadyQueuesL1Bitmap s d = 0); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) \<noteq> 0 \<and> word_log2 (ksReadyQueuesL1Bitmap s d) < l2BitmapSize\<rbrakk> \<Longrightarrow> ksReadyQueuesL2Bitmap_' (globals s').[unat d].[invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))] \<noteq> 0
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; d \<le> maxDomain; ksReadyQueuesL1Bitmap s d \<noteq> 0; bitmapQ_no_L1_orphans s; \<forall>d. (d \<le> maxDomain \<longrightarrow> ksReadyQueuesL1Bitmap_' (globals s').[unat d] = ksReadyQueuesL1Bitmap s d) \<and> (\<not> d \<le> maxDomain \<longrightarrow> ksReadyQueuesL1Bitmap s d = 0); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) \<noteq> 0 \<and> word_log2 (ksReadyQueuesL1Bitmap s d) < l2BitmapSize\<rbrakk> \<Longrightarrow> word_of_nat l2BitmapSize - 1 - word_of_nat (word_log2 (ksReadyQueuesL1Bitmap s d)) < 8 proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; d \<le> maxDomain; ksReadyQueuesL1Bitmap s d \<noteq> 0; bitmapQ_no_L1_orphans s; \<forall>d. (d \<le> maxDomain \<longrightarrow> ksReadyQueuesL1Bitmap_' (globals s').[unat d] = ksReadyQueuesL1Bitmap s d) \<and> (\<not> d \<le> maxDomain \<longrightarrow> ksReadyQueuesL1Bitmap s d = 0); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) \<noteq> 0 \<and> word_log2 (ksReadyQueuesL1Bitmap s d) < l2BitmapSize; cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s)\<rbrakk> \<Longrightarrow> ksReadyQueuesL2Bitmap_' (globals s').[unat d].[invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))] \<noteq> 0
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; d \<le> maxDomain; ksReadyQueuesL1Bitmap s d \<noteq> 0; bitmapQ_no_L1_orphans s; \<forall>d. (d \<le> maxDomain \<longrightarrow> ksReadyQueuesL1Bitmap_' (globals s').[unat d] = ksReadyQueuesL1Bitmap s d) \<and> (\<not> d \<le> maxDomain \<longrightarrow> ksReadyQueuesL1Bitmap s d = 0); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) \<noteq> 0 \<and> word_log2 (ksReadyQueuesL1Bitmap s d) < l2BitmapSize\<rbrakk> \<Longrightarrow> word_of_nat l2BitmapSize - 1 - word_of_nat (word_log2 (ksReadyQueuesL1Bitmap s d)) < 8 proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; d \<le> maxDomain; ksReadyQueuesL1Bitmap s d \<noteq> 0; bitmapQ_no_L1_orphans s; \<forall>d. (d \<le> maxDomain \<longrightarrow> ksReadyQueuesL1Bitmap_' (globals s').[unat d] = ksReadyQueuesL1Bitmap s d) \<and> (\<not> d \<le> maxDomain \<longrightarrow> ksReadyQueuesL1Bitmap s d = 0); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) \<noteq> 0 \<and> word_log2 (ksReadyQueuesL1Bitmap s d) < l2BitmapSize\<rbrakk> \<Longrightarrow> word_of_nat l2BitmapSize - 1 - word_of_nat (word_log2 (ksReadyQueuesL1Bitmap s d)) < 8 proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; d \<le> maxDomain; ksReadyQueuesL1Bitmap s d \<noteq> 0; bitmapQ_no_L1_orphans s; \<forall>d. (d \<le> maxDomain \<longrightarrow> ksReadyQueuesL1Bitmap_' (globals s').[unat d] = ksReadyQueuesL1Bitmap s d) \<and> (\<not> d \<le> maxDomain \<longrightarrow> ksReadyQueuesL1Bitmap s d = 0); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) \<noteq> 0; word_log2 (ksReadyQueuesL1Bitmap s d) < 8\<rbrakk> \<Longrightarrow> 7 - word_of_nat (word_log2 (ksReadyQueuesL1Bitmap s d)) < 8 proof (prove)
goal:
No subgoals! proof (state)
this:
ccorres (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) ret__unsigned_long_' (\<lambda>s. d \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s d \<noteq> 0 \<and> bitmapQ_no_L1_orphans s) (UNIV \<inter> \<lbrace>\<acute>dom = UCAST(8 \<rightarrow> 32) d\<rbrace>) hs (getHighestPrio d) (Call getHighestPrio_'proc)

goal:
No subgoals!