theory Detype_R

lemma setCTE_def2:
 "(setCTE src cte) =
     (do  ptr \<leftarrow> locateCTE src;
          modify (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> (cte_update cte (the (ps ptr)) src ptr )))) od)" apply (clarsimp simp:setCTE_def setObject_def split_def locateCTE_def bind_assoc) apply (rule ext) apply (rule_tac Q = "\<lambda>r s'. s'= x \<and> r = ksPSpace x " in monad_eq_split) apply (rule_tac Q = "\<lambda>ptr s'. s' = x \<and> snd ptr = the ((ksPSpace x) (fst ptr) ) " in monad_eq_split) apply (clarsimp simp:assert_def return_def fail_def bind_def simpler_modify_def) apply (clarsimp simp:simpler_updateObject_def fail_def) apply (wp|clarsimp simp:)+ apply (simp add:lookupAround2_char1) apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. setCTE src cte = do ptr <- locateCTE src;
modify (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> cte_update cte (the (ps ptr)) src ptr)))
od proof (prove)
goal (1 subgoal):
 1. do ps <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 src ps));
obj' <- updateObject cte (snd p) src (fst p) (snd (lookupAround2 src ps));
modify (ksPSpace_update (\<lambda>_. ps(fst p \<mapsto> obj')))
od = do x <- gets ksPSpace;
xa <- assert_opt (fst (lookupAround2 src x));
y <- assert (cte_check (snd xa) src (fst xa) (snd (lookupAround2 src x)));
modify (ksPSpace_update (\<lambda>ps. ps(fst xa \<mapsto> cte_update cte (the (ps (fst xa))) src (fst xa))))
od proof (prove)
goal (1 subgoal):
 1. \<And>x. (do ps <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 src ps));
obj' <- updateObject cte (snd p) src (fst p) (snd (lookupAround2 src ps));
modify (ksPSpace_update (\<lambda>_. ps(fst p \<mapsto> obj')))
od) x = (do x <- gets ksPSpace;
xa <- assert_opt (fst (lookupAround2 src x));
y <- assert (cte_check (snd xa) src (fst xa) (snd (lookupAround2 src x)));
modify (ksPSpace_update (\<lambda>ps. ps(fst xa \<mapsto> cte_update cte (the (ps (fst xa))) src (fst xa))))
od) x proof (prove)
goal (3 subgoals):
 1. \<And>x r s. s = x \<and> r = ksPSpace x \<Longrightarrow> (do p <- assert_opt (fst (lookupAround2 src r));
obj' <- updateObject cte (snd p) src (fst p) (snd (lookupAround2 src r));
modify (ksPSpace_update (\<lambda>_. r(fst p \<mapsto> obj')))
od) s = (do x <- assert_opt (fst (lookupAround2 src r));
y <- assert (cte_check (snd x) src (fst x) (snd (lookupAround2 src r)));
modify (ksPSpace_update (\<lambda>ps. ps(fst x \<mapsto> cte_update cte (the (ps (fst x))) src (fst x))))
od) s
 2. \<And>x. \<lbrace>?P2 x\<rbrace> gets ksPSpace \<lbrace>\<lambda>r s. s = x \<and> r = ksPSpace x\<rbrace>
 3. \<And>x. ?P2 x x proof (prove)
goal (5 subgoals):
 1. \<And>x r s ra sa. \<lbrakk>s = x \<and> r = ksPSpace x; sa = x \<and> snd ra = the (ksPSpace x (fst ra))\<rbrakk> \<Longrightarrow> (do obj' <- updateObject cte (snd ra) src (fst ra) (snd (lookupAround2 src r));
modify (ksPSpace_update (\<lambda>_. r(fst ra \<mapsto> obj')))
od) sa = (do y <- assert (cte_check (snd ra) src (fst ra) (snd (lookupAround2 src r)));
modify (ksPSpace_update (\<lambda>ps. ps(fst ra \<mapsto> cte_update cte (the (ps (fst ra))) src (fst ra))))
od) sa
 2. \<And>x r s. s = x \<and> r = ksPSpace x \<Longrightarrow> \<lbrace>?P3 x r s\<rbrace> assert_opt (fst (lookupAround2 src r)) \<lbrace>\<lambda>r s. s = x \<and> snd r = the (ksPSpace x (fst r))\<rbrace>
 3. \<And>x r s. s = x \<and> r = ksPSpace x \<Longrightarrow> ?P3 x r s s
 4. \<And>x. \<lbrace>?P2 x\<rbrace> gets ksPSpace \<lbrace>\<lambda>r s. s = x \<and> r = ksPSpace x\<rbrace>
 5. \<And>x. ?P2 x x proof (prove)
goal (5 subgoals):
 1. \<And>x a. (cte_check (the (ksPSpace x a)) src a (snd (lookupAround2 src (ksPSpace x))) \<longrightarrow> (\<Union>xa\<in>fst (updateObject cte (the (ksPSpace x a)) src a (snd (lookupAround2 src (ksPSpace x))) x). fst (case xa of (obj', s) \<Rightarrow> ({((), s\<lparr>ksPSpace := (ksPSpace x)(a \<mapsto> obj')\<rparr>)}, False))) = {((), ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) x)} \<and> (\<forall>xa\<in>fst (updateObject cte (the (ksPSpace x a)) src a (snd (lookupAround2 src (ksPSpace x))) x). \<not> snd (case xa of (obj', s) \<Rightarrow> ({((), s\<lparr>ksPSpace := (ksPSpace x)(a \<mapsto> obj')\<rparr>)}, False))) \<and> \<not> snd (updateObject cte (the (ksPSpace x a)) src a (snd (lookupAround2 src (ksPSpace x))) x)) \<and> (\<not> cte_check (the (ksPSpace x a)) src a (snd (lookupAround2 src (ksPSpace x))) \<longrightarrow> (\<forall>xa\<in>fst (updateObject cte (the (ksPSpace x a)) src a (snd (lookupAround2 src (ksPSpace x))) x). fst (case xa of (obj', s) \<Rightarrow> ({((), s\<lparr>ksPSpace := (ksPSpace x)(a \<mapsto> obj')\<rparr>)}, False)) = {}) \<and> ((\<exists>xa\<in>fst (updateObject cte (the (ksPSpace x a)) src a (snd (lookupAround2 src (ksPSpace x))) x). snd (case xa of (obj', s) \<Rightarrow> ({((), s\<lparr>ksPSpace := (ksPSpace x)(a \<mapsto> obj')\<rparr>)}, False))) \<or> snd (updateObject cte (the (ksPSpace x a)) src a (snd (lookupAround2 src (ksPSpace x))) x)))
 2. \<And>x r s. s = x \<and> r = ksPSpace x \<Longrightarrow> \<lbrace>?P3 x r s\<rbrace> assert_opt (fst (lookupAround2 src r)) \<lbrace>\<lambda>r s. s = x \<and> snd r = the (ksPSpace x (fst r))\<rbrace>
 3. \<And>x r s. s = x \<and> r = ksPSpace x \<Longrightarrow> ?P3 x r s s
 4. \<And>x. \<lbrace>?P2 x\<rbrace> gets ksPSpace \<lbrace>\<lambda>r s. s = x \<and> r = ksPSpace x\<rbrace>
 5. \<And>x. ?P2 x x proof (prove)
goal (4 subgoals):
 1. \<And>x r s. s = x \<and> r = ksPSpace x \<Longrightarrow> \<lbrace>?P3 x r s\<rbrace> assert_opt (fst (lookupAround2 src r)) \<lbrace>\<lambda>r s. s = x \<and> snd r = the (ksPSpace x (fst r))\<rbrace>
 2. \<And>x r s. s = x \<and> r = ksPSpace x \<Longrightarrow> ?P3 x r s s
 3. \<And>x. \<lbrace>?P2 x\<rbrace> gets ksPSpace \<lbrace>\<lambda>r s. s = x \<and> r = ksPSpace x\<rbrace>
 4. \<And>x. ?P2 x x proof (prove)
goal (3 subgoals):
 1. \<And>x a b. fst (lookupAround2 src (ksPSpace x)) = Some (a, b) \<Longrightarrow> b = the (ksPSpace x a)
 2. \<And>x. \<lbrace>?P2 x\<rbrace> gets ksPSpace \<lbrace>\<lambda>r s. s = x \<and> r = ksPSpace x\<rbrace>
 3. \<And>x. ?P2 x x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>?P2 x\<rbrace> gets ksPSpace \<lbrace>\<lambda>r s. s = x \<and> r = ksPSpace x\<rbrace>
 2. \<And>x. ?P2 x x proof (prove)
goal (1 subgoal):
 1. \<And>x. x = x \<and> ksPSpace x = ksPSpace x proof (prove)
goal:
No subgoals!