theory IsolatedThreadAction

lemma setObject_modify:
  fixes v :: "'a :: pspace_storable" shows
  "\<lbrakk> obj_at' (P :: 'a \<Rightarrow> bool) p s; updateObject v = updateObject_default v;
         (1 :: word32) < 2 ^ objBits v \<rbrakk>
    \<Longrightarrow> setObject p v s
      = modify (ksPSpace_update (\<lambda>ps. ps (p \<mapsto> injectKO v))) s" apply (clarsimp simp: setObject_def split_def exec_gets
                        obj_at'_def projectKOs lookupAround2_known1
                        assert_opt_def updateObject_default_def
                        bind_assoc) apply (simp add: projectKO_def alignCheck_assert) apply (simp add: project_inject objBits_def) apply (clarsimp simp only: objBitsT_koTypeOf[symmetric] koTypeOf_injectKO) apply (frule(2) in_magnitude_check[where s'=s]) apply (simp add: magnitudeCheck_assert in_monad) apply (simp add: simpler_modify_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>obj_at' P p s; updateObject v = updateObject_default v; 1 < 2 ^ objBits v\<rbrakk> \<Longrightarrow> setObject p v s = modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> injectKOS v))) s proof (prove)
goal (1 subgoal):
 1. \<And>ko obj. \<lbrakk>updateObject v = updateObject_default v; 1 < 2 ^ objBits v; ksPSpace s p = Some ko; is_aligned p (objBitsKO ko); projectKO_opt ko = Some obj; P obj; ps_clear p (objBitsKO ko) s\<rbrakk> \<Longrightarrow> (do x <- projectKO ko;
x <- alignCheck p (objBits v);
y <- magnitudeCheck p (snd (lookupAround2 p (ksPSpace s))) (objBits v);
modify (ksPSpace_update (\<lambda>_. (ksPSpace s)(p \<mapsto> injectKOS v)))
od) s = modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> injectKOS v))) s proof (prove)
goal (1 subgoal):
 1. \<And>ko obj. \<lbrakk>updateObject v = updateObject_default v; 1 < 2 ^ objBits v; ksPSpace s p = Some ko; is_aligned p (objBitsKO ko); projectKO_opt ko = Some obj; P obj; ps_clear p (objBitsKO ko) s\<rbrakk> \<Longrightarrow> (do x <- assert (is_aligned p (objBits v));
y <- magnitudeCheck p (snd (lookupAround2 p (ksPSpace s))) (objBits v);
modify (ksPSpace_update (\<lambda>_. (ksPSpace s)(p \<mapsto> injectKOS v)))
od) s = modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> injectKOS v))) s proof (prove)
goal (1 subgoal):
 1. \<And>ko obj. \<lbrakk>updateObject v = updateObject_default v; 1 < 2 ^ objBitsKO (injectKOS v); ksPSpace s p = Some ko; is_aligned p (objBitsKO ko); injectKOS obj = ko; P obj; ps_clear p (objBitsKO ko) s\<rbrakk> \<Longrightarrow> (do x <- assert (is_aligned p (objBitsKO (injectKOS v)));
y <- magnitudeCheck p (snd (lookupAround2 p (ksPSpace s))) (objBitsKO (injectKOS v));
modify (ksPSpace_update (\<lambda>_. (ksPSpace s)(p \<mapsto> injectKOS v)))
od) s = modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> injectKOS v))) s proof (prove)
goal (1 subgoal):
 1. \<And>ko obj. \<lbrakk>updateObject v = updateObject_default v; 1 < 2 ^ objBitsT (koType TYPE('a)); ksPSpace s p = Some (injectKOS obj); is_aligned p (objBitsT (koType TYPE('a))); P obj; ps_clear p (objBitsT (koType TYPE('a))) s\<rbrakk> \<Longrightarrow> (do x <- assert True;
y <- magnitudeCheck p (snd (lookupAround2 p (ksPSpace s))) (objBitsT (koType TYPE('a)));
modify (ksPSpace_update (\<lambda>_. (ksPSpace s)(p \<mapsto> injectKOS v)))
od) s = modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> injectKOS v))) s proof (prove)
goal (1 subgoal):
 1. \<And>ko obj. \<lbrakk>updateObject v = updateObject_default v; 1 < 2 ^ objBitsT (koType TYPE('a)); ksPSpace s p = Some (injectKOS obj); is_aligned p (objBitsT (koType TYPE('a))); P obj; ps_clear p (objBitsT (koType TYPE('a))) s; ((?v23 ko obj, s) \<in> fst (magnitudeCheck p (snd (lookupAround2 p (ksPSpace s))) (objBitsT (koType TYPE('a))) s)) = (s = s \<and> ps_clear p (objBitsT (koType TYPE('a))) s)\<rbrakk> \<Longrightarrow> (do x <- assert True;
y <- magnitudeCheck p (snd (lookupAround2 p (ksPSpace s))) (objBitsT (koType TYPE('a)));
modify (ksPSpace_update (\<lambda>_. (ksPSpace s)(p \<mapsto> injectKOS v)))
od) s = modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> injectKOS v))) s proof (prove)
goal (1 subgoal):
 1. \<And>obj. \<lbrakk>updateObject v = updateObject_default v; 1 < 2 ^ objBitsT (koType TYPE('a)); ksPSpace s p = Some (injectKOS obj); is_aligned p (objBitsT (koType TYPE('a))); P obj; ps_clear p (objBitsT (koType TYPE('a))) s; case snd (lookupAround2 p (ksPSpace s)) of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBitsT (koType TYPE('a)) \<le> z - p\<rbrakk> \<Longrightarrow> modify (ksPSpace_update (\<lambda>_. (ksPSpace s)(p \<mapsto> injectKOS v))) s = modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> injectKOS v))) s proof (prove)
goal:
No subgoals!