theory Detype_R

lemma createNewObjects_def2:
  "\<lbrakk>dslots \<noteq> []; length ( dslots ) < 2^word_bits;
    cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent s;
    \<forall>slot \<in> set dslots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s;
    pspace_no_overlap' ptr sz s;
    caps_no_overlap'' ptr sz s;
    caps_overlap_reserved'
    {ptr..ptr + of_nat (length dslots) * 2 ^ Types_H.getObjectSize ty us - 1} s;
    valid_pspace' s;
    distinct dslots;
    valid_arch_state' s;
    range_cover ptr sz (Types_H.getObjectSize ty us) (length dslots);
    ptr \<noteq> 0;
    ksCurDomain s \<le> maxDomain\<rbrakk>
   \<Longrightarrow> createNewObjects ty parent dslots ptr us d s =
       insertNewCaps ty parent dslots ptr us d s" apply (clarsimp simp:insertNewCaps_def createNewObjects_def neq_Nil_conv) proof - fix y ys have list_inc:  "\<And>n. [0.e.Suc n] = [0 .e. n] @ [n+1]" by simp assume le: "Suc (length (ys::word32 list)) < 2 ^ word_bits" assume list_nc: "\<forall>slot \<in> set ys. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s" assume dist: "distinct ys" assume extra: "y\<notin> set ys" "cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) y s" assume not_0: "ptr \<noteq> 0" assume kscd: "ksCurDomain s \<le> maxDomain" assume valid_psp: "valid_pspace' s" assume valid_arch_state: "valid_arch_state' s" assume psp_no_overlap: "pspace_no_overlap' ptr sz s" assume caps_no_overlap: "caps_no_overlap'' ptr sz s" assume caps_reserved: "caps_overlap_reserved'
    {ptr..ptr +  (1 + of_nat (length ys)) * 2 ^ (Types_H.getObjectSize ty us) - 1} s" assume range_cover: "range_cover ptr sz (Types_H.getObjectSize ty us) (Suc (length ys))" assume unt_at: "cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent s" show "zipWithM_x
        (\<lambda>num slot.
            RetypeDecls_H.createObject ty ((num << Types_H.getObjectSize ty us) + ptr) us d >>=
            insertNewCap parent slot)
        [0.e.of_nat (length ys)] (y # ys) s =
       (createNewCaps ty ptr (Suc (length ys)) us d >>= zipWithM_x (insertNewCap parent) (y # ys))  s" using le list_nc dist extra range_cover not_0 caps_reserved proof (induct ys arbitrary: y rule:rev_induct) case Nil show ?case by (clarsimp simp:zipWithM_x_def zipWith_def
          sequence_x_def createObject_def2[symmetric]) next case (snoc a as b) have caps_r:"caps_overlap_reserved'
        {ptr..ptr + (1 + of_nat (length as)) * 2 ^ Types_H.getObjectSize ty us - 1} s" using snoc.prems apply - apply (erule caps_overlap_reserved'_subseteq) apply (cut_tac is_aligned_no_overflow
          [where ptr = "ptr + ((1 + of_nat (length as)) << APIType_capBits ty us)"
            and sz = " Types_H.getObjectSize ty us"]) apply (clarsimp simp: power_add[symmetric] shiftl_t2n field_simps objSize_eq_capBits ) apply (rule order_trans[OF word_sub_1_le]) apply (drule(1) range_cover_no_0[where p = "Suc (length as)"]) apply simp apply (simp add:word_arith_nat_Suc power_add[symmetric] field_simps) apply (simp add:shiftl_t2n) apply (rule aligned_add_aligned[OF range_cover.aligned]) apply (simp add:objSize_eq_capBits)+ apply (rule is_aligned_shiftl_self) apply (simp add:range_cover_def objSize_eq_capBits)+ done show ?case apply simp using snoc.prems apply (subst upto_enum_inc_1) apply (rule word_of_nat_less) apply (simp add:word_bits_def minus_one_norm) apply (subst append_Cons[symmetric]) apply (subst zipWithM_x_append1) apply (clarsimp simp:unat_of_nat32 bind_assoc) apply (subst monad_eq) apply (rule snoc.hyps) apply (simp add:caps_r | rule range_cover_le)+ apply (simp add:snoc.hyps bind_assoc) apply (rule sym) apply (subst monad_eq) apply (erule createNewCaps_Cons[OF _ valid_psp valid_arch_state psp_no_overlap not_0]) apply (rule sym) apply (simp add:bind_assoc del:upto_enum_nat) apply (rule_tac Q = "(\<lambda>r s. (\<forall>cap\<in>set r. cap \<noteq> capability.NullCap) \<and>
                            cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent s \<and>
                            cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s \<and>
                            (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) \<and>
                            pspace_no_overlap' (ptr + (1 + of_nat (length as) << Types_H.getObjectSize ty us))
                            (Types_H.getObjectSize ty us) s
                            \<and> valid_pspace' s \<and> valid_arch_state' s \<and> Q r s)" for Q in monad_eq_split) apply (subst append_Cons[symmetric]) apply (subst zipWithM_x_append1) apply clarsimp apply assumption apply (clarsimp simp:field_simps) apply (subst monad_commute_simple[OF commute_commute]) apply (rule new_cap_object_commute) apply (clarsimp) apply (frule_tac p = "1 + length as" in range_cover_no_0[rotated]) apply clarsimp apply simp apply (subst (asm) Abs_fnat_hom_add[symmetric]) apply (intro conjI) apply (simp add:range_cover_def word_bits_def) apply (rule aligned_add_aligned[OF range_cover.aligned],simp) apply (rule is_aligned_shiftl_self) apply (simp add:range_cover_def) apply (simp add:range_cover_def) apply (clarsimp simp:field_simps shiftl_t2n) apply (clarsimp simp:createNewCaps_def) apply (wp createNewCaps_not_nc createNewCaps_pspace_no_overlap'[where sz = sz]
                  createNewCaps_cte_wp_at'[where sz = sz] hoare_vcg_ball_lift
                  createNewCaps_valid_pspace[where sz = sz]
                  createNewCaps_obj_at'[where sz=sz]) apply simp apply (rule range_cover_le) apply (simp add:objSize_eq_capBits caps_r)+ apply (wp createNewCaps_ret_len createNewCaps_valid_arch_state) apply (frule range_cover_le[where n = "Suc (length as)"]) apply simp+ using psp_no_overlap caps_r valid_psp unt_at caps_no_overlap valid_arch_state apply (clarsimp simp: valid_pspace'_def objSize_eq_capBits) apply (auto simp: kscd) done qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>dslots \<noteq> []; length dslots < 2 ^ word_bits; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent s; \<forall>slot\<in>set dslots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; pspace_no_overlap' ptr sz s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat (length dslots) * 2 ^ getObjectSize ty us - 1} s; valid_pspace' s; distinct dslots; valid_arch_state' s; range_cover ptr sz (getObjectSize ty us) (length dslots); ptr \<noteq> 0; ksCurDomain s \<le> maxDomain\<rbrakk> \<Longrightarrow> createNewObjects ty parent dslots ptr us d s = insertNewCaps ty parent dslots ptr us d s proof (prove)
goal (1 subgoal):
 1. \<And>y ys. \<lbrakk>Suc (length ys) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent s; pspace_no_overlap' ptr sz s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length ys)) * 2 ^ getObjectSize ty us - 1} s; valid_pspace' s; valid_arch_state' s; range_cover ptr sz (getObjectSize ty us) (Suc (length ys)); ptr \<noteq> 0; ksCurDomain s \<le> maxDomain; dslots = y # ys; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) y s; \<forall>slot\<in>set ys. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; y \<notin> set ys; distinct ys\<rbrakk> \<Longrightarrow> zipWithM_x (\<lambda>num slot. global.createObject ty ((num << getObjectSize ty us) + ptr) us d >>= insertNewCap parent slot) [0 .e. word_of_nat (length ys)] (y # ys) s = (createNewCaps ty ptr (Suc (length ys)) us d >>= zipWithM_x (insertNewCap parent) (y # ys)) s proof (state)
goal (1 subgoal):
 1. \<And>y ys. \<lbrakk>Suc (length ys) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent s; pspace_no_overlap' ptr sz s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length ys)) * 2 ^ getObjectSize ty us - 1} s; valid_pspace' s; valid_arch_state' s; range_cover ptr sz (getObjectSize ty us) (Suc (length ys)); ptr \<noteq> 0; ksCurDomain s \<le> maxDomain; dslots = y # ys; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) y s; \<forall>slot\<in>set ys. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; y \<notin> set ys; distinct ys\<rbrakk> \<Longrightarrow> zipWithM_x (\<lambda>num slot. global.createObject ty ((num << getObjectSize ty us) + ptr) us d >>= insertNewCap parent slot) [0 .e. word_of_nat (length ys)] (y # ys) s = (createNewCaps ty ptr (Suc (length ys)) us d >>= zipWithM_x (insertNewCap parent) (y # ys)) s proof (state)
goal (1 subgoal):
 1. \<And>y ys. \<lbrakk>Suc (length ys) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent s; pspace_no_overlap' ptr sz s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length ys)) * 2 ^ getObjectSize ty us - 1} s; valid_pspace' s; valid_arch_state' s; range_cover ptr sz (getObjectSize ty us) (Suc (length ys)); ptr \<noteq> 0; ksCurDomain s \<le> maxDomain; dslots = y # ys; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) y s; \<forall>slot\<in>set ys. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; y \<notin> set ys; distinct ys\<rbrakk> \<Longrightarrow> zipWithM_x (\<lambda>num slot. global.createObject ty ((num << getObjectSize ty us) + ptr) us d >>= insertNewCap parent slot) [0 .e. word_of_nat (length ys)] (y # ys) s = (createNewCaps ty ptr (Suc (length ys)) us d >>= zipWithM_x (insertNewCap parent) (y # ys)) s proof (prove)
goal (1 subgoal):
 1. \<And>n. [0 .e. Suc n] = [0 .e. n] @ [n + 1] proof (state)
this:
[0 .e. Suc ?n] = [0 .e. ?n] @ [?n + 1]

goal (1 subgoal):
 1. \<And>y ys. \<lbrakk>Suc (length ys) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent s; pspace_no_overlap' ptr sz s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length ys)) * 2 ^ getObjectSize ty us - 1} s; valid_pspace' s; valid_arch_state' s; range_cover ptr sz (getObjectSize ty us) (Suc (length ys)); ptr \<noteq> 0; ksCurDomain s \<le> maxDomain; dslots = y # ys; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) y s; \<forall>slot\<in>set ys. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; y \<notin> set ys; distinct ys\<rbrakk> \<Longrightarrow> zipWithM_x (\<lambda>num slot. global.createObject ty ((num << getObjectSize ty us) + ptr) us d >>= insertNewCap parent slot) [0 .e. word_of_nat (length ys)] (y # ys) s = (createNewCaps ty ptr (Suc (length ys)) us d >>= zipWithM_x (insertNewCap parent) (y # ys)) s proof (state)
this:
Suc (length ys) < 2 ^ word_bits

goal (1 subgoal):
 1. \<And>y ys. \<lbrakk>Suc (length ys) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent s; pspace_no_overlap' ptr sz s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length ys)) * 2 ^ getObjectSize ty us - 1} s; valid_pspace' s; valid_arch_state' s; range_cover ptr sz (getObjectSize ty us) (Suc (length ys)); ptr \<noteq> 0; ksCurDomain s \<le> maxDomain; dslots = y # ys; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) y s; \<forall>slot\<in>set ys. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; y \<notin> set ys; distinct ys\<rbrakk> \<Longrightarrow> zipWithM_x (\<lambda>num slot. global.createObject ty ((num << getObjectSize ty us) + ptr) us d >>= insertNewCap parent slot) [0 .e. word_of_nat (length ys)] (y # ys) s = (createNewCaps ty ptr (Suc (length ys)) us d >>= zipWithM_x (insertNewCap parent) (y # ys)) s proof (state)
this:
\<forall>slot\<in>set ys. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s

goal (1 subgoal):
 1. \<And>y ys. \<lbrakk>Suc (length ys) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent s; pspace_no_overlap' ptr sz s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length ys)) * 2 ^ getObjectSize ty us - 1} s; valid_pspace' s; valid_arch_state' s; range_cover ptr sz (getObjectSize ty us) (Suc (length ys)); ptr \<noteq> 0; ksCurDomain s \<le> maxDomain; dslots = y # ys; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) y s; \<forall>slot\<in>set ys. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; y \<notin> set ys; distinct ys\<rbrakk> \<Longrightarrow> zipWithM_x (\<lambda>num slot. global.createObject ty ((num << getObjectSize ty us) + ptr) us d >>= insertNewCap parent slot) [0 .e. word_of_nat (length ys)] (y # ys) s = (createNewCaps ty ptr (Suc (length ys)) us d >>= zipWithM_x (insertNewCap parent) (y # ys)) s proof (state)
this:
distinct ys

goal (1 subgoal):
 1. \<And>y ys. \<lbrakk>Suc (length ys) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent s; pspace_no_overlap' ptr sz s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length ys)) * 2 ^ getObjectSize ty us - 1} s; valid_pspace' s; valid_arch_state' s; range_cover ptr sz (getObjectSize ty us) (Suc (length ys)); ptr \<noteq> 0; ksCurDomain s \<le> maxDomain; dslots = y # ys; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) y s; \<forall>slot\<in>set ys. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; y \<notin> set ys; distinct ys\<rbrakk> \<Longrightarrow> zipWithM_x (\<lambda>num slot. global.createObject ty ((num << getObjectSize ty us) + ptr) us d >>= insertNewCap parent slot) [0 .e. word_of_nat (length ys)] (y # ys) s = (createNewCaps ty ptr (Suc (length ys)) us d >>= zipWithM_x (insertNewCap parent) (y # ys)) s proof (state)
this:
y \<notin> set ys
cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) y s

goal (1 subgoal):
 1. \<And>y ys. \<lbrakk>Suc (length ys) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent s; pspace_no_overlap' ptr sz s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length ys)) * 2 ^ getObjectSize ty us - 1} s; valid_pspace' s; valid_arch_state' s; range_cover ptr sz (getObjectSize ty us) (Suc (length ys)); ptr \<noteq> 0; ksCurDomain s \<le> maxDomain; dslots = y # ys; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) y s; \<forall>slot\<in>set ys. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; y \<notin> set ys; distinct ys\<rbrakk> \<Longrightarrow> zipWithM_x (\<lambda>num slot. global.createObject ty ((num << getObjectSize ty us) + ptr) us d >>= insertNewCap parent slot) [0 .e. word_of_nat (length ys)] (y # ys) s = (createNewCaps ty ptr (Suc (length ys)) us d >>= zipWithM_x (insertNewCap parent) (y # ys)) s proof (state)
this:
ptr \<noteq> 0

goal (1 subgoal):
 1. \<And>y ys. \<lbrakk>Suc (length ys) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent s; pspace_no_overlap' ptr sz s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length ys)) * 2 ^ getObjectSize ty us - 1} s; valid_pspace' s; valid_arch_state' s; range_cover ptr sz (getObjectSize ty us) (Suc (length ys)); ptr \<noteq> 0; ksCurDomain s \<le> maxDomain; dslots = y # ys; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) y s; \<forall>slot\<in>set ys. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; y \<notin> set ys; distinct ys\<rbrakk> \<Longrightarrow> zipWithM_x (\<lambda>num slot. global.createObject ty ((num << getObjectSize ty us) + ptr) us d >>= insertNewCap parent slot) [0 .e. word_of_nat (length ys)] (y # ys) s = (createNewCaps ty ptr (Suc (length ys)) us d >>= zipWithM_x (insertNewCap parent) (y # ys)) s proof (state)
this:
ksCurDomain s \<le> maxDomain

goal (1 subgoal):
 1. \<And>y ys. \<lbrakk>Suc (length ys) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent s; pspace_no_overlap' ptr sz s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length ys)) * 2 ^ getObjectSize ty us - 1} s; valid_pspace' s; valid_arch_state' s; range_cover ptr sz (getObjectSize ty us) (Suc (length ys)); ptr \<noteq> 0; ksCurDomain s \<le> maxDomain; dslots = y # ys; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) y s; \<forall>slot\<in>set ys. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; y \<notin> set ys; distinct ys\<rbrakk> \<Longrightarrow> zipWithM_x (\<lambda>num slot. global.createObject ty ((num << getObjectSize ty us) + ptr) us d >>= insertNewCap parent slot) [0 .e. word_of_nat (length ys)] (y # ys) s = (createNewCaps ty ptr (Suc (length ys)) us d >>= zipWithM_x (insertNewCap parent) (y # ys)) s proof (state)
this:
valid_pspace' s

goal (1 subgoal):
 1. \<And>y ys. \<lbrakk>Suc (length ys) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent s; pspace_no_overlap' ptr sz s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length ys)) * 2 ^ getObjectSize ty us - 1} s; valid_pspace' s; valid_arch_state' s; range_cover ptr sz (getObjectSize ty us) (Suc (length ys)); ptr \<noteq> 0; ksCurDomain s \<le> maxDomain; dslots = y # ys; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) y s; \<forall>slot\<in>set ys. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; y \<notin> set ys; distinct ys\<rbrakk> \<Longrightarrow> zipWithM_x (\<lambda>num slot. global.createObject ty ((num << getObjectSize ty us) + ptr) us d >>= insertNewCap parent slot) [0 .e. word_of_nat (length ys)] (y # ys) s = (createNewCaps ty ptr (Suc (length ys)) us d >>= zipWithM_x (insertNewCap parent) (y # ys)) s proof (state)
this:
valid_arch_state' s

goal (1 subgoal):
 1. \<And>y ys. \<lbrakk>Suc (length ys) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent s; pspace_no_overlap' ptr sz s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length ys)) * 2 ^ getObjectSize ty us - 1} s; valid_pspace' s; valid_arch_state' s; range_cover ptr sz (getObjectSize ty us) (Suc (length ys)); ptr \<noteq> 0; ksCurDomain s \<le> maxDomain; dslots = y # ys; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) y s; \<forall>slot\<in>set ys. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; y \<notin> set ys; distinct ys\<rbrakk> \<Longrightarrow> zipWithM_x (\<lambda>num slot. global.createObject ty ((num << getObjectSize ty us) + ptr) us d >>= insertNewCap parent slot) [0 .e. word_of_nat (length ys)] (y # ys) s = (createNewCaps ty ptr (Suc (length ys)) us d >>= zipWithM_x (insertNewCap parent) (y # ys)) s proof (state)
this:
pspace_no_overlap' ptr sz s

goal (1 subgoal):
 1. \<And>y ys. \<lbrakk>Suc (length ys) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent s; pspace_no_overlap' ptr sz s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length ys)) * 2 ^ getObjectSize ty us - 1} s; valid_pspace' s; valid_arch_state' s; range_cover ptr sz (getObjectSize ty us) (Suc (length ys)); ptr \<noteq> 0; ksCurDomain s \<le> maxDomain; dslots = y # ys; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) y s; \<forall>slot\<in>set ys. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; y \<notin> set ys; distinct ys\<rbrakk> \<Longrightarrow> zipWithM_x (\<lambda>num slot. global.createObject ty ((num << getObjectSize ty us) + ptr) us d >>= insertNewCap parent slot) [0 .e. word_of_nat (length ys)] (y # ys) s = (createNewCaps ty ptr (Suc (length ys)) us d >>= zipWithM_x (insertNewCap parent) (y # ys)) s proof (state)
this:
caps_no_overlap'' ptr sz s

goal (1 subgoal):
 1. \<And>y ys. \<lbrakk>Suc (length ys) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent s; pspace_no_overlap' ptr sz s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length ys)) * 2 ^ getObjectSize ty us - 1} s; valid_pspace' s; valid_arch_state' s; range_cover ptr sz (getObjectSize ty us) (Suc (length ys)); ptr \<noteq> 0; ksCurDomain s \<le> maxDomain; dslots = y # ys; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) y s; \<forall>slot\<in>set ys. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; y \<notin> set ys; distinct ys\<rbrakk> \<Longrightarrow> zipWithM_x (\<lambda>num slot. global.createObject ty ((num << getObjectSize ty us) + ptr) us d >>= insertNewCap parent slot) [0 .e. word_of_nat (length ys)] (y # ys) s = (createNewCaps ty ptr (Suc (length ys)) us d >>= zipWithM_x (insertNewCap parent) (y # ys)) s proof (state)
this:
caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length ys)) * 2 ^ getObjectSize ty us - 1} s

goal (1 subgoal):
 1. \<And>y ys. \<lbrakk>Suc (length ys) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent s; pspace_no_overlap' ptr sz s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length ys)) * 2 ^ getObjectSize ty us - 1} s; valid_pspace' s; valid_arch_state' s; range_cover ptr sz (getObjectSize ty us) (Suc (length ys)); ptr \<noteq> 0; ksCurDomain s \<le> maxDomain; dslots = y # ys; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) y s; \<forall>slot\<in>set ys. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; y \<notin> set ys; distinct ys\<rbrakk> \<Longrightarrow> zipWithM_x (\<lambda>num slot. global.createObject ty ((num << getObjectSize ty us) + ptr) us d >>= insertNewCap parent slot) [0 .e. word_of_nat (length ys)] (y # ys) s = (createNewCaps ty ptr (Suc (length ys)) us d >>= zipWithM_x (insertNewCap parent) (y # ys)) s proof (state)
this:
range_cover ptr sz (getObjectSize ty us) (Suc (length ys))

goal (1 subgoal):
 1. \<And>y ys. \<lbrakk>Suc (length ys) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent s; pspace_no_overlap' ptr sz s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length ys)) * 2 ^ getObjectSize ty us - 1} s; valid_pspace' s; valid_arch_state' s; range_cover ptr sz (getObjectSize ty us) (Suc (length ys)); ptr \<noteq> 0; ksCurDomain s \<le> maxDomain; dslots = y # ys; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) y s; \<forall>slot\<in>set ys. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; y \<notin> set ys; distinct ys\<rbrakk> \<Longrightarrow> zipWithM_x (\<lambda>num slot. global.createObject ty ((num << getObjectSize ty us) + ptr) us d >>= insertNewCap parent slot) [0 .e. word_of_nat (length ys)] (y # ys) s = (createNewCaps ty ptr (Suc (length ys)) us d >>= zipWithM_x (insertNewCap parent) (y # ys)) s proof (state)
this:
cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent s

goal (1 subgoal):
 1. \<And>y ys. \<lbrakk>Suc (length ys) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent s; pspace_no_overlap' ptr sz s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length ys)) * 2 ^ getObjectSize ty us - 1} s; valid_pspace' s; valid_arch_state' s; range_cover ptr sz (getObjectSize ty us) (Suc (length ys)); ptr \<noteq> 0; ksCurDomain s \<le> maxDomain; dslots = y # ys; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) y s; \<forall>slot\<in>set ys. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; y \<notin> set ys; distinct ys\<rbrakk> \<Longrightarrow> zipWithM_x (\<lambda>num slot. global.createObject ty ((num << getObjectSize ty us) + ptr) us d >>= insertNewCap parent slot) [0 .e. word_of_nat (length ys)] (y # ys) s = (createNewCaps ty ptr (Suc (length ys)) us d >>= zipWithM_x (insertNewCap parent) (y # ys)) s proof (prove)
goal (1 subgoal):
 1. zipWithM_x (\<lambda>num slot. global.createObject ty ((num << getObjectSize ty us) + ptr) us d >>= insertNewCap parent slot) [0 .e. word_of_nat (length ys)] (y # ys) s = (createNewCaps ty ptr (Suc (length ys)) us d >>= zipWithM_x (insertNewCap parent) (y # ys)) s proof (prove)
using this:
Suc (length ys) < 2 ^ word_bits
\<forall>slot\<in>set ys. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s
distinct ys
y \<notin> set ys
cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) y s
range_cover ptr sz (getObjectSize ty us) (Suc (length ys))
ptr \<noteq> 0
caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length ys)) * 2 ^ getObjectSize ty us - 1} s

goal (1 subgoal):
 1. zipWithM_x (\<lambda>num slot. global.createObject ty ((num << getObjectSize ty us) + ptr) us d >>= insertNewCap parent slot) [0 .e. word_of_nat (length ys)] (y # ys) s = (createNewCaps ty ptr (Suc (length ys)) us d >>= zipWithM_x (insertNewCap parent) (y # ys)) s proof (state)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>Suc (length []) < 2 ^ word_bits; \<forall>slot\<in>set []. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct []; y \<notin> set []; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) y s; range_cover ptr sz (getObjectSize ty us) (Suc (length [])); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length [])) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> zipWithM_x (\<lambda>num slot. global.createObject ty ((num << getObjectSize ty us) + ptr) us d >>= insertNewCap parent slot) [0 .e. word_of_nat (length [])] [y] s = (createNewCaps ty ptr (Suc (length [])) us d >>= zipWithM_x (insertNewCap parent) [y]) s
 2. \<And>x xs y. \<lbrakk>\<And>y. \<lbrakk>Suc (length xs) < 2 ^ word_bits; \<forall>slot\<in>set xs. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct xs; y \<notin> set xs; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) y s; range_cover ptr sz (getObjectSize ty us) (Suc (length xs)); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length xs)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> zipWithM_x (\<lambda>num slot. global.createObject ty ((num << getObjectSize ty us) + ptr) us d >>= insertNewCap parent slot) [0 .e. word_of_nat (length xs)] (y # xs) s = (createNewCaps ty ptr (Suc (length xs)) us d >>= zipWithM_x (insertNewCap parent) (y # xs)) s; Suc (length (xs @ [x])) < 2 ^ word_bits; \<forall>slot\<in>set (xs @ [x]). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct (xs @ [x]); y \<notin> set (xs @ [x]); cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) y s; range_cover ptr sz (getObjectSize ty us) (Suc (length (xs @ [x]))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length (xs @ [x]))) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> zipWithM_x (\<lambda>num slot. global.createObject ty ((num << getObjectSize ty us) + ptr) us d >>= insertNewCap parent slot) [0 .e. word_of_nat (length (xs @ [x]))] (y # xs @ [x]) s = (createNewCaps ty ptr (Suc (length (xs @ [x]))) us d >>= zipWithM_x (insertNewCap parent) (y # xs @ [x])) s proof (state)
this:
Suc (length []) < 2 ^ word_bits
\<forall>slot\<in>set []. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s
distinct []
y \<notin> set []
cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) y s
range_cover ptr sz (getObjectSize ty us) (Suc (length []))
ptr \<noteq> 0
caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length [])) * 2 ^ getObjectSize ty us - 1} s

goal (2 subgoals):
 1. \<And>y. \<lbrakk>Suc (length []) < 2 ^ word_bits; \<forall>slot\<in>set []. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct []; y \<notin> set []; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) y s; range_cover ptr sz (getObjectSize ty us) (Suc (length [])); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length [])) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> zipWithM_x (\<lambda>num slot. global.createObject ty ((num << getObjectSize ty us) + ptr) us d >>= insertNewCap parent slot) [0 .e. word_of_nat (length [])] [y] s = (createNewCaps ty ptr (Suc (length [])) us d >>= zipWithM_x (insertNewCap parent) [y]) s
 2. \<And>x xs y. \<lbrakk>\<And>y. \<lbrakk>Suc (length xs) < 2 ^ word_bits; \<forall>slot\<in>set xs. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct xs; y \<notin> set xs; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) y s; range_cover ptr sz (getObjectSize ty us) (Suc (length xs)); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length xs)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> zipWithM_x (\<lambda>num slot. global.createObject ty ((num << getObjectSize ty us) + ptr) us d >>= insertNewCap parent slot) [0 .e. word_of_nat (length xs)] (y # xs) s = (createNewCaps ty ptr (Suc (length xs)) us d >>= zipWithM_x (insertNewCap parent) (y # xs)) s; Suc (length (xs @ [x])) < 2 ^ word_bits; \<forall>slot\<in>set (xs @ [x]). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct (xs @ [x]); y \<notin> set (xs @ [x]); cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) y s; range_cover ptr sz (getObjectSize ty us) (Suc (length (xs @ [x]))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length (xs @ [x]))) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> zipWithM_x (\<lambda>num slot. global.createObject ty ((num << getObjectSize ty us) + ptr) us d >>= insertNewCap parent slot) [0 .e. word_of_nat (length (xs @ [x]))] (y # xs @ [x]) s = (createNewCaps ty ptr (Suc (length (xs @ [x]))) us d >>= zipWithM_x (insertNewCap parent) (y # xs @ [x])) s proof (prove)
goal (1 subgoal):
 1. zipWithM_x (\<lambda>num slot. global.createObject ty ((num << getObjectSize ty us) + ptr) us d >>= insertNewCap parent slot) [0 .e. word_of_nat (length [])] [y] s = (createNewCaps ty ptr (Suc (length [])) us d >>= zipWithM_x (insertNewCap parent) [y]) s proof (state)
this:
zipWithM_x (\<lambda>num slot. global.createObject ty ((num << getObjectSize ty us) + ptr) us d >>= insertNewCap parent slot) [0 .e. word_of_nat (length [])] [y] s = (createNewCaps ty ptr (Suc (length [])) us d >>= zipWithM_x (insertNewCap parent) [y]) s

goal (1 subgoal):
 1. \<And>x xs y. \<lbrakk>\<And>y. \<lbrakk>Suc (length xs) < 2 ^ word_bits; \<forall>slot\<in>set xs. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct xs; y \<notin> set xs; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) y s; range_cover ptr sz (getObjectSize ty us) (Suc (length xs)); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length xs)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> zipWithM_x (\<lambda>num slot. global.createObject ty ((num << getObjectSize ty us) + ptr) us d >>= insertNewCap parent slot) [0 .e. word_of_nat (length xs)] (y # xs) s = (createNewCaps ty ptr (Suc (length xs)) us d >>= zipWithM_x (insertNewCap parent) (y # xs)) s; Suc (length (xs @ [x])) < 2 ^ word_bits; \<forall>slot\<in>set (xs @ [x]). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct (xs @ [x]); y \<notin> set (xs @ [x]); cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) y s; range_cover ptr sz (getObjectSize ty us) (Suc (length (xs @ [x]))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length (xs @ [x]))) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> zipWithM_x (\<lambda>num slot. global.createObject ty ((num << getObjectSize ty us) + ptr) us d >>= insertNewCap parent slot) [0 .e. word_of_nat (length (xs @ [x]))] (y # xs @ [x]) s = (createNewCaps ty ptr (Suc (length (xs @ [x]))) us d >>= zipWithM_x (insertNewCap parent) (y # xs @ [x])) s proof (state)
goal (1 subgoal):
 1. \<And>x xs y. \<lbrakk>\<And>y. \<lbrakk>Suc (length xs) < 2 ^ word_bits; \<forall>slot\<in>set xs. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct xs; y \<notin> set xs; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) y s; range_cover ptr sz (getObjectSize ty us) (Suc (length xs)); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length xs)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> zipWithM_x (\<lambda>num slot. global.createObject ty ((num << getObjectSize ty us) + ptr) us d >>= insertNewCap parent slot) [0 .e. word_of_nat (length xs)] (y # xs) s = (createNewCaps ty ptr (Suc (length xs)) us d >>= zipWithM_x (insertNewCap parent) (y # xs)) s; Suc (length (xs @ [x])) < 2 ^ word_bits; \<forall>slot\<in>set (xs @ [x]). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct (xs @ [x]); y \<notin> set (xs @ [x]); cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) y s; range_cover ptr sz (getObjectSize ty us) (Suc (length (xs @ [x]))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length (xs @ [x]))) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> zipWithM_x (\<lambda>num slot. global.createObject ty ((num << getObjectSize ty us) + ptr) us d >>= insertNewCap parent slot) [0 .e. word_of_nat (length (xs @ [x]))] (y # xs @ [x]) s = (createNewCaps ty ptr (Suc (length (xs @ [x]))) us d >>= zipWithM_x (insertNewCap parent) (y # xs @ [x])) s proof (state)
this:
\<lbrakk>Suc (length as) < 2 ^ word_bits; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct as; ?y \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) ?y s; range_cover ptr sz (getObjectSize ty us) (Suc (length as)); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> zipWithM_x (\<lambda>num slot. global.createObject ty ((num << getObjectSize ty us) + ptr) us d >>= insertNewCap parent slot) [0 .e. word_of_nat (length as)] (?y # as) s = (createNewCaps ty ptr (Suc (length as)) us d >>= zipWithM_x (insertNewCap parent) (?y # as)) s
Suc (length (as @ [a])) < 2 ^ word_bits
\<forall>slot\<in>set (as @ [a]). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s
distinct (as @ [a])
b \<notin> set (as @ [a])
cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s
range_cover ptr sz (getObjectSize ty us) (Suc (length (as @ [a])))
ptr \<noteq> 0
caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length (as @ [a]))) * 2 ^ getObjectSize ty us - 1} s

goal (1 subgoal):
 1. \<And>x xs y. \<lbrakk>\<And>y. \<lbrakk>Suc (length xs) < 2 ^ word_bits; \<forall>slot\<in>set xs. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct xs; y \<notin> set xs; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) y s; range_cover ptr sz (getObjectSize ty us) (Suc (length xs)); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length xs)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> zipWithM_x (\<lambda>num slot. global.createObject ty ((num << getObjectSize ty us) + ptr) us d >>= insertNewCap parent slot) [0 .e. word_of_nat (length xs)] (y # xs) s = (createNewCaps ty ptr (Suc (length xs)) us d >>= zipWithM_x (insertNewCap parent) (y # xs)) s; Suc (length (xs @ [x])) < 2 ^ word_bits; \<forall>slot\<in>set (xs @ [x]). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct (xs @ [x]); y \<notin> set (xs @ [x]); cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) y s; range_cover ptr sz (getObjectSize ty us) (Suc (length (xs @ [x]))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length (xs @ [x]))) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> zipWithM_x (\<lambda>num slot. global.createObject ty ((num << getObjectSize ty us) + ptr) us d >>= insertNewCap parent slot) [0 .e. word_of_nat (length (xs @ [x]))] (y # xs @ [x]) s = (createNewCaps ty ptr (Suc (length (xs @ [x]))) us d >>= zipWithM_x (insertNewCap parent) (y # xs @ [x])) s proof (prove)
goal (1 subgoal):
 1. caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s proof (prove)
using this:
Suc (length (as @ [a])) < 2 ^ word_bits
\<forall>slot\<in>set (as @ [a]). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s
distinct (as @ [a])
b \<notin> set (as @ [a])
cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s
range_cover ptr sz (getObjectSize ty us) (Suc (length (as @ [a])))
ptr \<noteq> 0
caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length (as @ [a]))) * 2 ^ getObjectSize ty us - 1} s

goal (1 subgoal):
 1. caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Suc (length (as @ [a])) < 2 ^ word_bits; \<forall>slot\<in>set (as @ [a]). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct (as @ [a]); b \<notin> set (as @ [a]); cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length (as @ [a]))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length (as @ [a]))) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Suc (length (as @ [a])) < 2 ^ word_bits; \<forall>slot\<in>set (as @ [a]). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct (as @ [a]); b \<notin> set (as @ [a]); cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length (as @ [a]))); ptr \<noteq> 0\<rbrakk> \<Longrightarrow> {ptr..ptr + (1 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} \<subseteq> {ptr..ptr + (1 + word_of_nat (length (as @ [a]))) * 2 ^ getObjectSize ty us - 1} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Suc (length (as @ [a])) < 2 ^ word_bits; \<forall>slot\<in>set (as @ [a]). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct (as @ [a]); b \<notin> set (as @ [a]); cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length (as @ [a]))); ptr \<noteq> 0; ptr + (1 + word_of_nat (length as) << APIType_capBits ty us) \<le> ptr + (1 + word_of_nat (length as) << APIType_capBits ty us) + 2 ^ getObjectSize ty us - 1\<rbrakk> \<Longrightarrow> {ptr..ptr + (1 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} \<subseteq> {ptr..ptr + (1 + word_of_nat (length (as @ [a]))) * 2 ^ getObjectSize ty us - 1}
 2. \<lbrakk>Suc (length (as @ [a])) < 2 ^ word_bits; \<forall>slot\<in>set (as @ [a]). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct (as @ [a]); b \<notin> set (as @ [a]); cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length (as @ [a]))); ptr \<noteq> 0\<rbrakk> \<Longrightarrow> is_aligned (ptr + (1 + word_of_nat (length as) << APIType_capBits ty us)) (getObjectSize ty us) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (APIType_capBits ty us) (Suc (Suc (length as))); ptr \<noteq> 0; ptr + (2 ^ APIType_capBits ty us + word_of_nat (length as) * 2 ^ APIType_capBits ty us) \<le> ptr + (word_of_nat (length as) * 2 ^ APIType_capBits ty us + 2 * 2 ^ APIType_capBits ty us) - 1; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct as; a \<notin> set as; b \<noteq> a; b \<notin> set as; ptr \<le> ptr + (2 ^ APIType_capBits ty us + word_of_nat (length as) * 2 ^ APIType_capBits ty us) - 1\<rbrakk> \<Longrightarrow> ptr + (2 ^ APIType_capBits ty us + word_of_nat (length as) * 2 ^ APIType_capBits ty us) - 1 \<le> ptr + (word_of_nat (length as) * 2 ^ APIType_capBits ty us + 2 * 2 ^ APIType_capBits ty us) - 1
 2. \<lbrakk>Suc (length (as @ [a])) < 2 ^ word_bits; \<forall>slot\<in>set (as @ [a]). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct (as @ [a]); b \<notin> set (as @ [a]); cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length (as @ [a]))); ptr \<noteq> 0\<rbrakk> \<Longrightarrow> is_aligned (ptr + (1 + word_of_nat (length as) << APIType_capBits ty us)) (getObjectSize ty us) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (APIType_capBits ty us) (Suc (Suc (length as))); ptr \<noteq> 0; ptr + (2 ^ APIType_capBits ty us + word_of_nat (length as) * 2 ^ APIType_capBits ty us) \<le> ptr + (word_of_nat (length as) * 2 ^ APIType_capBits ty us + 2 * 2 ^ APIType_capBits ty us) - 1; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct as; a \<notin> set as; b \<noteq> a; b \<notin> set as; ptr \<le> ptr + (2 ^ APIType_capBits ty us + word_of_nat (length as) * 2 ^ APIType_capBits ty us) - 1\<rbrakk> \<Longrightarrow> ptr + (2 ^ APIType_capBits ty us + word_of_nat (length as) * 2 ^ APIType_capBits ty us) \<noteq> 0
 2. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (APIType_capBits ty us) (Suc (Suc (length as))); ptr \<noteq> 0; ptr + (2 ^ APIType_capBits ty us + word_of_nat (length as) * 2 ^ APIType_capBits ty us) \<le> ptr + (word_of_nat (length as) * 2 ^ APIType_capBits ty us + 2 * 2 ^ APIType_capBits ty us) - 1; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct as; a \<notin> set as; b \<noteq> a; b \<notin> set as; ptr \<le> ptr + (2 ^ APIType_capBits ty us + word_of_nat (length as) * 2 ^ APIType_capBits ty us) - 1\<rbrakk> \<Longrightarrow> ptr + (2 ^ APIType_capBits ty us + word_of_nat (length as) * 2 ^ APIType_capBits ty us) \<le> ptr + (word_of_nat (length as) * 2 ^ APIType_capBits ty us + 2 * 2 ^ APIType_capBits ty us) - 1
 3. \<lbrakk>Suc (length (as @ [a])) < 2 ^ word_bits; \<forall>slot\<in>set (as @ [a]). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct (as @ [a]); b \<notin> set (as @ [a]); cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length (as @ [a]))); ptr \<noteq> 0\<rbrakk> \<Longrightarrow> is_aligned (ptr + (1 + word_of_nat (length as) << APIType_capBits ty us)) (getObjectSize ty us) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (APIType_capBits ty us) (Suc (Suc (length as))); ptr + (2 ^ APIType_capBits ty us + word_of_nat (length as) * 2 ^ APIType_capBits ty us) \<le> ptr + (word_of_nat (length as) * 2 ^ APIType_capBits ty us + 2 * 2 ^ APIType_capBits ty us) - 1; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct as; a \<notin> set as; b \<noteq> a; b \<notin> set as; ptr \<le> ptr + (2 ^ APIType_capBits ty us + word_of_nat (length as) * 2 ^ APIType_capBits ty us) - 1\<rbrakk> \<Longrightarrow> Suc (length as) < Suc (Suc (length as))
 2. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (APIType_capBits ty us) (Suc (Suc (length as))); ptr + (2 ^ APIType_capBits ty us + word_of_nat (length as) * 2 ^ APIType_capBits ty us) \<le> ptr + (word_of_nat (length as) * 2 ^ APIType_capBits ty us + 2 * 2 ^ APIType_capBits ty us) - 1; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct as; a \<notin> set as; b \<noteq> a; b \<notin> set as; ptr \<le> ptr + (2 ^ APIType_capBits ty us + word_of_nat (length as) * 2 ^ APIType_capBits ty us) - 1; ptr + word_of_nat (Suc (length as)) * 2 ^ APIType_capBits ty us \<noteq> 0\<rbrakk> \<Longrightarrow> ptr + (2 ^ APIType_capBits ty us + word_of_nat (length as) * 2 ^ APIType_capBits ty us) \<noteq> 0
 3. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (APIType_capBits ty us) (Suc (Suc (length as))); ptr \<noteq> 0; ptr + (2 ^ APIType_capBits ty us + word_of_nat (length as) * 2 ^ APIType_capBits ty us) \<le> ptr + (word_of_nat (length as) * 2 ^ APIType_capBits ty us + 2 * 2 ^ APIType_capBits ty us) - 1; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct as; a \<notin> set as; b \<noteq> a; b \<notin> set as; ptr \<le> ptr + (2 ^ APIType_capBits ty us + word_of_nat (length as) * 2 ^ APIType_capBits ty us) - 1\<rbrakk> \<Longrightarrow> ptr + (2 ^ APIType_capBits ty us + word_of_nat (length as) * 2 ^ APIType_capBits ty us) \<le> ptr + (word_of_nat (length as) * 2 ^ APIType_capBits ty us + 2 * 2 ^ APIType_capBits ty us) - 1
 4. \<lbrakk>Suc (length (as @ [a])) < 2 ^ word_bits; \<forall>slot\<in>set (as @ [a]). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct (as @ [a]); b \<notin> set (as @ [a]); cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length (as @ [a]))); ptr \<noteq> 0\<rbrakk> \<Longrightarrow> is_aligned (ptr + (1 + word_of_nat (length as) << APIType_capBits ty us)) (getObjectSize ty us) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (APIType_capBits ty us) (Suc (Suc (length as))); ptr + (2 ^ APIType_capBits ty us + word_of_nat (length as) * 2 ^ APIType_capBits ty us) \<le> ptr + (word_of_nat (length as) * 2 ^ APIType_capBits ty us + 2 * 2 ^ APIType_capBits ty us) - 1; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct as; a \<notin> set as; b \<noteq> a; b \<notin> set as; ptr \<le> ptr + (2 ^ APIType_capBits ty us + word_of_nat (length as) * 2 ^ APIType_capBits ty us) - 1; ptr + word_of_nat (Suc (length as)) * 2 ^ APIType_capBits ty us \<noteq> 0\<rbrakk> \<Longrightarrow> ptr + (2 ^ APIType_capBits ty us + word_of_nat (length as) * 2 ^ APIType_capBits ty us) \<noteq> 0
 2. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (APIType_capBits ty us) (Suc (Suc (length as))); ptr \<noteq> 0; ptr + (2 ^ APIType_capBits ty us + word_of_nat (length as) * 2 ^ APIType_capBits ty us) \<le> ptr + (word_of_nat (length as) * 2 ^ APIType_capBits ty us + 2 * 2 ^ APIType_capBits ty us) - 1; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct as; a \<notin> set as; b \<noteq> a; b \<notin> set as; ptr \<le> ptr + (2 ^ APIType_capBits ty us + word_of_nat (length as) * 2 ^ APIType_capBits ty us) - 1\<rbrakk> \<Longrightarrow> ptr + (2 ^ APIType_capBits ty us + word_of_nat (length as) * 2 ^ APIType_capBits ty us) \<le> ptr + (word_of_nat (length as) * 2 ^ APIType_capBits ty us + 2 * 2 ^ APIType_capBits ty us) - 1
 3. \<lbrakk>Suc (length (as @ [a])) < 2 ^ word_bits; \<forall>slot\<in>set (as @ [a]). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct (as @ [a]); b \<notin> set (as @ [a]); cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length (as @ [a]))); ptr \<noteq> 0\<rbrakk> \<Longrightarrow> is_aligned (ptr + (1 + word_of_nat (length as) << APIType_capBits ty us)) (getObjectSize ty us) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (APIType_capBits ty us) (Suc (Suc (length as))); ptr \<noteq> 0; ptr + (2 ^ APIType_capBits ty us + word_of_nat (length as) * 2 ^ APIType_capBits ty us) \<le> ptr + (word_of_nat (length as) * 2 ^ APIType_capBits ty us + 2 * 2 ^ APIType_capBits ty us) - 1; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct as; a \<notin> set as; b \<noteq> a; b \<notin> set as; ptr \<le> ptr + (2 ^ APIType_capBits ty us + word_of_nat (length as) * 2 ^ APIType_capBits ty us) - 1\<rbrakk> \<Longrightarrow> ptr + (2 ^ APIType_capBits ty us + word_of_nat (length as) * 2 ^ APIType_capBits ty us) \<le> ptr + (word_of_nat (length as) * 2 ^ APIType_capBits ty us + 2 * 2 ^ APIType_capBits ty us) - 1
 2. \<lbrakk>Suc (length (as @ [a])) < 2 ^ word_bits; \<forall>slot\<in>set (as @ [a]). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct (as @ [a]); b \<notin> set (as @ [a]); cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length (as @ [a]))); ptr \<noteq> 0\<rbrakk> \<Longrightarrow> is_aligned (ptr + (1 + word_of_nat (length as) << APIType_capBits ty us)) (getObjectSize ty us) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Suc (length (as @ [a])) < 2 ^ word_bits; \<forall>slot\<in>set (as @ [a]). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct (as @ [a]); b \<notin> set (as @ [a]); cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length (as @ [a]))); ptr \<noteq> 0\<rbrakk> \<Longrightarrow> is_aligned (ptr + (1 + word_of_nat (length as) << APIType_capBits ty us)) (getObjectSize ty us) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>Suc (length (as @ [a])) < 2 ^ word_bits; \<forall>slot\<in>set (as @ [a]). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct (as @ [a]); b \<notin> set (as @ [a]); cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length (as @ [a]))); ptr \<noteq> 0\<rbrakk> \<Longrightarrow> range_cover ptr ?sz26 ?n25 ?n26
 2. \<lbrakk>Suc (length (as @ [a])) < 2 ^ word_bits; \<forall>slot\<in>set (as @ [a]). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct (as @ [a]); b \<notin> set (as @ [a]); cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length (as @ [a]))); ptr \<noteq> 0\<rbrakk> \<Longrightarrow> is_aligned (1 + word_of_nat (length as) << APIType_capBits ty us) (getObjectSize ty us)
 3. \<lbrakk>Suc (length (as @ [a])) < 2 ^ word_bits; \<forall>slot\<in>set (as @ [a]). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct (as @ [a]); b \<notin> set (as @ [a]); cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length (as @ [a]))); ptr \<noteq> 0\<rbrakk> \<Longrightarrow> getObjectSize ty us \<le> ?n25 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (APIType_capBits ty us) (Suc (Suc (length as))); ptr \<noteq> 0\<rbrakk> \<Longrightarrow> is_aligned (1 + word_of_nat (length as) << APIType_capBits ty us) (APIType_capBits ty us)
 2. \<lbrakk>Suc (length (as @ [a])) < 2 ^ word_bits; \<forall>slot\<in>set (as @ [a]). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct (as @ [a]); b \<notin> set (as @ [a]); cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length (as @ [a]))); ptr \<noteq> 0\<rbrakk> \<Longrightarrow> getObjectSize ty us \<le> APIType_capBits ty us proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Suc (length (as @ [a])) < 2 ^ word_bits; \<forall>slot\<in>set (as @ [a]). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct (as @ [a]); b \<notin> set (as @ [a]); cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length (as @ [a]))); ptr \<noteq> 0\<rbrakk> \<Longrightarrow> getObjectSize ty us \<le> APIType_capBits ty us proof (prove)
goal:
No subgoals! proof (state)
this:
caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s

goal (1 subgoal):
 1. \<And>x xs y. \<lbrakk>\<And>y. \<lbrakk>Suc (length xs) < 2 ^ word_bits; \<forall>slot\<in>set xs. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct xs; y \<notin> set xs; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) y s; range_cover ptr sz (getObjectSize ty us) (Suc (length xs)); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length xs)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> zipWithM_x (\<lambda>num slot. global.createObject ty ((num << getObjectSize ty us) + ptr) us d >>= insertNewCap parent slot) [0 .e. word_of_nat (length xs)] (y # xs) s = (createNewCaps ty ptr (Suc (length xs)) us d >>= zipWithM_x (insertNewCap parent) (y # xs)) s; Suc (length (xs @ [x])) < 2 ^ word_bits; \<forall>slot\<in>set (xs @ [x]). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct (xs @ [x]); y \<notin> set (xs @ [x]); cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) y s; range_cover ptr sz (getObjectSize ty us) (Suc (length (xs @ [x]))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length (xs @ [x]))) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> zipWithM_x (\<lambda>num slot. global.createObject ty ((num << getObjectSize ty us) + ptr) us d >>= insertNewCap parent slot) [0 .e. word_of_nat (length (xs @ [x]))] (y # xs @ [x]) s = (createNewCaps ty ptr (Suc (length (xs @ [x]))) us d >>= zipWithM_x (insertNewCap parent) (y # xs @ [x])) s proof (prove)
goal (1 subgoal):
 1. zipWithM_x (\<lambda>num slot. global.createObject ty ((num << getObjectSize ty us) + ptr) us d >>= insertNewCap parent slot) [0 .e. word_of_nat (length (as @ [a]))] (b # as @ [a]) s = (createNewCaps ty ptr (Suc (length (as @ [a]))) us d >>= zipWithM_x (insertNewCap parent) (b # as @ [a])) s proof (prove)
goal (1 subgoal):
 1. zipWithM_x (\<lambda>num slot. global.createObject ty ((num << getObjectSize ty us) + ptr) us d >>= insertNewCap parent slot) [0 .e. 1 + word_of_nat (length as)] (b # as @ [a]) s = (createNewCaps ty ptr (Suc (Suc (length as))) us d >>= zipWithM_x (insertNewCap parent) (b # as @ [a])) s proof (prove)
using this:
Suc (length (as @ [a])) < 2 ^ word_bits
\<forall>slot\<in>set (as @ [a]). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s
distinct (as @ [a])
b \<notin> set (as @ [a])
cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s
range_cover ptr sz (getObjectSize ty us) (Suc (length (as @ [a])))
ptr \<noteq> 0
caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length (as @ [a]))) * 2 ^ getObjectSize ty us - 1} s

goal (1 subgoal):
 1. zipWithM_x (\<lambda>num slot. global.createObject ty ((num << getObjectSize ty us) + ptr) us d >>= insertNewCap parent slot) [0 .e. 1 + word_of_nat (length as)] (b # as @ [a]) s = (createNewCaps ty ptr (Suc (Suc (length as))) us d >>= zipWithM_x (insertNewCap parent) (b # as @ [a])) s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Suc (length (as @ [a])) < 2 ^ word_bits; \<forall>slot\<in>set (as @ [a]). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct (as @ [a]); b \<notin> set (as @ [a]); cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length (as @ [a]))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length (as @ [a]))) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> word_of_nat (length as) < 2 ^ word_bits - 1
 2. \<lbrakk>Suc (length (as @ [a])) < 2 ^ word_bits; \<forall>slot\<in>set (as @ [a]). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct (as @ [a]); b \<notin> set (as @ [a]); cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length (as @ [a]))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length (as @ [a]))) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> zipWithM_x (\<lambda>num slot. global.createObject ty ((num << getObjectSize ty us) + ptr) us d >>= insertNewCap parent slot) ([0 .e. word_of_nat (length as)] @ [1 + word_of_nat (length as)]) (b # as @ [a]) s = (createNewCaps ty ptr (Suc (Suc (length as))) us d >>= zipWithM_x (insertNewCap parent) (b # as @ [a])) s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Suc (length (as @ [a])) < 2 ^ word_bits; \<forall>slot\<in>set (as @ [a]). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct (as @ [a]); b \<notin> set (as @ [a]); cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length (as @ [a]))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length (as @ [a]))) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> length as < unat (2 ^ word_bits - 1)
 2. \<lbrakk>Suc (length (as @ [a])) < 2 ^ word_bits; \<forall>slot\<in>set (as @ [a]). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct (as @ [a]); b \<notin> set (as @ [a]); cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length (as @ [a]))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length (as @ [a]))) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> zipWithM_x (\<lambda>num slot. global.createObject ty ((num << getObjectSize ty us) + ptr) us d >>= insertNewCap parent slot) ([0 .e. word_of_nat (length as)] @ [1 + word_of_nat (length as)]) (b # as @ [a]) s = (createNewCaps ty ptr (Suc (Suc (length as))) us d >>= zipWithM_x (insertNewCap parent) (b # as @ [a])) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Suc (length (as @ [a])) < 2 ^ word_bits; \<forall>slot\<in>set (as @ [a]). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct (as @ [a]); b \<notin> set (as @ [a]); cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length (as @ [a]))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length (as @ [a]))) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> zipWithM_x (\<lambda>num slot. global.createObject ty ((num << getObjectSize ty us) + ptr) us d >>= insertNewCap parent slot) ([0 .e. word_of_nat (length as)] @ [1 + word_of_nat (length as)]) (b # as @ [a]) s = (createNewCaps ty ptr (Suc (Suc (length as))) us d >>= zipWithM_x (insertNewCap parent) (b # as @ [a])) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Suc (length (as @ [a])) < 2 ^ word_bits; \<forall>slot\<in>set (as @ [a]). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct (as @ [a]); b \<notin> set (as @ [a]); cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length (as @ [a]))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length (as @ [a]))) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> zipWithM_x (\<lambda>num slot. global.createObject ty ((num << getObjectSize ty us) + ptr) us d >>= insertNewCap parent slot) ([0 .e. word_of_nat (length as)] @ [1 + word_of_nat (length as)]) ((b # as) @ [a]) s = (createNewCaps ty ptr (Suc (Suc (length as))) us d >>= zipWithM_x (insertNewCap parent) (b # as @ [a])) s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Suc (length (as @ [a])) < 2 ^ word_bits; \<forall>slot\<in>set (as @ [a]). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct (as @ [a]); b \<notin> set (as @ [a]); cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length (as @ [a]))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length (as @ [a]))) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> length [0 .e. word_of_nat (length as)] = length (b # as)
 2. \<lbrakk>Suc (length (as @ [a])) < 2 ^ word_bits; \<forall>slot\<in>set (as @ [a]). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct (as @ [a]); b \<notin> set (as @ [a]); cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length (as @ [a]))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length (as @ [a]))) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> (do _ <- zipWithM_x (\<lambda>num slot. global.createObject ty ((num << getObjectSize ty us) + ptr) us d >>= insertNewCap parent slot) [0 .e. word_of_nat (length as)] (b # as);
global.createObject ty ((1 + word_of_nat (length as) << getObjectSize ty us) + ptr) us d >>= insertNewCap parent a
od) s = (createNewCaps ty ptr (Suc (Suc (length as))) us d >>= zipWithM_x (insertNewCap parent) (b # as @ [a])) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Suc (length (as @ [a])) < 2 ^ word_bits; \<forall>slot\<in>set (as @ [a]). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct (as @ [a]); b \<notin> set (as @ [a]); cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length (as @ [a]))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length (as @ [a]))) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> (do _ <- zipWithM_x (\<lambda>num slot. global.createObject ty ((num << getObjectSize ty us) + ptr) us d >>= insertNewCap parent slot) [0 .e. word_of_nat (length as)] (b # as);
global.createObject ty ((1 + word_of_nat (length as) << getObjectSize ty us) + ptr) us d >>= insertNewCap parent a
od) s = (createNewCaps ty ptr (Suc (Suc (length as))) us d >>= zipWithM_x (insertNewCap parent) (b # as @ [a])) s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Suc (length (as @ [a])) < 2 ^ word_bits; \<forall>slot\<in>set (as @ [a]). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct (as @ [a]); b \<notin> set (as @ [a]); cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length (as @ [a]))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length (as @ [a]))) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> zipWithM_x (\<lambda>num slot. global.createObject ty ((num << getObjectSize ty us) + ptr) us d >>= insertNewCap parent slot) [0 .e. word_of_nat (length as)] (b # as) s = ?b128 s
 2. \<lbrakk>Suc (length (as @ [a])) < 2 ^ word_bits; \<forall>slot\<in>set (as @ [a]). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct (as @ [a]); b \<notin> set (as @ [a]); cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length (as @ [a]))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length (as @ [a]))) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> (do _ <- ?b128;
global.createObject ty ((1 + word_of_nat (length as) << getObjectSize ty us) + ptr) us d >>= insertNewCap parent a
od) s = (createNewCaps ty ptr (Suc (Suc (length as))) us d >>= zipWithM_x (insertNewCap parent) (b # as @ [a])) s proof (prove)
goal (9 subgoals):
 1. \<lbrakk>Suc (length (as @ [a])) < 2 ^ word_bits; \<forall>slot\<in>set (as @ [a]). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct (as @ [a]); b \<notin> set (as @ [a]); cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length (as @ [a]))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length (as @ [a]))) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> Suc (length as) < 2 ^ word_bits
 2. \<lbrakk>Suc (length (as @ [a])) < 2 ^ word_bits; \<forall>slot\<in>set (as @ [a]). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct (as @ [a]); b \<notin> set (as @ [a]); cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length (as @ [a]))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length (as @ [a]))) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s
 3. \<lbrakk>Suc (length (as @ [a])) < 2 ^ word_bits; \<forall>slot\<in>set (as @ [a]). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct (as @ [a]); b \<notin> set (as @ [a]); cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length (as @ [a]))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length (as @ [a]))) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> distinct as
 4. \<lbrakk>Suc (length (as @ [a])) < 2 ^ word_bits; \<forall>slot\<in>set (as @ [a]). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct (as @ [a]); b \<notin> set (as @ [a]); cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length (as @ [a]))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length (as @ [a]))) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> b \<notin> set as
 5. \<lbrakk>Suc (length (as @ [a])) < 2 ^ word_bits; \<forall>slot\<in>set (as @ [a]). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct (as @ [a]); b \<notin> set (as @ [a]); cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length (as @ [a]))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length (as @ [a]))) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s
 6. \<lbrakk>Suc (length (as @ [a])) < 2 ^ word_bits; \<forall>slot\<in>set (as @ [a]). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct (as @ [a]); b \<notin> set (as @ [a]); cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length (as @ [a]))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length (as @ [a]))) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> range_cover ptr sz (getObjectSize ty us) (Suc (length as))
 7. \<lbrakk>Suc (length (as @ [a])) < 2 ^ word_bits; \<forall>slot\<in>set (as @ [a]). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct (as @ [a]); b \<notin> set (as @ [a]); cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length (as @ [a]))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length (as @ [a]))) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> ptr \<noteq> 0
 8. \<lbrakk>Suc (length (as @ [a])) < 2 ^ word_bits; \<forall>slot\<in>set (as @ [a]). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct (as @ [a]); b \<notin> set (as @ [a]); cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length (as @ [a]))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length (as @ [a]))) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s
 9. \<lbrakk>Suc (length (as @ [a])) < 2 ^ word_bits; \<forall>slot\<in>set (as @ [a]). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct (as @ [a]); b \<notin> set (as @ [a]); cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length (as @ [a]))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length (as @ [a]))) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> (do _ <- createNewCaps ty ptr (Suc (length as)) us d >>= zipWithM_x (insertNewCap parent) (b # as);
global.createObject ty ((1 + word_of_nat (length as) << getObjectSize ty us) + ptr) us d >>= insertNewCap parent a
od) s = (createNewCaps ty ptr (Suc (Suc (length as))) us d >>= zipWithM_x (insertNewCap parent) (b # as @ [a])) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> (do _ <- createNewCaps ty ptr (Suc (length as)) us d >>= zipWithM_x (insertNewCap parent) (b # as);
global.createObject ty ((1 + word_of_nat (length as) << getObjectSize ty us) + ptr) us d >>= insertNewCap parent a
od) s = (createNewCaps ty ptr (Suc (Suc (length as))) us d >>= zipWithM_x (insertNewCap parent) (b # as @ [a])) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> (do x <- createNewCaps ty ptr (Suc (length as)) us d;
_ <- zipWithM_x (insertNewCap parent) (b # as) x;
global.createObject ty ((1 + word_of_nat (length as) << getObjectSize ty us) + ptr) us d >>= insertNewCap parent a
od) s = (createNewCaps ty ptr (Suc (Suc (length as))) us d >>= zipWithM_x (insertNewCap parent) (b # as @ [a])) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> (createNewCaps ty ptr (Suc (Suc (length as))) us d >>= zipWithM_x (insertNewCap parent) (b # as @ [a])) s = (do x <- createNewCaps ty ptr (Suc (length as)) us d;
_ <- zipWithM_x (insertNewCap parent) (b # as) x;
global.createObject ty ((1 + word_of_nat (length as) << getObjectSize ty us) + ptr) us d >>= insertNewCap parent a
od) s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> createNewCaps ty ptr (Suc (Suc (length as))) us d s = ?b143 s
 2. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> (?b143 >>= zipWithM_x (insertNewCap parent) (b # as @ [a])) s = (do x <- createNewCaps ty ptr (Suc (length as)) us d;
_ <- zipWithM_x (insertNewCap parent) (b # as) x;
global.createObject ty ((1 + word_of_nat (length as) << getObjectSize ty us) + ptr) us d >>= insertNewCap parent a
od) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> (do x <- createNewCaps ty ptr (Suc (length as)) us d;
r <- global.createObject ty ((1 + word_of_nat (length as) << getObjectSize ty us) + ptr) us d;
return (x @ [r])
od >>= zipWithM_x (insertNewCap parent) (b # as @ [a])) s = (do x <- createNewCaps ty ptr (Suc (length as)) us d;
_ <- zipWithM_x (insertNewCap parent) (b # as) x;
global.createObject ty ((1 + word_of_nat (length as) << getObjectSize ty us) + ptr) us d >>= insertNewCap parent a
od) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> (do x <- createNewCaps ty ptr (Suc (length as)) us d;
_ <- zipWithM_x (insertNewCap parent) (b # as) x;
global.createObject ty ((1 + word_of_nat (length as) << getObjectSize ty us) + ptr) us d >>= insertNewCap parent a
od) s = (do x <- createNewCaps ty ptr (Suc (length as)) us d;
r <- global.createObject ty ((1 + word_of_nat (length as) << getObjectSize ty us) + ptr) us d;
return (x @ [r])
od >>= zipWithM_x (insertNewCap parent) (b # as @ [a])) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> (do x <- createNewCaps ty ptr (Suc (length as)) us d;
_ <- zipWithM_x (insertNewCap parent) (b # as) x;
global.createObject ty ((1 + word_of_nat (length as) << getObjectSize ty us) + ptr) us d >>= insertNewCap parent a
od) s = (do x <- createNewCaps ty ptr (Suc (length as)) us d;
r <- global.createObject ty ((1 + word_of_nat (length as) << getObjectSize ty us) + ptr) us d;
zipWithM_x (insertNewCap parent) (b # as @ [a]) (x @ [r])
od) s proof (prove)
goal (3 subgoals):
 1. \<And>r sa. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s; (\<forall>cap\<in>set r. cap \<noteq> capability.NullCap) \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent sa \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b sa \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot sa) \<and> pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) sa \<and> valid_pspace' sa \<and> valid_arch_state' sa \<and> ?Q151 r sa\<rbrakk> \<Longrightarrow> (do _ <- zipWithM_x (insertNewCap parent) (b # as) r;
global.createObject ty ((1 + word_of_nat (length as) << getObjectSize ty us) + ptr) us d >>= insertNewCap parent a
od) sa = (do ra <- global.createObject ty ((1 + word_of_nat (length as) << getObjectSize ty us) + ptr) us d;
zipWithM_x (insertNewCap parent) (b # as @ [a]) (r @ [ra])
od) sa
 2. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> \<lbrace>?P148\<rbrace> createNewCaps ty ptr (Suc (length as)) us d \<lbrace>\<lambda>r s. (\<forall>cap\<in>set r. cap \<noteq> capability.NullCap) \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent s \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) \<and> pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) s \<and> valid_pspace' s \<and> valid_arch_state' s \<and> ?Q151 r s\<rbrace>
 3. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> ?P148 s proof (prove)
goal (3 subgoals):
 1. \<And>r sa. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s; (\<forall>cap\<in>set r. cap \<noteq> capability.NullCap) \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent sa \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b sa \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot sa) \<and> pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) sa \<and> valid_pspace' sa \<and> valid_arch_state' sa \<and> ?Q151 r sa\<rbrakk> \<Longrightarrow> (do _ <- zipWithM_x (insertNewCap parent) (b # as) r;
global.createObject ty ((1 + word_of_nat (length as) << getObjectSize ty us) + ptr) us d >>= insertNewCap parent a
od) sa = (do ra <- global.createObject ty ((1 + word_of_nat (length as) << getObjectSize ty us) + ptr) us d;
zipWithM_x (insertNewCap parent) ((b # as) @ [a]) (r @ [ra])
od) sa
 2. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> \<lbrace>?P148\<rbrace> createNewCaps ty ptr (Suc (length as)) us d \<lbrace>\<lambda>r s. (\<forall>cap\<in>set r. cap \<noteq> capability.NullCap) \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent s \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) \<and> pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) s \<and> valid_pspace' s \<and> valid_arch_state' s \<and> ?Q151 r s\<rbrace>
 3. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> ?P148 s proof (prove)
goal (4 subgoals):
 1. \<And>r sa ra. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s; (\<forall>cap\<in>set r. cap \<noteq> capability.NullCap) \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent sa \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b sa \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot sa) \<and> pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) sa \<and> valid_pspace' sa \<and> valid_arch_state' sa \<and> ?Q151 r sa\<rbrakk> \<Longrightarrow> length (b # as) = length r
 2. \<And>r sa. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s; (\<forall>cap\<in>set r. cap \<noteq> capability.NullCap) \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent sa \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b sa \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot sa) \<and> pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) sa \<and> valid_pspace' sa \<and> valid_arch_state' sa \<and> ?Q151 r sa\<rbrakk> \<Longrightarrow> (do _ <- zipWithM_x (insertNewCap parent) (b # as) r;
global.createObject ty ((1 + word_of_nat (length as) << getObjectSize ty us) + ptr) us d >>= insertNewCap parent a
od) sa = (do ra <- global.createObject ty ((1 + word_of_nat (length as) << getObjectSize ty us) + ptr) us d;
_ <- zipWithM_x (insertNewCap parent) (b # as) r;
insertNewCap parent a ra
od) sa
 3. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> \<lbrace>?P148\<rbrace> createNewCaps ty ptr (Suc (length as)) us d \<lbrace>\<lambda>r s. (\<forall>cap\<in>set r. cap \<noteq> capability.NullCap) \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent s \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) \<and> pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) s \<and> valid_pspace' s \<and> valid_arch_state' s \<and> ?Q151 r s\<rbrace>
 4. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> ?P148 s proof (prove)
goal (4 subgoals):
 1. \<And>r sa. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct as; a \<notin> set as; b \<noteq> a; b \<notin> set as; \<forall>cap\<in>set r. cap \<noteq> capability.NullCap; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent sa; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b sa; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot sa; pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) sa; valid_pspace' sa; valid_arch_state' sa; ?Q151 r sa\<rbrakk> \<Longrightarrow> Suc (length as) = length r
 2. \<And>r sa. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s; (\<forall>cap\<in>set r. cap \<noteq> capability.NullCap) \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent sa \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b sa \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot sa) \<and> pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) sa \<and> valid_pspace' sa \<and> valid_arch_state' sa \<and> ?Q151 r sa\<rbrakk> \<Longrightarrow> (do _ <- zipWithM_x (insertNewCap parent) (b # as) r;
global.createObject ty ((1 + word_of_nat (length as) << getObjectSize ty us) + ptr) us d >>= insertNewCap parent a
od) sa = (do ra <- global.createObject ty ((1 + word_of_nat (length as) << getObjectSize ty us) + ptr) us d;
_ <- zipWithM_x (insertNewCap parent) (b # as) r;
insertNewCap parent a ra
od) sa
 3. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> \<lbrace>?P148\<rbrace> createNewCaps ty ptr (Suc (length as)) us d \<lbrace>\<lambda>r s. (\<forall>cap\<in>set r. cap \<noteq> capability.NullCap) \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent s \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) \<and> pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) s \<and> valid_pspace' s \<and> valid_arch_state' s \<and> ?Q151 r s\<rbrace>
 4. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> ?P148 s proof (prove)
goal (3 subgoals):
 1. \<And>r sa. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s; (\<forall>cap\<in>set r. cap \<noteq> capability.NullCap) \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent sa \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b sa \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot sa) \<and> pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) sa \<and> valid_pspace' sa \<and> valid_arch_state' sa \<and> Suc (length as) = length r\<rbrakk> \<Longrightarrow> (do _ <- zipWithM_x (insertNewCap parent) (b # as) r;
global.createObject ty ((1 + word_of_nat (length as) << getObjectSize ty us) + ptr) us d >>= insertNewCap parent a
od) sa = (do ra <- global.createObject ty ((1 + word_of_nat (length as) << getObjectSize ty us) + ptr) us d;
_ <- zipWithM_x (insertNewCap parent) (b # as) r;
insertNewCap parent a ra
od) sa
 2. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> \<lbrace>?P148\<rbrace> createNewCaps ty ptr (Suc (length as)) us d \<lbrace>\<lambda>r s. (\<forall>cap\<in>set r. cap \<noteq> capability.NullCap) \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent s \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) \<and> pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) s \<and> valid_pspace' s \<and> valid_arch_state' s \<and> Suc (length as) = length r\<rbrace>
 3. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> ?P148 s proof (prove)
goal (3 subgoals):
 1. \<And>r sa. \<lbrakk>Suc (length r) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length r)); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (word_of_nat (length as) * 2 ^ getObjectSize ty us + 2 * 2 ^ getObjectSize ty us) - 1} s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct as; a \<notin> set as; b \<noteq> a; b \<notin> set as; \<forall>cap\<in>set r. cap \<noteq> capability.NullCap; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent sa; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b sa; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot sa; pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) sa; valid_pspace' sa; valid_arch_state' sa; Suc (length as) = length r\<rbrakk> \<Longrightarrow> (do _ <- zipWithM_x (insertNewCap parent) (b # as) r;
global.createObject ty (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) us d >>= insertNewCap parent a
od) sa = (do ra <- global.createObject ty (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) us d;
_ <- zipWithM_x (insertNewCap parent) (b # as) r;
insertNewCap parent a ra
od) sa
 2. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> \<lbrace>?P148\<rbrace> createNewCaps ty ptr (Suc (length as)) us d \<lbrace>\<lambda>r s. (\<forall>cap\<in>set r. cap \<noteq> capability.NullCap) \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent s \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) \<and> pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) s \<and> valid_pspace' s \<and> valid_arch_state' s \<and> Suc (length as) = length r\<rbrace>
 3. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> ?P148 s proof (prove)
goal (5 subgoals):
 1. \<And>r sa. \<lbrakk>Suc (length r) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length r)); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (word_of_nat (length as) * 2 ^ getObjectSize ty us + 2 * 2 ^ getObjectSize ty us) - 1} s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct as; a \<notin> set as; b \<noteq> a; b \<notin> set as; \<forall>cap\<in>set r. cap \<noteq> capability.NullCap; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent sa; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b sa; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot sa; pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) sa; valid_pspace' sa; valid_arch_state' sa; Suc (length as) = length r\<rbrakk> \<Longrightarrow> monad_commute (?P183 r sa) (global.createObject ty (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) us d) (zipWithM_x (insertNewCap parent) (b # as) r)
 2. \<And>r sa. \<lbrakk>Suc (length r) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length r)); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (word_of_nat (length as) * 2 ^ getObjectSize ty us + 2 * 2 ^ getObjectSize ty us) - 1} s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct as; a \<notin> set as; b \<noteq> a; b \<notin> set as; \<forall>cap\<in>set r. cap \<noteq> capability.NullCap; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent sa; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b sa; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot sa; pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) sa; valid_pspace' sa; valid_arch_state' sa; Suc (length as) = length r\<rbrakk> \<Longrightarrow> ?P183 r sa sa
 3. \<And>r sa. \<lbrakk>Suc (length r) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length r)); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (word_of_nat (length as) * 2 ^ getObjectSize ty us + 2 * 2 ^ getObjectSize ty us) - 1} s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct as; a \<notin> set as; b \<noteq> a; b \<notin> set as; \<forall>cap\<in>set r. cap \<noteq> capability.NullCap; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent sa; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b sa; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot sa; pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) sa; valid_pspace' sa; valid_arch_state' sa; Suc (length as) = length r\<rbrakk> \<Longrightarrow> (do y <- global.createObject ty (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) us d;
x <- zipWithM_x (insertNewCap parent) (b # as) r;
insertNewCap parent a y
od) sa = (do ra <- global.createObject ty (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) us d;
_ <- zipWithM_x (insertNewCap parent) (b # as) r;
insertNewCap parent a ra
od) sa
 4. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> \<lbrace>?P148\<rbrace> createNewCaps ty ptr (Suc (length as)) us d \<lbrace>\<lambda>r s. (\<forall>cap\<in>set r. cap \<noteq> capability.NullCap) \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent s \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) \<and> pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) s \<and> valid_pspace' s \<and> valid_arch_state' s \<and> Suc (length as) = length r\<rbrace>
 5. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> ?P148 s proof (prove)
goal (4 subgoals):
 1. \<And>r sa. \<lbrakk>Suc (length r) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length r)); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (word_of_nat (length as) * 2 ^ getObjectSize ty us + 2 * 2 ^ getObjectSize ty us) - 1} s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct as; a \<notin> set as; b \<noteq> a; b \<notin> set as; \<forall>cap\<in>set r. cap \<noteq> capability.NullCap; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent sa; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b sa; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot sa; pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) sa; valid_pspace' sa; valid_arch_state' sa; Suc (length as) = length r\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent and (\<lambda>s. \<forall>slot\<in>set (b # as). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) and pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) and valid_pspace' and valid_arch_state' and K (distinct (map fst (zip (b # as) r))) and K (\<forall>cap\<in>set r. cap \<noteq> capability.NullCap) and K (getObjectSize ty us < word_bits) and K (is_aligned (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) \<and> ptr + (1 + word_of_nat (length as) << getObjectSize ty us) \<noteq> 0)) sa
 2. \<And>r sa. \<lbrakk>Suc (length r) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length r)); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (word_of_nat (length as) * 2 ^ getObjectSize ty us + 2 * 2 ^ getObjectSize ty us) - 1} s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct as; a \<notin> set as; b \<noteq> a; b \<notin> set as; \<forall>cap\<in>set r. cap \<noteq> capability.NullCap; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent sa; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b sa; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot sa; pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) sa; valid_pspace' sa; valid_arch_state' sa; Suc (length as) = length r\<rbrakk> \<Longrightarrow> (do y <- global.createObject ty (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) us d;
x <- zipWithM_x (insertNewCap parent) (b # as) r;
insertNewCap parent a y
od) sa = (do ra <- global.createObject ty (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) us d;
_ <- zipWithM_x (insertNewCap parent) (b # as) r;
insertNewCap parent a ra
od) sa
 3. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> \<lbrace>?P148\<rbrace> createNewCaps ty ptr (Suc (length as)) us d \<lbrace>\<lambda>r s. (\<forall>cap\<in>set r. cap \<noteq> capability.NullCap) \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent s \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) \<and> pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) s \<and> valid_pspace' s \<and> valid_arch_state' s \<and> Suc (length as) = length r\<rbrace>
 4. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> ?P148 s proof (prove)
goal (4 subgoals):
 1. \<And>r sa. \<lbrakk>Suc (length r) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length r)); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (word_of_nat (length as) * 2 ^ getObjectSize ty us + 2 * 2 ^ getObjectSize ty us) - 1} s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct as; a \<notin> set as; b \<noteq> a; b \<notin> set as; \<forall>cap\<in>set r. cap \<noteq> capability.NullCap; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent sa; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b sa; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot sa; pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) sa; valid_pspace' sa; valid_arch_state' sa; Suc (length as) = length r\<rbrakk> \<Longrightarrow> getObjectSize ty us < word_bits \<and> is_aligned (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) \<and> ptr + (1 + word_of_nat (length as) << getObjectSize ty us) \<noteq> 0
 2. \<And>r sa. \<lbrakk>Suc (length r) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length r)); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (word_of_nat (length as) * 2 ^ getObjectSize ty us + 2 * 2 ^ getObjectSize ty us) - 1} s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct as; a \<notin> set as; b \<noteq> a; b \<notin> set as; \<forall>cap\<in>set r. cap \<noteq> capability.NullCap; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent sa; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b sa; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot sa; pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) sa; valid_pspace' sa; valid_arch_state' sa; Suc (length as) = length r\<rbrakk> \<Longrightarrow> (do y <- global.createObject ty (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) us d;
x <- zipWithM_x (insertNewCap parent) (b # as) r;
insertNewCap parent a y
od) sa = (do ra <- global.createObject ty (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) us d;
_ <- zipWithM_x (insertNewCap parent) (b # as) r;
insertNewCap parent a ra
od) sa
 3. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> \<lbrace>?P148\<rbrace> createNewCaps ty ptr (Suc (length as)) us d \<lbrace>\<lambda>r s. (\<forall>cap\<in>set r. cap \<noteq> capability.NullCap) \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent s \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) \<and> pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) s \<and> valid_pspace' s \<and> valid_arch_state' s \<and> Suc (length as) = length r\<rbrace>
 4. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> ?P148 s proof (prove)
goal (6 subgoals):
 1. \<And>r sa. \<lbrakk>Suc (length r) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length r)); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (word_of_nat (length as) * 2 ^ getObjectSize ty us + 2 * 2 ^ getObjectSize ty us) - 1} s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct as; a \<notin> set as; b \<noteq> a; b \<notin> set as; \<forall>cap\<in>set r. cap \<noteq> capability.NullCap; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent sa; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b sa; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot sa; pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) sa; valid_pspace' sa; valid_arch_state' sa; Suc (length as) = length r\<rbrakk> \<Longrightarrow> 1 + length as < Suc (length r)
 2. \<And>r sa. \<lbrakk>Suc (length r) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length r)); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (word_of_nat (length as) * 2 ^ getObjectSize ty us + 2 * 2 ^ getObjectSize ty us) - 1} s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct as; a \<notin> set as; b \<noteq> a; b \<notin> set as; \<forall>cap\<in>set r. cap \<noteq> capability.NullCap; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent sa; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b sa; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot sa; pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) sa; valid_pspace' sa; valid_arch_state' sa; Suc (length as) = length r\<rbrakk> \<Longrightarrow> ptr \<noteq> 0
 3. \<And>r sa. \<lbrakk>Suc (length r) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length r)); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (word_of_nat (length as) * 2 ^ getObjectSize ty us + 2 * 2 ^ getObjectSize ty us) - 1} s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct as; a \<notin> set as; b \<noteq> a; b \<notin> set as; \<forall>cap\<in>set r. cap \<noteq> capability.NullCap; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent sa; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b sa; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot sa; pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) sa; valid_pspace' sa; valid_arch_state' sa; Suc (length as) = length r; ptr + word_of_nat (1 + length as) * 2 ^ getObjectSize ty us \<noteq> 0\<rbrakk> \<Longrightarrow> getObjectSize ty us < word_bits \<and> is_aligned (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) \<and> ptr + (1 + word_of_nat (length as) << getObjectSize ty us) \<noteq> 0
 4. \<And>r sa. \<lbrakk>Suc (length r) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length r)); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (word_of_nat (length as) * 2 ^ getObjectSize ty us + 2 * 2 ^ getObjectSize ty us) - 1} s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct as; a \<notin> set as; b \<noteq> a; b \<notin> set as; \<forall>cap\<in>set r. cap \<noteq> capability.NullCap; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent sa; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b sa; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot sa; pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) sa; valid_pspace' sa; valid_arch_state' sa; Suc (length as) = length r\<rbrakk> \<Longrightarrow> (do y <- global.createObject ty (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) us d;
x <- zipWithM_x (insertNewCap parent) (b # as) r;
insertNewCap parent a y
od) sa = (do ra <- global.createObject ty (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) us d;
_ <- zipWithM_x (insertNewCap parent) (b # as) r;
insertNewCap parent a ra
od) sa
 5. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> \<lbrace>?P148\<rbrace> createNewCaps ty ptr (Suc (length as)) us d \<lbrace>\<lambda>r s. (\<forall>cap\<in>set r. cap \<noteq> capability.NullCap) \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent s \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) \<and> pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) s \<and> valid_pspace' s \<and> valid_arch_state' s \<and> Suc (length as) = length r\<rbrace>
 6. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> ?P148 s proof (prove)
goal (5 subgoals):
 1. \<And>r sa. \<lbrakk>Suc (length r) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length r)); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (word_of_nat (length as) * 2 ^ getObjectSize ty us + 2 * 2 ^ getObjectSize ty us) - 1} s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct as; a \<notin> set as; b \<noteq> a; b \<notin> set as; \<forall>cap\<in>set r. cap \<noteq> capability.NullCap; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent sa; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b sa; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot sa; pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) sa; valid_pspace' sa; valid_arch_state' sa; Suc (length as) = length r\<rbrakk> \<Longrightarrow> ptr \<noteq> 0
 2. \<And>r sa. \<lbrakk>Suc (length r) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length r)); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (word_of_nat (length as) * 2 ^ getObjectSize ty us + 2 * 2 ^ getObjectSize ty us) - 1} s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct as; a \<notin> set as; b \<noteq> a; b \<notin> set as; \<forall>cap\<in>set r. cap \<noteq> capability.NullCap; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent sa; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b sa; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot sa; pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) sa; valid_pspace' sa; valid_arch_state' sa; Suc (length as) = length r; ptr + word_of_nat (1 + length as) * 2 ^ getObjectSize ty us \<noteq> 0\<rbrakk> \<Longrightarrow> getObjectSize ty us < word_bits \<and> is_aligned (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) \<and> ptr + (1 + word_of_nat (length as) << getObjectSize ty us) \<noteq> 0
 3. \<And>r sa. \<lbrakk>Suc (length r) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length r)); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (word_of_nat (length as) * 2 ^ getObjectSize ty us + 2 * 2 ^ getObjectSize ty us) - 1} s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct as; a \<notin> set as; b \<noteq> a; b \<notin> set as; \<forall>cap\<in>set r. cap \<noteq> capability.NullCap; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent sa; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b sa; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot sa; pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) sa; valid_pspace' sa; valid_arch_state' sa; Suc (length as) = length r\<rbrakk> \<Longrightarrow> (do y <- global.createObject ty (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) us d;
x <- zipWithM_x (insertNewCap parent) (b # as) r;
insertNewCap parent a y
od) sa = (do ra <- global.createObject ty (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) us d;
_ <- zipWithM_x (insertNewCap parent) (b # as) r;
insertNewCap parent a ra
od) sa
 4. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> \<lbrace>?P148\<rbrace> createNewCaps ty ptr (Suc (length as)) us d \<lbrace>\<lambda>r s. (\<forall>cap\<in>set r. cap \<noteq> capability.NullCap) \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent s \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) \<and> pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) s \<and> valid_pspace' s \<and> valid_arch_state' s \<and> Suc (length as) = length r\<rbrace>
 5. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> ?P148 s proof (prove)
goal (4 subgoals):
 1. \<And>r sa. \<lbrakk>Suc (length r) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length r)); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (word_of_nat (length as) * 2 ^ getObjectSize ty us + 2 * 2 ^ getObjectSize ty us) - 1} s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct as; a \<notin> set as; b \<noteq> a; b \<notin> set as; \<forall>cap\<in>set r. cap \<noteq> capability.NullCap; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent sa; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b sa; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot sa; pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) sa; valid_pspace' sa; valid_arch_state' sa; Suc (length as) = length r; ptr + word_of_nat (1 + length as) * 2 ^ getObjectSize ty us \<noteq> 0\<rbrakk> \<Longrightarrow> getObjectSize ty us < word_bits \<and> is_aligned (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) \<and> ptr + (1 + word_of_nat (length as) << getObjectSize ty us) \<noteq> 0
 2. \<And>r sa. \<lbrakk>Suc (length r) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length r)); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (word_of_nat (length as) * 2 ^ getObjectSize ty us + 2 * 2 ^ getObjectSize ty us) - 1} s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct as; a \<notin> set as; b \<noteq> a; b \<notin> set as; \<forall>cap\<in>set r. cap \<noteq> capability.NullCap; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent sa; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b sa; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot sa; pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) sa; valid_pspace' sa; valid_arch_state' sa; Suc (length as) = length r\<rbrakk> \<Longrightarrow> (do y <- global.createObject ty (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) us d;
x <- zipWithM_x (insertNewCap parent) (b # as) r;
insertNewCap parent a y
od) sa = (do ra <- global.createObject ty (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) us d;
_ <- zipWithM_x (insertNewCap parent) (b # as) r;
insertNewCap parent a ra
od) sa
 3. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> \<lbrace>?P148\<rbrace> createNewCaps ty ptr (Suc (length as)) us d \<lbrace>\<lambda>r s. (\<forall>cap\<in>set r. cap \<noteq> capability.NullCap) \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent s \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) \<and> pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) s \<and> valid_pspace' s \<and> valid_arch_state' s \<and> Suc (length as) = length r\<rbrace>
 4. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> ?P148 s proof (prove)
goal (4 subgoals):
 1. \<And>r sa. \<lbrakk>Suc (length r) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length r)); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (word_of_nat (length as) * 2 ^ getObjectSize ty us + 2 * 2 ^ getObjectSize ty us) - 1} s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct as; a \<notin> set as; b \<noteq> a; b \<notin> set as; \<forall>cap\<in>set r. cap \<noteq> capability.NullCap; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent sa; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b sa; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot sa; pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) sa; valid_pspace' sa; valid_arch_state' sa; Suc (length as) = length r; ptr + (word_of_nat 1 + word_of_nat (length as)) * 2 ^ getObjectSize ty us \<noteq> 0\<rbrakk> \<Longrightarrow> getObjectSize ty us < word_bits \<and> is_aligned (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) \<and> ptr + (1 + word_of_nat (length as) << getObjectSize ty us) \<noteq> 0
 2. \<And>r sa. \<lbrakk>Suc (length r) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length r)); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (word_of_nat (length as) * 2 ^ getObjectSize ty us + 2 * 2 ^ getObjectSize ty us) - 1} s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct as; a \<notin> set as; b \<noteq> a; b \<notin> set as; \<forall>cap\<in>set r. cap \<noteq> capability.NullCap; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent sa; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b sa; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot sa; pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) sa; valid_pspace' sa; valid_arch_state' sa; Suc (length as) = length r\<rbrakk> \<Longrightarrow> (do y <- global.createObject ty (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) us d;
x <- zipWithM_x (insertNewCap parent) (b # as) r;
insertNewCap parent a y
od) sa = (do ra <- global.createObject ty (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) us d;
_ <- zipWithM_x (insertNewCap parent) (b # as) r;
insertNewCap parent a ra
od) sa
 3. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> \<lbrace>?P148\<rbrace> createNewCaps ty ptr (Suc (length as)) us d \<lbrace>\<lambda>r s. (\<forall>cap\<in>set r. cap \<noteq> capability.NullCap) \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent s \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) \<and> pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) s \<and> valid_pspace' s \<and> valid_arch_state' s \<and> Suc (length as) = length r\<rbrace>
 4. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> ?P148 s proof (prove)
goal (6 subgoals):
 1. \<And>r sa. \<lbrakk>Suc (length r) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length r)); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (word_of_nat (length as) * 2 ^ getObjectSize ty us + 2 * 2 ^ getObjectSize ty us) - 1} s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct as; a \<notin> set as; b \<noteq> a; b \<notin> set as; \<forall>cap\<in>set r. cap \<noteq> capability.NullCap; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent sa; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b sa; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot sa; pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) sa; valid_pspace' sa; valid_arch_state' sa; Suc (length as) = length r; ptr + (word_of_nat 1 + word_of_nat (length as)) * 2 ^ getObjectSize ty us \<noteq> 0\<rbrakk> \<Longrightarrow> getObjectSize ty us < word_bits
 2. \<And>r sa. \<lbrakk>Suc (length r) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length r)); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (word_of_nat (length as) * 2 ^ getObjectSize ty us + 2 * 2 ^ getObjectSize ty us) - 1} s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct as; a \<notin> set as; b \<noteq> a; b \<notin> set as; \<forall>cap\<in>set r. cap \<noteq> capability.NullCap; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent sa; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b sa; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot sa; pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) sa; valid_pspace' sa; valid_arch_state' sa; Suc (length as) = length r; ptr + (word_of_nat 1 + word_of_nat (length as)) * 2 ^ getObjectSize ty us \<noteq> 0\<rbrakk> \<Longrightarrow> is_aligned (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us)
 3. \<And>r sa. \<lbrakk>Suc (length r) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length r)); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (word_of_nat (length as) * 2 ^ getObjectSize ty us + 2 * 2 ^ getObjectSize ty us) - 1} s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct as; a \<notin> set as; b \<noteq> a; b \<notin> set as; \<forall>cap\<in>set r. cap \<noteq> capability.NullCap; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent sa; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b sa; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot sa; pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) sa; valid_pspace' sa; valid_arch_state' sa; Suc (length as) = length r; ptr + (word_of_nat 1 + word_of_nat (length as)) * 2 ^ getObjectSize ty us \<noteq> 0\<rbrakk> \<Longrightarrow> ptr + (1 + word_of_nat (length as) << getObjectSize ty us) \<noteq> 0
 4. \<And>r sa. \<lbrakk>Suc (length r) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length r)); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (word_of_nat (length as) * 2 ^ getObjectSize ty us + 2 * 2 ^ getObjectSize ty us) - 1} s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct as; a \<notin> set as; b \<noteq> a; b \<notin> set as; \<forall>cap\<in>set r. cap \<noteq> capability.NullCap; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent sa; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b sa; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot sa; pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) sa; valid_pspace' sa; valid_arch_state' sa; Suc (length as) = length r\<rbrakk> \<Longrightarrow> (do y <- global.createObject ty (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) us d;
x <- zipWithM_x (insertNewCap parent) (b # as) r;
insertNewCap parent a y
od) sa = (do ra <- global.createObject ty (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) us d;
_ <- zipWithM_x (insertNewCap parent) (b # as) r;
insertNewCap parent a ra
od) sa
 5. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> \<lbrace>?P148\<rbrace> createNewCaps ty ptr (Suc (length as)) us d \<lbrace>\<lambda>r s. (\<forall>cap\<in>set r. cap \<noteq> capability.NullCap) \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent s \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) \<and> pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) s \<and> valid_pspace' s \<and> valid_arch_state' s \<and> Suc (length as) = length r\<rbrace>
 6. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> ?P148 s proof (prove)
goal (5 subgoals):
 1. \<And>r sa. \<lbrakk>Suc (length r) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length r)); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (word_of_nat (length as) * 2 ^ getObjectSize ty us + 2 * 2 ^ getObjectSize ty us) - 1} s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct as; a \<notin> set as; b \<noteq> a; b \<notin> set as; \<forall>cap\<in>set r. cap \<noteq> capability.NullCap; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent sa; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b sa; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot sa; pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) sa; valid_pspace' sa; valid_arch_state' sa; Suc (length as) = length r; ptr + (word_of_nat 1 + word_of_nat (length as)) * 2 ^ getObjectSize ty us \<noteq> 0\<rbrakk> \<Longrightarrow> is_aligned (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us)
 2. \<And>r sa. \<lbrakk>Suc (length r) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length r)); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (word_of_nat (length as) * 2 ^ getObjectSize ty us + 2 * 2 ^ getObjectSize ty us) - 1} s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct as; a \<notin> set as; b \<noteq> a; b \<notin> set as; \<forall>cap\<in>set r. cap \<noteq> capability.NullCap; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent sa; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b sa; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot sa; pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) sa; valid_pspace' sa; valid_arch_state' sa; Suc (length as) = length r; ptr + (word_of_nat 1 + word_of_nat (length as)) * 2 ^ getObjectSize ty us \<noteq> 0\<rbrakk> \<Longrightarrow> ptr + (1 + word_of_nat (length as) << getObjectSize ty us) \<noteq> 0
 3. \<And>r sa. \<lbrakk>Suc (length r) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length r)); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (word_of_nat (length as) * 2 ^ getObjectSize ty us + 2 * 2 ^ getObjectSize ty us) - 1} s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct as; a \<notin> set as; b \<noteq> a; b \<notin> set as; \<forall>cap\<in>set r. cap \<noteq> capability.NullCap; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent sa; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b sa; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot sa; pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) sa; valid_pspace' sa; valid_arch_state' sa; Suc (length as) = length r\<rbrakk> \<Longrightarrow> (do y <- global.createObject ty (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) us d;
x <- zipWithM_x (insertNewCap parent) (b # as) r;
insertNewCap parent a y
od) sa = (do ra <- global.createObject ty (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) us d;
_ <- zipWithM_x (insertNewCap parent) (b # as) r;
insertNewCap parent a ra
od) sa
 4. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> \<lbrace>?P148\<rbrace> createNewCaps ty ptr (Suc (length as)) us d \<lbrace>\<lambda>r s. (\<forall>cap\<in>set r. cap \<noteq> capability.NullCap) \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent s \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) \<and> pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) s \<and> valid_pspace' s \<and> valid_arch_state' s \<and> Suc (length as) = length r\<rbrace>
 5. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> ?P148 s proof (prove)
goal (6 subgoals):
 1. \<And>r sa. \<lbrakk>Suc (length r) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length r)); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (word_of_nat (length as) * 2 ^ getObjectSize ty us + 2 * 2 ^ getObjectSize ty us) - 1} s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct as; a \<notin> set as; b \<noteq> a; b \<notin> set as; \<forall>cap\<in>set r. cap \<noteq> capability.NullCap; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent sa; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b sa; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot sa; pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) sa; valid_pspace' sa; valid_arch_state' sa; Suc (length as) = length r; ptr + (word_of_nat 1 + word_of_nat (length as)) * 2 ^ getObjectSize ty us \<noteq> 0\<rbrakk> \<Longrightarrow> is_aligned (1 + word_of_nat (length as) << getObjectSize ty us) (getObjectSize ty us)
 2. \<And>r sa. \<lbrakk>Suc (length r) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length r)); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (word_of_nat (length as) * 2 ^ getObjectSize ty us + 2 * 2 ^ getObjectSize ty us) - 1} s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct as; a \<notin> set as; b \<noteq> a; b \<notin> set as; \<forall>cap\<in>set r. cap \<noteq> capability.NullCap; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent sa; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b sa; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot sa; pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) sa; valid_pspace' sa; valid_arch_state' sa; Suc (length as) = length r; ptr + (word_of_nat 1 + word_of_nat (length as)) * 2 ^ getObjectSize ty us \<noteq> 0\<rbrakk> \<Longrightarrow> getObjectSize ty us \<le> getObjectSize ty us
 3. \<And>r sa. \<lbrakk>Suc (length r) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length r)); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (word_of_nat (length as) * 2 ^ getObjectSize ty us + 2 * 2 ^ getObjectSize ty us) - 1} s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct as; a \<notin> set as; b \<noteq> a; b \<notin> set as; \<forall>cap\<in>set r. cap \<noteq> capability.NullCap; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent sa; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b sa; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot sa; pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) sa; valid_pspace' sa; valid_arch_state' sa; Suc (length as) = length r; ptr + (word_of_nat 1 + word_of_nat (length as)) * 2 ^ getObjectSize ty us \<noteq> 0\<rbrakk> \<Longrightarrow> ptr + (1 + word_of_nat (length as) << getObjectSize ty us) \<noteq> 0
 4. \<And>r sa. \<lbrakk>Suc (length r) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length r)); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (word_of_nat (length as) * 2 ^ getObjectSize ty us + 2 * 2 ^ getObjectSize ty us) - 1} s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct as; a \<notin> set as; b \<noteq> a; b \<notin> set as; \<forall>cap\<in>set r. cap \<noteq> capability.NullCap; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent sa; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b sa; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot sa; pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) sa; valid_pspace' sa; valid_arch_state' sa; Suc (length as) = length r\<rbrakk> \<Longrightarrow> (do y <- global.createObject ty (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) us d;
x <- zipWithM_x (insertNewCap parent) (b # as) r;
insertNewCap parent a y
od) sa = (do ra <- global.createObject ty (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) us d;
_ <- zipWithM_x (insertNewCap parent) (b # as) r;
insertNewCap parent a ra
od) sa
 5. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> \<lbrace>?P148\<rbrace> createNewCaps ty ptr (Suc (length as)) us d \<lbrace>\<lambda>r s. (\<forall>cap\<in>set r. cap \<noteq> capability.NullCap) \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent s \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) \<and> pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) s \<and> valid_pspace' s \<and> valid_arch_state' s \<and> Suc (length as) = length r\<rbrace>
 6. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> ?P148 s proof (prove)
goal (5 subgoals):
 1. \<And>r sa. \<lbrakk>Suc (length r) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length r)); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (word_of_nat (length as) * 2 ^ getObjectSize ty us + 2 * 2 ^ getObjectSize ty us) - 1} s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct as; a \<notin> set as; b \<noteq> a; b \<notin> set as; \<forall>cap\<in>set r. cap \<noteq> capability.NullCap; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent sa; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b sa; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot sa; pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) sa; valid_pspace' sa; valid_arch_state' sa; Suc (length as) = length r; ptr + (word_of_nat 1 + word_of_nat (length as)) * 2 ^ getObjectSize ty us \<noteq> 0\<rbrakk> \<Longrightarrow> getObjectSize ty us \<le> getObjectSize ty us
 2. \<And>r sa. \<lbrakk>Suc (length r) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length r)); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (word_of_nat (length as) * 2 ^ getObjectSize ty us + 2 * 2 ^ getObjectSize ty us) - 1} s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct as; a \<notin> set as; b \<noteq> a; b \<notin> set as; \<forall>cap\<in>set r. cap \<noteq> capability.NullCap; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent sa; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b sa; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot sa; pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) sa; valid_pspace' sa; valid_arch_state' sa; Suc (length as) = length r; ptr + (word_of_nat 1 + word_of_nat (length as)) * 2 ^ getObjectSize ty us \<noteq> 0\<rbrakk> \<Longrightarrow> ptr + (1 + word_of_nat (length as) << getObjectSize ty us) \<noteq> 0
 3. \<And>r sa. \<lbrakk>Suc (length r) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length r)); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (word_of_nat (length as) * 2 ^ getObjectSize ty us + 2 * 2 ^ getObjectSize ty us) - 1} s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct as; a \<notin> set as; b \<noteq> a; b \<notin> set as; \<forall>cap\<in>set r. cap \<noteq> capability.NullCap; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent sa; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b sa; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot sa; pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) sa; valid_pspace' sa; valid_arch_state' sa; Suc (length as) = length r\<rbrakk> \<Longrightarrow> (do y <- global.createObject ty (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) us d;
x <- zipWithM_x (insertNewCap parent) (b # as) r;
insertNewCap parent a y
od) sa = (do ra <- global.createObject ty (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) us d;
_ <- zipWithM_x (insertNewCap parent) (b # as) r;
insertNewCap parent a ra
od) sa
 4. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> \<lbrace>?P148\<rbrace> createNewCaps ty ptr (Suc (length as)) us d \<lbrace>\<lambda>r s. (\<forall>cap\<in>set r. cap \<noteq> capability.NullCap) \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent s \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) \<and> pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) s \<and> valid_pspace' s \<and> valid_arch_state' s \<and> Suc (length as) = length r\<rbrace>
 5. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> ?P148 s proof (prove)
goal (4 subgoals):
 1. \<And>r sa. \<lbrakk>Suc (length r) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length r)); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (word_of_nat (length as) * 2 ^ getObjectSize ty us + 2 * 2 ^ getObjectSize ty us) - 1} s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct as; a \<notin> set as; b \<noteq> a; b \<notin> set as; \<forall>cap\<in>set r. cap \<noteq> capability.NullCap; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent sa; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b sa; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot sa; pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) sa; valid_pspace' sa; valid_arch_state' sa; Suc (length as) = length r; ptr + (word_of_nat 1 + word_of_nat (length as)) * 2 ^ getObjectSize ty us \<noteq> 0\<rbrakk> \<Longrightarrow> ptr + (1 + word_of_nat (length as) << getObjectSize ty us) \<noteq> 0
 2. \<And>r sa. \<lbrakk>Suc (length r) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length r)); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (word_of_nat (length as) * 2 ^ getObjectSize ty us + 2 * 2 ^ getObjectSize ty us) - 1} s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct as; a \<notin> set as; b \<noteq> a; b \<notin> set as; \<forall>cap\<in>set r. cap \<noteq> capability.NullCap; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent sa; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b sa; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot sa; pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) sa; valid_pspace' sa; valid_arch_state' sa; Suc (length as) = length r\<rbrakk> \<Longrightarrow> (do y <- global.createObject ty (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) us d;
x <- zipWithM_x (insertNewCap parent) (b # as) r;
insertNewCap parent a y
od) sa = (do ra <- global.createObject ty (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) us d;
_ <- zipWithM_x (insertNewCap parent) (b # as) r;
insertNewCap parent a ra
od) sa
 3. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> \<lbrace>?P148\<rbrace> createNewCaps ty ptr (Suc (length as)) us d \<lbrace>\<lambda>r s. (\<forall>cap\<in>set r. cap \<noteq> capability.NullCap) \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent s \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) \<and> pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) s \<and> valid_pspace' s \<and> valid_arch_state' s \<and> Suc (length as) = length r\<rbrace>
 4. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> ?P148 s proof (prove)
goal (4 subgoals):
 1. \<And>r sa. \<lbrakk>Suc (length r) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; is_aligned ptr (getObjectSize ty us) \<and> sz < 32 \<and> getObjectSize ty us \<le> sz \<and> Suc (length r + unat (ptr && mask sz >> getObjectSize ty us)) \<le> 2 ^ (sz - getObjectSize ty us); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (word_of_nat (length as) * 2 ^ getObjectSize ty us + 2 * 2 ^ getObjectSize ty us) - 1} s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct as; a \<notin> set as; b \<noteq> a; b \<notin> set as; \<forall>cap\<in>set r. cap \<noteq> capability.NullCap; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent sa; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b sa; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot sa; pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) sa; valid_pspace' sa; valid_arch_state' sa; Suc (length as) = length r; ptr + (1 + word_of_nat (length as)) * 2 ^ getObjectSize ty us \<noteq> 0\<rbrakk> \<Longrightarrow> ptr + (1 + word_of_nat (length as) << getObjectSize ty us) \<noteq> 0
 2. \<And>r sa. \<lbrakk>Suc (length r) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length r)); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (word_of_nat (length as) * 2 ^ getObjectSize ty us + 2 * 2 ^ getObjectSize ty us) - 1} s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct as; a \<notin> set as; b \<noteq> a; b \<notin> set as; \<forall>cap\<in>set r. cap \<noteq> capability.NullCap; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent sa; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b sa; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot sa; pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) sa; valid_pspace' sa; valid_arch_state' sa; Suc (length as) = length r\<rbrakk> \<Longrightarrow> (do y <- global.createObject ty (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) us d;
x <- zipWithM_x (insertNewCap parent) (b # as) r;
insertNewCap parent a y
od) sa = (do ra <- global.createObject ty (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) us d;
_ <- zipWithM_x (insertNewCap parent) (b # as) r;
insertNewCap parent a ra
od) sa
 3. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> \<lbrace>?P148\<rbrace> createNewCaps ty ptr (Suc (length as)) us d \<lbrace>\<lambda>r s. (\<forall>cap\<in>set r. cap \<noteq> capability.NullCap) \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent s \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) \<and> pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) s \<and> valid_pspace' s \<and> valid_arch_state' s \<and> Suc (length as) = length r\<rbrace>
 4. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> ?P148 s proof (prove)
goal (3 subgoals):
 1. \<And>r sa. \<lbrakk>Suc (length r) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (length r)); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (word_of_nat (length as) * 2 ^ getObjectSize ty us + 2 * 2 ^ getObjectSize ty us) - 1} s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct as; a \<notin> set as; b \<noteq> a; b \<notin> set as; \<forall>cap\<in>set r. cap \<noteq> capability.NullCap; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent sa; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b sa; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot sa; pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) sa; valid_pspace' sa; valid_arch_state' sa; Suc (length as) = length r\<rbrakk> \<Longrightarrow> (do y <- global.createObject ty (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) us d;
x <- zipWithM_x (insertNewCap parent) (b # as) r;
insertNewCap parent a y
od) sa = (do ra <- global.createObject ty (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) us d;
_ <- zipWithM_x (insertNewCap parent) (b # as) r;
insertNewCap parent a ra
od) sa
 2. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> \<lbrace>?P148\<rbrace> createNewCaps ty ptr (Suc (length as)) us d \<lbrace>\<lambda>r s. (\<forall>cap\<in>set r. cap \<noteq> capability.NullCap) \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent s \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) \<and> pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) s \<and> valid_pspace' s \<and> valid_arch_state' s \<and> Suc (length as) = length r\<rbrace>
 3. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> ?P148 s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> \<lbrace>?P148\<rbrace> createNewCaps ty ptr (Suc (length as)) us d \<lbrace>\<lambda>r s. (\<forall>cap\<in>set r. cap \<noteq> capability.NullCap) \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent s \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) \<and> pspace_no_overlap' (ptr + (1 + word_of_nat (length as) << getObjectSize ty us)) (getObjectSize ty us) s \<and> valid_pspace' s \<and> valid_arch_state' s \<and> Suc (length as) = length r\<rbrace>
 2. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> ?P148 s proof (prove)
goal (4 subgoals):
 1. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> Suc (length as) \<noteq> 0
 2. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> range_cover ptr sz (APIType_capBits ty us) (Suc (length as))
 3. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> \<lbrace>?P'213\<rbrace> createNewCaps ty ptr (Suc (length as)) us d \<lbrace>\<lambda>rv s. valid_arch_state' s \<and> Suc (length as) = length rv\<rbrace>
 4. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> True \<and> (cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent s \<and> range_cover ptr sz (APIType_capBits ty us) (Suc (length as)) \<and> Suc (length as) \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) \<and> (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s \<and> range_cover ptr sz (APIType_capBits ty us) (Suc (length as)) \<and> Suc (length as) \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) \<and> (\<forall>x\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) x s \<and> range_cover ptr sz (APIType_capBits ty us) (Suc (length as)) \<and> Suc (length as) \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) \<and> (range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))) \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> ptr \<noteq> 0) \<and> (pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat (Suc (length as)) * 2 ^ APIType_capBits ty us - 1} s \<and> ksCurDomain s \<le> maxDomain) \<and> ?P'213 s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> range_cover ptr sz (APIType_capBits ty us) (Suc (length as))
 2. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> \<lbrace>?P'213\<rbrace> createNewCaps ty ptr (Suc (length as)) us d \<lbrace>\<lambda>rv s. valid_arch_state' s \<and> Suc (length as) = length rv\<rbrace>
 3. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> True \<and> (cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent s \<and> range_cover ptr sz (APIType_capBits ty us) (Suc (length as)) \<and> Suc (length as) \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) \<and> (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s \<and> range_cover ptr sz (APIType_capBits ty us) (Suc (length as)) \<and> Suc (length as) \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) \<and> (\<forall>x\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) x s \<and> range_cover ptr sz (APIType_capBits ty us) (Suc (length as)) \<and> Suc (length as) \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) \<and> (range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))) \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> ptr \<noteq> 0) \<and> (pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat (Suc (length as)) * 2 ^ APIType_capBits ty us - 1} s \<and> ksCurDomain s \<le> maxDomain) \<and> ?P'213 s proof (prove)
goal (4 subgoals):
 1. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> range_cover ptr sz (APIType_capBits ty us) ?m216
 2. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> Suc (length as) \<le> ?m216
 3. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> \<lbrace>?P'213\<rbrace> createNewCaps ty ptr (Suc (length as)) us d \<lbrace>\<lambda>rv s. valid_arch_state' s \<and> Suc (length as) = length rv\<rbrace>
 4. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> True \<and> (cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent s \<and> range_cover ptr sz (APIType_capBits ty us) (Suc (length as)) \<and> Suc (length as) \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) \<and> (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s \<and> range_cover ptr sz (APIType_capBits ty us) (Suc (length as)) \<and> Suc (length as) \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) \<and> (\<forall>x\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) x s \<and> range_cover ptr sz (APIType_capBits ty us) (Suc (length as)) \<and> Suc (length as) \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) \<and> (range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))) \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> ptr \<noteq> 0) \<and> (pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat (Suc (length as)) * 2 ^ APIType_capBits ty us - 1} s \<and> ksCurDomain s \<le> maxDomain) \<and> ?P'213 s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (APIType_capBits ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ APIType_capBits ty us - 1} s\<rbrakk> \<Longrightarrow> \<lbrace>?P'213\<rbrace> createNewCaps ty ptr (Suc (length as)) us d \<lbrace>\<lambda>rv s. valid_arch_state' s \<and> Suc (length as) = length rv\<rbrace>
 2. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> True \<and> (cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent s \<and> range_cover ptr sz (APIType_capBits ty us) (Suc (length as)) \<and> Suc (length as) \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) \<and> (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s \<and> range_cover ptr sz (APIType_capBits ty us) (Suc (length as)) \<and> Suc (length as) \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) \<and> (\<forall>x\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) x s \<and> range_cover ptr sz (APIType_capBits ty us) (Suc (length as)) \<and> Suc (length as) \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) \<and> (range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))) \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> ptr \<noteq> 0) \<and> (pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat (Suc (length as)) * 2 ^ APIType_capBits ty us - 1} s \<and> ksCurDomain s \<le> maxDomain) \<and> ?P'213 s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> True \<and> (cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent s \<and> range_cover ptr sz (APIType_capBits ty us) (Suc (length as)) \<and> Suc (length as) \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) \<and> (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s \<and> range_cover ptr sz (APIType_capBits ty us) (Suc (length as)) \<and> Suc (length as) \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) \<and> (\<forall>x\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) x s \<and> range_cover ptr sz (APIType_capBits ty us) (Suc (length as)) \<and> Suc (length as) \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) \<and> (range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))) \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> ptr \<noteq> 0) \<and> (pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat (Suc (length as)) * 2 ^ APIType_capBits ty us - 1} s \<and> ksCurDomain s \<le> maxDomain) \<and> ((\<lambda>s. valid_arch_state' s \<and> valid_pspace' s \<and> pspace_no_overlap' ptr ?sz221 s \<and> (?tp221 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us)) and K (range_cover ptr ?sz221 (APIType_capBits ty us) (Suc (length as)) \<and> Suc (length as) \<noteq> 0)) s \<and> K (Suc (length as) < 2 ^ word_bits \<and> Suc (length as) \<noteq> 0) s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s\<rbrakk> \<Longrightarrow> Suc (length as) \<le> Suc (Suc (length as))
 2. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s; range_cover ptr sz (getObjectSize ty us) (Suc (length as))\<rbrakk> \<Longrightarrow> True \<and> (cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent s \<and> range_cover ptr sz (APIType_capBits ty us) (Suc (length as)) \<and> Suc (length as) \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) \<and> (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s \<and> range_cover ptr sz (APIType_capBits ty us) (Suc (length as)) \<and> Suc (length as) \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) \<and> (\<forall>x\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) x s \<and> range_cover ptr sz (APIType_capBits ty us) (Suc (length as)) \<and> Suc (length as) \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) \<and> (range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))) \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> ptr \<noteq> 0) \<and> (pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat (Suc (length as)) * 2 ^ APIType_capBits ty us - 1} s \<and> ksCurDomain s \<le> maxDomain) \<and> ((\<lambda>s. valid_arch_state' s \<and> valid_pspace' s \<and> pspace_no_overlap' ptr ?sz221 s \<and> (?tp221 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us)) and K (range_cover ptr ?sz221 (APIType_capBits ty us) (Suc (length as)) \<and> Suc (length as) \<noteq> 0)) s \<and> K (Suc (length as) < 2 ^ word_bits \<and> Suc (length as) \<noteq> 0) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s; range_cover ptr sz (getObjectSize ty us) (Suc (length as))\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent s \<and> range_cover ptr sz (APIType_capBits ty us) (Suc (length as)) \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> range_cover ptr sz (APIType_capBits ty us) (Suc (length as)) \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> ((\<exists>x. x \<in> set as) \<longrightarrow> range_cover ptr sz (APIType_capBits ty us) (Suc (length as)) \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length as)) * 2 ^ APIType_capBits ty us - 1} s \<and> ksCurDomain s \<le> maxDomain \<and> valid_arch_state' s \<and> valid_pspace' s \<and> pspace_no_overlap' ptr ?sz221 s \<and> (?tp221 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us) \<and> range_cover ptr ?sz221 (APIType_capBits ty us) (Suc (length as)) proof (prove)
using this:
pspace_no_overlap' ptr sz s
caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s
valid_pspace' s
cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent s
caps_no_overlap'' ptr sz s
valid_arch_state' s

goal (1 subgoal):
 1. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s \<and> (\<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s); distinct as \<and> a \<notin> set as; b \<noteq> a \<and> b \<notin> set as; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (getObjectSize ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ getObjectSize ty us - 1} s; range_cover ptr sz (getObjectSize ty us) (Suc (length as))\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent s \<and> range_cover ptr sz (APIType_capBits ty us) (Suc (length as)) \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> range_cover ptr sz (APIType_capBits ty us) (Suc (length as)) \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> ((\<exists>x. x \<in> set as) \<longrightarrow> range_cover ptr sz (APIType_capBits ty us) (Suc (length as)) \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length as)) * 2 ^ APIType_capBits ty us - 1} s \<and> ksCurDomain s \<le> maxDomain \<and> valid_arch_state' s \<and> valid_pspace' s \<and> pspace_no_overlap' ptr ?sz221 s \<and> (?tp221 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us) \<and> range_cover ptr ?sz221 (APIType_capBits ty us) (Suc (length as)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Suc (Suc (length as)) < 2 ^ word_bits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) b s; range_cover ptr sz (APIType_capBits ty us) (Suc (Suc (length as))); ptr \<noteq> 0; caps_overlap_reserved' {ptr..ptr + (2 + word_of_nat (length as)) * 2 ^ APIType_capBits ty us - 1} s; range_cover ptr sz (APIType_capBits ty us) (Suc (length as)); pspace_no_overlap' ptr sz s; caps_overlap_reserved' {ptr..ptr + (1 + word_of_nat (length as)) * 2 ^ APIType_capBits ty us - 1} s; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent s; caps_no_overlap'' ptr sz s; valid_arch_state' s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) a s; \<forall>slot\<in>set as. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; distinct as; a \<notin> set as; b \<noteq> a; b \<notin> set as; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s\<rbrakk> \<Longrightarrow> ksCurDomain s \<le> maxDomain \<and> pspace_no_overlap' ptr ?sz221 s \<and> (?tp221 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us) \<and> range_cover ptr ?sz221 (APIType_capBits ty us) (Suc (length as)) proof (prove)
goal:
No subgoals! proof (state)
this:
zipWithM_x (\<lambda>num slot. global.createObject ty ((num << getObjectSize ty us) + ptr) us d >>= insertNewCap parent slot) [0 .e. word_of_nat (length (as @ [a]))] (b # as @ [a]) s = (createNewCaps ty ptr (Suc (length (as @ [a]))) us d >>= zipWithM_x (insertNewCap parent) (b # as @ [a])) s

goal:
No subgoals! proof (state)
this:
zipWithM_x (\<lambda>num slot. global.createObject ty ((num << getObjectSize ty us) + ptr) us d >>= insertNewCap parent slot) [0 .e. word_of_nat (length ys)] (y # ys) s = (createNewCaps ty ptr (Suc (length ys)) us d >>= zipWithM_x (insertNewCap parent) (y # ys)) s

goal:
No subgoals!