theory Detype_R

lemma createNewObjects_pspace_no_overlap':
  "\<lbrace>pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct'
  and K (range_cover ptr sz (Types_H.getObjectSize ty us) (Suc (length dests)))
  and K (ptr \<noteq> 0)
  and K (ty = APIObjectType apiobject_type.CapTableObject \<longrightarrow> us < 28)\<rbrace>
  createNewObjects ty src dests ptr us d
  \<lbrace>\<lambda>rv s.  pspace_aligned' s \<and> pspace_distinct' s \<and>
  pspace_no_overlap' ((of_nat (length dests) << APIType_capBits ty us) + ptr) sz s\<rbrace>" apply (rule hoare_gen_asm)+ proof (induct rule:rev_induct ) case Nil show ?case by (simp add:createNewObjects_def zipWithM_x_mapM mapM_Nil | wp)+ next case (snoc dest dests) have rc:"range_cover ptr sz (Types_H.getObjectSize ty us) (Suc (length dests))" apply (rule range_cover_le) apply (rule snoc) apply simp done show ?case using rc apply (subst createNewObjects_Cons) apply (drule range_cover.weak) apply (simp add: word_bits_def) apply (wp pspace_no_overlap'_lift) apply (simp add: conj_comms) apply (rule hoare_vcg_conj_lift) apply (rule hoare_post_imp[OF _ createObject_pspace_aligned_distinct']) apply simp apply (rule hoare_vcg_conj_lift) apply (rule hoare_post_imp[OF _ createObject_pspace_aligned_distinct']) apply simp apply (simp add:field_simps) apply (wp createObject_pspace_no_overlap') apply (clarsimp simp: conj_comms) apply (rule hoare_pre) apply (rule hoare_vcg_conj_lift) apply (rule hoare_post_imp[OF _ snoc.hyps]) apply (simp add:snoc)+ apply (rule hoare_vcg_conj_lift) apply (rule hoare_post_imp[OF _ snoc.hyps]) apply (simp add:snoc)+ apply wp apply (simp add: conj_comms field_simps) apply (rule hoare_post_imp) apply (erule context_conjI) apply (intro conjI) apply (rule aligned_add_aligned[OF range_cover.aligned
                                           is_aligned_shiftl_self]) apply simp apply simp apply simp apply (erule pspace_no_overlap'_le) apply (simp add: range_cover.sz[where 'a=32, folded word_bits_def])+ apply (rule hoare_post_imp[OF _ snoc.hyps]) apply (simp add:field_simps snoc)+ using snoc apply simp done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct' and K (range_cover ptr sz (getObjectSize ty us) (Suc (length dests))) and K (ptr \<noteq> 0) and K (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28)\<rbrace> createNewObjects ty src dests ptr us d \<lbrace>\<lambda>rv s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) sz s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; ptr \<noteq> 0; range_cover ptr sz (getObjectSize ty us) (Suc (length dests))\<rbrakk> \<Longrightarrow> \<lbrace>pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct'\<rbrace> createNewObjects ty src dests ptr us d \<lbrace>\<lambda>rv s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) sz s\<rbrace> proof (state)
goal (2 subgoals):
 1. \<lbrakk>ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; ptr \<noteq> 0; range_cover ptr sz (getObjectSize ty us) (Suc (length []))\<rbrakk> \<Longrightarrow> \<lbrace>pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct'\<rbrace> createNewObjects ty src [] ptr us d \<lbrace>\<lambda>rv s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ((word_of_nat (length []) << APIType_capBits ty us) + ptr) sz s\<rbrace>
 2. \<And>x xs. \<lbrakk>\<lbrakk>ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; ptr \<noteq> 0; range_cover ptr sz (getObjectSize ty us) (Suc (length xs))\<rbrakk> \<Longrightarrow> \<lbrace>pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct'\<rbrace> createNewObjects ty src xs ptr us d \<lbrace>\<lambda>rv s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ((word_of_nat (length xs) << APIType_capBits ty us) + ptr) sz s\<rbrace>; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; ptr \<noteq> 0; range_cover ptr sz (getObjectSize ty us) (Suc (length (xs @ [x])))\<rbrakk> \<Longrightarrow> \<lbrace>pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct'\<rbrace> createNewObjects ty src (xs @ [x]) ptr us d \<lbrace>\<lambda>rv s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ((word_of_nat (length (xs @ [x])) << APIType_capBits ty us) + ptr) sz s\<rbrace> proof (state)
this:
ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28
ptr \<noteq> 0
range_cover ptr sz (getObjectSize ty us) (Suc (length []))

goal (2 subgoals):
 1. \<lbrakk>ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; ptr \<noteq> 0; range_cover ptr sz (getObjectSize ty us) (Suc (length []))\<rbrakk> \<Longrightarrow> \<lbrace>pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct'\<rbrace> createNewObjects ty src [] ptr us d \<lbrace>\<lambda>rv s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ((word_of_nat (length []) << APIType_capBits ty us) + ptr) sz s\<rbrace>
 2. \<And>x xs. \<lbrakk>\<lbrakk>ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; ptr \<noteq> 0; range_cover ptr sz (getObjectSize ty us) (Suc (length xs))\<rbrakk> \<Longrightarrow> \<lbrace>pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct'\<rbrace> createNewObjects ty src xs ptr us d \<lbrace>\<lambda>rv s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ((word_of_nat (length xs) << APIType_capBits ty us) + ptr) sz s\<rbrace>; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; ptr \<noteq> 0; range_cover ptr sz (getObjectSize ty us) (Suc (length (xs @ [x])))\<rbrakk> \<Longrightarrow> \<lbrace>pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct'\<rbrace> createNewObjects ty src (xs @ [x]) ptr us d \<lbrace>\<lambda>rv s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ((word_of_nat (length (xs @ [x])) << APIType_capBits ty us) + ptr) sz s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct'\<rbrace> createNewObjects ty src [] ptr us d \<lbrace>\<lambda>rv s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ((word_of_nat (length []) << APIType_capBits ty us) + ptr) sz s\<rbrace> proof (state)
this:
\<lbrace>pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct'\<rbrace> createNewObjects ty src [] ptr us d \<lbrace>\<lambda>rv s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ((word_of_nat (length []) << APIType_capBits ty us) + ptr) sz s\<rbrace>

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; ptr \<noteq> 0; range_cover ptr sz (getObjectSize ty us) (Suc (length xs))\<rbrakk> \<Longrightarrow> \<lbrace>pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct'\<rbrace> createNewObjects ty src xs ptr us d \<lbrace>\<lambda>rv s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ((word_of_nat (length xs) << APIType_capBits ty us) + ptr) sz s\<rbrace>; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; ptr \<noteq> 0; range_cover ptr sz (getObjectSize ty us) (Suc (length (xs @ [x])))\<rbrakk> \<Longrightarrow> \<lbrace>pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct'\<rbrace> createNewObjects ty src (xs @ [x]) ptr us d \<lbrace>\<lambda>rv s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ((word_of_nat (length (xs @ [x])) << APIType_capBits ty us) + ptr) sz s\<rbrace> proof (state)
goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; ptr \<noteq> 0; range_cover ptr sz (getObjectSize ty us) (Suc (length xs))\<rbrakk> \<Longrightarrow> \<lbrace>pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct'\<rbrace> createNewObjects ty src xs ptr us d \<lbrace>\<lambda>rv s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ((word_of_nat (length xs) << APIType_capBits ty us) + ptr) sz s\<rbrace>; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; ptr \<noteq> 0; range_cover ptr sz (getObjectSize ty us) (Suc (length (xs @ [x])))\<rbrakk> \<Longrightarrow> \<lbrace>pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct'\<rbrace> createNewObjects ty src (xs @ [x]) ptr us d \<lbrace>\<lambda>rv s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ((word_of_nat (length (xs @ [x])) << APIType_capBits ty us) + ptr) sz s\<rbrace> proof (state)
this:
\<lbrakk>ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; ptr \<noteq> 0; range_cover ptr sz (getObjectSize ty us) (Suc (length dests))\<rbrakk> \<Longrightarrow> \<lbrace>pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct'\<rbrace> createNewObjects ty src dests ptr us d \<lbrace>\<lambda>rv s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) sz s\<rbrace>
ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28
ptr \<noteq> 0
range_cover ptr sz (getObjectSize ty us) (Suc (length (dests @ [dest])))

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; ptr \<noteq> 0; range_cover ptr sz (getObjectSize ty us) (Suc (length xs))\<rbrakk> \<Longrightarrow> \<lbrace>pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct'\<rbrace> createNewObjects ty src xs ptr us d \<lbrace>\<lambda>rv s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ((word_of_nat (length xs) << APIType_capBits ty us) + ptr) sz s\<rbrace>; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; ptr \<noteq> 0; range_cover ptr sz (getObjectSize ty us) (Suc (length (xs @ [x])))\<rbrakk> \<Longrightarrow> \<lbrace>pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct'\<rbrace> createNewObjects ty src (xs @ [x]) ptr us d \<lbrace>\<lambda>rv s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ((word_of_nat (length (xs @ [x])) << APIType_capBits ty us) + ptr) sz s\<rbrace> proof (prove)
goal (1 subgoal):
 1. range_cover ptr sz (getObjectSize ty us) (Suc (length dests)) proof (prove)
goal (2 subgoals):
 1. range_cover ptr sz (getObjectSize ty us) ?m
 2. Suc (length dests) \<le> ?m proof (prove)
goal (1 subgoal):
 1. Suc (length dests) \<le> Suc (length (dests @ [dest])) proof (prove)
goal:
No subgoals! proof (state)
this:
range_cover ptr sz (getObjectSize ty us) (Suc (length dests))

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; ptr \<noteq> 0; range_cover ptr sz (getObjectSize ty us) (Suc (length xs))\<rbrakk> \<Longrightarrow> \<lbrace>pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct'\<rbrace> createNewObjects ty src xs ptr us d \<lbrace>\<lambda>rv s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ((word_of_nat (length xs) << APIType_capBits ty us) + ptr) sz s\<rbrace>; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; ptr \<noteq> 0; range_cover ptr sz (getObjectSize ty us) (Suc (length (xs @ [x])))\<rbrakk> \<Longrightarrow> \<lbrace>pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct'\<rbrace> createNewObjects ty src (xs @ [x]) ptr us d \<lbrace>\<lambda>rv s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ((word_of_nat (length (xs @ [x])) << APIType_capBits ty us) + ptr) sz s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct'\<rbrace> createNewObjects ty src (dests @ [dest]) ptr us d \<lbrace>\<lambda>rv s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ((word_of_nat (length (dests @ [dest])) << APIType_capBits ty us) + ptr) sz s\<rbrace> proof (prove)
using this:
range_cover ptr sz (getObjectSize ty us) (Suc (length dests))

goal (1 subgoal):
 1. \<lbrace>pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct'\<rbrace> createNewObjects ty src (dests @ [dest]) ptr us d \<lbrace>\<lambda>rv s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ((word_of_nat (length (dests @ [dest])) << APIType_capBits ty us) + ptr) sz s\<rbrace> proof (prove)
goal (2 subgoals):
 1. range_cover ptr sz (getObjectSize ty us) (Suc (length dests)) \<Longrightarrow> length dests < 2 ^ word_bits
 2. range_cover ptr sz (getObjectSize ty us) (Suc (length dests)) \<Longrightarrow> \<lbrace>pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct'\<rbrace> do createNewObjects ty src dests ptr us d;
global.createObject ty ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) us d >>= insertNewCap src dest
od \<lbrace>\<lambda>rv s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ((word_of_nat (length (dests @ [dest])) << APIType_capBits ty us) + ptr) sz s\<rbrace> proof (prove)
goal (2 subgoals):
 1. Suc (length dests) < 2 ^ LENGTH(32) \<Longrightarrow> length dests < 2 ^ word_bits
 2. range_cover ptr sz (getObjectSize ty us) (Suc (length dests)) \<Longrightarrow> \<lbrace>pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct'\<rbrace> do createNewObjects ty src dests ptr us d;
global.createObject ty ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) us d >>= insertNewCap src dest
od \<lbrace>\<lambda>rv s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ((word_of_nat (length (dests @ [dest])) << APIType_capBits ty us) + ptr) sz s\<rbrace> proof (prove)
goal (1 subgoal):
 1. range_cover ptr sz (getObjectSize ty us) (Suc (length dests)) \<Longrightarrow> \<lbrace>pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct'\<rbrace> do createNewObjects ty src dests ptr us d;
global.createObject ty ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) us d >>= insertNewCap src dest
od \<lbrace>\<lambda>rv s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ((word_of_nat (length (dests @ [dest])) << APIType_capBits ty us) + ptr) sz s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x. range_cover ptr sz (getObjectSize ty us) (Suc (length dests)) \<Longrightarrow> \<lbrace>?B10 x\<rbrace> global.createObject ty ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) us d \<lbrace>\<lambda>xa s. pspace_aligned' s \<and> pspace_distinct' s \<and> ((\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s) and pspace_no_overlap' ((word_of_nat (length (dests @ [dest])) << APIType_capBits ty us) + ptr) sz) s\<rbrace>
 2. range_cover ptr sz (getObjectSize ty us) (Suc (length dests)) \<Longrightarrow> \<lbrace>?Q9\<rbrace> createNewObjects ty src dests ptr us d \<lbrace>?B10\<rbrace>
 3. \<And>s. \<lbrakk>range_cover ptr sz (getObjectSize ty us) (Suc (length dests)); (pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> ?Q9 s proof (prove)
goal (3 subgoals):
 1. range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)) \<Longrightarrow> \<lbrace>?B10 ()\<rbrace> global.createObject ty ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) us d \<lbrace>\<lambda>xa s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ((1 + word_of_nat (length dests) << APIType_capBits ty us) + ptr) sz s\<rbrace>
 2. range_cover ptr sz (getObjectSize ty us) (Suc (length dests)) \<Longrightarrow> \<lbrace>?Q9\<rbrace> createNewObjects ty src dests ptr us d \<lbrace>?B10\<rbrace>
 3. \<And>s. \<lbrakk>range_cover ptr sz (getObjectSize ty us) (Suc (length dests)); (pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> ?Q9 s proof (prove)
goal (4 subgoals):
 1. range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)) \<Longrightarrow> \<lbrace>?P25 ()\<rbrace> global.createObject ty ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) us d \<lbrace>\<lambda>rv. pspace_aligned'\<rbrace>
 2. range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)) \<Longrightarrow> \<lbrace>?P'24 ()\<rbrace> global.createObject ty ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) us d \<lbrace>\<lambda>rv s. pspace_distinct' s \<and> pspace_no_overlap' ((1 + word_of_nat (length dests) << APIType_capBits ty us) + ptr) sz s\<rbrace>
 3. range_cover ptr sz (getObjectSize ty us) (Suc (length dests)) \<Longrightarrow> \<lbrace>?Q9\<rbrace> createNewObjects ty src dests ptr us d \<lbrace>\<lambda>a b. ?P25 a b \<and> ?P'24 a b\<rbrace>
 4. \<And>s. \<lbrakk>range_cover ptr sz (getObjectSize ty us) (Suc (length dests)); (pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> ?Q9 s proof (prove)
goal (4 subgoals):
 1. \<And>rv s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); pspace_aligned' s \<and> pspace_distinct' s\<rbrakk> \<Longrightarrow> pspace_aligned' s
 2. range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)) \<Longrightarrow> \<lbrace>?P'24 ()\<rbrace> global.createObject ty ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) us d \<lbrace>\<lambda>rv s. pspace_distinct' s \<and> pspace_no_overlap' ((1 + word_of_nat (length dests) << APIType_capBits ty us) + ptr) sz s\<rbrace>
 3. range_cover ptr sz (getObjectSize ty us) (Suc (length dests)) \<Longrightarrow> \<lbrace>?Q9\<rbrace> createNewObjects ty src dests ptr us d \<lbrace>\<lambda>a b. (pspace_aligned' and K (is_aligned ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (APIType_capBits ty us)) and pspace_distinct' and pspace_no_overlap' ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (APIType_capBits ty us) and K (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28)) b \<and> ?P'24 a b\<rbrace>
 4. \<And>s. \<lbrakk>range_cover ptr sz (getObjectSize ty us) (Suc (length dests)); (pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> ?Q9 s proof (prove)
goal (3 subgoals):
 1. range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)) \<Longrightarrow> \<lbrace>?P'24 ()\<rbrace> global.createObject ty ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) us d \<lbrace>\<lambda>rv s. pspace_distinct' s \<and> pspace_no_overlap' ((1 + word_of_nat (length dests) << APIType_capBits ty us) + ptr) sz s\<rbrace>
 2. range_cover ptr sz (getObjectSize ty us) (Suc (length dests)) \<Longrightarrow> \<lbrace>?Q9\<rbrace> createNewObjects ty src dests ptr us d \<lbrace>\<lambda>a b. (pspace_aligned' and K (is_aligned ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (APIType_capBits ty us)) and pspace_distinct' and pspace_no_overlap' ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (APIType_capBits ty us) and K (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28)) b \<and> ?P'24 a b\<rbrace>
 3. \<And>s. \<lbrakk>range_cover ptr sz (getObjectSize ty us) (Suc (length dests)); (pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> ?Q9 s proof (prove)
goal (4 subgoals):
 1. range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)) \<Longrightarrow> \<lbrace>?P34 ()\<rbrace> global.createObject ty ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) us d \<lbrace>\<lambda>rv. pspace_distinct'\<rbrace>
 2. range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)) \<Longrightarrow> \<lbrace>?P'33 ()\<rbrace> global.createObject ty ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) us d \<lbrace>\<lambda>rv. pspace_no_overlap' ((1 + word_of_nat (length dests) << APIType_capBits ty us) + ptr) sz\<rbrace>
 3. range_cover ptr sz (getObjectSize ty us) (Suc (length dests)) \<Longrightarrow> \<lbrace>?Q9\<rbrace> createNewObjects ty src dests ptr us d \<lbrace>\<lambda>a b. (pspace_aligned' and K (is_aligned ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (APIType_capBits ty us)) and pspace_distinct' and pspace_no_overlap' ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (APIType_capBits ty us) and K (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28)) b \<and> ?P34 a b \<and> ?P'33 a b\<rbrace>
 4. \<And>s. \<lbrakk>range_cover ptr sz (getObjectSize ty us) (Suc (length dests)); (pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> ?Q9 s proof (prove)
goal (4 subgoals):
 1. \<And>rv s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); pspace_aligned' s \<and> pspace_distinct' s\<rbrakk> \<Longrightarrow> pspace_distinct' s
 2. range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)) \<Longrightarrow> \<lbrace>?P'33 ()\<rbrace> global.createObject ty ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) us d \<lbrace>\<lambda>rv. pspace_no_overlap' ((1 + word_of_nat (length dests) << APIType_capBits ty us) + ptr) sz\<rbrace>
 3. range_cover ptr sz (getObjectSize ty us) (Suc (length dests)) \<Longrightarrow> \<lbrace>?Q9\<rbrace> createNewObjects ty src dests ptr us d \<lbrace>\<lambda>a b. (pspace_aligned' and K (is_aligned ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (APIType_capBits ty us)) and pspace_distinct' and pspace_no_overlap' ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (APIType_capBits ty us) and K (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28)) b \<and> (pspace_aligned' and K (is_aligned ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (APIType_capBits ty us)) and pspace_distinct' and pspace_no_overlap' ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (APIType_capBits ty us) and K (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28)) b \<and> ?P'33 a b\<rbrace>
 4. \<And>s. \<lbrakk>range_cover ptr sz (getObjectSize ty us) (Suc (length dests)); (pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> ?Q9 s proof (prove)
goal (3 subgoals):
 1. range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)) \<Longrightarrow> \<lbrace>?P'33 ()\<rbrace> global.createObject ty ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) us d \<lbrace>\<lambda>rv. pspace_no_overlap' ((1 + word_of_nat (length dests) << APIType_capBits ty us) + ptr) sz\<rbrace>
 2. range_cover ptr sz (getObjectSize ty us) (Suc (length dests)) \<Longrightarrow> \<lbrace>?Q9\<rbrace> createNewObjects ty src dests ptr us d \<lbrace>\<lambda>a b. (pspace_aligned' and K (is_aligned ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (APIType_capBits ty us)) and pspace_distinct' and pspace_no_overlap' ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (APIType_capBits ty us) and K (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28)) b \<and> (pspace_aligned' and K (is_aligned ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (APIType_capBits ty us)) and pspace_distinct' and pspace_no_overlap' ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (APIType_capBits ty us) and K (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28)) b \<and> ?P'33 a b\<rbrace>
 3. \<And>s. \<lbrakk>range_cover ptr sz (getObjectSize ty us) (Suc (length dests)); (pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> ?Q9 s proof (prove)
goal (3 subgoals):
 1. range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)) \<Longrightarrow> \<lbrace>?P'33 ()\<rbrace> global.createObject ty (ptr + (word_of_nat (length dests) << APIType_capBits ty us)) us d \<lbrace>\<lambda>rv. pspace_no_overlap' (ptr + (1 + word_of_nat (length dests) << APIType_capBits ty us)) sz\<rbrace>
 2. range_cover ptr sz (getObjectSize ty us) (Suc (length dests)) \<Longrightarrow> \<lbrace>?Q9\<rbrace> createNewObjects ty src dests ptr us d \<lbrace>\<lambda>a b. (pspace_aligned' and K (is_aligned ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (APIType_capBits ty us)) and pspace_distinct' and pspace_no_overlap' ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (APIType_capBits ty us) and K (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28)) b \<and> (pspace_aligned' and K (is_aligned ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (APIType_capBits ty us)) and pspace_distinct' and pspace_no_overlap' ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (APIType_capBits ty us) and K (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28)) b \<and> ?P'33 a b\<rbrace>
 3. \<And>s. \<lbrakk>range_cover ptr sz (getObjectSize ty us) (Suc (length dests)); (pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> ?Q9 s proof (prove)
goal (2 subgoals):
 1. range_cover ptr sz (getObjectSize ty us) (Suc (length dests)) \<Longrightarrow> \<lbrace>?Q9\<rbrace> createNewObjects ty src dests ptr us d \<lbrace>\<lambda>a b. (pspace_aligned' and K (is_aligned ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (APIType_capBits ty us)) and pspace_distinct' and pspace_no_overlap' ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (APIType_capBits ty us) and K (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28)) b \<and> (pspace_aligned' and K (is_aligned ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (APIType_capBits ty us)) and pspace_distinct' and pspace_no_overlap' ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (APIType_capBits ty us) and K (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28)) b \<and> pspace_no_overlap' (ptr + (word_of_nat (length dests) << APIType_capBits ty us)) sz b \<and> pspace_aligned' b \<and> pspace_distinct' b \<and> range_cover ptr sz (APIType_capBits ty us) (length dests + 2) \<and> ptr \<noteq> 0\<rbrace>
 2. \<And>s. \<lbrakk>range_cover ptr sz (getObjectSize ty us) (Suc (length dests)); (pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> ?Q9 s proof (prove)
goal (2 subgoals):
 1. range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)) \<Longrightarrow> \<lbrace>?Q9\<rbrace> createNewObjects ty src dests ptr us d \<lbrace>\<lambda>a b. pspace_aligned' b \<and> pspace_distinct' b \<and> ptr \<noteq> 0 \<and> range_cover ptr sz (APIType_capBits ty us) (Suc (Suc (length dests))) \<and> pspace_no_overlap' (ptr + (word_of_nat (length dests) << APIType_capBits ty us)) sz b \<and> is_aligned ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (APIType_capBits ty us) \<and> (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28) \<and> pspace_no_overlap' ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (APIType_capBits ty us) b\<rbrace>
 2. \<And>s. \<lbrakk>range_cover ptr sz (getObjectSize ty us) (Suc (length dests)); (pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> ?Q9 s proof (prove)
goal (3 subgoals):
 1. range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)) \<Longrightarrow> \<lbrace>?Q46\<rbrace> createNewObjects ty src dests ptr us d \<lbrace>\<lambda>a b. pspace_aligned' b \<and> pspace_distinct' b \<and> ptr \<noteq> 0 \<and> range_cover ptr sz (APIType_capBits ty us) (Suc (Suc (length dests))) \<and> pspace_no_overlap' (ptr + (word_of_nat (length dests) << APIType_capBits ty us)) sz b \<and> is_aligned ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (APIType_capBits ty us) \<and> (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28) \<and> pspace_no_overlap' ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (APIType_capBits ty us) b\<rbrace>
 2. \<And>s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ?Q9 s\<rbrakk> \<Longrightarrow> ?Q46 s
 3. \<And>s. \<lbrakk>range_cover ptr sz (getObjectSize ty us) (Suc (length dests)); (pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> ?Q9 s proof (prove)
goal (4 subgoals):
 1. range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)) \<Longrightarrow> \<lbrace>?P49\<rbrace> createNewObjects ty src dests ptr us d \<lbrace>\<lambda>rv. pspace_aligned'\<rbrace>
 2. range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)) \<Longrightarrow> \<lbrace>?P'49\<rbrace> createNewObjects ty src dests ptr us d \<lbrace>\<lambda>rv s. pspace_distinct' s \<and> ptr \<noteq> 0 \<and> range_cover ptr sz (APIType_capBits ty us) (Suc (Suc (length dests))) \<and> pspace_no_overlap' (ptr + (word_of_nat (length dests) << APIType_capBits ty us)) sz s \<and> is_aligned ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (APIType_capBits ty us) \<and> (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28) \<and> pspace_no_overlap' ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (APIType_capBits ty us) s\<rbrace>
 3. \<And>s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ?Q9 s\<rbrakk> \<Longrightarrow> ?P49 s \<and> ?P'49 s
 4. \<And>s. \<lbrakk>range_cover ptr sz (getObjectSize ty us) (Suc (length dests)); (pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> ?Q9 s proof (prove)
goal (7 subgoals):
 1. \<And>rv s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) sz s\<rbrakk> \<Longrightarrow> pspace_aligned' s
 2. range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)) \<Longrightarrow> ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28
 3. range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)) \<Longrightarrow> ptr \<noteq> 0
 4. range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)) \<Longrightarrow> range_cover ptr sz (getObjectSize ty us) (Suc (length dests))
 5. range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)) \<Longrightarrow> \<lbrace>?P'49\<rbrace> createNewObjects ty src dests ptr us d \<lbrace>\<lambda>rv s. pspace_distinct' s \<and> ptr \<noteq> 0 \<and> range_cover ptr sz (APIType_capBits ty us) (Suc (Suc (length dests))) \<and> pspace_no_overlap' (ptr + (word_of_nat (length dests) << APIType_capBits ty us)) sz s \<and> is_aligned ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (APIType_capBits ty us) \<and> (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28) \<and> pspace_no_overlap' ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (APIType_capBits ty us) s\<rbrace>
 6. \<And>s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ?Q9 s\<rbrakk> \<Longrightarrow> (pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s \<and> ?P'49 s
 7. \<And>s. \<lbrakk>range_cover ptr sz (getObjectSize ty us) (Suc (length dests)); (pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> ?Q9 s proof (prove)
goal (3 subgoals):
 1. range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)) \<Longrightarrow> \<lbrace>?P'49\<rbrace> createNewObjects ty src dests ptr us d \<lbrace>\<lambda>rv s. pspace_distinct' s \<and> range_cover ptr sz (APIType_capBits ty us) (Suc (Suc (length dests))) \<and> pspace_no_overlap' (ptr + (word_of_nat (length dests) << APIType_capBits ty us)) sz s \<and> is_aligned ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (APIType_capBits ty us) \<and> pspace_no_overlap' ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (APIType_capBits ty us) s\<rbrace>
 2. \<And>s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ?Q9 s\<rbrakk> \<Longrightarrow> (pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s \<and> ?P'49 s
 3. \<And>s. \<lbrakk>range_cover ptr sz (getObjectSize ty us) (Suc (length dests)); (pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> ?Q9 s proof (prove)
goal (4 subgoals):
 1. range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)) \<Longrightarrow> \<lbrace>?P58\<rbrace> createNewObjects ty src dests ptr us d \<lbrace>\<lambda>rv. pspace_distinct'\<rbrace>
 2. range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)) \<Longrightarrow> \<lbrace>?P'58\<rbrace> createNewObjects ty src dests ptr us d \<lbrace>\<lambda>rv s. range_cover ptr sz (APIType_capBits ty us) (Suc (Suc (length dests))) \<and> pspace_no_overlap' (ptr + (word_of_nat (length dests) << APIType_capBits ty us)) sz s \<and> is_aligned ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (APIType_capBits ty us) \<and> pspace_no_overlap' ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (APIType_capBits ty us) s\<rbrace>
 3. \<And>s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ?Q9 s\<rbrakk> \<Longrightarrow> (pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s \<and> ?P58 s \<and> ?P'58 s
 4. \<And>s. \<lbrakk>range_cover ptr sz (getObjectSize ty us) (Suc (length dests)); (pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> ?Q9 s proof (prove)
goal (7 subgoals):
 1. \<And>rv s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) sz s\<rbrakk> \<Longrightarrow> pspace_distinct' s
 2. range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)) \<Longrightarrow> ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28
 3. range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)) \<Longrightarrow> ptr \<noteq> 0
 4. range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)) \<Longrightarrow> range_cover ptr sz (getObjectSize ty us) (Suc (length dests))
 5. range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)) \<Longrightarrow> \<lbrace>?P'58\<rbrace> createNewObjects ty src dests ptr us d \<lbrace>\<lambda>rv s. range_cover ptr sz (APIType_capBits ty us) (Suc (Suc (length dests))) \<and> pspace_no_overlap' (ptr + (word_of_nat (length dests) << APIType_capBits ty us)) sz s \<and> is_aligned ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (APIType_capBits ty us) \<and> pspace_no_overlap' ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (APIType_capBits ty us) s\<rbrace>
 6. \<And>s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ?Q9 s\<rbrakk> \<Longrightarrow> (pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s \<and> (pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s \<and> ?P'58 s
 7. \<And>s. \<lbrakk>range_cover ptr sz (getObjectSize ty us) (Suc (length dests)); (pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> ?Q9 s proof (prove)
goal (3 subgoals):
 1. range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)) \<Longrightarrow> \<lbrace>?P'58\<rbrace> createNewObjects ty src dests ptr us d \<lbrace>\<lambda>rv s. range_cover ptr sz (APIType_capBits ty us) (Suc (Suc (length dests))) \<and> pspace_no_overlap' (ptr + (word_of_nat (length dests) << APIType_capBits ty us)) sz s \<and> is_aligned ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (APIType_capBits ty us) \<and> pspace_no_overlap' ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (APIType_capBits ty us) s\<rbrace>
 2. \<And>s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ?Q9 s\<rbrakk> \<Longrightarrow> (pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s \<and> (pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s \<and> ?P'58 s
 3. \<And>s. \<lbrakk>range_cover ptr sz (getObjectSize ty us) (Suc (length dests)); (pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> ?Q9 s proof (prove)
goal (3 subgoals):
 1. range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)) \<Longrightarrow> \<lbrace>?P'68\<rbrace> createNewObjects ty src dests ptr us d \<lbrace>\<lambda>rv s. pspace_no_overlap' (ptr + (word_of_nat (length dests) << APIType_capBits ty us)) sz s \<and> is_aligned ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (APIType_capBits ty us) \<and> pspace_no_overlap' ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (APIType_capBits ty us) s\<rbrace>
 2. \<And>s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ?Q9 s\<rbrakk> \<Longrightarrow> (pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s \<and> (pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s \<and> range_cover ptr sz (APIType_capBits ty us) (Suc (Suc (length dests))) \<and> ?P'68 s
 3. \<And>s. \<lbrakk>range_cover ptr sz (getObjectSize ty us) (Suc (length dests)); (pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> ?Q9 s proof (prove)
goal (3 subgoals):
 1. range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)) \<Longrightarrow> \<lbrace>?P'68\<rbrace> createNewObjects ty src dests ptr us d \<lbrace>\<lambda>rv s. pspace_no_overlap' (ptr + (word_of_nat (length dests) << APIType_capBits ty us)) sz s \<and> is_aligned (ptr + (word_of_nat (length dests) << APIType_capBits ty us)) (APIType_capBits ty us) \<and> pspace_no_overlap' (ptr + (word_of_nat (length dests) << APIType_capBits ty us)) (APIType_capBits ty us) s\<rbrace>
 2. \<And>s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ?Q9 s\<rbrakk> \<Longrightarrow> (pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s \<and> (pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s \<and> range_cover ptr sz (APIType_capBits ty us) (Suc (Suc (length dests))) \<and> ?P'68 s
 3. \<And>s. \<lbrakk>range_cover ptr sz (getObjectSize ty us) (Suc (length dests)); (pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> ?Q9 s proof (prove)
goal (4 subgoals):
 1. \<And>rv s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ?Q72 rv s\<rbrakk> \<Longrightarrow> pspace_no_overlap' (ptr + (word_of_nat (length dests) << APIType_capBits ty us)) sz s \<and> is_aligned (ptr + (word_of_nat (length dests) << APIType_capBits ty us)) (APIType_capBits ty us) \<and> pspace_no_overlap' (ptr + (word_of_nat (length dests) << APIType_capBits ty us)) (APIType_capBits ty us) s
 2. range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)) \<Longrightarrow> \<lbrace>?P'68\<rbrace> createNewObjects ty src dests ptr us d \<lbrace>?Q72\<rbrace>
 3. \<And>s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ?Q9 s\<rbrakk> \<Longrightarrow> (pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s \<and> (pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s \<and> range_cover ptr sz (APIType_capBits ty us) (Suc (Suc (length dests))) \<and> ?P'68 s
 4. \<And>s. \<lbrakk>range_cover ptr sz (getObjectSize ty us) (Suc (length dests)); (pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> ?Q9 s proof (prove)
goal (4 subgoals):
 1. \<And>rv s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); pspace_no_overlap' (ptr + (word_of_nat (length dests) << APIType_capBits ty us)) sz s\<rbrakk> \<Longrightarrow> is_aligned (ptr + (word_of_nat (length dests) << APIType_capBits ty us)) (APIType_capBits ty us) \<and> pspace_no_overlap' (ptr + (word_of_nat (length dests) << APIType_capBits ty us)) (APIType_capBits ty us) s
 2. range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)) \<Longrightarrow> \<lbrace>?P'68\<rbrace> createNewObjects ty src dests ptr us d \<lbrace>\<lambda>rv. pspace_no_overlap' (ptr + (word_of_nat (length dests) << APIType_capBits ty us)) sz\<rbrace>
 3. \<And>s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ?Q9 s\<rbrakk> \<Longrightarrow> (pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s \<and> (pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s \<and> range_cover ptr sz (APIType_capBits ty us) (Suc (Suc (length dests))) \<and> ?P'68 s
 4. \<And>s. \<lbrakk>range_cover ptr sz (getObjectSize ty us) (Suc (length dests)); (pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> ?Q9 s proof (prove)
goal (5 subgoals):
 1. \<And>rv s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); pspace_no_overlap' (ptr + (word_of_nat (length dests) << APIType_capBits ty us)) sz s\<rbrakk> \<Longrightarrow> is_aligned (ptr + (word_of_nat (length dests) << APIType_capBits ty us)) (APIType_capBits ty us)
 2. \<And>rv s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); pspace_no_overlap' (ptr + (word_of_nat (length dests) << APIType_capBits ty us)) sz s\<rbrakk> \<Longrightarrow> pspace_no_overlap' (ptr + (word_of_nat (length dests) << APIType_capBits ty us)) (APIType_capBits ty us) s
 3. range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)) \<Longrightarrow> \<lbrace>?P'68\<rbrace> createNewObjects ty src dests ptr us d \<lbrace>\<lambda>rv. pspace_no_overlap' (ptr + (word_of_nat (length dests) << APIType_capBits ty us)) sz\<rbrace>
 4. \<And>s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ?Q9 s\<rbrakk> \<Longrightarrow> (pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s \<and> (pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s \<and> range_cover ptr sz (APIType_capBits ty us) (Suc (Suc (length dests))) \<and> ?P'68 s
 5. \<And>s. \<lbrakk>range_cover ptr sz (getObjectSize ty us) (Suc (length dests)); (pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> ?Q9 s proof (prove)
goal (6 subgoals):
 1. \<And>rv s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); pspace_no_overlap' (ptr + (word_of_nat (length dests) << APIType_capBits ty us)) sz s\<rbrakk> \<Longrightarrow> range_cover ptr (?sz80 rv s) (?n78 rv s) (?n80 rv s)
 2. \<And>rv s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); pspace_no_overlap' (ptr + (word_of_nat (length dests) << APIType_capBits ty us)) sz s\<rbrakk> \<Longrightarrow> APIType_capBits ty us \<le> ?n78 rv s
 3. \<And>rv s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); pspace_no_overlap' (ptr + (word_of_nat (length dests) << APIType_capBits ty us)) sz s\<rbrakk> \<Longrightarrow> pspace_no_overlap' (ptr + (word_of_nat (length dests) << APIType_capBits ty us)) (APIType_capBits ty us) s
 4. range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)) \<Longrightarrow> \<lbrace>?P'68\<rbrace> createNewObjects ty src dests ptr us d \<lbrace>\<lambda>rv. pspace_no_overlap' (ptr + (word_of_nat (length dests) << APIType_capBits ty us)) sz\<rbrace>
 5. \<And>s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ?Q9 s\<rbrakk> \<Longrightarrow> (pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s \<and> (pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s \<and> range_cover ptr sz (APIType_capBits ty us) (Suc (Suc (length dests))) \<and> ?P'68 s
 6. \<And>s. \<lbrakk>range_cover ptr sz (getObjectSize ty us) (Suc (length dests)); (pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> ?Q9 s proof (prove)
goal (5 subgoals):
 1. \<And>rv s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); pspace_no_overlap' (ptr + (word_of_nat (length dests) << APIType_capBits ty us)) sz s\<rbrakk> \<Longrightarrow> APIType_capBits ty us \<le> APIType_capBits ty us
 2. \<And>rv s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); pspace_no_overlap' (ptr + (word_of_nat (length dests) << APIType_capBits ty us)) sz s\<rbrakk> \<Longrightarrow> pspace_no_overlap' (ptr + (word_of_nat (length dests) << APIType_capBits ty us)) (APIType_capBits ty us) s
 3. range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)) \<Longrightarrow> \<lbrace>?P'68\<rbrace> createNewObjects ty src dests ptr us d \<lbrace>\<lambda>rv. pspace_no_overlap' (ptr + (word_of_nat (length dests) << APIType_capBits ty us)) sz\<rbrace>
 4. \<And>s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ?Q9 s\<rbrakk> \<Longrightarrow> (pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s \<and> (pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s \<and> range_cover ptr sz (APIType_capBits ty us) (Suc (Suc (length dests))) \<and> ?P'68 s
 5. \<And>s. \<lbrakk>range_cover ptr sz (getObjectSize ty us) (Suc (length dests)); (pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> ?Q9 s proof (prove)
goal (4 subgoals):
 1. \<And>rv s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); pspace_no_overlap' (ptr + (word_of_nat (length dests) << APIType_capBits ty us)) sz s\<rbrakk> \<Longrightarrow> pspace_no_overlap' (ptr + (word_of_nat (length dests) << APIType_capBits ty us)) (APIType_capBits ty us) s
 2. range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)) \<Longrightarrow> \<lbrace>?P'68\<rbrace> createNewObjects ty src dests ptr us d \<lbrace>\<lambda>rv. pspace_no_overlap' (ptr + (word_of_nat (length dests) << APIType_capBits ty us)) sz\<rbrace>
 3. \<And>s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ?Q9 s\<rbrakk> \<Longrightarrow> (pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s \<and> (pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s \<and> range_cover ptr sz (APIType_capBits ty us) (Suc (Suc (length dests))) \<and> ?P'68 s
 4. \<And>s. \<lbrakk>range_cover ptr sz (getObjectSize ty us) (Suc (length dests)); (pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> ?Q9 s proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); pspace_no_overlap' (ptr + (word_of_nat (length dests) << APIType_capBits ty us)) sz s\<rbrakk> \<Longrightarrow> pspace_no_overlap' (ptr + (word_of_nat (length dests) << APIType_capBits ty us)) (APIType_capBits ty us) s
 2. range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)) \<Longrightarrow> \<lbrace>?P'68\<rbrace> createNewObjects ty src dests ptr us d \<lbrace>\<lambda>rv. pspace_no_overlap' (ptr + (word_of_nat (length dests) << APIType_capBits ty us)) sz\<rbrace>
 3. \<And>s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ?Q9 s\<rbrakk> \<Longrightarrow> (pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s \<and> (pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s \<and> range_cover ptr sz (APIType_capBits ty us) (Suc (Suc (length dests))) \<and> ?P'68 s
 4. \<And>s. \<lbrakk>range_cover ptr sz (getObjectSize ty us) (Suc (length dests)); (pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> ?Q9 s proof (prove)
goal (5 subgoals):
 1. \<And>s. range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)) \<Longrightarrow> APIType_capBits ty us \<le> sz
 2. \<And>s. range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)) \<Longrightarrow> sz < word_bits
 3. range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)) \<Longrightarrow> \<lbrace>?P'68\<rbrace> createNewObjects ty src dests ptr us d \<lbrace>\<lambda>rv. pspace_no_overlap' (ptr + (word_of_nat (length dests) << APIType_capBits ty us)) sz\<rbrace>
 4. \<And>s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ?Q9 s\<rbrakk> \<Longrightarrow> (pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s \<and> (pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s \<and> range_cover ptr sz (APIType_capBits ty us) (Suc (Suc (length dests))) \<and> ?P'68 s
 5. \<And>s. \<lbrakk>range_cover ptr sz (getObjectSize ty us) (Suc (length dests)); (pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> ?Q9 s proof (prove)
goal (3 subgoals):
 1. range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)) \<Longrightarrow> \<lbrace>?P'68\<rbrace> createNewObjects ty src dests ptr us d \<lbrace>\<lambda>rv. pspace_no_overlap' (ptr + (word_of_nat (length dests) << APIType_capBits ty us)) sz\<rbrace>
 2. \<And>s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ?Q9 s\<rbrakk> \<Longrightarrow> (pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s \<and> (pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s \<and> range_cover ptr sz (APIType_capBits ty us) (Suc (Suc (length dests))) \<and> ?P'68 s
 3. \<And>s. \<lbrakk>range_cover ptr sz (getObjectSize ty us) (Suc (length dests)); (pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> ?Q9 s proof (prove)
goal (6 subgoals):
 1. \<And>rv s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) sz s\<rbrakk> \<Longrightarrow> pspace_no_overlap' (ptr + (word_of_nat (length dests) << APIType_capBits ty us)) sz s
 2. range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)) \<Longrightarrow> ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28
 3. range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)) \<Longrightarrow> ptr \<noteq> 0
 4. range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)) \<Longrightarrow> range_cover ptr sz (getObjectSize ty us) (Suc (length dests))
 5. \<And>s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ?Q9 s\<rbrakk> \<Longrightarrow> (pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s \<and> (pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s \<and> range_cover ptr sz (APIType_capBits ty us) (Suc (Suc (length dests))) \<and> (pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s
 6. \<And>s. \<lbrakk>range_cover ptr sz (getObjectSize ty us) (Suc (length dests)); (pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> ?Q9 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); pspace_no_overlap' ptr sz s \<and> pspace_aligned' s \<and> pspace_distinct' s\<rbrakk> \<Longrightarrow> range_cover ptr sz (APIType_capBits ty us) (Suc (Suc (length dests))) proof (prove)
using this:
\<lbrakk>ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; ptr \<noteq> 0; range_cover ptr sz (getObjectSize ty us) (Suc (length dests))\<rbrakk> \<Longrightarrow> \<lbrace>pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct'\<rbrace> createNewObjects ty src dests ptr us d \<lbrace>\<lambda>rv s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) sz s\<rbrace>
ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28
ptr \<noteq> 0
range_cover ptr sz (getObjectSize ty us) (Suc (length (dests @ [dest])))

goal (1 subgoal):
 1. \<And>s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); pspace_no_overlap' ptr sz s \<and> pspace_aligned' s \<and> pspace_distinct' s\<rbrakk> \<Longrightarrow> range_cover ptr sz (APIType_capBits ty us) (Suc (Suc (length dests))) proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct'\<rbrace> createNewObjects ty src (dests @ [dest]) ptr us d \<lbrace>\<lambda>rv s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ((word_of_nat (length (dests @ [dest])) << APIType_capBits ty us) + ptr) sz s\<rbrace>

goal:
No subgoals!