theory Detype_R

lemma placeNewObject_modify_commute:
  "monad_commute
     (K (is_aligned ptr (objBitsKO (injectKOS val) + us) \<and>
         objBitsKO (injectKOS val) + us < word_bits) and
      pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) and
      pspace_aligned' and ko_wp_at' (\<lambda>a. objBitsKO (f (Some a)) = objBitsKO a) ptr')
     (placeNewObject ptr val us)
     (modify (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr')))))" apply (clarsimp simp:monad_commute_def simpler_modify_def
    bind_def split_def return_def) apply (subst simpler_placeNewObject_def) apply ((simp add:range_cover_def)+)[4] apply (clarsimp simp: simpler_modify_def) apply (frule(1) range_cover_full) apply (simp add: simpler_placeNewObject_def) apply (subgoal_tac "pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us)
            (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)") prefer 2 apply (clarsimp simp:ko_wp_at'_def) apply (subst pspace_no_overlap'_def) apply (intro allI impI) apply (case_tac "x = ptr'") apply (subgoal_tac "objBitsKO koa = objBitsKO ko") apply (drule(1) pspace_no_overlapD') apply (clarsimp simp:field_simps) apply (clarsimp) apply (drule_tac x = x and s = s in pspace_no_overlapD'[rotated]) apply (simp) apply (clarsimp simp:field_simps) apply (subgoal_tac "pspace_aligned'
    (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)") prefer 2 apply (subst pspace_aligned'_def) apply (rule ballI) apply (erule domE) apply (clarsimp simp:ko_wp_at'_def split:if_split_asm) apply (drule(1) pspace_alignedD')+ apply simp apply (simp add:simpler_placeNewObject_def) apply (clarsimp simp:simpler_modify_def Fun.comp_def
      singleton_iff image_def) apply (intro conjI update_ksPSpaceI ext) apply (clarsimp simp:ko_wp_at'_def foldr_upd_app_if) apply (frule(1) pspace_no_overlapD') apply (drule subsetD[rotated]) apply (rule new_cap_addrs_subset) apply (erule range_cover_rel) apply simp apply simp apply (drule_tac x = ptr' in in_empty_interE) apply (clarsimp simp:is_aligned_no_overflow) apply (clarsimp simp:range_cover_def ptr_add_def
     is_aligned_neg_mask_eq obj_range'_def p_assoc_help) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monad_commute (K (is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> objBitsKO (injectKOS val) + us < word_bits) and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) and pspace_aligned' and ko_wp_at' (\<lambda>a. objBitsKO (f (Some a)) = objBitsKO a) ptr') (placeNewObject ptr val us) (modify (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))))) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; ko_wp_at' (\<lambda>a. objBitsKO (f (Some a)) = objBitsKO a) ptr' s\<rbrakk> \<Longrightarrow> (\<Union>x\<in>fst (placeNewObject ptr val us s). {(((), ()), ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) (snd x))}) = (\<Union>x\<in>fst (placeNewObject ptr val us (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)). {(((), ()), snd x)}) \<and> snd (placeNewObject ptr val us s) = snd (placeNewObject ptr val us (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)) proof (prove)
goal (5 subgoals):
 1. \<And>s. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; ko_wp_at' (\<lambda>a. objBitsKO (f (Some a)) = objBitsKO a) ptr' s\<rbrakk> \<Longrightarrow> us < word_bits
 2. \<And>s. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; ko_wp_at' (\<lambda>a. objBitsKO (f (Some a)) = objBitsKO a) ptr' s\<rbrakk> \<Longrightarrow> is_aligned ptr (objBitsKO (injectKOS val) + us)
 3. \<And>s. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; ko_wp_at' (\<lambda>a. objBitsKO (f (Some a)) = objBitsKO a) ptr' s\<rbrakk> \<Longrightarrow> pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s
 4. \<And>s. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; ko_wp_at' (\<lambda>a. objBitsKO (f (Some a)) = objBitsKO a) ptr' s\<rbrakk> \<Longrightarrow> pspace_aligned' s
 5. \<And>s. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; ko_wp_at' (\<lambda>a. objBitsKO (f (Some a)) = objBitsKO a) ptr' s\<rbrakk> \<Longrightarrow> (\<Union>x\<in>fst (modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s). {(((), ()), ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) (snd x))}) = (\<Union>x\<in>fst (placeNewObject ptr val us (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)). {(((), ()), snd x)}) \<and> snd (placeNewObject ptr val us s) = snd (placeNewObject ptr val us (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; ko_wp_at' (\<lambda>a. objBitsKO (f (Some a)) = objBitsKO a) ptr' s\<rbrakk> \<Longrightarrow> (\<Union>x\<in>fst (modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s). {(((), ()), ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) (snd x))}) = (\<Union>x\<in>fst (placeNewObject ptr val us (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)). {(((), ()), snd x)}) \<and> snd (placeNewObject ptr val us s) = snd (placeNewObject ptr val us (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; ko_wp_at' (\<lambda>a. objBitsKO (f (Some a)) = objBitsKO a) ptr' s\<rbrakk> \<Longrightarrow> {(((), ()), ksPSpace_update ((\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) \<circ> (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s)} = (\<Union>x\<in>fst (placeNewObject ptr val us (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)). {(((), ()), snd x)}) \<and> snd (placeNewObject ptr val us s) = snd (placeNewObject ptr val us (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; ko_wp_at' (\<lambda>a. objBitsKO (f (Some a)) = objBitsKO a) ptr' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0)\<rbrakk> \<Longrightarrow> {(((), ()), ksPSpace_update ((\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) \<circ> (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s)} = (\<Union>x\<in>fst (placeNewObject ptr val us (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)). {(((), ()), snd x)}) \<and> snd (placeNewObject ptr val us s) = snd (placeNewObject ptr val us (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; ko_wp_at' (\<lambda>a. objBitsKO (f (Some a)) = objBitsKO a) ptr' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0)\<rbrakk> \<Longrightarrow> {(((), ()), ksPSpace_update ((\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) \<circ> (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s)} = (\<Union>x\<in>fst (placeNewObject ptr val us (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)). {(((), ()), snd x)}) \<and> snd (modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s) = snd (placeNewObject ptr val us (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; ko_wp_at' (\<lambda>a. objBitsKO (f (Some a)) = objBitsKO a) ptr' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)\<rbrakk> \<Longrightarrow> {(((), ()), ksPSpace_update ((\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) \<circ> (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s)} = (\<Union>x\<in>fst (placeNewObject ptr val us (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)). {(((), ()), snd x)}) \<and> snd (modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s) = snd (placeNewObject ptr val us (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s))
 2. \<And>s. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; ko_wp_at' (\<lambda>a. objBitsKO (f (Some a)) = objBitsKO a) ptr' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0)\<rbrakk> \<Longrightarrow> pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; ko_wp_at' (\<lambda>a. objBitsKO (f (Some a)) = objBitsKO a) ptr' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0)\<rbrakk> \<Longrightarrow> pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)
 2. \<And>s. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; ko_wp_at' (\<lambda>a. objBitsKO (f (Some a)) = objBitsKO a) ptr' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)\<rbrakk> \<Longrightarrow> {(((), ()), ksPSpace_update ((\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) \<circ> (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s)} = (\<Union>x\<in>fst (placeNewObject ptr val us (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)). {(((), ()), snd x)}) \<and> snd (modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s) = snd (placeNewObject ptr val us (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)) proof (prove)
goal (2 subgoals):
 1. \<And>s ko. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0); ksPSpace s ptr' = Some ko; is_aligned ptr' (objBitsKO ko); objBitsKO (f (Some ko)) = objBitsKO ko; ps_clear ptr' (objBitsKO ko) s\<rbrakk> \<Longrightarrow> pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)
 2. \<And>s. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; ko_wp_at' (\<lambda>a. objBitsKO (f (Some a)) = objBitsKO a) ptr' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)\<rbrakk> \<Longrightarrow> {(((), ()), ksPSpace_update ((\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) \<circ> (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s)} = (\<Union>x\<in>fst (placeNewObject ptr val us (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)). {(((), ()), snd x)}) \<and> snd (modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s) = snd (placeNewObject ptr val us (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)) proof (prove)
goal (2 subgoals):
 1. \<And>s ko. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0); ksPSpace s ptr' = Some ko; is_aligned ptr' (objBitsKO ko); objBitsKO (f (Some ko)) = objBitsKO ko; ps_clear ptr' (objBitsKO ko) s\<rbrakk> \<Longrightarrow> \<forall>x ko. ksPSpace (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s) x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> up_aligned_area ptr (objBitsKO (injectKOS val) + us) = {}
 2. \<And>s. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; ko_wp_at' (\<lambda>a. objBitsKO (f (Some a)) = objBitsKO a) ptr' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)\<rbrakk> \<Longrightarrow> {(((), ()), ksPSpace_update ((\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) \<circ> (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s)} = (\<Union>x\<in>fst (placeNewObject ptr val us (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)). {(((), ()), snd x)}) \<and> snd (modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s) = snd (placeNewObject ptr val us (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)) proof (prove)
goal (2 subgoals):
 1. \<And>s ko x koa. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0); ksPSpace s ptr' = Some ko; is_aligned ptr' (objBitsKO ko); objBitsKO (f (Some ko)) = objBitsKO ko; ps_clear ptr' (objBitsKO ko) s; ksPSpace (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s) x = Some koa\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO koa - 1} \<inter> up_aligned_area ptr (objBitsKO (injectKOS val) + us) = {}
 2. \<And>s. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; ko_wp_at' (\<lambda>a. objBitsKO (f (Some a)) = objBitsKO a) ptr' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)\<rbrakk> \<Longrightarrow> {(((), ()), ksPSpace_update ((\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) \<circ> (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s)} = (\<Union>x\<in>fst (placeNewObject ptr val us (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)). {(((), ()), snd x)}) \<and> snd (modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s) = snd (placeNewObject ptr val us (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)) proof (prove)
goal (3 subgoals):
 1. \<And>s ko x koa. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0); ksPSpace s ptr' = Some ko; is_aligned ptr' (objBitsKO ko); objBitsKO (f (Some ko)) = objBitsKO ko; ps_clear ptr' (objBitsKO ko) s; ksPSpace (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s) x = Some koa; x = ptr'\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO koa - 1} \<inter> up_aligned_area ptr (objBitsKO (injectKOS val) + us) = {}
 2. \<And>s ko x koa. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0); ksPSpace s ptr' = Some ko; is_aligned ptr' (objBitsKO ko); objBitsKO (f (Some ko)) = objBitsKO ko; ps_clear ptr' (objBitsKO ko) s; ksPSpace (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s) x = Some koa; x \<noteq> ptr'\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO koa - 1} \<inter> up_aligned_area ptr (objBitsKO (injectKOS val) + us) = {}
 3. \<And>s. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; ko_wp_at' (\<lambda>a. objBitsKO (f (Some a)) = objBitsKO a) ptr' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)\<rbrakk> \<Longrightarrow> {(((), ()), ksPSpace_update ((\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) \<circ> (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s)} = (\<Union>x\<in>fst (placeNewObject ptr val us (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)). {(((), ()), snd x)}) \<and> snd (modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s) = snd (placeNewObject ptr val us (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)) proof (prove)
goal (4 subgoals):
 1. \<And>s ko x koa. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0); ksPSpace s ptr' = Some ko; is_aligned ptr' (objBitsKO ko); objBitsKO (f (Some ko)) = objBitsKO ko; ps_clear ptr' (objBitsKO ko) s; ksPSpace (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s) x = Some koa; x = ptr'; objBitsKO koa = objBitsKO ko\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO koa - 1} \<inter> up_aligned_area ptr (objBitsKO (injectKOS val) + us) = {}
 2. \<And>s ko x koa. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0); ksPSpace s ptr' = Some ko; is_aligned ptr' (objBitsKO ko); objBitsKO (f (Some ko)) = objBitsKO ko; ps_clear ptr' (objBitsKO ko) s; ksPSpace (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s) x = Some koa; x = ptr'\<rbrakk> \<Longrightarrow> objBitsKO koa = objBitsKO ko
 3. \<And>s ko x koa. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0); ksPSpace s ptr' = Some ko; is_aligned ptr' (objBitsKO ko); objBitsKO (f (Some ko)) = objBitsKO ko; ps_clear ptr' (objBitsKO ko) s; ksPSpace (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s) x = Some koa; x \<noteq> ptr'\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO koa - 1} \<inter> up_aligned_area ptr (objBitsKO (injectKOS val) + us) = {}
 4. \<And>s. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; ko_wp_at' (\<lambda>a. objBitsKO (f (Some a)) = objBitsKO a) ptr' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)\<rbrakk> \<Longrightarrow> {(((), ()), ksPSpace_update ((\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) \<circ> (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s)} = (\<Union>x\<in>fst (placeNewObject ptr val us (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)). {(((), ()), snd x)}) \<and> snd (modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s) = snd (placeNewObject ptr val us (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)) proof (prove)
goal (4 subgoals):
 1. \<And>s ko x koa. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0); is_aligned ptr' (objBitsKO ko); objBitsKO (f (Some ko)) = objBitsKO ko; ps_clear ptr' (objBitsKO ko) s; ksPSpace (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s) x = Some koa; x = ptr'; objBitsKO koa = objBitsKO ko; {ptr'..ptr' + 2 ^ objBitsKO ko - 1} \<inter> {ptr..(ptr && ~~ mask (objBitsKO (injectKOS val) + us)) + 2 ^ (objBitsKO (injectKOS val) + us) - 1} = {}\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO koa - 1} \<inter> up_aligned_area ptr (objBitsKO (injectKOS val) + us) = {}
 2. \<And>s ko x koa. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0); ksPSpace s ptr' = Some ko; is_aligned ptr' (objBitsKO ko); objBitsKO (f (Some ko)) = objBitsKO ko; ps_clear ptr' (objBitsKO ko) s; ksPSpace (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s) x = Some koa; x = ptr'\<rbrakk> \<Longrightarrow> objBitsKO koa = objBitsKO ko
 3. \<And>s ko x koa. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0); ksPSpace s ptr' = Some ko; is_aligned ptr' (objBitsKO ko); objBitsKO (f (Some ko)) = objBitsKO ko; ps_clear ptr' (objBitsKO ko) s; ksPSpace (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s) x = Some koa; x \<noteq> ptr'\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO koa - 1} \<inter> up_aligned_area ptr (objBitsKO (injectKOS val) + us) = {}
 4. \<And>s. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; ko_wp_at' (\<lambda>a. objBitsKO (f (Some a)) = objBitsKO a) ptr' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)\<rbrakk> \<Longrightarrow> {(((), ()), ksPSpace_update ((\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) \<circ> (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s)} = (\<Union>x\<in>fst (placeNewObject ptr val us (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)). {(((), ()), snd x)}) \<and> snd (modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s) = snd (placeNewObject ptr val us (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)) proof (prove)
goal (3 subgoals):
 1. \<And>s ko x koa. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0); ksPSpace s ptr' = Some ko; is_aligned ptr' (objBitsKO ko); objBitsKO (f (Some ko)) = objBitsKO ko; ps_clear ptr' (objBitsKO ko) s; ksPSpace (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s) x = Some koa; x = ptr'\<rbrakk> \<Longrightarrow> objBitsKO koa = objBitsKO ko
 2. \<And>s ko x koa. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0); ksPSpace s ptr' = Some ko; is_aligned ptr' (objBitsKO ko); objBitsKO (f (Some ko)) = objBitsKO ko; ps_clear ptr' (objBitsKO ko) s; ksPSpace (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s) x = Some koa; x \<noteq> ptr'\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO koa - 1} \<inter> up_aligned_area ptr (objBitsKO (injectKOS val) + us) = {}
 3. \<And>s. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; ko_wp_at' (\<lambda>a. objBitsKO (f (Some a)) = objBitsKO a) ptr' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)\<rbrakk> \<Longrightarrow> {(((), ()), ksPSpace_update ((\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) \<circ> (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s)} = (\<Union>x\<in>fst (placeNewObject ptr val us (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)). {(((), ()), snd x)}) \<and> snd (modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s) = snd (placeNewObject ptr val us (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)) proof (prove)
goal (2 subgoals):
 1. \<And>s ko x koa. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0); ksPSpace s ptr' = Some ko; is_aligned ptr' (objBitsKO ko); objBitsKO (f (Some ko)) = objBitsKO ko; ps_clear ptr' (objBitsKO ko) s; ksPSpace (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s) x = Some koa; x \<noteq> ptr'\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO koa - 1} \<inter> up_aligned_area ptr (objBitsKO (injectKOS val) + us) = {}
 2. \<And>s. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; ko_wp_at' (\<lambda>a. objBitsKO (f (Some a)) = objBitsKO a) ptr' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)\<rbrakk> \<Longrightarrow> {(((), ()), ksPSpace_update ((\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) \<circ> (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s)} = (\<Union>x\<in>fst (placeNewObject ptr val us (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)). {(((), ()), snd x)}) \<and> snd (modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s) = snd (placeNewObject ptr val us (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)) proof (prove)
goal (3 subgoals):
 1. \<And>s ko x koa. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_aligned' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0); ksPSpace s ptr' = Some ko; is_aligned ptr' (objBitsKO ko); objBitsKO (f (Some ko)) = objBitsKO ko; ps_clear ptr' (objBitsKO ko) s; ksPSpace (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s) x = Some koa; x \<noteq> ptr'\<rbrakk> \<Longrightarrow> ksPSpace s x = Some (?ko55 s ko x koa)
 2. \<And>s ko x koa. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_aligned' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0); ksPSpace s ptr' = Some ko; is_aligned ptr' (objBitsKO ko); objBitsKO (f (Some ko)) = objBitsKO ko; ps_clear ptr' (objBitsKO ko) s; ksPSpace (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s) x = Some koa; x \<noteq> ptr'; {x..x + 2 ^ objBitsKO (?ko55 s ko x koa) - 1} \<inter> {ptr..(ptr && ~~ mask (objBitsKO (injectKOS val) + us)) + 2 ^ (objBitsKO (injectKOS val) + us) - 1} = {}\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO koa - 1} \<inter> up_aligned_area ptr (objBitsKO (injectKOS val) + us) = {}
 3. \<And>s. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; ko_wp_at' (\<lambda>a. objBitsKO (f (Some a)) = objBitsKO a) ptr' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)\<rbrakk> \<Longrightarrow> {(((), ()), ksPSpace_update ((\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) \<circ> (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s)} = (\<Union>x\<in>fst (placeNewObject ptr val us (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)). {(((), ()), snd x)}) \<and> snd (modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s) = snd (placeNewObject ptr val us (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)) proof (prove)
goal (2 subgoals):
 1. \<And>s ko x koa. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_aligned' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0); ksPSpace s ptr' = Some ko; is_aligned ptr' (objBitsKO ko); objBitsKO (f (Some ko)) = objBitsKO ko; ps_clear ptr' (objBitsKO ko) s; ksPSpace (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s) x = Some koa; x \<noteq> ptr'; {x..x + 2 ^ objBitsKO koa - 1} \<inter> {ptr..(ptr && ~~ mask (objBitsKO (injectKOS val) + us)) + 2 ^ (objBitsKO (injectKOS val) + us) - 1} = {}\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO koa - 1} \<inter> up_aligned_area ptr (objBitsKO (injectKOS val) + us) = {}
 2. \<And>s. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; ko_wp_at' (\<lambda>a. objBitsKO (f (Some a)) = objBitsKO a) ptr' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)\<rbrakk> \<Longrightarrow> {(((), ()), ksPSpace_update ((\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) \<circ> (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s)} = (\<Union>x\<in>fst (placeNewObject ptr val us (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)). {(((), ()), snd x)}) \<and> snd (modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s) = snd (placeNewObject ptr val us (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; ko_wp_at' (\<lambda>a. objBitsKO (f (Some a)) = objBitsKO a) ptr' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)\<rbrakk> \<Longrightarrow> {(((), ()), ksPSpace_update ((\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) \<circ> (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s)} = (\<Union>x\<in>fst (placeNewObject ptr val us (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)). {(((), ()), snd x)}) \<and> snd (modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s) = snd (placeNewObject ptr val us (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; ko_wp_at' (\<lambda>a. objBitsKO (f (Some a)) = objBitsKO a) ptr' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s); pspace_aligned' (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)\<rbrakk> \<Longrightarrow> {(((), ()), ksPSpace_update ((\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) \<circ> (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s)} = (\<Union>x\<in>fst (placeNewObject ptr val us (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)). {(((), ()), snd x)}) \<and> snd (modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s) = snd (placeNewObject ptr val us (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s))
 2. \<And>s. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; ko_wp_at' (\<lambda>a. objBitsKO (f (Some a)) = objBitsKO a) ptr' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)\<rbrakk> \<Longrightarrow> pspace_aligned' (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; ko_wp_at' (\<lambda>a. objBitsKO (f (Some a)) = objBitsKO a) ptr' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)\<rbrakk> \<Longrightarrow> pspace_aligned' (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)
 2. \<And>s. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; ko_wp_at' (\<lambda>a. objBitsKO (f (Some a)) = objBitsKO a) ptr' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s); pspace_aligned' (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)\<rbrakk> \<Longrightarrow> {(((), ()), ksPSpace_update ((\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) \<circ> (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s)} = (\<Union>x\<in>fst (placeNewObject ptr val us (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)). {(((), ()), snd x)}) \<and> snd (modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s) = snd (placeNewObject ptr val us (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; ko_wp_at' (\<lambda>a. objBitsKO (f (Some a)) = objBitsKO a) ptr' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)\<rbrakk> \<Longrightarrow> \<forall>x\<in>dom (ksPSpace (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)). is_aligned x (objBitsKO (the (ksPSpace (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s) x)))
 2. \<And>s. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; ko_wp_at' (\<lambda>a. objBitsKO (f (Some a)) = objBitsKO a) ptr' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s); pspace_aligned' (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)\<rbrakk> \<Longrightarrow> {(((), ()), ksPSpace_update ((\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) \<circ> (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s)} = (\<Union>x\<in>fst (placeNewObject ptr val us (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)). {(((), ()), snd x)}) \<and> snd (modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s) = snd (placeNewObject ptr val us (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)) proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; ko_wp_at' (\<lambda>a. objBitsKO (f (Some a)) = objBitsKO a) ptr' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s); x \<in> dom (ksPSpace (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s))\<rbrakk> \<Longrightarrow> is_aligned x (objBitsKO (the (ksPSpace (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s) x)))
 2. \<And>s. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; ko_wp_at' (\<lambda>a. objBitsKO (f (Some a)) = objBitsKO a) ptr' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s); pspace_aligned' (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)\<rbrakk> \<Longrightarrow> {(((), ()), ksPSpace_update ((\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) \<circ> (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s)} = (\<Union>x\<in>fst (placeNewObject ptr val us (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)). {(((), ()), snd x)}) \<and> snd (modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s) = snd (placeNewObject ptr val us (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)) proof (prove)
goal (2 subgoals):
 1. \<And>s x r. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; ko_wp_at' (\<lambda>a. objBitsKO (f (Some a)) = objBitsKO a) ptr' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s); ksPSpace (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s) x = Some r\<rbrakk> \<Longrightarrow> is_aligned x (objBitsKO (the (ksPSpace (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s) x)))
 2. \<And>s. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; ko_wp_at' (\<lambda>a. objBitsKO (f (Some a)) = objBitsKO a) ptr' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s); pspace_aligned' (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)\<rbrakk> \<Longrightarrow> {(((), ()), ksPSpace_update ((\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) \<circ> (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s)} = (\<Union>x\<in>fst (placeNewObject ptr val us (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)). {(((), ()), snd x)}) \<and> snd (modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s) = snd (placeNewObject ptr val us (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)) proof (prove)
goal (2 subgoals):
 1. \<And>s x r ko. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s); x \<noteq> ptr'; ksPSpace s ptr' = Some ko; is_aligned ptr' (objBitsKO ko); objBitsKO (f (Some ko)) = objBitsKO ko; ps_clear ptr' (objBitsKO ko) s; ksPSpace s x = Some r\<rbrakk> \<Longrightarrow> is_aligned x (objBitsKO r)
 2. \<And>s. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; ko_wp_at' (\<lambda>a. objBitsKO (f (Some a)) = objBitsKO a) ptr' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s); pspace_aligned' (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)\<rbrakk> \<Longrightarrow> {(((), ()), ksPSpace_update ((\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) \<circ> (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s)} = (\<Union>x\<in>fst (placeNewObject ptr val us (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)). {(((), ()), snd x)}) \<and> snd (modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s) = snd (placeNewObject ptr val us (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)) proof (prove)
goal (2 subgoals):
 1. \<And>s x r ko. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s); x \<noteq> ptr'; is_aligned ptr' (objBitsKO ko); objBitsKO (f (Some ko)) = objBitsKO ko; ps_clear ptr' (objBitsKO ko) s; is_aligned ptr' (objBitsKO ko); is_aligned x (objBitsKO r)\<rbrakk> \<Longrightarrow> is_aligned x (objBitsKO r)
 2. \<And>s. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; ko_wp_at' (\<lambda>a. objBitsKO (f (Some a)) = objBitsKO a) ptr' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s); pspace_aligned' (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)\<rbrakk> \<Longrightarrow> {(((), ()), ksPSpace_update ((\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) \<circ> (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s)} = (\<Union>x\<in>fst (placeNewObject ptr val us (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)). {(((), ()), snd x)}) \<and> snd (modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s) = snd (placeNewObject ptr val us (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; ko_wp_at' (\<lambda>a. objBitsKO (f (Some a)) = objBitsKO a) ptr' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s); pspace_aligned' (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)\<rbrakk> \<Longrightarrow> {(((), ()), ksPSpace_update ((\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) \<circ> (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s)} = (\<Union>x\<in>fst (placeNewObject ptr val us (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)). {(((), ()), snd x)}) \<and> snd (modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s) = snd (placeNewObject ptr val us (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; ko_wp_at' (\<lambda>a. objBitsKO (f (Some a)) = objBitsKO a) ptr' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s); pspace_aligned' (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)\<rbrakk> \<Longrightarrow> {(((), ()), ksPSpace_update ((\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) \<circ> (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s)} = (\<Union>x\<in>fst (modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) ((ksPSpace s)(ptr' \<mapsto> f (ksPSpace s ptr'))))) (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)). {(((), ()), snd x)}) \<and> snd (modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s) = snd (modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) ((ksPSpace s)(ptr' \<mapsto> f (ksPSpace s ptr'))))) (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; ko_wp_at' (\<lambda>a. objBitsKO (f (Some a)) = objBitsKO a) ptr' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s); pspace_aligned' (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)\<rbrakk> \<Longrightarrow> s\<lparr>ksPSpace := (foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))(ptr' \<mapsto> f (foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s) ptr'))\<rparr> = s\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) ((ksPSpace s)(ptr' \<mapsto> f (ksPSpace s ptr')))\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; ko_wp_at' (\<lambda>a. objBitsKO (f (Some a)) = objBitsKO a) ptr' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s); pspace_aligned' (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s)\<rbrakk> \<Longrightarrow> ((foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))(ptr' \<mapsto> f (foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s) ptr'))) x = foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) ((ksPSpace s)(ptr' \<mapsto> f (ksPSpace s ptr'))) x proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s); pspace_aligned' (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s); ksPSpace s ptr' = Some ko; is_aligned ptr' (objBitsKO ko); objBitsKO (f (Some ko)) = objBitsKO ko; ps_clear ptr' (objBitsKO ko) s; ptr' \<in> set (new_cap_addrs (2 ^ us) ptr (injectKOS val))\<rbrakk> \<Longrightarrow> f (Some (injectKOS val)) = injectKOS val proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s); pspace_aligned' (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s); ksPSpace s ptr' = Some ko; is_aligned ptr' (objBitsKO ko); objBitsKO (f (Some ko)) = objBitsKO ko; ps_clear ptr' (objBitsKO ko) s; ptr' \<in> set (new_cap_addrs (2 ^ us) ptr (injectKOS val)); {ptr'..ptr' + 2 ^ objBitsKO ko - 1} \<inter> {ptr..(ptr && ~~ mask (objBitsKO (injectKOS val) + us)) + 2 ^ (objBitsKO (injectKOS val) + us) - 1} = {}\<rbrakk> \<Longrightarrow> f (Some (injectKOS val)) = injectKOS val proof (prove)
goal (2 subgoals):
 1. \<And>s ko. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s); pspace_aligned' (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s); ksPSpace s ptr' = Some ko; is_aligned ptr' (objBitsKO ko); objBitsKO (f (Some ko)) = objBitsKO ko; ps_clear ptr' (objBitsKO ko) s; {ptr'..ptr' + 2 ^ objBitsKO ko - 1} \<inter> {ptr..(ptr && ~~ mask (objBitsKO (injectKOS val) + us)) + 2 ^ (objBitsKO (injectKOS val) + us) - 1} = {}\<rbrakk> \<Longrightarrow> set (new_cap_addrs (2 ^ us) ptr (injectKOS val)) \<subseteq> ?B114 s ko
 2. \<And>s ko. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s); pspace_aligned' (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s); ksPSpace s ptr' = Some ko; is_aligned ptr' (objBitsKO ko); objBitsKO (f (Some ko)) = objBitsKO ko; ps_clear ptr' (objBitsKO ko) s; {ptr'..ptr' + 2 ^ objBitsKO ko - 1} \<inter> {ptr..(ptr && ~~ mask (objBitsKO (injectKOS val) + us)) + 2 ^ (objBitsKO (injectKOS val) + us) - 1} = {}; ptr' \<in> ?B114 s ko\<rbrakk> \<Longrightarrow> f (Some (injectKOS val)) = injectKOS val proof (prove)
goal (2 subgoals):
 1. \<And>s ko. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s); pspace_aligned' (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s); ksPSpace s ptr' = Some ko; is_aligned ptr' (objBitsKO ko); objBitsKO (f (Some ko)) = objBitsKO ko; ps_clear ptr' (objBitsKO ko) s; {ptr'..ptr' + 2 ^ objBitsKO ko - 1} \<inter> {ptr..(ptr && ~~ mask (objBitsKO (injectKOS val) + us)) + 2 ^ (objBitsKO (injectKOS val) + us) - 1} = {}\<rbrakk> \<Longrightarrow> range_cover ptr (?sz117 s ko) (objBitsKO (injectKOS val)) (2 ^ us)
 2. \<And>s ko. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s); pspace_aligned' (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s); ksPSpace s ptr' = Some ko; is_aligned ptr' (objBitsKO ko); objBitsKO (f (Some ko)) = objBitsKO ko; ps_clear ptr' (objBitsKO ko) s; {ptr'..ptr' + 2 ^ objBitsKO ko - 1} \<inter> {ptr..(ptr && ~~ mask (objBitsKO (injectKOS val) + us)) + 2 ^ (objBitsKO (injectKOS val) + us) - 1} = {}; ptr' \<in> {ptr..ptr_add (ptr && ~~ mask (?sz117 s ko)) (2 ^ ?sz117 s ko - 1)}\<rbrakk> \<Longrightarrow> f (Some (injectKOS val)) = injectKOS val proof (prove)
goal (3 subgoals):
 1. \<And>s ko. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s); pspace_aligned' (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s); ksPSpace s ptr' = Some ko; is_aligned ptr' (objBitsKO ko); objBitsKO (f (Some ko)) = objBitsKO ko; ps_clear ptr' (objBitsKO ko) s; {ptr'..ptr' + 2 ^ objBitsKO ko - 1} \<inter> {ptr..(ptr && ~~ mask (objBitsKO (injectKOS val) + us)) + 2 ^ (objBitsKO (injectKOS val) + us) - 1} = {}\<rbrakk> \<Longrightarrow> objBitsKO (injectKOS val) \<le> objBitsKO (injectKOS val) + us
 2. \<And>s ko. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s); pspace_aligned' (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s); ksPSpace s ptr' = Some ko; is_aligned ptr' (objBitsKO ko); objBitsKO (f (Some ko)) = objBitsKO ko; ps_clear ptr' (objBitsKO ko) s; {ptr'..ptr' + 2 ^ objBitsKO ko - 1} \<inter> {ptr..(ptr && ~~ mask (objBitsKO (injectKOS val) + us)) + 2 ^ (objBitsKO (injectKOS val) + us) - 1} = {}\<rbrakk> \<Longrightarrow> 2 ^ us = 2 ^ (objBitsKO (injectKOS val) + us - objBitsKO (injectKOS val)) * Suc 0
 3. \<And>s ko. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s); pspace_aligned' (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s); ksPSpace s ptr' = Some ko; is_aligned ptr' (objBitsKO ko); objBitsKO (f (Some ko)) = objBitsKO ko; ps_clear ptr' (objBitsKO ko) s; {ptr'..ptr' + 2 ^ objBitsKO ko - 1} \<inter> {ptr..(ptr && ~~ mask (objBitsKO (injectKOS val) + us)) + 2 ^ (objBitsKO (injectKOS val) + us) - 1} = {}; ptr' \<in> {ptr..ptr_add (ptr && ~~ mask (objBitsKO (injectKOS val) + us)) (2 ^ (objBitsKO (injectKOS val) + us) - 1)}\<rbrakk> \<Longrightarrow> f (Some (injectKOS val)) = injectKOS val proof (prove)
goal (2 subgoals):
 1. \<And>s ko. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s); pspace_aligned' (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s); ksPSpace s ptr' = Some ko; is_aligned ptr' (objBitsKO ko); objBitsKO (f (Some ko)) = objBitsKO ko; ps_clear ptr' (objBitsKO ko) s; {ptr'..ptr' + 2 ^ objBitsKO ko - 1} \<inter> {ptr..(ptr && ~~ mask (objBitsKO (injectKOS val) + us)) + 2 ^ (objBitsKO (injectKOS val) + us) - 1} = {}\<rbrakk> \<Longrightarrow> 2 ^ us = 2 ^ (objBitsKO (injectKOS val) + us - objBitsKO (injectKOS val)) * Suc 0
 2. \<And>s ko. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s); pspace_aligned' (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s); ksPSpace s ptr' = Some ko; is_aligned ptr' (objBitsKO ko); objBitsKO (f (Some ko)) = objBitsKO ko; ps_clear ptr' (objBitsKO ko) s; {ptr'..ptr' + 2 ^ objBitsKO ko - 1} \<inter> {ptr..(ptr && ~~ mask (objBitsKO (injectKOS val) + us)) + 2 ^ (objBitsKO (injectKOS val) + us) - 1} = {}; ptr' \<in> {ptr..ptr_add (ptr && ~~ mask (objBitsKO (injectKOS val) + us)) (2 ^ (objBitsKO (injectKOS val) + us) - 1)}\<rbrakk> \<Longrightarrow> f (Some (injectKOS val)) = injectKOS val proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s); pspace_aligned' (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s); ksPSpace s ptr' = Some ko; is_aligned ptr' (objBitsKO ko); objBitsKO (f (Some ko)) = objBitsKO ko; ps_clear ptr' (objBitsKO ko) s; {ptr'..ptr' + 2 ^ objBitsKO ko - 1} \<inter> {ptr..(ptr && ~~ mask (objBitsKO (injectKOS val) + us)) + 2 ^ (objBitsKO (injectKOS val) + us) - 1} = {}; ptr' \<in> {ptr..ptr_add (ptr && ~~ mask (objBitsKO (injectKOS val) + us)) (2 ^ (objBitsKO (injectKOS val) + us) - 1)}\<rbrakk> \<Longrightarrow> f (Some (injectKOS val)) = injectKOS val proof (prove)
goal (3 subgoals):
 1. \<And>s ko. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s); pspace_aligned' (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s); ksPSpace s ptr' = Some ko; is_aligned ptr' (objBitsKO ko); objBitsKO (f (Some ko)) = objBitsKO ko; ps_clear ptr' (objBitsKO ko) s; ptr' \<in> {ptr..ptr_add (ptr && ~~ mask (objBitsKO (injectKOS val) + us)) (2 ^ (objBitsKO (injectKOS val) + us) - 1)}\<rbrakk> \<Longrightarrow> ptr' \<in> {ptr'..ptr' + 2 ^ objBitsKO ko - 1}
 2. \<And>s ko. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s); pspace_aligned' (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s); ksPSpace s ptr' = Some ko; is_aligned ptr' (objBitsKO ko); objBitsKO (f (Some ko)) = objBitsKO ko; ps_clear ptr' (objBitsKO ko) s; ptr' \<in> {ptr..ptr_add (ptr && ~~ mask (objBitsKO (injectKOS val) + us)) (2 ^ (objBitsKO (injectKOS val) + us) - 1)}\<rbrakk> \<Longrightarrow> ptr' \<in> {ptr..(ptr && ~~ mask (objBitsKO (injectKOS val) + us)) + 2 ^ (objBitsKO (injectKOS val) + us) - 1}
 3. \<And>s ko. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s); pspace_aligned' (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s); ksPSpace s ptr' = Some ko; is_aligned ptr' (objBitsKO ko); objBitsKO (f (Some ko)) = objBitsKO ko; ps_clear ptr' (objBitsKO ko) s; ptr' \<in> {ptr..ptr_add (ptr && ~~ mask (objBitsKO (injectKOS val) + us)) (2 ^ (objBitsKO (injectKOS val) + us) - 1)}; False\<rbrakk> \<Longrightarrow> f (Some (injectKOS val)) = injectKOS val proof (prove)
goal (2 subgoals):
 1. \<And>s ko. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s); pspace_aligned' (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s); ksPSpace s ptr' = Some ko; is_aligned ptr' (objBitsKO ko); objBitsKO (f (Some ko)) = objBitsKO ko; ps_clear ptr' (objBitsKO ko) s; ptr' \<in> {ptr..ptr_add (ptr && ~~ mask (objBitsKO (injectKOS val) + us)) (2 ^ (objBitsKO (injectKOS val) + us) - 1)}\<rbrakk> \<Longrightarrow> ptr' \<in> {ptr..(ptr && ~~ mask (objBitsKO (injectKOS val) + us)) + 2 ^ (objBitsKO (injectKOS val) + us) - 1}
 2. \<And>s ko. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s); pspace_aligned' (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s); ksPSpace s ptr' = Some ko; is_aligned ptr' (objBitsKO ko); objBitsKO (f (Some ko)) = objBitsKO ko; ps_clear ptr' (objBitsKO ko) s; ptr' \<in> {ptr..ptr_add (ptr && ~~ mask (objBitsKO (injectKOS val) + us)) (2 ^ (objBitsKO (injectKOS val) + us) - 1)}; False\<rbrakk> \<Longrightarrow> f (Some (injectKOS val)) = injectKOS val proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s); pspace_aligned' (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (ps ptr'))) s); ksPSpace s ptr' = Some ko; is_aligned ptr' (objBitsKO ko); objBitsKO (f (Some ko)) = objBitsKO ko; ps_clear ptr' (objBitsKO ko) s; ptr' \<in> {ptr..ptr_add (ptr && ~~ mask (objBitsKO (injectKOS val) + us)) (2 ^ (objBitsKO (injectKOS val) + us) - 1)}; False\<rbrakk> \<Longrightarrow> f (Some (injectKOS val)) = injectKOS val proof (prove)
goal:
No subgoals!