theory Schedule_C

lemma isHighestPrio_ccorres:
  "ccorres (\<lambda>rv rv'. rv = to_bool rv') ret__unsigned_long_'
           (\<lambda>s. d \<le> maxDomain \<and> bitmapQ_no_L1_orphans s)
           (UNIV \<inter> \<lbrace>\<acute>dom = ucast d\<rbrace> \<inter> \<lbrace>\<acute>prio = ucast p\<rbrace>) hs
           (isHighestPrio d p)
           (Call isHighestPrio_'proc)" supply Collect_const [simp del] supply prio_and_dom_limit_helpers[simp] supply Collect_const_mem [simp] 
  (* FIXME: these should likely be in simpset for CRefine, or even in general *)
   supply from_bool_eq_if[simp] from_bool_eq_if'[simp] from_bool_0[simp] if_1_0_0[simp]
          ccorres_IF_True[simp] supply if_weak_cong[cong] 
  (* when numDomains = 1, array bounds checks would become _ = 0 rather than _ < 1, changing the
     shape of the proof compared to when numDomains > 1 *)
   including no_less_1_simps apply (cinit lift: dom_' prio_') apply clarsimp apply (rule ccorres_move_const_guard) apply (rule ccorres_pre_getReadyQueuesL1Bitmap, rename_tac l1) apply (rule ccorres_rhs_assoc2) apply (rule ccorres_cond_seq2[THEN iffD1]) apply ccorres_rewrite apply (rule_tac xf'=ret__int_' and val="from_bool (l1 = 0)"
             and R="\<lambda>s. l1 = ksReadyQueuesL1Bitmap s d \<and> d \<le> maxDomain" and R'=UNIV
             in ccorres_symb_exec_r_known_rv) apply vcg apply clarsimp apply (fastforce simp: rf_sr_ksReadyQueuesL1Bitmap_simp) apply ceqv apply clarsimp apply (rule ccorres_cond[where R=\<top>], blast) apply (rule_tac P="l1 = 0" in ccorres_gen_asm, clarsimp) apply (rule ccorres_return_C; clarsimp) apply (rule ccorres_rhs_assoc)+ apply (ctac add: getHighestPrio_ccorres) apply (rename_tac hprio hprio') apply csymbr apply (rule ccorres_return_C, simp, simp, simp) apply (rule wp_post_taut) apply (vcg exspec=getHighestPrio_modifies)+ apply (clarsimp simp: word_le_nat_alt maxDomain_le_unat_ucast_explicit
                  split: if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (\<lambda>rv rv'. rv = to_bool rv') ret__unsigned_long_' (\<lambda>s. d \<le> maxDomain \<and> bitmapQ_no_L1_orphans s) (UNIV \<inter> \<lbrace>\<acute>dom = UCAST(8 \<rightarrow> 32) d\<rbrace> \<inter> \<lbrace>\<acute>prio = UCAST(8 \<rightarrow> 32) p\<rbrace>) hs (isHighestPrio d p) (Call isHighestPrio_'proc) proof (prove)
goal (1 subgoal):
 1. ccorres (\<lambda>rv rv'. rv = to_bool rv') ret__unsigned_long_' (\<lambda>s. d \<le> maxDomain \<and> bitmapQ_no_L1_orphans s) (UNIV \<inter> \<lbrace>\<acute>dom = UCAST(8 \<rightarrow> 32) d\<rbrace> \<inter> \<lbrace>\<acute>prio = UCAST(8 \<rightarrow> 32) p\<rbrace>) hs (isHighestPrio d p) (Call isHighestPrio_'proc) proof (prove)
goal (1 subgoal):
 1. ccorres (\<lambda>rv rv'. rv = to_bool rv') ret__unsigned_long_' (\<lambda>s. d \<le> maxDomain \<and> bitmapQ_no_L1_orphans s) (UNIV \<inter> \<lbrace>\<acute>dom = UCAST(8 \<rightarrow> 32) d\<rbrace> \<inter> \<lbrace>\<acute>prio = UCAST(8 \<rightarrow> 32) p\<rbrace>) hs (isHighestPrio d p) (Call isHighestPrio_'proc) proof (prove)
goal (1 subgoal):
 1. ccorres (\<lambda>rv rv'. rv = to_bool rv') ret__unsigned_long_' (\<lambda>s. d \<le> maxDomain \<and> bitmapQ_no_L1_orphans s) (UNIV \<inter> \<lbrace>\<acute>dom = UCAST(8 \<rightarrow> 32) d\<rbrace> \<inter> \<lbrace>\<acute>prio = UCAST(8 \<rightarrow> 32) p\<rbrace>) hs (isHighestPrio d p) (Call isHighestPrio_'proc) proof (prove)
goal (1 subgoal):
 1. ccorres (\<lambda>rv rv'. rv = to_bool rv') ret__unsigned_long_' (\<lambda>s. d \<le> maxDomain \<and> bitmapQ_no_L1_orphans s) (UNIV \<inter> \<lbrace>\<acute>dom = UCAST(8 \<rightarrow> 32) d\<rbrace> \<inter> \<lbrace>\<acute>prio = UCAST(8 \<rightarrow> 32) p\<rbrace>) hs (isHighestPrio d p) (Call isHighestPrio_'proc) proof (prove)
goal (1 subgoal):
 1. ccorres (\<lambda>rv rv'. rv = to_bool rv') ret__unsigned_long_' (\<lambda>s. d \<le> maxDomain \<and> bitmapQ_no_L1_orphans s) (UNIV \<inter> \<lbrace>\<acute>dom = UCAST(8 \<rightarrow> 32) d\<rbrace> \<inter> \<lbrace>\<acute>prio = UCAST(8 \<rightarrow> 32) p\<rbrace>) hs (isHighestPrio d p) (Call isHighestPrio_'proc) proof (prove)
goal (1 subgoal):
 1. ccorres (\<lambda>rv rv'. rv = to_bool rv') ret__unsigned_long_' (\<lambda>s. d \<le> maxDomain \<and> bitmapQ_no_L1_orphans s) (UNIV \<inter> \<lbrace>\<acute>dom = UCAST(8 \<rightarrow> 32) d\<rbrace> \<inter> \<lbrace>\<acute>prio = UCAST(8 \<rightarrow> 32) p\<rbrace>) hs (isHighestPrio d p) (Call isHighestPrio_'proc) proof (prove)
goal (1 subgoal):
 1. ccorres (\<lambda>rv rv'. rv = to_bool rv') ret__unsigned_long_' (\<lambda>s. d \<le> maxDomain \<and> bitmapQ_no_L1_orphans s) (UNIV \<inter> \<lbrace>\<acute>dom = UCAST(8 \<rightarrow> 32) d\<rbrace> \<inter> \<lbrace>\<acute>prio = UCAST(8 \<rightarrow> 32) p\<rbrace>) hs (isHighestPrio d p) (Call isHighestPrio_'proc) proof (prove)
goal (1 subgoal):
 1. ccorres (\<lambda>rv rv'. rv = to_bool rv') ret__unsigned_long_' (\<lambda>s. d \<le> maxDomain \<and> bitmapQ_no_L1_orphans s) (UNIV \<inter> \<lbrace>\<acute>dom = UCAST(8 \<rightarrow> 32) d\<rbrace> \<inter> \<lbrace>\<acute>prio = UCAST(8 \<rightarrow> 32) p\<rbrace>) hs (isHighestPrio d p) (Call isHighestPrio_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>prio dom. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) p; dom = UCAST(8 \<rightarrow> 32) d\<rbrakk> \<Longrightarrow> ccorres (\<lambda>rv rv'. rv = to_bool rv') ret__unsigned_long_' (?Q214 prio dom) (?Q'214 prio dom) (SKIP # hs) (do l1 <- getReadyQueuesL1Bitmap d;
if l1 = 0 then return True else do hprio <- getHighestPrio d;
return (hprio \<le> p)
od
od) (Guard ArrayBounds \<lbrace>dom < 0x10\<rbrace> (\<acute>ret__int :== (if \<acute>ksReadyQueuesL1Bitmap.[unat dom] = 0 then 1 else 0));;
(IF \<acute>ret__int \<noteq> 0 THEN
  SKIP
ELSE
  \<acute>ret__unsigned_long :== CALL getHighestPrio_'proc(dom);;
\<acute>ret__int :== (if \<acute>ret__unsigned_long \<le> prio then 1 else 0)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) (ret__int_' s))))
 2. \<And>prio dom s s'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) p; dom = UCAST(8 \<rightarrow> 32) d; (s, s') \<in> rf_sr; d \<le> maxDomain \<and> bitmapQ_no_L1_orphans s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q214 prio dom s \<and> s' \<in> ?Q'214 prio dom proof (prove)
goal (2 subgoals):
 1. ccorres (\<lambda>rv rv'. rv = to_bool rv') ret__unsigned_long_' (?Q214 (UCAST(8 \<rightarrow> 32) p) (UCAST(8 \<rightarrow> 32) d)) (?Q'214 (UCAST(8 \<rightarrow> 32) p) (UCAST(8 \<rightarrow> 32) d)) (SKIP # hs) (do l1 <- getReadyQueuesL1Bitmap d;
if l1 = 0 then return True else do hprio <- getHighestPrio d;
return (hprio \<le> p)
od
od) (Guard ArrayBounds \<lbrace>UCAST(8 \<rightarrow> 32) d < 0x10\<rbrace> (\<acute>ret__int :== (if \<acute>ksReadyQueuesL1Bitmap.[unat d] = 0 then 1 else 0));;
(IF \<acute>ret__int \<noteq> 0 THEN
  SKIP
ELSE
  \<acute>ret__unsigned_long :== CALL getHighestPrio_'proc(UCAST(8 \<rightarrow> 32) d);;
\<acute>ret__int :== (if \<acute>ret__unsigned_long \<le> UCAST(8 \<rightarrow> 32) p then 1 else 0)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) (ret__int_' s))))
 2. \<And>prio dom s s'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) p; dom = UCAST(8 \<rightarrow> 32) d; (s, s') \<in> rf_sr; d \<le> maxDomain \<and> bitmapQ_no_L1_orphans s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q214 prio dom s \<and> s' \<in> ?Q'214 prio dom proof (prove)
goal (2 subgoals):
 1. ccorres (\<lambda>rv rv'. rv = to_bool rv') ret__unsigned_long_' (?P227 (UCAST(8 \<rightarrow> 32) p) (UCAST(8 \<rightarrow> 32) d)) (?Q'214 (UCAST(8 \<rightarrow> 32) p) (UCAST(8 \<rightarrow> 32) d)) (SKIP # hs) (do l1 <- getReadyQueuesL1Bitmap d;
if l1 = 0 then return True else do hprio <- getHighestPrio d;
return (hprio \<le> p)
od
od) (\<acute>ret__int :== (if \<acute>ksReadyQueuesL1Bitmap.[unat d] = 0 then 1 else 0);;
(IF \<acute>ret__int \<noteq> 0 THEN
  SKIP
ELSE
  \<acute>ret__unsigned_long :== CALL getHighestPrio_'proc(UCAST(8 \<rightarrow> 32) d);;
\<acute>ret__int :== (if \<acute>ret__unsigned_long \<le> UCAST(8 \<rightarrow> 32) p then 1 else 0)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) (ret__int_' s))))
 2. \<And>prio dom s s'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) p; dom = UCAST(8 \<rightarrow> 32) d; (s, s') \<in> rf_sr; d \<le> maxDomain \<and> bitmapQ_no_L1_orphans s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (?P227 prio dom and K (dom < 0x10)) s \<and> s' \<in> ?Q'214 prio dom proof (prove)
goal (2 subgoals):
 1. \<And>l1. ccorres (\<lambda>rv rv'. rv = to_bool rv') ret__unsigned_long_' (\<lambda>a. ?P231 (UCAST(8 \<rightarrow> 32) p) (UCAST(8 \<rightarrow> 32) d) a l1) (?P'232 (UCAST(8 \<rightarrow> 32) p) (UCAST(8 \<rightarrow> 32) d) l1) (SKIP # hs) (if l1 = 0 then return True else do hprio <- getHighestPrio d;
return (hprio \<le> p)
od) (\<acute>ret__int :== (if \<acute>ksReadyQueuesL1Bitmap.[unat d] = 0 then 1 else 0);;
(IF \<acute>ret__int \<noteq> 0 THEN
  SKIP
ELSE
  \<acute>ret__unsigned_long :== CALL getHighestPrio_'proc(UCAST(8 \<rightarrow> 32) d);;
\<acute>ret__int :== (if \<acute>ret__unsigned_long \<le> UCAST(8 \<rightarrow> 32) p then 1 else 0)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) (ret__int_' s))))
 2. \<And>prio dom s s'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) p; dom = UCAST(8 \<rightarrow> 32) d; (s, s') \<in> rf_sr; d \<le> maxDomain \<and> bitmapQ_no_L1_orphans s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. d \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap a d = rv \<longrightarrow> ?P231 prio dom a rv)) and K (dom < 0x10)) s \<and> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat d] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> ?P'232 prio dom rv} proof (prove)
goal (2 subgoals):
 1. \<And>l1. ccorres (\<lambda>rv rv'. rv = to_bool rv') ret__unsigned_long_' (?P236 (UCAST(8 \<rightarrow> 32) p) (UCAST(8 \<rightarrow> 32) d) l1) (?P'232 (UCAST(8 \<rightarrow> 32) p) (UCAST(8 \<rightarrow> 32) d) l1) (SKIP # hs) (if l1 = 0 then return True else do hprio <- getHighestPrio d;
return (hprio \<le> p)
od) (\<acute>ret__int :== (if \<acute>ksReadyQueuesL1Bitmap.[unat d] = 0 then 1 else 0);;
IF \<acute>ret__int \<noteq> 0 THEN
  SKIP
ELSE
  \<acute>ret__unsigned_long :== CALL getHighestPrio_'proc(UCAST(8 \<rightarrow> 32) d);;
\<acute>ret__int :== (if \<acute>ret__unsigned_long \<le> UCAST(8 \<rightarrow> 32) p then 1 else 0)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) (ret__int_' s)))
 2. \<And>prio dom s s'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) p; dom = UCAST(8 \<rightarrow> 32) d; (s, s') \<in> rf_sr; d \<le> maxDomain \<and> bitmapQ_no_L1_orphans s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. d \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap a d = rv \<longrightarrow> ?P236 prio dom rv a)) and K (dom < 0x10)) s \<and> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat d] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> ?P'232 prio dom rv} proof (prove)
goal (2 subgoals):
 1. \<And>l1. ccorres (\<lambda>rv rv'. rv = to_bool rv') ret__unsigned_long_' (?P236 (UCAST(8 \<rightarrow> 32) p) (UCAST(8 \<rightarrow> 32) d) l1) (?P'232 (UCAST(8 \<rightarrow> 32) p) (UCAST(8 \<rightarrow> 32) d) l1) (SKIP # hs) (if l1 = 0 then return True else do hprio <- getHighestPrio d;
return (hprio \<le> p)
od) (\<acute>ret__int :== (if \<acute>ksReadyQueuesL1Bitmap.[unat d] = 0 then 1 else 0);;
IF \<acute>ret__int \<noteq> 0 THEN
  SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) (ret__int_' s))
ELSE
  \<acute>ret__unsigned_long :== CALL getHighestPrio_'proc(UCAST(8 \<rightarrow> 32) d);;
\<acute>ret__int :== (if \<acute>ret__unsigned_long \<le> UCAST(8 \<rightarrow> 32) p then 1 else 0);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) (ret__int_' s))
FI)
 2. \<And>prio dom s s'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) p; dom = UCAST(8 \<rightarrow> 32) d; (s, s') \<in> rf_sr; d \<le> maxDomain \<and> bitmapQ_no_L1_orphans s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. d \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap a d = rv \<longrightarrow> ?P236 prio dom rv a)) and K (dom < 0x10)) s \<and> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat d] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> ?P'232 prio dom rv} proof (prove)
goal (2 subgoals):
 1. \<And>l1. ccorres (\<lambda>a b. a = to_bool b) ret__unsigned_long_' (?P236 (UCAST(8 \<rightarrow> 32) p) (UCAST(8 \<rightarrow> 32) d) l1) (?P'232 (UCAST(8 \<rightarrow> 32) p) (UCAST(8 \<rightarrow> 32) d) l1) (SKIP # hs) (if l1 = 0 then return True else do hprio <- getHighestPrio d;
return (hprio \<le> p)
od) (\<acute>ret__int :== (if \<acute>ksReadyQueuesL1Bitmap.[unat d] = 0 then 1 else 0);;
IF \<acute>ret__int \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) (ret__int_' s))
ELSE
  \<acute>ret__unsigned_long :== CALL getHighestPrio_'proc(UCAST(8 \<rightarrow> 32) d);;
\<acute>ret__int :== (if \<acute>ret__unsigned_long \<le> UCAST(8 \<rightarrow> 32) p then 1 else 0);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) (ret__int_' s))
FI)
 2. \<And>prio dom s s'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) p; dom = UCAST(8 \<rightarrow> 32) d; (s, s') \<in> rf_sr; d \<le> maxDomain \<and> bitmapQ_no_L1_orphans s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. d \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap a d = rv \<longrightarrow> ?P236 prio dom rv a)) and K (dom < 0x10)) s \<and> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat d] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> ?P'232 prio dom rv} proof (prove)
goal (5 subgoals):
 1. \<And>l1 s. \<Gamma>\<turnstile> (UNIV \<inter> {s'. (l1 = ksReadyQueuesL1Bitmap s d \<and> d \<le> maxDomain) \<and> (s, s') \<in> rf_sr}) \<acute>ret__int :== (if \<acute>ksReadyQueuesL1Bitmap.[unat d] = 0 then 1 else 0) ({s'. (s, s') \<in> rf_sr} \<inter> \<lbrace>\<acute>ret__int = from_bool (l1 = 0)\<rbrace>)
 2. \<And>l1 rv' t t'. ceqv \<Gamma> ret__int_' rv' t t' (IF \<acute>ret__int \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) (ret__int_' s))
ELSE
  \<acute>ret__unsigned_long :== CALL getHighestPrio_'proc(UCAST(8 \<rightarrow> 32) d);;
\<acute>ret__int :== (if \<acute>ret__unsigned_long \<le> UCAST(8 \<rightarrow> 32) p then 1 else 0);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) (ret__int_' s))
FI) (?y'355 l1 rv')
 3. \<And>l1. ccorres (\<lambda>a b. a = to_bool b) ret__unsigned_long_' (?P359 (UCAST(8 \<rightarrow> 32) p) (UCAST(8 \<rightarrow> 32) d) l1) (?Q355 l1) (SKIP # hs) (if l1 = 0 then return True else do hprio <- getHighestPrio d;
return (hprio \<le> p)
od) (?y'355 l1 (from_bool (l1 = 0)))
 4. \<And>l1. \<Gamma>\<turnstile>\<^bsub>/?Ft355 l1\<^esub> (?P'357 (UCAST(8 \<rightarrow> 32) p) (UCAST(8 \<rightarrow> 32) d) l1) \<acute>ret__int :== (if \<acute>ksReadyQueuesL1Bitmap.[unat d] = 0 then 1 else 0) {s. \<forall>rv. ret__int_' s = from_bool (l1 = 0) \<longrightarrow> s \<in> ?Q355 l1}
 5. \<And>prio dom s s'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) p; dom = UCAST(8 \<rightarrow> 32) d; (s, s') \<in> rf_sr; d \<le> maxDomain \<and> bitmapQ_no_L1_orphans s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. d \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap a d = rv \<longrightarrow> (?P359 prio dom rv and (\<lambda>s. rv = ksReadyQueuesL1Bitmap s d \<and> d \<le> maxDomain)) a)) and K (dom < 0x10)) s \<and> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat d] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> ?P'357 prio dom rv \<inter> UNIV} proof (prove)
goal (5 subgoals):
 1. \<And>l1 s. UNIV \<inter> {s'. l1 = ksReadyQueuesL1Bitmap s d \<and> d \<le> maxDomain \<and> (s, s') \<in> rf_sr} \<subseteq> {sa. (s, sa\<lparr>ret__int_' := if ksReadyQueuesL1Bitmap_' (globals sa).[unat d] = 0 then 1 else 0\<rparr>) \<in> rf_sr \<and> (if ksReadyQueuesL1Bitmap_' (globals sa).[unat d] = 0 then 1 else 0) = from_bool (l1 = 0)}
 2. \<And>l1 rv' t t'. ceqv \<Gamma> ret__int_' rv' t t' (IF \<acute>ret__int \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) (ret__int_' s))
ELSE
  \<acute>ret__unsigned_long :== CALL getHighestPrio_'proc(UCAST(8 \<rightarrow> 32) d);;
\<acute>ret__int :== (if \<acute>ret__unsigned_long \<le> UCAST(8 \<rightarrow> 32) p then 1 else 0);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) (ret__int_' s))
FI) (?y'355 l1 rv')
 3. \<And>l1. ccorres (\<lambda>a b. a = to_bool b) ret__unsigned_long_' (?P359 (UCAST(8 \<rightarrow> 32) p) (UCAST(8 \<rightarrow> 32) d) l1) (?Q355 l1) (SKIP # hs) (if l1 = 0 then return True else do hprio <- getHighestPrio d;
return (hprio \<le> p)
od) (?y'355 l1 (from_bool (l1 = 0)))
 4. \<And>l1. \<Gamma>\<turnstile>\<^bsub>/?Ft355 l1\<^esub> (?P'357 (UCAST(8 \<rightarrow> 32) p) (UCAST(8 \<rightarrow> 32) d) l1) \<acute>ret__int :== (if \<acute>ksReadyQueuesL1Bitmap.[unat d] = 0 then 1 else 0) {s. \<forall>rv. ret__int_' s = from_bool (l1 = 0) \<longrightarrow> s \<in> ?Q355 l1}
 5. \<And>prio dom s s'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) p; dom = UCAST(8 \<rightarrow> 32) d; (s, s') \<in> rf_sr; d \<le> maxDomain \<and> bitmapQ_no_L1_orphans s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. d \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap a d = rv \<longrightarrow> (?P359 prio dom rv and (\<lambda>s. rv = ksReadyQueuesL1Bitmap s d \<and> d \<le> maxDomain)) a)) and K (dom < 0x10)) s \<and> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat d] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> ?P'357 prio dom rv \<inter> UNIV} proof (prove)
goal (5 subgoals):
 1. \<And>s x. \<lbrakk>d \<le> maxDomain; (s, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> (ksReadyQueuesL1Bitmap_' (globals x).[unat d] = 0) = (ksReadyQueuesL1Bitmap s d = 0)
 2. \<And>l1 rv' t t'. ceqv \<Gamma> ret__int_' rv' t t' (IF \<acute>ret__int \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) (ret__int_' s))
ELSE
  \<acute>ret__unsigned_long :== CALL getHighestPrio_'proc(UCAST(8 \<rightarrow> 32) d);;
\<acute>ret__int :== (if \<acute>ret__unsigned_long \<le> UCAST(8 \<rightarrow> 32) p then 1 else 0);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) (ret__int_' s))
FI) (?y'355 l1 rv')
 3. \<And>l1. ccorres (\<lambda>a b. a = to_bool b) ret__unsigned_long_' (?P359 (UCAST(8 \<rightarrow> 32) p) (UCAST(8 \<rightarrow> 32) d) l1) (?Q355 l1) (SKIP # hs) (if l1 = 0 then return True else do hprio <- getHighestPrio d;
return (hprio \<le> p)
od) (?y'355 l1 (from_bool (l1 = 0)))
 4. \<And>l1. \<Gamma>\<turnstile>\<^bsub>/?Ft355 l1\<^esub> (?P'357 (UCAST(8 \<rightarrow> 32) p) (UCAST(8 \<rightarrow> 32) d) l1) \<acute>ret__int :== (if \<acute>ksReadyQueuesL1Bitmap.[unat d] = 0 then 1 else 0) {s. \<forall>rv. ret__int_' s = from_bool (l1 = 0) \<longrightarrow> s \<in> ?Q355 l1}
 5. \<And>prio dom s s'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) p; dom = UCAST(8 \<rightarrow> 32) d; (s, s') \<in> rf_sr; d \<le> maxDomain \<and> bitmapQ_no_L1_orphans s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. d \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap a d = rv \<longrightarrow> (?P359 prio dom rv and (\<lambda>s. rv = ksReadyQueuesL1Bitmap s d \<and> d \<le> maxDomain)) a)) and K (dom < 0x10)) s \<and> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat d] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> ?P'357 prio dom rv \<inter> UNIV} proof (prove)
goal (4 subgoals):
 1. \<And>l1 rv' t t'. ceqv \<Gamma> ret__int_' rv' t t' (IF \<acute>ret__int \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) (ret__int_' s))
ELSE
  \<acute>ret__unsigned_long :== CALL getHighestPrio_'proc(UCAST(8 \<rightarrow> 32) d);;
\<acute>ret__int :== (if \<acute>ret__unsigned_long \<le> UCAST(8 \<rightarrow> 32) p then 1 else 0);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) (ret__int_' s))
FI) (?y'355 l1 rv')
 2. \<And>l1. ccorres (\<lambda>a b. a = to_bool b) ret__unsigned_long_' (?P359 (UCAST(8 \<rightarrow> 32) p) (UCAST(8 \<rightarrow> 32) d) l1) (?Q355 l1) (SKIP # hs) (if l1 = 0 then return True else do hprio <- getHighestPrio d;
return (hprio \<le> p)
od) (?y'355 l1 (from_bool (l1 = 0)))
 3. \<And>l1. \<Gamma>\<turnstile>\<^bsub>/?Ft355 l1\<^esub> (?P'357 (UCAST(8 \<rightarrow> 32) p) (UCAST(8 \<rightarrow> 32) d) l1) \<acute>ret__int :== (if \<acute>ksReadyQueuesL1Bitmap.[unat d] = 0 then 1 else 0) {s. \<forall>rv. ret__int_' s = from_bool (l1 = 0) \<longrightarrow> s \<in> ?Q355 l1}
 4. \<And>prio dom s s'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) p; dom = UCAST(8 \<rightarrow> 32) d; (s, s') \<in> rf_sr; d \<le> maxDomain \<and> bitmapQ_no_L1_orphans s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. d \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap a d = rv \<longrightarrow> (?P359 prio dom rv and (\<lambda>s. rv = ksReadyQueuesL1Bitmap s d \<and> d \<le> maxDomain)) a)) and K (dom < 0x10)) s \<and> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat d] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> ?P'357 prio dom rv \<inter> UNIV} proof (prove)
goal (3 subgoals):
 1. \<And>l1. ccorres (\<lambda>a b. a = to_bool b) ret__unsigned_long_' (?P359 (UCAST(8 \<rightarrow> 32) p) (UCAST(8 \<rightarrow> 32) d) l1) (?Q355 l1) (SKIP # hs) (if l1 = 0 then return True else do hprio <- getHighestPrio d;
return (hprio \<le> p)
od) (IF from_bool (l1 = 0) \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) (from_bool (l1 = 0)))
ELSE
  \<acute>ret__unsigned_long :== CALL getHighestPrio_'proc(UCAST(8 \<rightarrow> 32) d);;
\<acute>ret__int :== (if \<acute>ret__unsigned_long \<le> UCAST(8 \<rightarrow> 32) p then 1 else 0);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) (ret__int_' s))
FI)
 2. \<And>l1. \<Gamma>\<turnstile>\<^bsub>/?Ft355 l1\<^esub> (?P'357 (UCAST(8 \<rightarrow> 32) p) (UCAST(8 \<rightarrow> 32) d) l1) \<acute>ret__int :== (if \<acute>ksReadyQueuesL1Bitmap.[unat d] = 0 then 1 else 0) {s. \<forall>rv. ret__int_' s = from_bool (l1 = 0) \<longrightarrow> s \<in> ?Q355 l1}
 3. \<And>prio dom s s'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) p; dom = UCAST(8 \<rightarrow> 32) d; (s, s') \<in> rf_sr; d \<le> maxDomain \<and> bitmapQ_no_L1_orphans s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. d \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap a d = rv \<longrightarrow> (?P359 prio dom rv and (\<lambda>s. rv = ksReadyQueuesL1Bitmap s d \<and> d \<le> maxDomain)) a)) and K (dom < 0x10)) s \<and> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat d] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> ?P'357 prio dom rv \<inter> UNIV} proof (prove)
goal (3 subgoals):
 1. \<And>l1. ccorres (\<lambda>a b. a = to_bool b) ret__unsigned_long_' (?P359 (UCAST(8 \<rightarrow> 32) p) (UCAST(8 \<rightarrow> 32) d) l1) (?Q355 l1) (SKIP # hs) (if l1 = 0 then return True else do hprio <- getHighestPrio d;
return (hprio \<le> p)
od) (IF l1 = 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) (from_bool (l1 = 0)))
ELSE
  \<acute>ret__unsigned_long :== CALL getHighestPrio_'proc(UCAST(8 \<rightarrow> 32) d);;
\<acute>ret__int :== (if \<acute>ret__unsigned_long \<le> UCAST(8 \<rightarrow> 32) p then 1 else 0);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) (ret__int_' s))
FI)
 2. \<And>l1. \<Gamma>\<turnstile>\<^bsub>/?Ft355 l1\<^esub> (?P'357 (UCAST(8 \<rightarrow> 32) p) (UCAST(8 \<rightarrow> 32) d) l1) \<acute>ret__int :== (if \<acute>ksReadyQueuesL1Bitmap.[unat d] = 0 then 1 else 0) {s. \<forall>rv. ret__int_' s = from_bool (l1 = 0) \<longrightarrow> s \<in> ?Q355 l1}
 3. \<And>prio dom s s'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) p; dom = UCAST(8 \<rightarrow> 32) d; (s, s') \<in> rf_sr; d \<le> maxDomain \<and> bitmapQ_no_L1_orphans s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. d \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap a d = rv \<longrightarrow> (?P359 prio dom rv and (\<lambda>s. rv = ksReadyQueuesL1Bitmap s d \<and> d \<le> maxDomain)) a)) and K (dom < 0x10)) s \<and> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat d] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> ?P'357 prio dom rv \<inter> UNIV} proof (prove)
goal (4 subgoals):
 1. \<And>l1. ccorres (\<lambda>a b. a = to_bool b) ret__unsigned_long_' (?Pt459 (UCAST(8 \<rightarrow> 32) p) (UCAST(8 \<rightarrow> 32) d) l1) (?Rt455 l1) (SKIP # hs) (return True) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) (from_bool (l1 = 0))))
 2. \<And>l1. ccorres (\<lambda>a b. a = to_bool b) ret__unsigned_long_' (?Pf458 (UCAST(8 \<rightarrow> 32) p) (UCAST(8 \<rightarrow> 32) d) l1) (?Rf455 l1) (SKIP # hs) (do hprio <- getHighestPrio d;
return (hprio \<le> p)
od) (\<acute>ret__unsigned_long :== CALL getHighestPrio_'proc(UCAST(8 \<rightarrow> 32) d);;
\<acute>ret__int :== (if \<acute>ret__unsigned_long \<le> UCAST(8 \<rightarrow> 32) p then 1 else 0);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) (ret__int_' s)))
 3. \<And>l1. \<Gamma>\<turnstile>\<^bsub>/?Ft355 l1\<^esub> (?P'357 (UCAST(8 \<rightarrow> 32) p) (UCAST(8 \<rightarrow> 32) d) l1) \<acute>ret__int :== (if \<acute>ksReadyQueuesL1Bitmap.[unat d] = 0 then 1 else 0) {s. \<forall>rv. ret__int_' s = from_bool (l1 = 0) \<longrightarrow> s \<in> ?Rt455 l1 \<inter> \<lbrace>l1 = 0\<rbrace> \<union> ?Rf455 l1 \<inter> - \<lbrace>l1 = 0\<rbrace>}
 4. \<And>prio dom s s'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) p; dom = UCAST(8 \<rightarrow> 32) d; (s, s') \<in> rf_sr; d \<le> maxDomain \<and> bitmapQ_no_L1_orphans s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. d \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap a d = rv \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. rv = 0 \<longrightarrow> ?Pt459 prio dom rv s) and (\<lambda>s. rv \<noteq> 0 \<longrightarrow> ?Pf458 prio dom rv s) and (\<lambda>s. rv = ksReadyQueuesL1Bitmap s d \<and> d \<le> maxDomain)) a)) and K (dom < 0x10)) s \<and> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat d] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> ?P'357 prio dom rv \<inter> UNIV} proof (prove)
goal (4 subgoals):
 1. ccorres (\<lambda>a b. a = to_bool b) ret__unsigned_long_' (?G480 (UCAST(8 \<rightarrow> 32) p) (UCAST(8 \<rightarrow> 32) d) 0) (?Rt455 0) (SKIP # hs) (return True) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) true))
 2. \<And>l1. ccorres (\<lambda>a b. a = to_bool b) ret__unsigned_long_' (?Pf458 (UCAST(8 \<rightarrow> 32) p) (UCAST(8 \<rightarrow> 32) d) l1) (?Rf455 l1) (SKIP # hs) (do hprio <- getHighestPrio d;
return (hprio \<le> p)
od) (\<acute>ret__unsigned_long :== CALL getHighestPrio_'proc(UCAST(8 \<rightarrow> 32) d);;
\<acute>ret__int :== (if \<acute>ret__unsigned_long \<le> UCAST(8 \<rightarrow> 32) p then 1 else 0);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) (ret__int_' s)))
 3. \<And>l1. \<Gamma>\<turnstile>\<^bsub>/?Ft355 l1\<^esub> (?P'357 (UCAST(8 \<rightarrow> 32) p) (UCAST(8 \<rightarrow> 32) d) l1) \<acute>ret__int :== (if \<acute>ksReadyQueuesL1Bitmap.[unat d] = 0 then 1 else 0) {s. \<forall>rv. ret__int_' s = from_bool (l1 = 0) \<longrightarrow> s \<in> ?Rt455 l1 \<inter> \<lbrace>l1 = 0\<rbrace> \<union> ?Rf455 l1 \<inter> - \<lbrace>l1 = 0\<rbrace>}
 4. \<And>prio dom s s'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) p; dom = UCAST(8 \<rightarrow> 32) d; (s, s') \<in> rf_sr; d \<le> maxDomain \<and> bitmapQ_no_L1_orphans s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. d \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap a d = rv \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. rv = 0 \<longrightarrow> (?G480 prio dom rv and (\<lambda>_. rv = 0)) s) and (\<lambda>s. rv \<noteq> 0 \<longrightarrow> ?Pf458 prio dom rv s) and (\<lambda>s. rv = ksReadyQueuesL1Bitmap s d \<and> d \<le> maxDomain)) a)) and K (dom < 0x10)) s \<and> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat d] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> ?P'357 prio dom rv \<inter> UNIV} proof (prove)
goal (3 subgoals):
 1. \<And>l1. ccorres (\<lambda>a b. a = to_bool b) ret__unsigned_long_' (?Pf458 (UCAST(8 \<rightarrow> 32) p) (UCAST(8 \<rightarrow> 32) d) l1) (?Rf455 l1) (SKIP # hs) (do hprio <- getHighestPrio d;
return (hprio \<le> p)
od) (\<acute>ret__unsigned_long :== CALL getHighestPrio_'proc(UCAST(8 \<rightarrow> 32) d);;
\<acute>ret__int :== (if \<acute>ret__unsigned_long \<le> UCAST(8 \<rightarrow> 32) p then 1 else 0);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) (ret__int_' s)))
 2. \<And>l1. \<Gamma>\<turnstile>\<^bsub>/?Ft355 l1\<^esub> (?P'357 (UCAST(8 \<rightarrow> 32) p) (UCAST(8 \<rightarrow> 32) d) l1) \<acute>ret__int :== (if \<acute>ksReadyQueuesL1Bitmap.[unat d] = 0 then 1 else 0) {s. \<forall>rv. ret__int_' s = from_bool (l1 = 0) \<longrightarrow> s \<in> \<lbrace>True = to_bool (SCAST(32 signed \<rightarrow> 32) true)\<rbrace> \<inter> \<lbrace>l1 = 0\<rbrace> \<union> ?Rf455 l1 \<inter> - \<lbrace>l1 = 0\<rbrace>}
 3. \<And>prio dom s s'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) p; dom = UCAST(8 \<rightarrow> 32) d; (s, s') \<in> rf_sr; d \<le> maxDomain \<and> bitmapQ_no_L1_orphans s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. d \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap a d = rv \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. rv = 0 \<longrightarrow> ((\<lambda>a. True) and (\<lambda>_. rv = 0)) s) and (\<lambda>s. rv \<noteq> 0 \<longrightarrow> ?Pf458 prio dom rv s) and (\<lambda>s. rv = ksReadyQueuesL1Bitmap s d \<and> d \<le> maxDomain)) a)) and K (dom < 0x10)) s \<and> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat d] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> ?P'357 prio dom rv \<inter> UNIV} proof (prove)
goal (3 subgoals):
 1. \<And>l1. ccorres (\<lambda>a b. a = to_bool b) ret__unsigned_long_' (?Pf458 (UCAST(8 \<rightarrow> 32) p) (UCAST(8 \<rightarrow> 32) d) l1) (?Rf455 l1) (SKIP # hs) (do hprio <- getHighestPrio d;
return (hprio \<le> p)
od) (\<acute>ret__unsigned_long :== CALL getHighestPrio_'proc(UCAST(8 \<rightarrow> 32) d);;
(\<acute>ret__int :== (if \<acute>ret__unsigned_long \<le> UCAST(8 \<rightarrow> 32) p then 1 else 0);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) (ret__int_' s))))
 2. \<And>l1. \<Gamma>\<turnstile>\<^bsub>/?Ft355 l1\<^esub> (?P'357 (UCAST(8 \<rightarrow> 32) p) (UCAST(8 \<rightarrow> 32) d) l1) \<acute>ret__int :== (if \<acute>ksReadyQueuesL1Bitmap.[unat d] = 0 then 1 else 0) {s. \<forall>rv. ret__int_' s = from_bool (l1 = 0) \<longrightarrow> s \<in> \<lbrace>True = to_bool (SCAST(32 signed \<rightarrow> 32) true)\<rbrace> \<inter> \<lbrace>l1 = 0\<rbrace> \<union> ?Rf455 l1 \<inter> - \<lbrace>l1 = 0\<rbrace>}
 3. \<And>prio dom s s'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) p; dom = UCAST(8 \<rightarrow> 32) d; (s, s') \<in> rf_sr; d \<le> maxDomain \<and> bitmapQ_no_L1_orphans s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. d \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap a d = rv \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. rv = 0 \<longrightarrow> ((\<lambda>a. True) and (\<lambda>_. rv = 0)) s) and (\<lambda>s. rv \<noteq> 0 \<longrightarrow> ?Pf458 prio dom rv s) and (\<lambda>s. rv = ksReadyQueuesL1Bitmap s d \<and> d \<le> maxDomain)) a)) and K (dom < 0x10)) s \<and> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat d] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> ?P'357 prio dom rv \<inter> UNIV} proof (prove)
goal (5 subgoals):
 1. \<And>l1 rv ret__unsigned_long. ret__unsigned_long = UCAST(8 \<rightarrow> 32) rv \<Longrightarrow> ccorres (\<lambda>a b. a = to_bool b) ret__unsigned_long_' (?Q510 l1 rv) (?Q'510 l1 rv ret__unsigned_long) (SKIP # hs) (return (rv \<le> p)) (\<acute>ret__int :== (if ret__unsigned_long \<le> UCAST(8 \<rightarrow> 32) p then 1 else 0);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) (ret__int_' s)))
 2. \<And>l1. \<lbrace>?R513 (UCAST(8 \<rightarrow> 32) p) (UCAST(8 \<rightarrow> 32) d) l1\<rbrace> getHighestPrio d \<lbrace>?Q510 l1\<rbrace>
 3. \<And>l1. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'510 l1) \<acute>ret__unsigned_long :== CALL getHighestPrio_'proc(UCAST(8 \<rightarrow> 32) d) {s. \<forall>rv. ret__unsigned_long_' s = UCAST(8 \<rightarrow> 32) rv \<longrightarrow> s \<in> ?Q'510 l1 rv (ret__unsigned_long_' s)}
 4. \<And>l1. \<Gamma>\<turnstile>\<^bsub>/?Ft355 l1\<^esub> (?P'357 (UCAST(8 \<rightarrow> 32) p) (UCAST(8 \<rightarrow> 32) d) l1) \<acute>ret__int :== (if \<acute>ksReadyQueuesL1Bitmap.[unat d] = 0 then 1 else 0) {s. \<forall>rv. ret__int_' s = from_bool (l1 = 0) \<longrightarrow> s \<in> \<lbrace>True = to_bool (SCAST(32 signed \<rightarrow> 32) true)\<rbrace> \<inter> \<lbrace>l1 = 0\<rbrace> \<union> {s. dom_'_update (\<lambda>_. UCAST(8 \<rightarrow> 32) d) s \<in> UNIV \<inter> \<lbrace>\<acute>dom = UCAST(8 \<rightarrow> 32) d\<rbrace>} \<inter> ?R'510 l1 \<inter> - \<lbrace>l1 = 0\<rbrace>}
 5. \<And>prio dom s s'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) p; dom = UCAST(8 \<rightarrow> 32) d; (s, s') \<in> rf_sr; d \<le> maxDomain \<and> bitmapQ_no_L1_orphans s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. d \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap a d = rv \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. rv = 0 \<longrightarrow> ((\<lambda>a. True) and (\<lambda>_. rv = 0)) s) and (\<lambda>s. rv \<noteq> 0 \<longrightarrow> ((\<lambda>a. d \<le> maxDomain \<and> ksReadyQueuesL1Bitmap a d \<noteq> 0 \<and> bitmapQ_no_L1_orphans a) and ?R513 prio dom rv) s) and (\<lambda>s. rv = ksReadyQueuesL1Bitmap s d \<and> d \<le> maxDomain)) a)) and K (dom < 0x10)) s \<and> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat d] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> ?P'357 prio dom rv \<inter> UNIV} proof (prove)
goal (5 subgoals):
 1. \<And>l1 hprio hprio'. hprio' = UCAST(8 \<rightarrow> 32) hprio \<Longrightarrow> ccorres (\<lambda>a b. a = to_bool b) ret__unsigned_long_' (?Q510 l1 hprio) (?Q'510 l1 hprio hprio') (SKIP # hs) (return (hprio \<le> p)) (\<acute>ret__int :== (if hprio' \<le> UCAST(8 \<rightarrow> 32) p then 1 else 0);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) (ret__int_' s)))
 2. \<And>l1. \<lbrace>?R513 (UCAST(8 \<rightarrow> 32) p) (UCAST(8 \<rightarrow> 32) d) l1\<rbrace> getHighestPrio d \<lbrace>?Q510 l1\<rbrace>
 3. \<And>l1. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'510 l1) \<acute>ret__unsigned_long :== CALL getHighestPrio_'proc(UCAST(8 \<rightarrow> 32) d) {s. \<forall>rv. ret__unsigned_long_' s = UCAST(8 \<rightarrow> 32) rv \<longrightarrow> s \<in> ?Q'510 l1 rv (ret__unsigned_long_' s)}
 4. \<And>l1. \<Gamma>\<turnstile>\<^bsub>/?Ft355 l1\<^esub> (?P'357 (UCAST(8 \<rightarrow> 32) p) (UCAST(8 \<rightarrow> 32) d) l1) \<acute>ret__int :== (if \<acute>ksReadyQueuesL1Bitmap.[unat d] = 0 then 1 else 0) {s. \<forall>rv. ret__int_' s = from_bool (l1 = 0) \<longrightarrow> s \<in> \<lbrace>True = to_bool (SCAST(32 signed \<rightarrow> 32) true)\<rbrace> \<inter> \<lbrace>l1 = 0\<rbrace> \<union> {s. dom_'_update (\<lambda>_. UCAST(8 \<rightarrow> 32) d) s \<in> UNIV \<inter> \<lbrace>\<acute>dom = UCAST(8 \<rightarrow> 32) d\<rbrace>} \<inter> ?R'510 l1 \<inter> - \<lbrace>l1 = 0\<rbrace>}
 5. \<And>prio dom s s'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) p; dom = UCAST(8 \<rightarrow> 32) d; (s, s') \<in> rf_sr; d \<le> maxDomain \<and> bitmapQ_no_L1_orphans s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. d \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap a d = rv \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. rv = 0 \<longrightarrow> ((\<lambda>a. True) and (\<lambda>_. rv = 0)) s) and (\<lambda>s. rv \<noteq> 0 \<longrightarrow> ((\<lambda>a. d \<le> maxDomain \<and> ksReadyQueuesL1Bitmap a d \<noteq> 0 \<and> bitmapQ_no_L1_orphans a) and ?R513 prio dom rv) s) and (\<lambda>s. rv = ksReadyQueuesL1Bitmap s d \<and> d \<le> maxDomain)) a)) and K (dom < 0x10)) s \<and> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat d] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> ?P'357 prio dom rv \<inter> UNIV} proof (prove)
goal (5 subgoals):
 1. \<And>l1 hprio hprio'. hprio' = UCAST(8 \<rightarrow> 32) hprio \<Longrightarrow> ccorres (\<lambda>a b. a = to_bool b) ret__unsigned_long_' (?Q510 l1 hprio) (?G'564 l1 hprio hprio') (SKIP # hs) (return (hprio \<le> p)) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) (if hprio' \<le> UCAST(8 \<rightarrow> 32) p then 1 else 0)))
 2. \<And>l1. \<lbrace>?R513 (UCAST(8 \<rightarrow> 32) p) (UCAST(8 \<rightarrow> 32) d) l1\<rbrace> getHighestPrio d \<lbrace>?Q510 l1\<rbrace>
 3. \<And>l1. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'510 l1) \<acute>ret__unsigned_long :== CALL getHighestPrio_'proc(UCAST(8 \<rightarrow> 32) d) {s. \<forall>rv. ret__unsigned_long_' s = UCAST(8 \<rightarrow> 32) rv \<longrightarrow> s \<in> {sa. sa\<lparr>ret__int_' := if ret__unsigned_long_' s \<le> UCAST(8 \<rightarrow> 32) p then 1 else 0\<rparr> \<in> ?G'564 l1 rv (ret__unsigned_long_' s)}}
 4. \<And>l1. \<Gamma>\<turnstile>\<^bsub>/?Ft355 l1\<^esub> (?P'357 (UCAST(8 \<rightarrow> 32) p) (UCAST(8 \<rightarrow> 32) d) l1) \<acute>ret__int :== (if \<acute>ksReadyQueuesL1Bitmap.[unat d] = 0 then 1 else 0) {s. \<forall>rv. ret__int_' s = from_bool (l1 = 0) \<longrightarrow> s \<in> \<lbrace>True = to_bool (SCAST(32 signed \<rightarrow> 32) true)\<rbrace> \<inter> \<lbrace>l1 = 0\<rbrace> \<union> {s. dom_'_update (\<lambda>_. UCAST(8 \<rightarrow> 32) d) s \<in> UNIV \<inter> \<lbrace>\<acute>dom = UCAST(8 \<rightarrow> 32) d\<rbrace>} \<inter> ?R'510 l1 \<inter> - \<lbrace>l1 = 0\<rbrace>}
 5. \<And>prio dom s s'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) p; dom = UCAST(8 \<rightarrow> 32) d; (s, s') \<in> rf_sr; d \<le> maxDomain \<and> bitmapQ_no_L1_orphans s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. d \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap a d = rv \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. rv = 0 \<longrightarrow> ((\<lambda>a. True) and (\<lambda>_. rv = 0)) s) and (\<lambda>s. rv \<noteq> 0 \<longrightarrow> ((\<lambda>a. d \<le> maxDomain \<and> ksReadyQueuesL1Bitmap a d \<noteq> 0 \<and> bitmapQ_no_L1_orphans a) and ?R513 prio dom rv) s) and (\<lambda>s. rv = ksReadyQueuesL1Bitmap s d \<and> d \<le> maxDomain)) a)) and K (dom < 0x10)) s \<and> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat d] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> ?P'357 prio dom rv \<inter> UNIV} proof (prove)
goal (4 subgoals):
 1. \<And>l1. \<lbrace>?R513 (UCAST(8 \<rightarrow> 32) p) (UCAST(8 \<rightarrow> 32) d) l1\<rbrace> getHighestPrio d \<lbrace>\<lambda>a b. True\<rbrace>
 2. \<And>l1. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'510 l1) \<acute>ret__unsigned_long :== CALL getHighestPrio_'proc(UCAST(8 \<rightarrow> 32) d) {s. \<forall>rv. ret__unsigned_long_' s = UCAST(8 \<rightarrow> 32) rv \<longrightarrow> s \<in> {sa. sa\<lparr>ret__int_' := if ret__unsigned_long_' s \<le> UCAST(8 \<rightarrow> 32) p then 1 else 0\<rparr> \<in> \<lbrace>(rv \<le> p) = to_bool (SCAST(32 signed \<rightarrow> 32) (if \<^bsup>s\<^esup>ret__unsigned_long \<le> UCAST(8 \<rightarrow> 32) p then 1 else 0))\<rbrace>}}
 3. \<And>l1. \<Gamma>\<turnstile>\<^bsub>/?Ft355 l1\<^esub> (?P'357 (UCAST(8 \<rightarrow> 32) p) (UCAST(8 \<rightarrow> 32) d) l1) \<acute>ret__int :== (if \<acute>ksReadyQueuesL1Bitmap.[unat d] = 0 then 1 else 0) {s. \<forall>rv. ret__int_' s = from_bool (l1 = 0) \<longrightarrow> s \<in> \<lbrace>True = to_bool (SCAST(32 signed \<rightarrow> 32) true)\<rbrace> \<inter> \<lbrace>l1 = 0\<rbrace> \<union> {s. dom_'_update (\<lambda>_. UCAST(8 \<rightarrow> 32) d) s \<in> UNIV \<inter> \<lbrace>\<acute>dom = UCAST(8 \<rightarrow> 32) d\<rbrace>} \<inter> ?R'510 l1 \<inter> - \<lbrace>l1 = 0\<rbrace>}
 4. \<And>prio dom s s'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) p; dom = UCAST(8 \<rightarrow> 32) d; (s, s') \<in> rf_sr; d \<le> maxDomain \<and> bitmapQ_no_L1_orphans s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. d \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap a d = rv \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. rv = 0 \<longrightarrow> ((\<lambda>a. True) and (\<lambda>_. rv = 0)) s) and (\<lambda>s. rv \<noteq> 0 \<longrightarrow> ((\<lambda>a. d \<le> maxDomain \<and> ksReadyQueuesL1Bitmap a d \<noteq> 0 \<and> bitmapQ_no_L1_orphans a) and ?R513 prio dom rv) s) and (\<lambda>s. rv = ksReadyQueuesL1Bitmap s d \<and> d \<le> maxDomain)) a)) and K (dom < 0x10)) s \<and> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat d] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> ?P'357 prio dom rv \<inter> UNIV} proof (prove)
goal (3 subgoals):
 1. \<And>l1. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'510 l1) \<acute>ret__unsigned_long :== CALL getHighestPrio_'proc(UCAST(8 \<rightarrow> 32) d) {s. \<forall>rv. ret__unsigned_long_' s = UCAST(8 \<rightarrow> 32) rv \<longrightarrow> s \<in> {sa. sa\<lparr>ret__int_' := if ret__unsigned_long_' s \<le> UCAST(8 \<rightarrow> 32) p then 1 else 0\<rparr> \<in> \<lbrace>(rv \<le> p) = to_bool (SCAST(32 signed \<rightarrow> 32) (if \<^bsup>s\<^esup>ret__unsigned_long \<le> UCAST(8 \<rightarrow> 32) p then 1 else 0))\<rbrace>}}
 2. \<And>l1. \<Gamma>\<turnstile>\<^bsub>/?Ft355 l1\<^esub> (?P'357 (UCAST(8 \<rightarrow> 32) p) (UCAST(8 \<rightarrow> 32) d) l1) \<acute>ret__int :== (if \<acute>ksReadyQueuesL1Bitmap.[unat d] = 0 then 1 else 0) {s. \<forall>rv. ret__int_' s = from_bool (l1 = 0) \<longrightarrow> s \<in> \<lbrace>True = to_bool (SCAST(32 signed \<rightarrow> 32) true)\<rbrace> \<inter> \<lbrace>l1 = 0\<rbrace> \<union> {s. dom_'_update (\<lambda>_. UCAST(8 \<rightarrow> 32) d) s \<in> UNIV \<inter> \<lbrace>\<acute>dom = UCAST(8 \<rightarrow> 32) d\<rbrace>} \<inter> ?R'510 l1 \<inter> - \<lbrace>l1 = 0\<rbrace>}
 3. \<And>prio dom s s'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) p; dom = UCAST(8 \<rightarrow> 32) d; (s, s') \<in> rf_sr; d \<le> maxDomain \<and> bitmapQ_no_L1_orphans s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. d \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap a d = rv \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. rv = 0 \<longrightarrow> ((\<lambda>a. True) and (\<lambda>_. rv = 0)) s) and (\<lambda>s. rv \<noteq> 0 \<longrightarrow> ((\<lambda>a. d \<le> maxDomain \<and> ksReadyQueuesL1Bitmap a d \<noteq> 0 \<and> bitmapQ_no_L1_orphans a) and (\<lambda>a. True)) s) and (\<lambda>s. rv = ksReadyQueuesL1Bitmap s d \<and> d \<le> maxDomain)) a)) and K (dom < 0x10)) s \<and> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat d] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> ?P'357 prio dom rv \<inter> UNIV} proof (prove)
goal (1 subgoal):
 1. \<And>prio dom s s'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) p; dom = UCAST(8 \<rightarrow> 32) d; (s, s') \<in> rf_sr; d \<le> maxDomain \<and> bitmapQ_no_L1_orphans s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. d \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap a d = rv \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. rv = 0 \<longrightarrow> ((\<lambda>a. True) and (\<lambda>_. rv = 0)) s) and (\<lambda>s. rv \<noteq> 0 \<longrightarrow> ((\<lambda>a. d \<le> maxDomain \<and> ksReadyQueuesL1Bitmap a d \<noteq> 0 \<and> bitmapQ_no_L1_orphans a) and (\<lambda>a. True)) s) and (\<lambda>s. rv = ksReadyQueuesL1Bitmap s d \<and> d \<le> maxDomain)) a)) and K (dom < 0x10)) s \<and> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat d] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> \<lbrace>\<forall>rva. (if \<acute>ksReadyQueuesL1Bitmap.[unat d] = 0 then 1 else 0) = from_bool (rv = 0) \<longrightarrow> True = to_bool (SCAST(32 signed \<rightarrow> 32) true) \<and> rv = 0 \<or> True \<and> dom = dom \<and> (\<forall>t rv. \<^bsup>t\<^esup>ret__unsigned_long = UCAST(8 \<rightarrow> 32) rv \<longrightarrow> (rv \<le> p) = to_bool (SCAST(32 signed \<rightarrow> 32) (if UCAST(8 \<rightarrow> 32) rv \<le> prio then 1 else 0))) \<and> rv \<noteq> 0\<rbrace> \<inter> UNIV} proof (prove)
goal:
No subgoals!