theory Detype_R

lemma getPDE_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)
     ((getObject src) :: KernelStateData_H.kernel_state \<Rightarrow>
                         (pde \<times> KernelStateData_H.kernel_state) set \<times> bool)" apply (rule commute_name_pre_state) 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 (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 (rule monad_commute_guard_imp) apply (rule commute_commute) apply (rule commute_rewrite[OF getPDE_det,where R = \<top>]) apply assumption apply (simp add:placeNewObject_def2) apply (wp createObjects_orig_ko_wp_at2') apply (simp add:monad_commute_def bind_def) apply (auto simp:ko_wp_at'_def) 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) (getObject src) 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) (getObject src) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>(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; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0)\<rbrakk> \<Longrightarrow> monad_commute ((=) s) (placeNewObject ptr val sz) (getObject src)
 2. \<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> range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0) proof (prove)
goal (2 subgoals):
 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> range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0)
 2. \<And>s. \<lbrakk>(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; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0)\<rbrakk> \<Longrightarrow> monad_commute ((=) s) (placeNewObject ptr val sz) (getObject src) proof (prove)
goal (3 subgoals):
 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> is_aligned ptr (objBitsKO (injectKOS val) + sz)
 2. \<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> objBitsKO (injectKOS val) + sz < word_bits
 3. \<And>s. \<lbrakk>(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; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0)\<rbrakk> \<Longrightarrow> monad_commute ((=) s) (placeNewObject ptr val sz) (getObject src) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pde_at' src s \<and> pspace_distinct' s \<and> pspace_aligned' s \<and> pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s \<and> is_aligned ptr (objBitsKO (injectKOS val) + sz) \<and> objBitsKO (injectKOS val) + sz < word_bits; range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0)\<rbrakk> \<Longrightarrow> monad_commute ((=) s) (placeNewObject ptr val sz) (getObject src) proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0); 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) (getObject src) proof (prove)
goal (1 subgoal):
 1. \<And>s ko x8. \<lbrakk>range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0); 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) (getObject src) proof (prove)
goal (1 subgoal):
 1. \<And>s ko arch_kernel_object. \<lbrakk>range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0); 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) (getObject src) proof (prove)
goal (1 subgoal):
 1. \<And>s ko arch_kernel_object x3. \<lbrakk>range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0); 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) (getObject src) proof (prove)
goal (1 subgoal):
 1. \<And>s x3. \<lbrakk>range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0); 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) (getObject src) proof (prove)
goal (1 subgoal):
 1. \<And>s pde. \<lbrakk>range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0); 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) (getObject src) proof (prove)
goal (2 subgoals):
 1. \<And>s pde. \<lbrakk>range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0); 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) (getObject src)
 2. \<And>s pde. \<lbrakk>range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0); 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>range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0); 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>range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0); 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) (getObject src) proof (prove)
goal (1 subgoal):
 1. \<And>s pde. \<lbrakk>range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0); 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) (getObject src) proof (prove)
goal (2 subgoals):
 1. \<And>s pde. \<lbrakk>range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0); 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 (?P20 s pde) (placeNewObject ptr val sz) (getObject src)
 2. \<And>s pde sa. \<lbrakk>range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0); 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; s = sa\<rbrakk> \<Longrightarrow> ?P20 s pde sa proof (prove)
goal (2 subgoals):
 1. \<And>s pde. \<lbrakk>range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0); 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 (?P20 s pde) (getObject src) (placeNewObject ptr val sz)
 2. \<And>s pde sa. \<lbrakk>range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0); 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; s = sa\<rbrakk> \<Longrightarrow> ?P20 s pde sa proof (prove)
goal (4 subgoals):
 1. \<And>s pde sa. \<lbrakk>range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0); 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; ?Q25 s pde sa\<rbrakk> \<Longrightarrow> ko_wp_at' ((=) (KOArch (KOPDE (?pde26 s pde sa)))) src sa
 2. \<And>s pde. \<lbrakk>range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0); 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> \<lbrace>?P25 s pde\<rbrace> placeNewObject ptr val sz \<lbrace>\<lambda>x. ?Q25 s pde\<rbrace>
 3. \<And>s pde. \<lbrakk>range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0); 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 (\<lambda>_. True) (\<lambda>sa. ({(?pde26 s pde sa, sa)}, False)) (placeNewObject ptr val sz)
 4. \<And>s pde sa. \<lbrakk>range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0); 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; s = sa\<rbrakk> \<Longrightarrow> (?P25 s pde and ?Q25 s pde and (\<lambda>_. True)) sa proof (prove)
goal (3 subgoals):
 1. \<And>s pde. \<lbrakk>range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0); 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> \<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>range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0); 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 (\<lambda>_. True) (\<lambda>sa. ({(?pde26 s pde sa, sa)}, False)) (placeNewObject ptr val sz)
 3. \<And>s pde sa. \<lbrakk>range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0); 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; s = sa\<rbrakk> \<Longrightarrow> (?P25 s pde and (\<lambda>sa. ko_wp_at' ((=) (KOArch (KOPDE (?pde26 s pde sa)))) src sa) and (\<lambda>_. True)) sa proof (prove)
goal (3 subgoals):
 1. \<And>s pde. \<lbrakk>range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0); 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> \<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>range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0); 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 (\<lambda>_. True) (\<lambda>sa. ({(?pde26 s pde sa, sa)}, False)) (placeNewObject ptr val sz)
 3. \<And>s pde sa. \<lbrakk>range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0); 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; s = sa\<rbrakk> \<Longrightarrow> (?P25 s pde and (\<lambda>sa. ko_wp_at' ((=) (KOArch (KOPDE (?pde26 s pde sa)))) src sa) and (\<lambda>_. True)) sa proof (prove)
goal (2 subgoals):
 1. \<And>s pde. \<lbrakk>range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0); 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 (\<lambda>_. True) (\<lambda>sa. ({(?pde34 s pde, sa)}, False)) (placeNewObject ptr val sz)
 2. \<And>s pde sa. \<lbrakk>range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0); 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; 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>_. True)) sa proof (prove)
goal (1 subgoal):
 1. \<And>s pde sa. \<lbrakk>range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0); 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; 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>_. True)) sa proof (prove)
goal:
No subgoals!