theory SR_lemmas_C

lemma setObject_eq:
  fixes ko :: "('a :: pspace_storable)"
  assumes x: "\<And>(val :: 'a) old ptr ptr' next. updateObject val old ptr ptr' next =
                (updateObject_default val old ptr ptr' next :: kernel_object kernel)"
  assumes P: "\<And>(v::'a::pspace_storable). (1 :: word32) < 2 ^ (objBits v)"
  and     ob: "\<And>(v :: 'a) (v' :: 'a). objBits v = objBits v'"
  and objat: "obj_at' (P :: ('a::pspace_storable \<Rightarrow> bool)) p s"
  shows  "((), s\<lparr> ksPSpace := (ksPSpace s)(p \<mapsto> injectKO ko)\<rparr>) \<in> fst (setObject p ko s)" using objat unfolding setObject_def obj_at'_def apply (clarsimp simp: updateObject_default_def in_monad return_def lookupAround2_char1
                        split_def x P lookupAround2_char1 projectKOs
                        objBits_def[symmetric] in_magnitude_check project_inject) apply (frule ssubst [OF ob, where P = "is_aligned p" and v1 = ko]) apply (simp add: P in_magnitude_check) apply (rule conjI) apply (rule_tac x = obj in exI) apply simp apply (erule ssubst [OF ob]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((), s\<lparr>ksPSpace := (ksPSpace s)(p \<mapsto> injectKOS ko)\<rparr>) \<in> fst (setObject p ko s) proof (prove)
using this:
obj_at' P p s

goal (1 subgoal):
 1. ((), s\<lparr>ksPSpace := (ksPSpace s)(p \<mapsto> injectKOS ko)\<rparr>) \<in> fst (setObject p ko s) proof (prove)
using this:
\<exists>ko obj. ksPSpace s p = Some ko \<and> is_aligned p (objBitsKO ko) \<and> fst (projectKO ko s) = {(obj, s)} \<and> P obj \<and> ps_clear p (objBitsKO ko) s

goal (1 subgoal):
 1. ((), s\<lparr>ksPSpace := (ksPSpace s)(p \<mapsto> injectKOS ko)\<rparr>) \<in> fst ((do ps <- gets ksPSpace;
map <- return (psMap ps);
(before, after) <- return (lookupAround2 (fromPPtr p) map);
(ptr', obj) <- maybeToMonad before;
obj' <- updateObject ko obj (fromPPtr p) ptr' after;
map' <- return (data_map_insert ptr' obj' map);
ps' <- return (psMap_update (\<lambda>_. map') ps);
modify (ksPSpace_update (\<lambda>_. ps'))
od) s) proof (prove)
goal (1 subgoal):
 1. \<And>obj. \<lbrakk>ksPSpace s p = Some (injectKOS obj); is_aligned p (objBits obj); P obj; ps_clear p (objBits obj) s\<rbrakk> \<Longrightarrow> (\<exists>uu_. injectKOS uu_ = injectKOS obj) \<and> is_aligned p (objBits ko) \<and> (\<exists>s''. ((), s'') \<in> fst (magnitudeCheck p (snd (lookupAround2 p (ksPSpace s))) (objBits ko) s) \<and> s\<lparr>ksPSpace := (ksPSpace s)(p \<mapsto> injectKOS ko)\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(p \<mapsto> injectKOS ko)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>obj. \<lbrakk>ksPSpace s p = Some (injectKOS obj); is_aligned p (objBits obj); P obj; ps_clear p (objBits obj) s; is_aligned p (objBits ko)\<rbrakk> \<Longrightarrow> (\<exists>uu_. injectKOS uu_ = injectKOS obj) \<and> is_aligned p (objBits ko) \<and> (\<exists>s''. ((), s'') \<in> fst (magnitudeCheck p (snd (lookupAround2 p (ksPSpace s))) (objBits ko) s) \<and> s\<lparr>ksPSpace := (ksPSpace s)(p \<mapsto> injectKOS ko)\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(p \<mapsto> injectKOS ko)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>obj. \<lbrakk>ksPSpace s p = Some (injectKOS obj); is_aligned p (objBits obj); P obj; ps_clear p (objBits obj) s; is_aligned p (objBits ko)\<rbrakk> \<Longrightarrow> (\<exists>uu_. injectKOS uu_ = injectKOS obj) \<and> ps_clear p (objBits ko) s proof (prove)
goal (2 subgoals):
 1. \<And>obj. \<lbrakk>ksPSpace s p = Some (injectKOS obj); is_aligned p (objBits obj); P obj; ps_clear p (objBits obj) s; is_aligned p (objBits ko)\<rbrakk> \<Longrightarrow> \<exists>uu_. injectKOS uu_ = injectKOS obj
 2. \<And>obj. \<lbrakk>ksPSpace s p = Some (injectKOS obj); is_aligned p (objBits obj); P obj; ps_clear p (objBits obj) s; is_aligned p (objBits ko)\<rbrakk> \<Longrightarrow> ps_clear p (objBits ko) s proof (prove)
goal (2 subgoals):
 1. \<And>obj. \<lbrakk>ksPSpace s p = Some (injectKOS obj); is_aligned p (objBits obj); P obj; ps_clear p (objBits obj) s; is_aligned p (objBits ko)\<rbrakk> \<Longrightarrow> injectKOS obj = injectKOS obj
 2. \<And>obj. \<lbrakk>ksPSpace s p = Some (injectKOS obj); is_aligned p (objBits obj); P obj; ps_clear p (objBits obj) s; is_aligned p (objBits ko)\<rbrakk> \<Longrightarrow> ps_clear p (objBits ko) s proof (prove)
goal (1 subgoal):
 1. \<And>obj. \<lbrakk>ksPSpace s p = Some (injectKOS obj); is_aligned p (objBits obj); P obj; ps_clear p (objBits obj) s; is_aligned p (objBits ko)\<rbrakk> \<Longrightarrow> ps_clear p (objBits ko) s proof (prove)
goal:
No subgoals!