theory PageTableDuplicates

lemma createNewObjects_valid_duplicates'[wp]:
 "\<lbrace> (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_no_overlap' ptr sz
  and pspace_aligned' and pspace_distinct' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits)
  and K (range_cover ptr sz (Types_H.getObjectSize ty us) (length dest) \<and>
      ptr \<noteq> 0 \<and> (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28) ) \<rbrace>
       createNewObjects ty src dest ptr us d
  \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>" 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) show ?case apply (rule hoare_gen_asm) apply clarsimp apply (frule range_cover.weak) apply (subst createNewObjects_Cons) apply (simp add: word_bits_def) apply wp apply (wp snoc.hyps) apply (rule hoare_vcg_conj_lift) apply (rule hoare_post_imp[OF _ createNewObjects_pspace_no_overlap'[where sz = sz]]) apply clarsimp apply (rule hoare_vcg_conj_lift) apply (rule hoare_post_imp[OF _ createNewObjects_pspace_no_overlap'[where sz = sz]]) apply clarsimp apply (rule hoare_vcg_conj_lift) apply (rule hoare_post_imp[OF _ createNewObjects_pspace_no_overlap'[where sz = sz]]) apply (rule pspace_no_overlap'_le) apply fastforce apply (simp add: range_cover.sz[where 'a=32, folded word_bits_def])+ apply wp apply clarsimp apply (frule range_cover.aligned) apply (intro conjI aligned_add_aligned) apply (erule range_cover_le,simp) apply (rule is_aligned_shiftl_self) apply simp apply simp done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits) and K (range_cover ptr sz (getObjectSize ty us) (length dest) \<and> ptr \<noteq> 0 \<and> (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28))\<rbrace> createNewObjects ty src dest ptr us d \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (state)
goal (2 subgoals):
 1. \<lbrace>(\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits) and K (range_cover ptr sz (getObjectSize ty us) (length []) \<and> ptr \<noteq> 0 \<and> (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28))\<rbrace> createNewObjects ty src [] ptr us d \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>x xs. \<lbrace>(\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits) and K (range_cover ptr sz (getObjectSize ty us) (length xs) \<and> ptr \<noteq> 0 \<and> (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28))\<rbrace> createNewObjects ty src xs ptr us d \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> \<Longrightarrow> \<lbrace>(\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits) and K (range_cover ptr sz (getObjectSize ty us) (length (xs @ [x])) \<and> ptr \<noteq> 0 \<and> (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28))\<rbrace> createNewObjects ty src (xs @ [x]) ptr us d \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (state)
this:


goal (2 subgoals):
 1. \<lbrace>(\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits) and K (range_cover ptr sz (getObjectSize ty us) (length []) \<and> ptr \<noteq> 0 \<and> (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28))\<rbrace> createNewObjects ty src [] ptr us d \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>x xs. \<lbrace>(\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits) and K (range_cover ptr sz (getObjectSize ty us) (length xs) \<and> ptr \<noteq> 0 \<and> (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28))\<rbrace> createNewObjects ty src xs ptr us d \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> \<Longrightarrow> \<lbrace>(\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits) and K (range_cover ptr sz (getObjectSize ty us) (length (xs @ [x])) \<and> ptr \<noteq> 0 \<and> (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28))\<rbrace> createNewObjects ty src (xs @ [x]) ptr us d \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits) and K (range_cover ptr sz (getObjectSize ty us) (length []) \<and> ptr \<noteq> 0 \<and> (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28))\<rbrace> createNewObjects ty src [] ptr us d \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (state)
this:
\<lbrace>(\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits) and K (range_cover ptr sz (getObjectSize ty us) (length []) \<and> ptr \<noteq> 0 \<and> (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28))\<rbrace> createNewObjects ty src [] ptr us d \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>

goal (1 subgoal):
 1. \<And>x xs. \<lbrace>(\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits) and K (range_cover ptr sz (getObjectSize ty us) (length xs) \<and> ptr \<noteq> 0 \<and> (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28))\<rbrace> createNewObjects ty src xs ptr us d \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> \<Longrightarrow> \<lbrace>(\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits) and K (range_cover ptr sz (getObjectSize ty us) (length (xs @ [x])) \<and> ptr \<noteq> 0 \<and> (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28))\<rbrace> createNewObjects ty src (xs @ [x]) ptr us d \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (state)
goal (1 subgoal):
 1. \<And>x xs. \<lbrace>(\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits) and K (range_cover ptr sz (getObjectSize ty us) (length xs) \<and> ptr \<noteq> 0 \<and> (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28))\<rbrace> createNewObjects ty src xs ptr us d \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> \<Longrightarrow> \<lbrace>(\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits) and K (range_cover ptr sz (getObjectSize ty us) (length (xs @ [x])) \<and> ptr \<noteq> 0 \<and> (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28))\<rbrace> createNewObjects ty src (xs @ [x]) ptr us d \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (state)
this:
\<lbrace>(\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits) and K (range_cover ptr sz (getObjectSize ty us) (length dests) \<and> ptr \<noteq> 0 \<and> (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28))\<rbrace> createNewObjects ty src dests ptr us d \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>

goal (1 subgoal):
 1. \<And>x xs. \<lbrace>(\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits) and K (range_cover ptr sz (getObjectSize ty us) (length xs) \<and> ptr \<noteq> 0 \<and> (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28))\<rbrace> createNewObjects ty src xs ptr us d \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> \<Longrightarrow> \<lbrace>(\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits) and K (range_cover ptr sz (getObjectSize ty us) (length (xs @ [x])) \<and> ptr \<noteq> 0 \<and> (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28))\<rbrace> createNewObjects ty src (xs @ [x]) ptr us d \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits) and K (range_cover ptr sz (getObjectSize ty us) (length (dests @ [dest])) \<and> ptr \<noteq> 0 \<and> (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28))\<rbrace> createNewObjects ty src (dests @ [dest]) ptr us d \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. range_cover ptr sz (getObjectSize ty us) (length (dests @ [dest])) \<and> ptr \<noteq> 0 \<and> (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28) \<Longrightarrow> \<lbrace>(\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits)\<rbrace> createNewObjects ty src (dests @ [dest]) ptr us d \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ptr \<noteq> 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. vs_valid_duplicates' (ksPSpace a) \<and> pspace_no_overlap' ptr sz a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> is_aligned (armKSGlobalPD (ksArchState a)) pdBits\<rbrace> createNewObjects ty src (dests @ [dest]) ptr us d \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ptr \<noteq> 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; Suc (length dests) < 2 ^ LENGTH(32)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. vs_valid_duplicates' (ksPSpace a) \<and> pspace_no_overlap' ptr sz a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> is_aligned (armKSGlobalPD (ksArchState a)) pdBits\<rbrace> createNewObjects ty src (dests @ [dest]) ptr us d \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ptr \<noteq> 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; Suc (length dests) < 2 ^ LENGTH(32)\<rbrakk> \<Longrightarrow> length dests < 2 ^ word_bits
 2. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ptr \<noteq> 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; Suc (length dests) < 2 ^ LENGTH(32)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. vs_valid_duplicates' (ksPSpace a) \<and> pspace_no_overlap' ptr sz a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> is_aligned (armKSGlobalPD (ksArchState a)) pdBits\<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>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ptr \<noteq> 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; Suc (length dests) < 2 ^ LENGTH(32)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. vs_valid_duplicates' (ksPSpace a) \<and> pspace_no_overlap' ptr sz a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> is_aligned (armKSGlobalPD (ksArchState a)) pdBits\<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>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ptr \<noteq> 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; Suc (length dests) < 2 ^ LENGTH(32)\<rbrakk> \<Longrightarrow> \<lbrace>?Q9\<rbrace> createNewObjects ty src dests ptr us d \<lbrace>\<lambda>x s. vs_valid_duplicates' (ksPSpace s) \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (getObjectSize ty us) s \<and> is_aligned (armKSGlobalPD (ksArchState s)) pdBits \<and> K (is_aligned ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (getObjectSize ty us)) s \<and> K (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28) s\<rbrace>
 2. \<And>s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ptr \<noteq> 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; Suc (length dests) < 2 ^ LENGTH(32); vs_valid_duplicates' (ksPSpace s) \<and> pspace_no_overlap' ptr sz s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> is_aligned (armKSGlobalPD (ksArchState s)) pdBits\<rbrakk> \<Longrightarrow> ?Q9 s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ptr \<noteq> 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; Suc (length dests) < 2 ^ LENGTH(32)\<rbrakk> \<Longrightarrow> \<lbrace>?P'22\<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) (getObjectSize ty us) s \<and> is_aligned (armKSGlobalPD (ksArchState s)) pdBits \<and> K (is_aligned ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (getObjectSize ty us)) s \<and> K (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28) s\<rbrace>
 2. \<And>s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ptr \<noteq> 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; Suc (length dests) < 2 ^ LENGTH(32); vs_valid_duplicates' (ksPSpace s) \<and> pspace_no_overlap' ptr sz s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> is_aligned (armKSGlobalPD (ksArchState s)) pdBits\<rbrakk> \<Longrightarrow> ((\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits) and K (range_cover ptr sz (getObjectSize ty us) (length dests) \<and> ptr \<noteq> 0 \<and> (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28))) s \<and> ?P'22 s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ptr \<noteq> 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; Suc (length dests) < 2 ^ LENGTH(32)\<rbrakk> \<Longrightarrow> \<lbrace>?P24\<rbrace> createNewObjects ty src dests ptr us d \<lbrace>\<lambda>rv. pspace_aligned'\<rbrace>
 2. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ptr \<noteq> 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; Suc (length dests) < 2 ^ LENGTH(32)\<rbrakk> \<Longrightarrow> \<lbrace>?P'24\<rbrace> createNewObjects ty src dests ptr us d \<lbrace>\<lambda>rv s. pspace_distinct' s \<and> pspace_no_overlap' ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (getObjectSize ty us) s \<and> is_aligned (armKSGlobalPD (ksArchState s)) pdBits \<and> K (is_aligned ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (getObjectSize ty us)) s \<and> K (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28) s\<rbrace>
 3. \<And>s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ptr \<noteq> 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; Suc (length dests) < 2 ^ LENGTH(32); vs_valid_duplicates' (ksPSpace s) \<and> pspace_no_overlap' ptr sz s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> is_aligned (armKSGlobalPD (ksArchState s)) pdBits\<rbrakk> \<Longrightarrow> ((\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits) and K (range_cover ptr sz (getObjectSize ty us) (length dests) \<and> ptr \<noteq> 0 \<and> (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28))) s \<and> ?P24 s \<and> ?P'24 s proof (prove)
goal (3 subgoals):
 1. \<And>rv s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ptr \<noteq> 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; Suc (length dests) < 2 ^ LENGTH(32); 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. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ptr \<noteq> 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; Suc (length dests) < 2 ^ LENGTH(32)\<rbrakk> \<Longrightarrow> \<lbrace>?P'24\<rbrace> createNewObjects ty src dests ptr us d \<lbrace>\<lambda>rv s. pspace_distinct' s \<and> pspace_no_overlap' ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (getObjectSize ty us) s \<and> is_aligned (armKSGlobalPD (ksArchState s)) pdBits \<and> K (is_aligned ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (getObjectSize ty us)) s \<and> K (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28) s\<rbrace>
 3. \<And>s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ptr \<noteq> 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; Suc (length dests) < 2 ^ LENGTH(32); vs_valid_duplicates' (ksPSpace s) \<and> pspace_no_overlap' ptr sz s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> is_aligned (armKSGlobalPD (ksArchState s)) pdBits\<rbrakk> \<Longrightarrow> ((\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits) and K (range_cover ptr sz (getObjectSize ty us) (length dests) \<and> ptr \<noteq> 0 \<and> (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28))) s \<and> (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)) s \<and> ?P'24 s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ptr \<noteq> 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; Suc (length dests) < 2 ^ LENGTH(32)\<rbrakk> \<Longrightarrow> \<lbrace>?P'24\<rbrace> createNewObjects ty src dests ptr us d \<lbrace>\<lambda>rv s. pspace_distinct' s \<and> pspace_no_overlap' ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (getObjectSize ty us) s \<and> is_aligned (armKSGlobalPD (ksArchState s)) pdBits \<and> K (is_aligned ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (getObjectSize ty us)) s \<and> K (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28) s\<rbrace>
 2. \<And>s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ptr \<noteq> 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; Suc (length dests) < 2 ^ LENGTH(32); vs_valid_duplicates' (ksPSpace s) \<and> pspace_no_overlap' ptr sz s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> is_aligned (armKSGlobalPD (ksArchState s)) pdBits\<rbrakk> \<Longrightarrow> ((\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits) and K (range_cover ptr sz (getObjectSize ty us) (length dests) \<and> ptr \<noteq> 0 \<and> (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28))) s \<and> (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)) s \<and> ?P'24 s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ptr \<noteq> 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; Suc (length dests) < 2 ^ LENGTH(32)\<rbrakk> \<Longrightarrow> \<lbrace>?P31\<rbrace> createNewObjects ty src dests ptr us d \<lbrace>\<lambda>rv. pspace_distinct'\<rbrace>
 2. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ptr \<noteq> 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; Suc (length dests) < 2 ^ LENGTH(32)\<rbrakk> \<Longrightarrow> \<lbrace>?P'31\<rbrace> createNewObjects ty src dests ptr us d \<lbrace>\<lambda>rv s. pspace_no_overlap' ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (getObjectSize ty us) s \<and> is_aligned (armKSGlobalPD (ksArchState s)) pdBits \<and> K (is_aligned ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (getObjectSize ty us)) s \<and> K (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28) s\<rbrace>
 3. \<And>s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ptr \<noteq> 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; Suc (length dests) < 2 ^ LENGTH(32); vs_valid_duplicates' (ksPSpace s) \<and> pspace_no_overlap' ptr sz s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> is_aligned (armKSGlobalPD (ksArchState s)) pdBits\<rbrakk> \<Longrightarrow> ((\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits) and K (range_cover ptr sz (getObjectSize ty us) (length dests) \<and> ptr \<noteq> 0 \<and> (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28))) s \<and> (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)) s \<and> ?P31 s \<and> ?P'31 s proof (prove)
goal (3 subgoals):
 1. \<And>rv s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ptr \<noteq> 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; Suc (length dests) < 2 ^ LENGTH(32); 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. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ptr \<noteq> 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; Suc (length dests) < 2 ^ LENGTH(32)\<rbrakk> \<Longrightarrow> \<lbrace>?P'31\<rbrace> createNewObjects ty src dests ptr us d \<lbrace>\<lambda>rv s. pspace_no_overlap' ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (getObjectSize ty us) s \<and> is_aligned (armKSGlobalPD (ksArchState s)) pdBits \<and> K (is_aligned ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (getObjectSize ty us)) s \<and> K (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28) s\<rbrace>
 3. \<And>s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ptr \<noteq> 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; Suc (length dests) < 2 ^ LENGTH(32); vs_valid_duplicates' (ksPSpace s) \<and> pspace_no_overlap' ptr sz s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> is_aligned (armKSGlobalPD (ksArchState s)) pdBits\<rbrakk> \<Longrightarrow> ((\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits) and K (range_cover ptr sz (getObjectSize ty us) (length dests) \<and> ptr \<noteq> 0 \<and> (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28))) s \<and> (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)) s \<and> (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)) s \<and> ?P'31 s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ptr \<noteq> 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; Suc (length dests) < 2 ^ LENGTH(32)\<rbrakk> \<Longrightarrow> \<lbrace>?P'31\<rbrace> createNewObjects ty src dests ptr us d \<lbrace>\<lambda>rv s. pspace_no_overlap' ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (getObjectSize ty us) s \<and> is_aligned (armKSGlobalPD (ksArchState s)) pdBits \<and> K (is_aligned ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (getObjectSize ty us)) s \<and> K (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28) s\<rbrace>
 2. \<And>s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ptr \<noteq> 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; Suc (length dests) < 2 ^ LENGTH(32); vs_valid_duplicates' (ksPSpace s) \<and> pspace_no_overlap' ptr sz s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> is_aligned (armKSGlobalPD (ksArchState s)) pdBits\<rbrakk> \<Longrightarrow> ((\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits) and K (range_cover ptr sz (getObjectSize ty us) (length dests) \<and> ptr \<noteq> 0 \<and> (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28))) s \<and> (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)) s \<and> (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)) s \<and> ?P'31 s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ptr \<noteq> 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; Suc (length dests) < 2 ^ LENGTH(32)\<rbrakk> \<Longrightarrow> \<lbrace>?P38\<rbrace> createNewObjects ty src dests ptr us d \<lbrace>\<lambda>rv. pspace_no_overlap' ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (getObjectSize ty us)\<rbrace>
 2. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ptr \<noteq> 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; Suc (length dests) < 2 ^ LENGTH(32)\<rbrakk> \<Longrightarrow> \<lbrace>?P'38\<rbrace> createNewObjects ty src dests ptr us d \<lbrace>\<lambda>rv s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits \<and> K (is_aligned ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (getObjectSize ty us)) s \<and> K (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28) s\<rbrace>
 3. \<And>s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ptr \<noteq> 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; Suc (length dests) < 2 ^ LENGTH(32); vs_valid_duplicates' (ksPSpace s) \<and> pspace_no_overlap' ptr sz s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> is_aligned (armKSGlobalPD (ksArchState s)) pdBits\<rbrakk> \<Longrightarrow> ((\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits) and K (range_cover ptr sz (getObjectSize ty us) (length dests) \<and> ptr \<noteq> 0 \<and> (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28))) s \<and> (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)) s \<and> (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)) s \<and> ?P38 s \<and> ?P'38 s proof (prove)
goal (3 subgoals):
 1. \<And>rv s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ptr \<noteq> 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; Suc (length dests) < 2 ^ LENGTH(32); 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' ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (getObjectSize ty us) s
 2. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ptr \<noteq> 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; Suc (length dests) < 2 ^ LENGTH(32)\<rbrakk> \<Longrightarrow> \<lbrace>?P'38\<rbrace> createNewObjects ty src dests ptr us d \<lbrace>\<lambda>rv s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits \<and> K (is_aligned ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (getObjectSize ty us)) s \<and> K (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28) s\<rbrace>
 3. \<And>s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ptr \<noteq> 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; Suc (length dests) < 2 ^ LENGTH(32); vs_valid_duplicates' (ksPSpace s) \<and> pspace_no_overlap' ptr sz s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> is_aligned (armKSGlobalPD (ksArchState s)) pdBits\<rbrakk> \<Longrightarrow> ((\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits) and K (range_cover ptr sz (getObjectSize ty us) (length dests) \<and> ptr \<noteq> 0 \<and> (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28))) s \<and> (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)) s \<and> (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)) s \<and> (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)) s \<and> ?P'38 s proof (prove)
goal (5 subgoals):
 1. \<And>rv s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ptr \<noteq> 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; Suc (length dests) < 2 ^ LENGTH(32); 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' ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (?sz45 rv s) s
 2. \<And>rv s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ptr \<noteq> 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; Suc (length dests) < 2 ^ LENGTH(32); 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> getObjectSize ty us \<le> ?sz45 rv s
 3. \<And>rv s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ptr \<noteq> 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; Suc (length dests) < 2 ^ LENGTH(32); 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> ?sz45 rv s < word_bits
 4. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ptr \<noteq> 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; Suc (length dests) < 2 ^ LENGTH(32)\<rbrakk> \<Longrightarrow> \<lbrace>?P'38\<rbrace> createNewObjects ty src dests ptr us d \<lbrace>\<lambda>rv s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits \<and> K (is_aligned ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (getObjectSize ty us)) s \<and> K (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28) s\<rbrace>
 5. \<And>s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ptr \<noteq> 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; Suc (length dests) < 2 ^ LENGTH(32); vs_valid_duplicates' (ksPSpace s) \<and> pspace_no_overlap' ptr sz s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> is_aligned (armKSGlobalPD (ksArchState s)) pdBits\<rbrakk> \<Longrightarrow> ((\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits) and K (range_cover ptr sz (getObjectSize ty us) (length dests) \<and> ptr \<noteq> 0 \<and> (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28))) s \<and> (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)) s \<and> (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)) s \<and> (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)) s \<and> ?P'38 s proof (prove)
goal (4 subgoals):
 1. \<And>rv s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ptr \<noteq> 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; Suc (length dests) < 2 ^ LENGTH(32); 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> getObjectSize ty us \<le> sz
 2. \<And>rv s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ptr \<noteq> 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; Suc (length dests) < 2 ^ LENGTH(32); 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> sz < word_bits
 3. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ptr \<noteq> 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; Suc (length dests) < 2 ^ LENGTH(32)\<rbrakk> \<Longrightarrow> \<lbrace>?P'38\<rbrace> createNewObjects ty src dests ptr us d \<lbrace>\<lambda>rv s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits \<and> K (is_aligned ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (getObjectSize ty us)) s \<and> K (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28) s\<rbrace>
 4. \<And>s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ptr \<noteq> 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; Suc (length dests) < 2 ^ LENGTH(32); vs_valid_duplicates' (ksPSpace s) \<and> pspace_no_overlap' ptr sz s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> is_aligned (armKSGlobalPD (ksArchState s)) pdBits\<rbrakk> \<Longrightarrow> ((\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits) and K (range_cover ptr sz (getObjectSize ty us) (length dests) \<and> ptr \<noteq> 0 \<and> (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28))) s \<and> (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)) s \<and> (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)) s \<and> (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)) s \<and> ?P'38 s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ptr \<noteq> 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; length dests < 4294967295\<rbrakk> \<Longrightarrow> \<lbrace>?P'38\<rbrace> createNewObjects ty src dests ptr us d \<lbrace>\<lambda>rv s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits \<and> is_aligned ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (APIType_capBits ty us)\<rbrace>
 2. \<And>s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ptr \<noteq> 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; Suc (length dests) < 2 ^ LENGTH(32); vs_valid_duplicates' (ksPSpace s) \<and> pspace_no_overlap' ptr sz s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> is_aligned (armKSGlobalPD (ksArchState s)) pdBits\<rbrakk> \<Longrightarrow> ((\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits) and K (range_cover ptr sz (getObjectSize ty us) (length dests) \<and> ptr \<noteq> 0 \<and> (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28))) s \<and> (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)) s \<and> (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)) s \<and> (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)) s \<and> ?P'38 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ptr \<noteq> 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; Suc (length dests) < 2 ^ LENGTH(32); vs_valid_duplicates' (ksPSpace s) \<and> pspace_no_overlap' ptr sz s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> is_aligned (armKSGlobalPD (ksArchState s)) pdBits\<rbrakk> \<Longrightarrow> ((\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits) and K (range_cover ptr sz (getObjectSize ty us) (length dests) \<and> ptr \<noteq> 0 \<and> (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28))) s \<and> (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)) s \<and> (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)) s \<and> (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)) s \<and> is_aligned (armKSGlobalPD (ksArchState s)) pdBits \<and> is_aligned ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (APIType_capBits ty us) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ptr \<noteq> 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; length dests < 4294967295; vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr sz s; pspace_aligned' s; pspace_distinct' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits\<rbrakk> \<Longrightarrow> range_cover ptr sz (APIType_capBits ty us) (length dests) \<and> is_aligned ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (APIType_capBits ty us) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ptr \<noteq> 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; length dests < 4294967295; vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr sz s; pspace_aligned' s; pspace_distinct' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr (APIType_capBits ty us)\<rbrakk> \<Longrightarrow> range_cover ptr sz (APIType_capBits ty us) (length dests) \<and> is_aligned ((word_of_nat (length dests) << APIType_capBits ty us) + ptr) (APIType_capBits ty us) proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ptr \<noteq> 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; length dests < 4294967295; vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr sz s; pspace_aligned' s; pspace_distinct' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr (APIType_capBits ty us)\<rbrakk> \<Longrightarrow> range_cover ptr sz (APIType_capBits ty us) (length dests)
 2. \<And>s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ptr \<noteq> 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; length dests < 4294967295; vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr sz s; pspace_aligned' s; pspace_distinct' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr (APIType_capBits ty us)\<rbrakk> \<Longrightarrow> is_aligned (word_of_nat (length dests) << APIType_capBits ty us) (?n64 s)
 3. \<And>s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ptr \<noteq> 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; length dests < 4294967295; vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr sz s; pspace_aligned' s; pspace_distinct' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr (APIType_capBits ty us)\<rbrakk> \<Longrightarrow> is_aligned ptr (APIType_capBits ty us)
 4. \<And>s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ptr \<noteq> 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; length dests < 4294967295; vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr sz s; pspace_aligned' s; pspace_distinct' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr (APIType_capBits ty us)\<rbrakk> \<Longrightarrow> APIType_capBits ty us \<le> ?n64 s proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ptr \<noteq> 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; length dests < 4294967295; vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr sz s; pspace_aligned' s; pspace_distinct' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr (APIType_capBits ty us)\<rbrakk> \<Longrightarrow> is_aligned (word_of_nat (length dests) << APIType_capBits ty us) (?n64 s)
 2. \<And>s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ptr \<noteq> 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; length dests < 4294967295; vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr sz s; pspace_aligned' s; pspace_distinct' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr (APIType_capBits ty us)\<rbrakk> \<Longrightarrow> is_aligned ptr (APIType_capBits ty us)
 3. \<And>s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ptr \<noteq> 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; length dests < 4294967295; vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr sz s; pspace_aligned' s; pspace_distinct' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr (APIType_capBits ty us)\<rbrakk> \<Longrightarrow> APIType_capBits ty us \<le> ?n64 s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ptr \<noteq> 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; length dests < 4294967295; vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr sz s; pspace_aligned' s; pspace_distinct' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr (APIType_capBits ty us)\<rbrakk> \<Longrightarrow> is_aligned ptr (APIType_capBits ty us)
 2. \<And>s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ptr \<noteq> 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; length dests < 4294967295; vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr sz s; pspace_aligned' s; pspace_distinct' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr (APIType_capBits ty us)\<rbrakk> \<Longrightarrow> APIType_capBits ty us \<le> APIType_capBits ty us proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) (Suc (length dests)); ptr \<noteq> 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; length dests < 4294967295; vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr sz s; pspace_aligned' s; pspace_distinct' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr (APIType_capBits ty us)\<rbrakk> \<Longrightarrow> APIType_capBits ty us \<le> APIType_capBits ty us proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>(\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits) and K (range_cover ptr sz (getObjectSize ty us) (length (dests @ [dest])) \<and> ptr \<noteq> 0 \<and> (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28))\<rbrace> createNewObjects ty src (dests @ [dest]) ptr us d \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>

goal:
No subgoals!