theory IpcCancel_R

lemma setQueue_after_addToBitmap:
  "(setQueue d p q >>= (\<lambda>rv. (when P (addToBitmap d p)) >>= (\<lambda>rv. threadSet f t))) =
   (when P (addToBitmap d p) >>= (\<lambda>rv. (threadSet f t) >>= (\<lambda>rv. setQueue d p q)))" apply (case_tac P, simp_all) prefer 2 apply (simp add: setQueue_after) apply (simp add: setQueue_def when_def) apply (subst oblivious_modify_swap) apply (simp add: threadSet_def getObject_def setObject_def
                   loadObject_default_def bitmap_fun_defs
                   split_def projectKO_def2 alignCheck_assert
                   magnitudeCheck_assert updateObject_default_def) apply (intro oblivious_bind, simp_all) apply (clarsimp simp: bind_assoc) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do rv <- setQueue d p q;
rv <- when P (addToBitmap d p);
threadSet f t
od = do rv <- when P (addToBitmap d p);
rv <- threadSet f t;
setQueue d p q
od proof (prove)
goal (2 subgoals):
 1. P \<Longrightarrow> do rv <- setQueue d p q;
rv <- addToBitmap d p;
threadSet f t
od = do rv <- addToBitmap d p;
rv <- threadSet f t;
setQueue d p q
od
 2. \<not> P \<Longrightarrow> do rv <- setQueue d p q;
threadSet f t
od = do rv <- threadSet f t;
setQueue d p q
od proof (prove)
goal (2 subgoals):
 1. \<not> P \<Longrightarrow> do rv <- setQueue d p q;
threadSet f t
od = do rv <- threadSet f t;
setQueue d p q
od
 2. P \<Longrightarrow> do rv <- setQueue d p q;
rv <- addToBitmap d p;
threadSet f t
od = do rv <- addToBitmap d p;
rv <- threadSet f t;
setQueue d p q
od proof (prove)
goal (1 subgoal):
 1. P \<Longrightarrow> do rv <- setQueue d p q;
rv <- addToBitmap d p;
threadSet f t
od = do rv <- addToBitmap d p;
rv <- threadSet f t;
setQueue d p q
od proof (prove)
goal (1 subgoal):
 1. P \<Longrightarrow> do rv <- modify (\<lambda>ks. ks\<lparr>ksReadyQueues := (ksReadyQueues ks)((d, p) := q)\<rparr>);
rv <- addToBitmap d p;
threadSet f t
od = do rv <- addToBitmap d p;
rv <- threadSet f t;
modify (\<lambda>ks. ks\<lparr>ksReadyQueues := (ksReadyQueues ks)((d, p) := q)\<rparr>)
od proof (prove)
goal (2 subgoals):
 1. P \<Longrightarrow> oblivious (\<lambda>ks. ks\<lparr>ksReadyQueues := (ksReadyQueues ks)((d, p) := q)\<rparr>) (do rv <- addToBitmap d p;
threadSet f t
od)
 2. P \<Longrightarrow> do rv <- do rv <- addToBitmap d p;
threadSet f t
od;
modify (\<lambda>ks. ks\<lparr>ksReadyQueues := (ksReadyQueues ks)((d, p) := q)\<rparr>)
od = do rv <- addToBitmap d p;
rv <- threadSet f t;
modify (\<lambda>ks. ks\<lparr>ksReadyQueues := (ksReadyQueues ks)((d, p) := q)\<rparr>)
od proof (prove)
goal (2 subgoals):
 1. P \<Longrightarrow> oblivious (\<lambda>ks. ks\<lparr>ksReadyQueues := (ksReadyQueues ks)((d, p) := q)\<rparr>) (do rv <- do y <- do l1 <- gets (\<lambda>ks. ksReadyQueuesL1Bitmap ks d);
modify (\<lambda>ks. ks\<lparr>ksReadyQueuesL1Bitmap := (ksReadyQueuesL1Bitmap ks)(d := l1 || 2 ^ prioToL1Index p)\<rparr>)
od;
l2 <- gets (\<lambda>ks. ksReadyQueuesL2Bitmap ks (d, invertL1Index (prioToL1Index p)));
modify (\<lambda>ks. ks\<lparr>ksReadyQueuesL2Bitmap := (ksReadyQueuesL2Bitmap ks)((d, invertL1Index (prioToL1Index p)) := l2 || 2 ^ unat (p && mask wordRadix))\<rparr>)
od;
tcb <- do map <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 (fromPPtr t) map));
y <- assert (fromPPtr t = fst p);
val <- assert_opt (projectKO_opt (snd p));
y <- assert (is_aligned (fromPPtr t) (objBits val));
y <- assert (case snd (lookupAround2 (fromPPtr t) map) of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits val \<le> z - fromPPtr t);
return val
od;
ps <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 (fromPPtr t) ps));
obj' <- do y <- assert (fromPPtr t = fst p);
_ <- assert_opt (projectKO_opt (snd p));
y <- assert (is_aligned (fromPPtr t) (objBits (f tcb)));
y <- assert (case snd (lookupAround2 (fromPPtr t) ps) of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits (f tcb) \<le> z - fromPPtr t);
return (KOTCB (f tcb))
od;
modify (ksPSpace_update (\<lambda>_. ps(fst p \<mapsto> obj')))
od)
 2. P \<Longrightarrow> do rv <- do rv <- addToBitmap d p;
threadSet f t
od;
modify (\<lambda>ks. ks\<lparr>ksReadyQueues := (ksReadyQueues ks)((d, p) := q)\<rparr>)
od = do rv <- addToBitmap d p;
rv <- threadSet f t;
modify (\<lambda>ks. ks\<lparr>ksReadyQueues := (ksReadyQueues ks)((d, p) := q)\<rparr>)
od proof (prove)
goal (1 subgoal):
 1. P \<Longrightarrow> do rv <- do rv <- addToBitmap d p;
threadSet f t
od;
modify (\<lambda>ks. ks\<lparr>ksReadyQueues := (ksReadyQueues ks)((d, p) := q)\<rparr>)
od = do rv <- addToBitmap d p;
rv <- threadSet f t;
modify (\<lambda>ks. ks\<lparr>ksReadyQueues := (ksReadyQueues ks)((d, p) := q)\<rparr>)
od proof (prove)
goal:
No subgoals!