theory Detype_R

lemma storePDE_placeNewObject_commute:
  "monad_commute
     (pde_at' src and pspace_distinct' and pspace_aligned' and
      pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) and
      K (is_aligned ptr (objBitsKO (injectKOS val) + sz) \<and>
      objBitsKO (injectKOS val) + sz < word_bits) )
     (placeNewObject ptr val sz) (storePDE src (new_pde::ARM_H.pde))" apply (rule commute_name_pre_state) apply (clarsimp simp:typ_at'_def ko_wp_at'_def) apply (case_tac ko,simp_all) apply (rename_tac arch_kernel_object) apply (case_tac arch_kernel_object,simp_all) apply clarsimp apply (rename_tac pde) apply (subgoal_tac "ko_wp_at' ((=) (KOArch (KOPDE pde))) src s") prefer 2 apply (clarsimp simp:ko_wp_at'_def) apply (subgoal_tac "range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0)") prefer 2 apply (rule range_cover_full) apply simp+ apply (rule monad_commute_guard_imp) apply (rule commute_commute) apply (rule commute_rewrite[OF storePDE_det]) apply assumption apply (simp add:placeNewObject_def2) apply (wp createObjects_orig_ko_wp_at2') apply (rule commute_commute) apply (subst modify_specify2[where g = "return",simplified]) apply (rule_tac commute_rewrite[where Q = "\<lambda>s.
    pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s \<and> pde_at' src s
    \<and> pspace_distinct' s \<and> pspace_aligned' s"]) apply (rule simpler_placeNewObject_def) apply simp+ apply (wp modify_pde_psp_no_overlap' modify_pde_pspace_distinct'
               modify_pde_pspace_aligned' modify_pde_pde_at') apply (simp add: modify_specify modify_mapM_x) apply (rule commute_commute[OF mapM_x_commute[where f = id]]) apply (rule modify_obj_commute) apply wp apply simp apply clarsimp apply (intro conjI,simp_all) apply (clarsimp simp:typ_at'_def ko_wp_at'_def objBits_simps archObjSize_def) apply (rule new_cap_addrs_distinct) apply (erule range_cover_rel) apply simp+ apply clarsimp apply (simp add:not_in_new_cap_addrs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monad_commute (pde_at' src and pspace_distinct' and pspace_aligned' and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) and K (is_aligned ptr (objBitsKO (injectKOS val) + sz) \<and> objBitsKO (injectKOS val) + sz < word_bits)) (placeNewObject ptr val sz) (storePDE src new_pde) proof (prove)
goal (1 subgoal):
 1. \<And>s. (pde_at' src and pspace_distinct' and pspace_aligned' and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) and K (is_aligned ptr (objBitsKO (injectKOS val) + sz) \<and> objBitsKO (injectKOS val) + sz < word_bits)) s \<Longrightarrow> monad_commute ((=) s) (placeNewObject ptr val sz) (storePDE src new_pde) proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some ko; pspace_aligned' s; is_aligned src (objBitsKO ko); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; koTypeOf ko = ArchT PDET; ps_clear src (objBitsKO ko) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits\<rbrakk> \<Longrightarrow> monad_commute ((=) s) (placeNewObject ptr val sz) (storePDE src new_pde) proof (prove)
goal (1 subgoal):
 1. \<And>s ko x8. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some (KOArch x8); pspace_aligned' s; is_aligned src (objBitsKO (KOArch x8)); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; archTypeOf x8 = PDET; ps_clear src (objBitsKO (KOArch x8)) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko = KOArch x8\<rbrakk> \<Longrightarrow> monad_commute ((=) s) (placeNewObject ptr val sz) (storePDE src new_pde) proof (prove)
goal (1 subgoal):
 1. \<And>s ko arch_kernel_object. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some (KOArch arch_kernel_object); pspace_aligned' s; is_aligned src (objBitsKO (KOArch arch_kernel_object)); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; archTypeOf arch_kernel_object = PDET; ps_clear src (objBitsKO (KOArch arch_kernel_object)) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko = KOArch arch_kernel_object\<rbrakk> \<Longrightarrow> monad_commute ((=) s) (placeNewObject ptr val sz) (storePDE src new_pde) proof (prove)
goal (1 subgoal):
 1. \<And>s ko arch_kernel_object x3. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some (KOArch (KOPDE x3)); pspace_aligned' s; is_aligned src (objBitsKO (KOArch (KOPDE x3))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; ps_clear src (objBitsKO (KOArch (KOPDE x3))) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko = KOArch (KOPDE x3); arch_kernel_object = KOPDE x3\<rbrakk> \<Longrightarrow> monad_commute ((=) s) (placeNewObject ptr val sz) (storePDE src new_pde) proof (prove)
goal (1 subgoal):
 1. \<And>s x3. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some (KOArch (KOPDE x3)); pspace_aligned' s; is_aligned src (objBitsKO (KOArch (KOPDE x3))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; ps_clear src (objBitsKO (KOArch (KOPDE x3))) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits\<rbrakk> \<Longrightarrow> monad_commute ((=) s) (placeNewObject ptr val sz) (storePDE src new_pde) proof (prove)
goal (1 subgoal):
 1. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits\<rbrakk> \<Longrightarrow> monad_commute ((=) s) (placeNewObject ptr val sz) (storePDE src new_pde) proof (prove)
goal (2 subgoals):
 1. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s\<rbrakk> \<Longrightarrow> monad_commute ((=) s) (placeNewObject ptr val sz) (storePDE src new_pde)
 2. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits\<rbrakk> \<Longrightarrow> ko_wp_at' ((=) (KOArch (KOPDE pde))) src s proof (prove)
goal (2 subgoals):
 1. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits\<rbrakk> \<Longrightarrow> ko_wp_at' ((=) (KOArch (KOPDE pde))) src s
 2. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s\<rbrakk> \<Longrightarrow> monad_commute ((=) s) (placeNewObject ptr val sz) (storePDE src new_pde) proof (prove)
goal (1 subgoal):
 1. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s\<rbrakk> \<Longrightarrow> monad_commute ((=) s) (placeNewObject ptr val sz) (storePDE src new_pde) proof (prove)
goal (2 subgoals):
 1. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0)\<rbrakk> \<Longrightarrow> monad_commute ((=) s) (placeNewObject ptr val sz) (storePDE src new_pde)
 2. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s\<rbrakk> \<Longrightarrow> range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0) proof (prove)
goal (2 subgoals):
 1. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s\<rbrakk> \<Longrightarrow> range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0)
 2. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0)\<rbrakk> \<Longrightarrow> monad_commute ((=) s) (placeNewObject ptr val sz) (storePDE src new_pde) proof (prove)
goal (3 subgoals):
 1. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s\<rbrakk> \<Longrightarrow> is_aligned ptr (objBitsKO (injectKOS val) + sz)
 2. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s\<rbrakk> \<Longrightarrow> objBitsKO (injectKOS val) + sz < word_bits
 3. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0)\<rbrakk> \<Longrightarrow> monad_commute ((=) s) (placeNewObject ptr val sz) (storePDE src new_pde) proof (prove)
goal (1 subgoal):
 1. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0)\<rbrakk> \<Longrightarrow> monad_commute ((=) s) (placeNewObject ptr val sz) (storePDE src new_pde) proof (prove)
goal (2 subgoals):
 1. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0)\<rbrakk> \<Longrightarrow> monad_commute (?P20 s pde) (placeNewObject ptr val sz) (storePDE src new_pde)
 2. \<And>s pde sa. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0); s = sa\<rbrakk> \<Longrightarrow> ?P20 s pde sa proof (prove)
goal (2 subgoals):
 1. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0)\<rbrakk> \<Longrightarrow> monad_commute (?P20 s pde) (storePDE src new_pde) (placeNewObject ptr val sz)
 2. \<And>s pde sa. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0); s = sa\<rbrakk> \<Longrightarrow> ?P20 s pde sa proof (prove)
goal (4 subgoals):
 1. \<And>s pde sa. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0); ?Q25 s pde sa\<rbrakk> \<Longrightarrow> ko_wp_at' ((=) (KOArch (KOPDE (?pde26 s pde sa)))) src sa
 2. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0)\<rbrakk> \<Longrightarrow> \<lbrace>?P25 s pde\<rbrace> placeNewObject ptr val sz \<lbrace>\<lambda>x. ?Q25 s pde\<rbrace>
 3. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0)\<rbrakk> \<Longrightarrow> monad_commute (?R25 s pde) (\<lambda>s. modify (ksPSpace_update (\<lambda>_. (ksPSpace s)(src \<mapsto> KOArch (KOPDE new_pde)))) s) (placeNewObject ptr val sz)
 4. \<And>s pde sa. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0); s = sa\<rbrakk> \<Longrightarrow> (?P25 s pde and ?Q25 s pde and ?R25 s pde) sa proof (prove)
goal (3 subgoals):
 1. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0)\<rbrakk> \<Longrightarrow> \<lbrace>?P25 s pde\<rbrace> placeNewObject ptr val sz \<lbrace>\<lambda>x sa. ko_wp_at' ((=) (KOArch (KOPDE (?pde26 s pde sa)))) src sa\<rbrace>
 2. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0)\<rbrakk> \<Longrightarrow> monad_commute (?R25 s pde) (\<lambda>s. modify (ksPSpace_update (\<lambda>_. (ksPSpace s)(src \<mapsto> KOArch (KOPDE new_pde)))) s) (placeNewObject ptr val sz)
 3. \<And>s pde sa. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0); s = sa\<rbrakk> \<Longrightarrow> (?P25 s pde and (\<lambda>sa. ko_wp_at' ((=) (KOArch (KOPDE (?pde26 s pde sa)))) src sa) and ?R25 s pde) sa proof (prove)
goal (3 subgoals):
 1. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0)\<rbrakk> \<Longrightarrow> \<lbrace>?P25 s pde\<rbrace> createObjects' ptr (Suc 0) (injectKOS val) sz \<lbrace>\<lambda>x sa. ko_wp_at' ((=) (KOArch (KOPDE (?pde26 s pde sa)))) src sa\<rbrace>
 2. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0)\<rbrakk> \<Longrightarrow> monad_commute (?R25 s pde) (\<lambda>s. modify (ksPSpace_update (\<lambda>_. (ksPSpace s)(src \<mapsto> KOArch (KOPDE new_pde)))) s) (placeNewObject ptr val sz)
 3. \<And>s pde sa. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0); s = sa\<rbrakk> \<Longrightarrow> (?P25 s pde and (\<lambda>sa. ko_wp_at' ((=) (KOArch (KOPDE (?pde26 s pde sa)))) src sa) and ?R25 s pde) sa proof (prove)
goal (2 subgoals):
 1. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0)\<rbrakk> \<Longrightarrow> monad_commute (?R25 s pde) (\<lambda>s. modify (ksPSpace_update (\<lambda>_. (ksPSpace s)(src \<mapsto> KOArch (KOPDE new_pde)))) s) (placeNewObject ptr val sz)
 2. \<And>s pde sa. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0); s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>sa. range_cover ptr (?sz31 s pde) (objBitsKO (injectKOS val) + sz) (Suc 0) \<and> Suc 0 \<noteq> 0 \<and> pspace_aligned' sa \<and> pspace_distinct' sa \<and> ko_wp_at' ((=) (KOArch (KOPDE (?pde34 s pde)))) src sa \<and> (KOArch (KOPDE (?pde34 s pde)) = injectKOS val \<longrightarrow> True) \<and> pspace_no_overlap' ptr (?sz31 s pde) sa) and ko_wp_at' ((=) (KOArch (KOPDE (?pde34 s pde)))) src and ?R25 s pde) sa proof (prove)
goal (2 subgoals):
 1. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0)\<rbrakk> \<Longrightarrow> monad_commute (?R25 s pde) (placeNewObject ptr val sz) (\<lambda>s. modify (ksPSpace_update (\<lambda>_. (ksPSpace s)(src \<mapsto> KOArch (KOPDE new_pde)))) s)
 2. \<And>s pde sa. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0); s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>sa. range_cover ptr (?sz31 s pde) (objBitsKO (injectKOS val) + sz) (Suc 0) \<and> Suc 0 \<noteq> 0 \<and> pspace_aligned' sa \<and> pspace_distinct' sa \<and> ko_wp_at' ((=) (KOArch (KOPDE (?pde34 s pde)))) src sa \<and> (KOArch (KOPDE (?pde34 s pde)) = injectKOS val \<longrightarrow> True) \<and> pspace_no_overlap' ptr (?sz31 s pde) sa) and ko_wp_at' ((=) (KOArch (KOPDE (?pde34 s pde)))) src and ?R25 s pde) sa proof (prove)
goal (2 subgoals):
 1. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0)\<rbrakk> \<Longrightarrow> monad_commute (?R39 s pde (?s39 s pde) (?pdea39 s pde)) (placeNewObject ptr val sz) (modify (ksPSpace_update (\<lambda>a. a(src \<mapsto> KOArch (KOPDE new_pde)))))
 2. \<And>s pde sa. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0); s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>sa. range_cover ptr (?sz31 s pde) (objBitsKO (injectKOS val) + sz) (Suc 0) \<and> Suc 0 \<noteq> 0 \<and> pspace_aligned' sa \<and> pspace_distinct' sa \<and> ko_wp_at' ((=) (KOArch (KOPDE (?pde34 s pde)))) src sa \<and> (KOArch (KOPDE (?pde34 s pde)) = injectKOS val \<longrightarrow> True) \<and> pspace_no_overlap' ptr (?sz31 s pde) sa) and ko_wp_at' ((=) (KOArch (KOPDE (?pde34 s pde)))) src and ?R39 s pde (?s39 s pde) (?pdea39 s pde)) sa proof (prove)
goal (4 subgoals):
 1. \<And>s pde sa. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) sa \<and> pde_at' src sa \<and> pspace_distinct' sa \<and> pspace_aligned' sa\<rbrakk> \<Longrightarrow> placeNewObject ptr val sz sa = ?t41 s pde sa
 2. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0)\<rbrakk> \<Longrightarrow> \<lbrace>?P45 s pde (?s39 s pde) (?pdea39 s pde)\<rbrace> modify (ksPSpace_update (\<lambda>a. a(src \<mapsto> KOArch (KOPDE new_pde)))) \<lbrace>\<lambda>x s. pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s \<and> pde_at' src s \<and> pspace_distinct' s \<and> pspace_aligned' s\<rbrace>
 3. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0)\<rbrakk> \<Longrightarrow> monad_commute (?R44 s pde (?s39 s pde) (?pdea39 s pde)) (?t41 s pde) (modify (ksPSpace_update (\<lambda>a. a(src \<mapsto> KOArch (KOPDE new_pde)))))
 4. \<And>s pde sa. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0); s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>sa. range_cover ptr (?sz31 s pde) (objBitsKO (injectKOS val) + sz) (Suc 0) \<and> Suc 0 \<noteq> 0 \<and> pspace_aligned' sa \<and> pspace_distinct' sa \<and> ko_wp_at' ((=) (KOArch (KOPDE (?pde34 s pde)))) src sa \<and> (KOArch (KOPDE (?pde34 s pde)) = injectKOS val \<longrightarrow> True) \<and> pspace_no_overlap' ptr (?sz31 s pde) sa) and ko_wp_at' ((=) (KOArch (KOPDE (?pde34 s pde)))) src and (?P45 s pde (?s39 s pde) (?pdea39 s pde) and (\<lambda>s. pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s \<and> pde_at' src s \<and> pspace_distinct' s \<and> pspace_aligned' s) and ?R44 s pde (?s39 s pde) (?pdea39 s pde))) sa proof (prove)
goal (7 subgoals):
 1. \<And>s pde sa. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) sa \<and> pde_at' src sa \<and> pspace_distinct' sa \<and> pspace_aligned' sa\<rbrakk> \<Longrightarrow> sz < word_bits
 2. \<And>s pde sa. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) sa \<and> pde_at' src sa \<and> pspace_distinct' sa \<and> pspace_aligned' sa\<rbrakk> \<Longrightarrow> is_aligned ptr (objBitsKO (injectKOS val) + sz)
 3. \<And>s pde sa. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) sa \<and> pde_at' src sa \<and> pspace_distinct' sa \<and> pspace_aligned' sa\<rbrakk> \<Longrightarrow> pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) sa
 4. \<And>s pde sa. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) sa \<and> pde_at' src sa \<and> pspace_distinct' sa \<and> pspace_aligned' sa\<rbrakk> \<Longrightarrow> pspace_aligned' sa
 5. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0)\<rbrakk> \<Longrightarrow> \<lbrace>?P45 s pde (?s39 s pde) (?pdea39 s pde)\<rbrace> modify (ksPSpace_update (\<lambda>a. a(src \<mapsto> KOArch (KOPDE new_pde)))) \<lbrace>\<lambda>x s. pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s \<and> pde_at' src s \<and> pspace_distinct' s \<and> pspace_aligned' s\<rbrace>
 6. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0)\<rbrakk> \<Longrightarrow> monad_commute (?R44 s pde (?s39 s pde) (?pdea39 s pde)) (\<lambda>sa. modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ sz) ptr (injectKOS val)) (ksPSpace sa))) sa) (modify (ksPSpace_update (\<lambda>a. a(src \<mapsto> KOArch (KOPDE new_pde)))))
 7. \<And>s pde sa. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0); s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>sa. range_cover ptr (?sz31 s pde) (objBitsKO (injectKOS val) + sz) (Suc 0) \<and> Suc 0 \<noteq> 0 \<and> pspace_aligned' sa \<and> pspace_distinct' sa \<and> ko_wp_at' ((=) (KOArch (KOPDE (?pde34 s pde)))) src sa \<and> (KOArch (KOPDE (?pde34 s pde)) = injectKOS val \<longrightarrow> True) \<and> pspace_no_overlap' ptr (?sz31 s pde) sa) and ko_wp_at' ((=) (KOArch (KOPDE (?pde34 s pde)))) src and (?P45 s pde (?s39 s pde) (?pdea39 s pde) and (\<lambda>s. pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s \<and> pde_at' src s \<and> pspace_distinct' s \<and> pspace_aligned' s) and ?R44 s pde (?s39 s pde) (?pdea39 s pde))) sa proof (prove)
goal (3 subgoals):
 1. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0)\<rbrakk> \<Longrightarrow> \<lbrace>?P45 s pde (?s39 s pde) (?pdea39 s pde)\<rbrace> modify (ksPSpace_update (\<lambda>a. a(src \<mapsto> KOArch (KOPDE new_pde)))) \<lbrace>\<lambda>x s. pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s \<and> pde_at' src s \<and> pspace_distinct' s \<and> pspace_aligned' s\<rbrace>
 2. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0)\<rbrakk> \<Longrightarrow> monad_commute (?R44 s pde (?s39 s pde) (?pdea39 s pde)) (\<lambda>sa. modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ sz) ptr (injectKOS val)) (ksPSpace sa))) sa) (modify (ksPSpace_update (\<lambda>a. a(src \<mapsto> KOArch (KOPDE new_pde)))))
 3. \<And>s pde sa. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0); s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>sa. range_cover ptr (?sz31 s pde) (objBitsKO (injectKOS val) + sz) (Suc 0) \<and> Suc 0 \<noteq> 0 \<and> pspace_aligned' sa \<and> pspace_distinct' sa \<and> ko_wp_at' ((=) (KOArch (KOPDE (?pde34 s pde)))) src sa \<and> (KOArch (KOPDE (?pde34 s pde)) = injectKOS val \<longrightarrow> True) \<and> pspace_no_overlap' ptr (?sz31 s pde) sa) and ko_wp_at' ((=) (KOArch (KOPDE (?pde34 s pde)))) src and (?P45 s pde (?s39 s pde) (?pdea39 s pde) and (\<lambda>s. pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s \<and> pde_at' src s \<and> pspace_distinct' s \<and> pspace_aligned' s) and ?R44 s pde (?s39 s pde) (?pdea39 s pde))) sa proof (prove)
goal (2 subgoals):
 1. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0)\<rbrakk> \<Longrightarrow> monad_commute (?R44 s pde (?s39 s pde) (?pdea39 s pde)) (\<lambda>sa. modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ sz) ptr (injectKOS val)) (ksPSpace sa))) sa) (modify (ksPSpace_update (\<lambda>a. a(src \<mapsto> KOArch (KOPDE new_pde)))))
 2. \<And>s pde sa. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0); s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>sa. range_cover ptr (?sz31 s pde) (objBitsKO (injectKOS val) + sz) (Suc 0) \<and> Suc 0 \<noteq> 0 \<and> pspace_aligned' sa \<and> pspace_distinct' sa \<and> ko_wp_at' ((=) (KOArch (KOPDE (?pde34 s pde)))) src sa \<and> (KOArch (KOPDE (?pde34 s pde)) = injectKOS val \<longrightarrow> True) \<and> pspace_no_overlap' ptr (?sz31 s pde) sa) and ko_wp_at' ((=) (KOArch (KOPDE (?pde34 s pde)))) src and ((\<lambda>a. (pde_at' src and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz)) a \<and> pde_at' src a \<and> (pde_at' src and pspace_distinct') a \<and> (pde_at' src and pspace_aligned') a) and (\<lambda>s. pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s \<and> pde_at' src s \<and> pspace_distinct' s \<and> pspace_aligned' s) and ?R44 s pde (?s39 s pde) (?pdea39 s pde))) sa proof (prove)
goal (2 subgoals):
 1. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0)\<rbrakk> \<Longrightarrow> monad_commute (?R44 s pde (?s39 s pde) (?pdea39 s pde)) (mapM_x (\<lambda>x. modify (ksPSpace_update (\<lambda>m. m(x \<mapsto> injectKOS val)))) (rev (new_cap_addrs (2 ^ sz) ptr (injectKOS val)))) (modify (ksPSpace_update (\<lambda>a. a(src \<mapsto> KOArch (KOPDE new_pde)))))
 2. \<And>s pde sa. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0); s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>sa. range_cover ptr (?sz31 s pde) (objBitsKO (injectKOS val) + sz) (Suc 0) \<and> Suc 0 \<noteq> 0 \<and> pspace_aligned' sa \<and> pspace_distinct' sa \<and> ko_wp_at' ((=) (KOArch (KOPDE (?pde34 s pde)))) src sa \<and> (KOArch (KOPDE (?pde34 s pde)) = injectKOS val \<longrightarrow> True) \<and> pspace_no_overlap' ptr (?sz31 s pde) sa) and ko_wp_at' ((=) (KOArch (KOPDE (?pde34 s pde)))) src and ((\<lambda>a. (pde_at' src and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz)) a \<and> pde_at' src a \<and> (pde_at' src and pspace_distinct') a \<and> (pde_at' src and pspace_aligned') a) and (\<lambda>s. pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s \<and> pde_at' src s \<and> pspace_distinct' s \<and> pspace_aligned' s) and ?R44 s pde (?s39 s pde) (?pdea39 s pde))) sa proof (prove)
goal (3 subgoals):
 1. \<And>s pde r. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0)\<rbrakk> \<Longrightarrow> monad_commute (\<lambda>a. ?P69 s pde (?s39 s pde) (?pdea39 s pde) a r) (modify (ksPSpace_update (\<lambda>a. a(src \<mapsto> KOArch (KOPDE new_pde))))) (modify (ksPSpace_update (\<lambda>m. m(r \<mapsto> injectKOS val))))
 2. \<And>s pde r x. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0)\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>a. ?P69 s pde (?s39 s pde) (?pdea39 s pde) a r) and K (id r \<noteq> id x) and (\<lambda>a. ?P69 s pde (?s39 s pde) (?pdea39 s pde) a x)\<rbrace> modify (ksPSpace_update (\<lambda>m. m(x \<mapsto> injectKOS val))) \<lbrace>\<lambda>v a. ?P69 s pde (?s39 s pde) (?pdea39 s pde) a r\<rbrace>
 3. \<And>s pde sa. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0); s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>sa. range_cover ptr (?sz31 s pde) (objBitsKO (injectKOS val) + sz) (Suc 0) \<and> Suc 0 \<noteq> 0 \<and> pspace_aligned' sa \<and> pspace_distinct' sa \<and> ko_wp_at' ((=) (KOArch (KOPDE (?pde34 s pde)))) src sa \<and> (KOArch (KOPDE (?pde34 s pde)) = injectKOS val \<longrightarrow> True) \<and> pspace_no_overlap' ptr (?sz31 s pde) sa) and ko_wp_at' ((=) (KOArch (KOPDE (?pde34 s pde)))) src and ((\<lambda>a. (pde_at' src and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz)) a \<and> pde_at' src a \<and> (pde_at' src and pspace_distinct') a \<and> (pde_at' src and pspace_aligned') a) and (\<lambda>s. pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s \<and> pde_at' src s \<and> pspace_distinct' s \<and> pspace_aligned' s) and (\<lambda>a. distinct (map id (rev (new_cap_addrs (2 ^ sz) ptr (injectKOS val)))) \<and> (\<forall>r\<in>set (rev (new_cap_addrs (2 ^ sz) ptr (injectKOS val))). ?P69 s pde (?s39 s pde) (?pdea39 s pde) a r)))) sa proof (prove)
goal (2 subgoals):
 1. \<And>s pde r x. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0)\<rbrakk> \<Longrightarrow> \<lbrace>K (src \<noteq> r) and K (id r \<noteq> id x) and K (src \<noteq> x)\<rbrace> modify (ksPSpace_update (\<lambda>m. m(x \<mapsto> injectKOS val))) \<lbrace>\<lambda>v. K (src \<noteq> r)\<rbrace>
 2. \<And>s pde sa. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0); s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>sa. range_cover ptr (?sz31 s pde) (objBitsKO (injectKOS val) + sz) (Suc 0) \<and> Suc 0 \<noteq> 0 \<and> pspace_aligned' sa \<and> pspace_distinct' sa \<and> ko_wp_at' ((=) (KOArch (KOPDE (?pde34 s pde)))) src sa \<and> (KOArch (KOPDE (?pde34 s pde)) = injectKOS val \<longrightarrow> True) \<and> pspace_no_overlap' ptr (?sz31 s pde) sa) and ko_wp_at' ((=) (KOArch (KOPDE (?pde34 s pde)))) src and ((\<lambda>a. (pde_at' src and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz)) a \<and> pde_at' src a \<and> (pde_at' src and pspace_distinct') a \<and> (pde_at' src and pspace_aligned') a) and (\<lambda>s. pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s \<and> pde_at' src s \<and> pspace_distinct' s \<and> pspace_aligned' s) and (\<lambda>a. distinct (map id (rev (new_cap_addrs (2 ^ sz) ptr (injectKOS val)))) \<and> (\<forall>r\<in>set (rev (new_cap_addrs (2 ^ sz) ptr (injectKOS val))). K (src \<noteq> r) a)))) sa proof (prove)
goal (2 subgoals):
 1. \<And>s pde r x sa. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0); (K (src \<noteq> r) and K (id r \<noteq> id x) and K (src \<noteq> x)) sa\<rbrakk> \<Longrightarrow> K (src \<noteq> r) sa
 2. \<And>s pde sa. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0); s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>sa. range_cover ptr (?sz31 s pde) (objBitsKO (injectKOS val) + sz) (Suc 0) \<and> Suc 0 \<noteq> 0 \<and> pspace_aligned' sa \<and> pspace_distinct' sa \<and> ko_wp_at' ((=) (KOArch (KOPDE (?pde34 s pde)))) src sa \<and> (KOArch (KOPDE (?pde34 s pde)) = injectKOS val \<longrightarrow> True) \<and> pspace_no_overlap' ptr (?sz31 s pde) sa) and ko_wp_at' ((=) (KOArch (KOPDE (?pde34 s pde)))) src and ((\<lambda>a. (pde_at' src and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz)) a \<and> pde_at' src a \<and> (pde_at' src and pspace_distinct') a \<and> (pde_at' src and pspace_aligned') a) and (\<lambda>s. pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s \<and> pde_at' src s \<and> pspace_distinct' s \<and> pspace_aligned' s) and (\<lambda>a. distinct (map id (rev (new_cap_addrs (2 ^ sz) ptr (injectKOS val)))) \<and> (\<forall>r\<in>set (rev (new_cap_addrs (2 ^ sz) ptr (injectKOS val))). K (src \<noteq> r) a)))) sa proof (prove)
goal (1 subgoal):
 1. \<And>s pde sa. \<lbrakk>pspace_distinct' s; ksPSpace s src = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s; ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0); s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>sa. range_cover ptr (?sz31 s pde) (objBitsKO (injectKOS val) + sz) (Suc 0) \<and> Suc 0 \<noteq> 0 \<and> pspace_aligned' sa \<and> pspace_distinct' sa \<and> ko_wp_at' ((=) (KOArch (KOPDE (?pde34 s pde)))) src sa \<and> (KOArch (KOPDE (?pde34 s pde)) = injectKOS val \<longrightarrow> True) \<and> pspace_no_overlap' ptr (?sz31 s pde) sa) and ko_wp_at' ((=) (KOArch (KOPDE (?pde34 s pde)))) src and ((\<lambda>a. (pde_at' src and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz)) a \<and> pde_at' src a \<and> (pde_at' src and pspace_distinct') a \<and> (pde_at' src and pspace_aligned') a) and (\<lambda>s. pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s \<and> pde_at' src s \<and> pspace_distinct' s \<and> pspace_aligned' s) and (\<lambda>a. distinct (map id (rev (new_cap_addrs (2 ^ sz) ptr (injectKOS val)))) \<and> (\<forall>r\<in>set (rev (new_cap_addrs (2 ^ sz) ptr (injectKOS val))). K (src \<noteq> r) a)))) sa proof (prove)
goal (1 subgoal):
 1. \<And>pde sa. \<lbrakk>pspace_distinct' sa; ksPSpace sa src = Some (KOArch (KOPDE pde)); pspace_aligned' sa; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) sa; ps_clear src (objBitsKO (KOArch (KOPDE pde))) sa; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src sa; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0)\<rbrakk> \<Longrightarrow> range_cover ptr (?sz31 sa pde) (objBitsKO (injectKOS val) + sz) (Suc 0) \<and> ko_wp_at' ((=) (KOArch (KOPDE (?pde34 sa pde)))) src sa \<and> pspace_no_overlap' ptr (?sz31 sa pde) sa \<and> ko_wp_at' ((=) (KOArch (KOPDE (?pde34 sa pde)))) src sa \<and> pde_at' src sa \<and> distinct (new_cap_addrs (2 ^ sz) ptr (injectKOS val)) \<and> (\<forall>r\<in>set (new_cap_addrs (2 ^ sz) ptr (injectKOS val)). src \<noteq> r) proof (prove)
goal (3 subgoals):
 1. \<And>pde sa. \<lbrakk>pspace_distinct' sa; ksPSpace sa src = Some (KOArch (KOPDE pde)); pspace_aligned' sa; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) sa; ps_clear src (objBitsKO (KOArch (KOPDE pde))) sa; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src sa; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0)\<rbrakk> \<Longrightarrow> pde_at' src sa
 2. \<And>pde sa. \<lbrakk>pspace_distinct' sa; ksPSpace sa src = Some (KOArch (KOPDE pde)); pspace_aligned' sa; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) sa; ps_clear src (objBitsKO (KOArch (KOPDE pde))) sa; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src sa; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0)\<rbrakk> \<Longrightarrow> distinct (new_cap_addrs (2 ^ sz) ptr (injectKOS val))
 3. \<And>pde sa. \<lbrakk>pspace_distinct' sa; ksPSpace sa src = Some (KOArch (KOPDE pde)); pspace_aligned' sa; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) sa; ps_clear src (objBitsKO (KOArch (KOPDE pde))) sa; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src sa; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0)\<rbrakk> \<Longrightarrow> \<forall>r\<in>set (new_cap_addrs (2 ^ sz) ptr (injectKOS val)). src \<noteq> r proof (prove)
goal (2 subgoals):
 1. \<And>pde sa. \<lbrakk>pspace_distinct' sa; ksPSpace sa src = Some (KOArch (KOPDE pde)); pspace_aligned' sa; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) sa; ps_clear src (objBitsKO (KOArch (KOPDE pde))) sa; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src sa; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0)\<rbrakk> \<Longrightarrow> distinct (new_cap_addrs (2 ^ sz) ptr (injectKOS val))
 2. \<And>pde sa. \<lbrakk>pspace_distinct' sa; ksPSpace sa src = Some (KOArch (KOPDE pde)); pspace_aligned' sa; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) sa; ps_clear src (objBitsKO (KOArch (KOPDE pde))) sa; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src sa; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0)\<rbrakk> \<Longrightarrow> \<forall>r\<in>set (new_cap_addrs (2 ^ sz) ptr (injectKOS val)). src \<noteq> r proof (prove)
goal (2 subgoals):
 1. \<And>pde sa. \<lbrakk>pspace_distinct' sa; ksPSpace sa src = Some (KOArch (KOPDE pde)); pspace_aligned' sa; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) sa; ps_clear src (objBitsKO (KOArch (KOPDE pde))) sa; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src sa; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0)\<rbrakk> \<Longrightarrow> range_cover ptr (?sz85 pde sa) (objBitsKO (injectKOS val)) (2 ^ sz)
 2. \<And>pde sa. \<lbrakk>pspace_distinct' sa; ksPSpace sa src = Some (KOArch (KOPDE pde)); pspace_aligned' sa; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) sa; ps_clear src (objBitsKO (KOArch (KOPDE pde))) sa; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src sa; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0)\<rbrakk> \<Longrightarrow> \<forall>r\<in>set (new_cap_addrs (2 ^ sz) ptr (injectKOS val)). src \<noteq> r proof (prove)
goal (3 subgoals):
 1. \<And>pde sa. \<lbrakk>pspace_distinct' sa; ksPSpace sa src = Some (KOArch (KOPDE pde)); pspace_aligned' sa; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) sa; ps_clear src (objBitsKO (KOArch (KOPDE pde))) sa; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src sa\<rbrakk> \<Longrightarrow> objBitsKO (injectKOS val) \<le> objBitsKO (injectKOS val) + sz
 2. \<And>pde sa. \<lbrakk>pspace_distinct' sa; ksPSpace sa src = Some (KOArch (KOPDE pde)); pspace_aligned' sa; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) sa; ps_clear src (objBitsKO (KOArch (KOPDE pde))) sa; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src sa\<rbrakk> \<Longrightarrow> 2 ^ sz = 2 ^ (objBitsKO (injectKOS val) + sz - objBitsKO (injectKOS val)) * Suc 0
 3. \<And>pde sa. \<lbrakk>pspace_distinct' sa; ksPSpace sa src = Some (KOArch (KOPDE pde)); pspace_aligned' sa; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) sa; ps_clear src (objBitsKO (KOArch (KOPDE pde))) sa; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src sa; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0)\<rbrakk> \<Longrightarrow> \<forall>r\<in>set (new_cap_addrs (2 ^ sz) ptr (injectKOS val)). src \<noteq> r proof (prove)
goal (1 subgoal):
 1. \<And>pde sa. \<lbrakk>pspace_distinct' sa; ksPSpace sa src = Some (KOArch (KOPDE pde)); pspace_aligned' sa; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) sa; ps_clear src (objBitsKO (KOArch (KOPDE pde))) sa; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src sa; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0)\<rbrakk> \<Longrightarrow> \<forall>r\<in>set (new_cap_addrs (2 ^ sz) ptr (injectKOS val)). src \<noteq> r proof (prove)
goal (1 subgoal):
 1. \<And>pde sa. \<lbrakk>pspace_distinct' sa; ksPSpace sa src = Some (KOArch (KOPDE pde)); pspace_aligned' sa; is_aligned src (objBitsKO (KOArch (KOPDE pde))); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) sa; ps_clear src (objBitsKO (KOArch (KOPDE pde))) sa; is_aligned ptr (objBitsKO (injectKOS val) + sz); objBitsKO (injectKOS val) + sz < word_bits; ko_wp_at' ((=) (KOArch (KOPDE pde))) src sa; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0); src \<in> set (new_cap_addrs (2 ^ sz) ptr (injectKOS val))\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!