theory PSpace_C

lemma setObject_obj_at_pre:
  "\<lbrakk> updateObject ko = updateObject_default ko;
       (1 :: word32) < 2 ^ objBits ko \<rbrakk>
   \<Longrightarrow>
   setObject p ko
     = (stateAssert (typ_at' (koTypeOf (injectKO ko)) p) []
           >>= (\<lambda>_. setObject p ko))" apply (rule ext) apply (case_tac "typ_at' (koTypeOf (injectKO ko)) p x") apply (simp add: stateAssert_def bind_def
                    get_def return_def) apply (simp add: stateAssert_def bind_def
                   get_def assert_def fail_def) apply (simp add: setObject_def exec_gets split_def
                   assert_opt_def split: option.split) apply (clarsimp simp add: fail_def) apply (simp add: bind_def simpler_modify_def split_def) apply (rule context_conjI) apply (clarsimp simp: updateObject_default_def
                         in_monad) apply (clarsimp simp: projectKOs in_magnitude_check) apply (frule iffD1[OF project_koType, OF exI]) apply (clarsimp simp: typ_at'_def ko_wp_at'_def) apply (simp only: objBitsT_koTypeOf[symmetric] objBits_def) apply simp apply (simp add: koTypeOf_injectKO) apply (rule empty_failD[OF empty_fail_updateObject_default]) apply (rule ccontr, erule nonemptyE) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>updateObject ko = updateObject_default ko; 1 < 2 ^ objBits ko\<rbrakk> \<Longrightarrow> setObject p ko = do _ <- stateAssert (typ_at' (koTypeOf (injectKOS ko)) p) [];
setObject p ko
od proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>updateObject ko = updateObject_default ko; 1 < 2 ^ objBits ko\<rbrakk> \<Longrightarrow> setObject p ko x = (do _ <- stateAssert (typ_at' (koTypeOf (injectKOS ko)) p) [];
setObject p ko
od) x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>updateObject ko = updateObject_default ko; 1 < 2 ^ objBits ko; typ_at' (koTypeOf (injectKOS ko)) p x\<rbrakk> \<Longrightarrow> setObject p ko x = (do _ <- stateAssert (typ_at' (koTypeOf (injectKOS ko)) p) [];
setObject p ko
od) x
 2. \<And>x. \<lbrakk>updateObject ko = updateObject_default ko; 1 < 2 ^ objBits ko; \<not> typ_at' (koTypeOf (injectKOS ko)) p x\<rbrakk> \<Longrightarrow> setObject p ko x = (do _ <- stateAssert (typ_at' (koTypeOf (injectKOS ko)) p) [];
setObject p ko
od) x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>updateObject ko = updateObject_default ko; 1 < 2 ^ objBits ko; \<not> typ_at' (koTypeOf (injectKOS ko)) p x\<rbrakk> \<Longrightarrow> setObject p ko x = (do _ <- stateAssert (typ_at' (koTypeOf (injectKOS ko)) p) [];
setObject p ko
od) x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>updateObject ko = updateObject_default ko; 1 < 2 ^ objBits ko; \<not> typ_at' (koTypeOf (injectKOS ko)) p x\<rbrakk> \<Longrightarrow> setObject p ko x = ({}, True) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>updateObject ko = updateObject_default ko; 1 < 2 ^ objBits ko; \<not> typ_at' (koTypeOf (injectKOS ko)) p x\<rbrakk> \<Longrightarrow> (fst (lookupAround2 p (ksPSpace x)) = None \<longrightarrow> fail x = ({}, True)) \<and> (\<forall>a b. fst (lookupAround2 p (ksPSpace x)) = Some (a, b) \<longrightarrow> (do obj' <- updateObject_default ko b p a (snd (lookupAround2 p (ksPSpace x)));
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(a \<mapsto> obj')))
od) x = ({}, True)) proof (prove)
goal (1 subgoal):
 1. \<And>x a b. \<lbrakk>updateObject ko = updateObject_default ko; 1 < 2 ^ objBits ko; \<not> typ_at' (koTypeOf (injectKOS ko)) p x; fst (lookupAround2 p (ksPSpace x)) = Some (a, b)\<rbrakk> \<Longrightarrow> (do obj' <- updateObject_default ko b p a (snd (lookupAround2 p (ksPSpace x)));
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(a \<mapsto> obj')))
od) x = ({}, True) proof (prove)
goal (1 subgoal):
 1. \<And>x a b. \<lbrakk>updateObject ko = updateObject_default ko; 1 < 2 ^ objBits ko; \<not> typ_at' (koTypeOf (injectKOS ko)) p x; fst (lookupAround2 p (ksPSpace x)) = Some (a, b)\<rbrakk> \<Longrightarrow> (\<forall>aa ba. (aa, ba) \<notin> fst (updateObject_default ko b p a (snd (lookupAround2 p (ksPSpace x))) x)) \<and> snd (updateObject_default ko b p a (snd (lookupAround2 p (ksPSpace x))) x) proof (prove)
goal (2 subgoals):
 1. \<And>x a b. \<lbrakk>updateObject ko = updateObject_default ko; 1 < 2 ^ objBits ko; \<not> typ_at' (koTypeOf (injectKOS ko)) p x; fst (lookupAround2 p (ksPSpace x)) = Some (a, b)\<rbrakk> \<Longrightarrow> \<forall>aa ba. (aa, ba) \<notin> fst (updateObject_default ko b p a (snd (lookupAround2 p (ksPSpace x))) x)
 2. \<And>x a b. \<lbrakk>updateObject ko = updateObject_default ko; 1 < 2 ^ objBits ko; \<not> typ_at' (koTypeOf (injectKOS ko)) p x; fst (lookupAround2 p (ksPSpace x)) = Some (a, b); \<forall>aa ba. (aa, ba) \<notin> fst (updateObject_default ko b p a (snd (lookupAround2 p (ksPSpace x))) x)\<rbrakk> \<Longrightarrow> snd (updateObject_default ko b p a (snd (lookupAround2 p (ksPSpace x))) x) proof (prove)
goal (2 subgoals):
 1. \<And>x b ba s'' uu_. \<lbrakk>updateObject ko = updateObject_default ko; 1 < 2 ^ objBits ko; \<not> typ_at' (koTypeOf (injectKOS ko)) p x; ksPSpace x p = Some b; ((), ba) \<in> fst (magnitudeCheck p (snd (lookupAround2 p (ksPSpace x))) (objBits ko) s''); is_aligned p (objBits ko); (uu_, s'') \<in> fst (projectKO b x)\<rbrakk> \<Longrightarrow> False
 2. \<And>x a b. \<lbrakk>updateObject ko = updateObject_default ko; 1 < 2 ^ objBits ko; \<not> typ_at' (koTypeOf (injectKOS ko)) p x; fst (lookupAround2 p (ksPSpace x)) = Some (a, b); \<forall>aa ba. (aa, ba) \<notin> fst (updateObject_default ko b p a (snd (lookupAround2 p (ksPSpace x))) x)\<rbrakk> \<Longrightarrow> snd (updateObject_default ko b p a (snd (lookupAround2 p (ksPSpace x))) x) proof (prove)
goal (2 subgoals):
 1. \<And>x b uu_. \<lbrakk>updateObject ko = updateObject_default ko; 1 < 2 ^ objBits ko; \<not> typ_at' (koTypeOf (injectKOS ko)) p x; ksPSpace x p = Some b; ps_clear p (objBits ko) x; is_aligned p (objBits ko); projectKO_opt b = Some uu_\<rbrakk> \<Longrightarrow> False
 2. \<And>x a b. \<lbrakk>updateObject ko = updateObject_default ko; 1 < 2 ^ objBits ko; \<not> typ_at' (koTypeOf (injectKOS ko)) p x; fst (lookupAround2 p (ksPSpace x)) = Some (a, b); \<forall>aa ba. (aa, ba) \<notin> fst (updateObject_default ko b p a (snd (lookupAround2 p (ksPSpace x))) x)\<rbrakk> \<Longrightarrow> snd (updateObject_default ko b p a (snd (lookupAround2 p (ksPSpace x))) x) proof (prove)
goal (2 subgoals):
 1. \<And>x b uu_. \<lbrakk>updateObject ko = updateObject_default ko; 1 < 2 ^ objBits ko; \<not> typ_at' (koTypeOf (injectKOS ko)) p x; ksPSpace x p = Some b; ps_clear p (objBits ko) x; is_aligned p (objBits ko); projectKO_opt b = Some uu_; koTypeOf b = koType TYPE('a)\<rbrakk> \<Longrightarrow> False
 2. \<And>x a b. \<lbrakk>updateObject ko = updateObject_default ko; 1 < 2 ^ objBits ko; \<not> typ_at' (koTypeOf (injectKOS ko)) p x; fst (lookupAround2 p (ksPSpace x)) = Some (a, b); \<forall>aa ba. (aa, ba) \<notin> fst (updateObject_default ko b p a (snd (lookupAround2 p (ksPSpace x))) x)\<rbrakk> \<Longrightarrow> snd (updateObject_default ko b p a (snd (lookupAround2 p (ksPSpace x))) x) proof (prove)
goal (2 subgoals):
 1. \<And>x b uu_. \<lbrakk>updateObject ko = updateObject_default ko; 1 < 2 ^ objBits ko; koType TYPE('a) = koTypeOf (injectKOS ko) \<longrightarrow> is_aligned p (objBitsKO b) \<longrightarrow> \<not> ps_clear p (objBitsKO b) x; ksPSpace x p = Some b; ps_clear p (objBits ko) x; is_aligned p (objBits ko); projectKO_opt b = Some uu_; koTypeOf b = koType TYPE('a)\<rbrakk> \<Longrightarrow> False
 2. \<And>x a b. \<lbrakk>updateObject ko = updateObject_default ko; 1 < 2 ^ objBits ko; \<not> typ_at' (koTypeOf (injectKOS ko)) p x; fst (lookupAround2 p (ksPSpace x)) = Some (a, b); \<forall>aa ba. (aa, ba) \<notin> fst (updateObject_default ko b p a (snd (lookupAround2 p (ksPSpace x))) x)\<rbrakk> \<Longrightarrow> snd (updateObject_default ko b p a (snd (lookupAround2 p (ksPSpace x))) x) proof (prove)
goal (2 subgoals):
 1. \<And>x b uu_. \<lbrakk>updateObject ko = updateObject_default ko; 1 < 2 ^ objBitsT (koTypeOf (injectKOS ko)); koType TYPE('a) = koTypeOf (injectKOS ko) \<longrightarrow> is_aligned p (objBitsT (koType TYPE('a))) \<longrightarrow> \<not> ps_clear p (objBitsT (koType TYPE('a))) x; ksPSpace x p = Some b; ps_clear p (objBitsT (koTypeOf (injectKOS ko))) x; is_aligned p (objBitsT (koTypeOf (injectKOS ko))); projectKO_opt b = Some uu_; koTypeOf b = koType TYPE('a)\<rbrakk> \<Longrightarrow> False
 2. \<And>x a b. \<lbrakk>updateObject ko = updateObject_default ko; 1 < 2 ^ objBits ko; \<not> typ_at' (koTypeOf (injectKOS ko)) p x; fst (lookupAround2 p (ksPSpace x)) = Some (a, b); \<forall>aa ba. (aa, ba) \<notin> fst (updateObject_default ko b p a (snd (lookupAround2 p (ksPSpace x))) x)\<rbrakk> \<Longrightarrow> snd (updateObject_default ko b p a (snd (lookupAround2 p (ksPSpace x))) x) proof (prove)
goal (2 subgoals):
 1. \<And>x b uu_. \<lbrakk>updateObject ko = updateObject_default ko; 1 < 2 ^ objBitsKO (injectKOS ko); koType TYPE('a) \<noteq> koTypeOf (injectKOS ko); ksPSpace x p = Some b; ps_clear p (objBitsKO (injectKOS ko)) x; is_aligned p (objBitsKO (injectKOS ko)); projectKO_opt b = Some uu_; koTypeOf b = koType TYPE('a)\<rbrakk> \<Longrightarrow> False
 2. \<And>x a b. \<lbrakk>updateObject ko = updateObject_default ko; 1 < 2 ^ objBits ko; \<not> typ_at' (koTypeOf (injectKOS ko)) p x; fst (lookupAround2 p (ksPSpace x)) = Some (a, b); \<forall>aa ba. (aa, ba) \<notin> fst (updateObject_default ko b p a (snd (lookupAround2 p (ksPSpace x))) x)\<rbrakk> \<Longrightarrow> snd (updateObject_default ko b p a (snd (lookupAround2 p (ksPSpace x))) x) proof (prove)
goal (1 subgoal):
 1. \<And>x a b. \<lbrakk>updateObject ko = updateObject_default ko; 1 < 2 ^ objBits ko; \<not> typ_at' (koTypeOf (injectKOS ko)) p x; fst (lookupAround2 p (ksPSpace x)) = Some (a, b); \<forall>aa ba. (aa, ba) \<notin> fst (updateObject_default ko b p a (snd (lookupAround2 p (ksPSpace x))) x)\<rbrakk> \<Longrightarrow> snd (updateObject_default ko b p a (snd (lookupAround2 p (ksPSpace x))) x) proof (prove)
goal (1 subgoal):
 1. \<And>x a b. \<lbrakk>updateObject ko = updateObject_default ko; 1 < 2 ^ objBits ko; \<not> typ_at' (koTypeOf (injectKOS ko)) p x; fst (lookupAround2 p (ksPSpace x)) = Some (a, b); \<forall>aa ba. (aa, ba) \<notin> fst (updateObject_default ko b p a (snd (lookupAround2 p (ksPSpace x))) x)\<rbrakk> \<Longrightarrow> fst (updateObject_default ko b p a (snd (lookupAround2 p (ksPSpace x))) x) = {} proof (prove)
goal (1 subgoal):
 1. \<And>x a b xa. \<lbrakk>updateObject ko = updateObject_default ko; 1 < 2 ^ objBits ko; \<not> typ_at' (koTypeOf (injectKOS ko)) p x; fst (lookupAround2 p (ksPSpace x)) = Some (a, b); \<forall>aa ba. (aa, ba) \<notin> fst (updateObject_default ko b p a (snd (lookupAround2 p (ksPSpace x))) x); xa \<in> fst (updateObject_default ko b p a (snd (lookupAround2 p (ksPSpace x))) x)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!