theory Retype_R

lemma createObjects_valid_pspace':
  assumes  mko: "makeObjectKO dev ty = Some val"
  and    not_0: "n \<noteq> 0"
  and    cover: "range_cover ptr sz (objBitsKO val + gbits) n"
  shows "\<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s
            \<and> caps_overlap_reserved' {ptr .. ptr + of_nat (n * 2^gbits * 2 ^ objBitsKO val ) - 1} s
            \<and> ptr \<noteq> 0\<rbrace>
  createObjects' ptr n val gbits \<lbrace>\<lambda>r. valid_pspace'\<rbrace>" apply (cut_tac not_0) apply (simp add: split_def createObjects'_def
                   lookupAround2_pspace_no
                   alignError_def unless_def) apply (rule hoare_pre) apply (wp|simp cong: if_cong del: data_map_insert_def del:fun_upd_apply)+ apply (wpc|wp)+ apply (subst new_cap_addrs_fold') apply (simp add:unat_1_0 unat_gt_0) apply (rule range_cover_not_zero_shift[OF _  cover]) apply simp+ apply (subst new_cap_addrs_fold') apply (simp add:unat_1_0 unat_gt_0) apply (rule range_cover_not_zero_shift[OF _  cover]) apply simp+ apply (subst data_map_insert_def[symmetric])+ apply (rule impI) apply (clarsimp simp: new_cap_addrs_fold'
                        valid_pspace'_def linorder_not_less
                        objBits_def[symmetric]) apply (simp only: imp_disjL[symmetric] imp_conjL[symmetric] imp_ex[symmetric]
                    range_cover.unat_of_nat_n_shift[OF cover,where gbits=gbits,simplified]) proof (intro conjI impI) fix s assume pn: "pspace_no_overlap' ptr sz s"
     and vo: "valid_objs' s"
     and ad: "pspace_aligned' s" "pspace_distinct' s"
     and pc: "caps_no_overlap'' ptr sz s"
    and mdb: "valid_mdb' s"
    and p_0: "ptr \<noteq> 0"
    and reserved : "caps_overlap_reserved' {ptr..ptr + of_nat n *2 ^ gbits * 2 ^ objBitsKO val - 1} s"
    and no_0_obj': "no_0_obj' s" have obj': "objBitsKO val \<le> sz" using cover by (simp add:range_cover_def) let ?s' = "s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>" note cover' = range_cover_rel[where sbit' = "objBitsKO val",OF cover _ refl,simplified] note ad' = retype_aligned_distinct'[OF ad pn cover'] note shift = range_cover.unat_of_nat_n_shift[OF cover,where gbits=gbits,simplified] have al: "is_aligned ptr (objBitsKO val)" using cover' by (simp add:range_cover_def) show pspace_aligned: "pspace_aligned' ?s'" using ad' range_cover.unat_of_nat_n_shift[OF cover,where gbits=gbits,simplified] by (simp add:field_simps) show "pspace_distinct' ?s'" using ad' shift by (simp add:field_simps) note obj_at_disj = retype_obj_at_disj' [OF ad pn cover'] note obj_at_disj' = obj_at_disj [unfolded foldr_upd_app_if[folded data_map_insert_def]] have obj_atC: "\<And>P x. x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<Longrightarrow> \<not> obj_at' P x s" apply (clarsimp simp: obj_at'_def) apply (drule subsetD [OF new_cap_addrs_subset [OF cover' ]]) apply (insert pspace_no_overlap_disjoint' [OF ad(1) pn]) apply (drule domI[where m = "ksPSpace s"]) apply (drule(1) orthD2) apply (clarsimp simp:ptr_add_def p_assoc_help) done have valid_cap: "\<And>cap q. \<lbrakk> s \<turnstile>' cap; cte_wp_at' (\<lambda>cte. cteCap cte = cap) q s \<rbrakk>
                      \<Longrightarrow> ?s' \<turnstile>' cap" apply (rule valid_untyped'_helper[OF _ _ _ pc _ ad pn ]) apply simp+ apply (subst mult.commute) apply (rule cover') using reserved apply (clarsimp simp:caps_overlap_reserved'_def cte_wp_at_ctes_of) apply (drule_tac x = cte in bspec) apply fastforce apply simp done show valid_objs: "valid_objs' ?s'" using vo apply (clarsimp simp: valid_objs'_def
                          foldr_upd_app_if[folded data_map_insert_def]
                   elim!: ranE
                   split: if_split_asm) apply (insert sym[OF mko])[1] apply (clarsimp simp: makeObjectKO_def
                    split: bool.split_asm sum.split_asm
                           ARM_H.object_type.split_asm
                           apiobject_type.split_asm
                           kernel_object.split_asm
                           arch_kernel_object.split_asm) apply (drule bspec, erule ranI) apply (subst mult.commute) apply (case_tac obj; simp add: valid_obj'_def) apply (rename_tac endpoint) apply (case_tac endpoint; simp add: valid_ep'_def obj_at_disj') apply (rename_tac notification) apply (case_tac notification; simp add: valid_ntfn'_def valid_bound_tcb'_def obj_at_disj') apply (rename_tac ntfn xa) apply (case_tac ntfn, simp_all, (clarsimp simp: obj_at_disj' split:option.splits)+) apply (rename_tac tcb) apply (case_tac tcb, clarsimp simp add: valid_tcb'_def) apply (frule pspace_alignedD' [OF _ ad(1)]) apply (frule pspace_distinctD' [OF _ ad(2)]) apply (simp add: objBits_simps) apply (subst mult.commute) apply (intro conjI ballI) apply (clarsimp elim!: ranE) apply (rule valid_cap[unfolded foldr_upd_app_if[folded data_map_insert_def]]) apply (fastforce) apply (rule_tac ptr="x + xa" in cte_wp_at_tcbI', assumption+) apply fastforce apply simp apply (rename_tac thread_state mcp priority bool option nat cptr vptr bound user_context) apply (case_tac thread_state, simp_all add: valid_tcb_state'_def
                                                  valid_bound_ntfn'_def obj_at_disj'
                                           split: option.splits)[2] apply (simp add: valid_cte'_def) apply (frule pspace_alignedD' [OF _ ad(1)]) apply (frule pspace_distinctD' [OF _ ad(2)]) apply (simp add: objBits_simps') apply (subst mult.commute) apply (erule valid_cap[unfolded foldr_upd_app_if[folded data_map_insert_def]]) apply (erule(2) cte_wp_at_cteI'[unfolded cte_level_bits_def]) apply simp apply (rename_tac arch_kernel_object) apply (case_tac arch_kernel_object; simp) apply (rename_tac asidpool) apply (case_tac asidpool, clarsimp simp: page_directory_at'_def
                                               typ_at_to_obj_at_arches
                                               obj_at_disj') apply (rename_tac pte) apply (case_tac pte; simp add: valid_mapping'_def) apply (rename_tac pde) apply (case_tac pde; simp add: valid_mapping'_def page_table_at'_def
                                   typ_at_to_obj_at_arches obj_at_disj') done have not_0: "0 \<notin> set (new_cap_addrs (2 ^ gbits * n) ptr val)" using p_0 apply clarsimp apply (drule subsetD [OF new_cap_addrs_subset [OF cover'],rotated]) apply (clarsimp simp:ptr_add_def) done show "valid_mdb' ?s'" apply (simp add: valid_mdb'_def foldr_upd_app_if[folded data_map_insert_def]) apply (subst mult.commute) apply (subst ctes_of_retype [OF mko ad]) apply (rule ad'[unfolded foldr_upd_app_if[folded data_map_insert_def]])+ apply (simp add: objBits_def[symmetric] new_cap_addrs_aligned [OF al]) apply (rule ballI, drule subsetD [OF new_cap_addrs_subset [OF cover']]) apply (insert pspace_no_overlap_disjoint' [OF ad(1) pn]) apply (drule_tac x = x in orthD1) apply (simp add:ptr_add_def p_assoc_help) apply fastforce apply (fold makeObject_cte) apply (rule retype_mdb.valid_n) apply unfold_locales apply (rule mdb[unfolded valid_mdb'_def]) apply (rule iffD2 [OF None_ctes_of_cte_at[unfolded cte_wp_at_obj_cases'], THEN sym]) apply (rule notI) apply (elim disjE conjE, simp_all add: obj_atC)[1] apply (thin_tac "S \<inter> T = {}" for S T) apply (clarsimp simp: obj_at'_def projectKOs objBits_simps) apply (drule pspace_no_overlapD' [OF _ pn]) apply (drule subsetD [OF new_cap_addrs_subset[OF cover']]) apply (frule_tac ptr'=p in mask_in_range) apply (drule(1) tcb_cte_cases_aligned_helpers) apply (drule_tac x = p in orthD1) apply (clarsimp simp:objBits_simps) apply (clarsimp simp:ptr_add_def p_assoc_help) apply (frule new_range_subset[OF cover']) apply (drule bspec [OF new_cap_addrs_aligned[OF al]]) apply (drule(1) disjoint_subset[rotated]) apply (drule_tac a=p in equals0D) apply (frule_tac ptr'=p in mask_in_range) apply (insert sym [OF mko],
             clarsimp simp: objBits_simps makeObjectKO_def obj_at'_def)[1] apply (insert sym[OF mko] cover',
            clarsimp simp: obj_at'_def objBits_simps
                           makeObjectKO_def projectKOs)[1] apply (drule(1) tcb_cte_cases_aligned_helpers(2)) apply clarsimp apply (drule subsetD [OF new_cap_addrs_subset,rotated]) apply (simp add:objBits_simps) apply (drule orthD1) apply (fastforce simp:p_assoc_help ptr_add_def) apply fastforce apply (simp add: not_0) done have data_map_ext: "\<And>x y. data_map_insert x y = (\<lambda>m. m (x \<mapsto> y))" by (rule ext) simp show no_0_obj: "no_0_obj' ?s'" using not_0 no_0_obj' by (simp add: no_0_obj'_def data_map_ext field_simps foldr_upd_app_other) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat (n * 2 ^ gbits * 2 ^ objBitsKO val) - 1} s \<and> ptr \<noteq> 0\<rbrace> createObjects' ptr n val gbits \<lbrace>\<lambda>r. valid_pspace'\<rbrace> proof (prove)
goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat (n * 2 ^ gbits * 2 ^ objBitsKO val) - 1} s \<and> ptr \<noteq> 0\<rbrace> createObjects' ptr n val gbits \<lbrace>\<lambda>r. valid_pspace'\<rbrace> proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s \<and> ptr \<noteq> 0\<rbrace> do y <- when (ptr && mask (objBitsKO val + gbits) \<noteq> 0) fail;
ps <- gets ksPSpace;
y <- case fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) ps) of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr);
modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> val)) (map (\<lambda>n. ptr + (n << objBitsKO val)) [0 .e. (word_of_nat n << gbits) - 1]) ps))
od \<lbrace>\<lambda>r. valid_pspace'\<rbrace> proof (prove)
goal (2 subgoals):
 1. 0 < n \<Longrightarrow> \<lbrace>?Q4\<rbrace> do y <- when (ptr && mask (objBitsKO val + gbits) \<noteq> 0) fail;
ps <- gets ksPSpace;
y <- case fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) ps) of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr);
modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> val)) (map (\<lambda>n. ptr + (n << objBitsKO val)) [0 .e. (word_of_nat n << gbits) - 1]) ps))
od \<lbrace>\<lambda>r. valid_pspace'\<rbrace>
 2. \<And>s. \<lbrakk>0 < n; pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s \<and> ptr \<noteq> 0\<rbrakk> \<Longrightarrow> ?Q4 s proof (prove)
goal (4 subgoals):
 1. \<And>ps. 0 < n \<Longrightarrow> \<lbrace>?B9 () ps\<rbrace> case fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) ps) of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr) \<lbrace>\<lambda>y s. valid_pspace' (s\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> val)) (map (\<lambda>n. ptr + (n << objBitsKO val)) [0 .e. (word_of_nat n << gbits) - 1]) ps\<rparr>)\<rbrace>
 2. \<And>x. 0 < n \<Longrightarrow> \<lbrace>?B8 x\<rbrace> gets ksPSpace \<lbrace>?B9 x\<rbrace>
 3. 0 < n \<Longrightarrow> \<lbrace>?Q4\<rbrace> when (ptr && mask (objBitsKO val + gbits) \<noteq> 0) fail \<lbrace>?B8\<rbrace>
 4. \<And>s. \<lbrakk>0 < n; pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s \<and> ptr \<noteq> 0\<rbrakk> \<Longrightarrow> ?Q4 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>0 < n; pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s \<and> ptr \<noteq> 0\<rbrakk> \<Longrightarrow> (if ptr && mask (objBitsKO val + gbits) \<noteq> 0 then \<lambda>_. True else (\<lambda>s. (fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<longrightarrow> valid_pspace' (s\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> val)) (map (\<lambda>n. ptr + (n << objBitsKO val)) [0 .e. (word_of_nat n << gbits) - 1]) (ksPSpace s)\<rparr>)) \<and> (\<forall>x. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some x \<longrightarrow> fst x < ptr \<longrightarrow> valid_pspace' (s\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> val)) (map (\<lambda>n. ptr + (n << objBitsKO val)) [0 .e. (word_of_nat n << gbits) - 1]) (ksPSpace s)\<rparr>)))) s proof (prove)
goal (2 subgoals):
 1. \<And>s a _ sa. \<lbrakk>0 < n; pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s \<and> ptr \<noteq> 0\<rbrakk> \<Longrightarrow> 1 \<le> word_of_nat n << gbits
 2. \<And>s. \<lbrakk>0 < n; pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s \<and> ptr \<noteq> 0\<rbrakk> \<Longrightarrow> (if ptr && mask (objBitsKO val + gbits) \<noteq> 0 then \<lambda>_. True else (\<lambda>s. (fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<longrightarrow> valid_pspace' (s\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> val)) (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val) (ksPSpace s)\<rparr>)) \<and> (\<forall>x. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some x \<longrightarrow> fst x < ptr \<longrightarrow> valid_pspace' (s\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> val)) (map (\<lambda>n. ptr + (n << objBitsKO val)) [0 .e. (word_of_nat n << gbits) - 1]) (ksPSpace s)\<rparr>)))) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>0 < n; pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s \<and> ptr \<noteq> 0\<rbrakk> \<Longrightarrow> word_of_nat n << gbits \<noteq> 0
 2. \<And>s. \<lbrakk>0 < n; pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s \<and> ptr \<noteq> 0\<rbrakk> \<Longrightarrow> (if ptr && mask (objBitsKO val + gbits) \<noteq> 0 then \<lambda>_. True else (\<lambda>s. (fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<longrightarrow> valid_pspace' (s\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> val)) (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val) (ksPSpace s)\<rparr>)) \<and> (\<forall>x. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some x \<longrightarrow> fst x < ptr \<longrightarrow> valid_pspace' (s\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> val)) (map (\<lambda>n. ptr + (n << objBitsKO val)) [0 .e. (word_of_nat n << gbits) - 1]) (ksPSpace s)\<rparr>)))) s proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>0 < n; pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s \<and> ptr \<noteq> 0\<rbrakk> \<Longrightarrow> n \<noteq> 0
 2. \<And>s. \<lbrakk>0 < n; pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s \<and> ptr \<noteq> 0\<rbrakk> \<Longrightarrow> gbits \<le> objBitsKO val + gbits
 3. \<And>s. \<lbrakk>0 < n; pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s \<and> ptr \<noteq> 0\<rbrakk> \<Longrightarrow> (if ptr && mask (objBitsKO val + gbits) \<noteq> 0 then \<lambda>_. True else (\<lambda>s. (fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<longrightarrow> valid_pspace' (s\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> val)) (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val) (ksPSpace s)\<rparr>)) \<and> (\<forall>x. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some x \<longrightarrow> fst x < ptr \<longrightarrow> valid_pspace' (s\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> val)) (map (\<lambda>n. ptr + (n << objBitsKO val)) [0 .e. (word_of_nat n << gbits) - 1]) (ksPSpace s)\<rparr>)))) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>0 < n; pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s \<and> ptr \<noteq> 0\<rbrakk> \<Longrightarrow> ptr && mask (objBitsKO val + gbits) = 0 \<longrightarrow> (fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<longrightarrow> valid_pspace' (s\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> val)) (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val) (ksPSpace s)\<rparr>)) \<and> (\<forall>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<longrightarrow> a < ptr \<longrightarrow> valid_pspace' (s\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> val)) (map (\<lambda>n. ptr + (n << objBitsKO val)) [0 .e. (word_of_nat n << gbits) - 1]) (ksPSpace s)\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<And>s _ a. \<lbrakk>0 < n; pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s \<and> ptr \<noteq> 0\<rbrakk> \<Longrightarrow> 1 \<le> word_of_nat n << gbits
 2. \<And>s. \<lbrakk>0 < n; pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s \<and> ptr \<noteq> 0\<rbrakk> \<Longrightarrow> ptr && mask (objBitsKO val + gbits) = 0 \<longrightarrow> (fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<longrightarrow> valid_pspace' (s\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> val)) (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val) (ksPSpace s)\<rparr>)) \<and> (\<forall>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<longrightarrow> a < ptr \<longrightarrow> valid_pspace' (s\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> val)) (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val) (ksPSpace s)\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>0 < n; pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s \<and> ptr \<noteq> 0\<rbrakk> \<Longrightarrow> word_of_nat n << gbits \<noteq> 0
 2. \<And>s. \<lbrakk>0 < n; pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s \<and> ptr \<noteq> 0\<rbrakk> \<Longrightarrow> ptr && mask (objBitsKO val + gbits) = 0 \<longrightarrow> (fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<longrightarrow> valid_pspace' (s\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> val)) (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val) (ksPSpace s)\<rparr>)) \<and> (\<forall>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<longrightarrow> a < ptr \<longrightarrow> valid_pspace' (s\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> val)) (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val) (ksPSpace s)\<rparr>)) proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>0 < n; pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s \<and> ptr \<noteq> 0\<rbrakk> \<Longrightarrow> n \<noteq> 0
 2. \<And>s. \<lbrakk>0 < n; pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s \<and> ptr \<noteq> 0\<rbrakk> \<Longrightarrow> gbits \<le> objBitsKO val + gbits
 3. \<And>s. \<lbrakk>0 < n; pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s \<and> ptr \<noteq> 0\<rbrakk> \<Longrightarrow> ptr && mask (objBitsKO val + gbits) = 0 \<longrightarrow> (fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<longrightarrow> valid_pspace' (s\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> val)) (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val) (ksPSpace s)\<rparr>)) \<and> (\<forall>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<longrightarrow> a < ptr \<longrightarrow> valid_pspace' (s\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> val)) (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val) (ksPSpace s)\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>0 < n; pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s \<and> ptr \<noteq> 0\<rbrakk> \<Longrightarrow> ptr && mask (objBitsKO val + gbits) = 0 \<longrightarrow> (fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<longrightarrow> valid_pspace' (s\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> val)) (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val) (ksPSpace s)\<rparr>)) \<and> (\<forall>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<longrightarrow> a < ptr \<longrightarrow> valid_pspace' (s\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> val)) (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val) (ksPSpace s)\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>0 < n; pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s \<and> ptr \<noteq> 0\<rbrakk> \<Longrightarrow> ptr && mask (objBitsKO val + gbits) = 0 \<longrightarrow> (fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<longrightarrow> valid_pspace' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val) (ksPSpace s)\<rparr>)) \<and> (\<forall>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<longrightarrow> a < ptr \<longrightarrow> valid_pspace' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val) (ksPSpace s)\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>0 < n; pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s \<and> ptr \<noteq> 0; ptr && mask (objBitsKO val + gbits) = 0\<rbrakk> \<Longrightarrow> (fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<longrightarrow> valid_pspace' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val) (ksPSpace s)\<rparr>)) \<and> (\<forall>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<longrightarrow> a < ptr \<longrightarrow> valid_pspace' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val) (ksPSpace s)\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> (fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<longrightarrow> valid_objs' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val) (ksPSpace s)\<rparr>) \<and> pspace_aligned' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val) (ksPSpace s)\<rparr>) \<and> pspace_distinct' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val) (ksPSpace s)\<rparr>) \<and> no_0_obj' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val) (ksPSpace s)\<rparr>) \<and> valid_mdb' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val) (ksPSpace s)\<rparr>)) \<and> (\<forall>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<longrightarrow> a < ptr \<longrightarrow> valid_objs' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val) (ksPSpace s)\<rparr>) \<and> pspace_aligned' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val) (ksPSpace s)\<rparr>) \<and> pspace_distinct' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val) (ksPSpace s)\<rparr>) \<and> no_0_obj' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val) (ksPSpace s)\<rparr>) \<and> valid_mdb' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val) (ksPSpace s)\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr) \<longrightarrow> valid_objs' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>) \<and> pspace_aligned' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>) \<and> pspace_distinct' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>) \<and> no_0_obj' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>) \<and> valid_mdb' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>) proof (state)
goal (5 subgoals):
 1. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> valid_objs' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>)
 2. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> pspace_aligned' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>)
 3. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> pspace_distinct' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>)
 4. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> no_0_obj' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>)
 5. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> valid_mdb' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>) proof (state)
goal (5 subgoals):
 1. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> valid_objs' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>)
 2. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> pspace_aligned' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>)
 3. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> pspace_distinct' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>)
 4. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> no_0_obj' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>)
 5. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> valid_mdb' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>) proof (state)
this:
pspace_no_overlap' ptr sz s
valid_objs' s
pspace_aligned' s
pspace_distinct' s
caps_no_overlap'' ptr sz s
valid_mdb' s
ptr \<noteq> 0
caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s
no_0_obj' s

goal (5 subgoals):
 1. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> valid_objs' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>)
 2. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> pspace_aligned' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>)
 3. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> pspace_distinct' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>)
 4. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> no_0_obj' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>)
 5. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> valid_mdb' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>) proof (prove)
goal (1 subgoal):
 1. objBitsKO val \<le> sz proof (prove)
using this:
range_cover ptr sz (objBitsKO val + gbits) n

goal (1 subgoal):
 1. objBitsKO val \<le> sz proof (state)
this:
objBitsKO val \<le> sz

goal (5 subgoals):
 1. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> valid_objs' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>)
 2. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> pspace_aligned' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>)
 3. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> pspace_distinct' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>)
 4. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> no_0_obj' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>)
 5. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> valid_mdb' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>) proof (state)
goal (5 subgoals):
 1. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> valid_objs' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>)
 2. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> pspace_aligned' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>)
 3. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> pspace_distinct' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>)
 4. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> no_0_obj' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>)
 5. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> valid_mdb' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>) proof (state)
this:
range_cover ptr sz (objBitsKO val) (2 ^ gbits * n)

goal (5 subgoals):
 1. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> valid_objs' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>)
 2. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> pspace_aligned' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>)
 3. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> pspace_distinct' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>)
 4. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> no_0_obj' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>)
 5. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> valid_mdb' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>) proof (state)
this:
pspace_distinct' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (2 ^ gbits * n) ptr val) (ksPSpace s)\<rparr>)
pspace_aligned' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (2 ^ gbits * n) ptr val) (ksPSpace s)\<rparr>)

goal (5 subgoals):
 1. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> valid_objs' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>)
 2. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> pspace_aligned' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>)
 3. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> pspace_distinct' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>)
 4. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> no_0_obj' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>)
 5. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> valid_mdb' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>) proof (state)
this:
unat (word_of_nat n << gbits) = n * 2 ^ gbits

goal (5 subgoals):
 1. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> valid_objs' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>)
 2. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> pspace_aligned' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>)
 3. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> pspace_distinct' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>)
 4. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> no_0_obj' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>)
 5. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> valid_mdb' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>) proof (prove)
goal (1 subgoal):
 1. is_aligned ptr (objBitsKO val) proof (prove)
using this:
range_cover ptr sz (objBitsKO val) (2 ^ gbits * n)

goal (1 subgoal):
 1. is_aligned ptr (objBitsKO val) proof (state)
this:
is_aligned ptr (objBitsKO val)

goal (5 subgoals):
 1. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> valid_objs' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>)
 2. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> pspace_aligned' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>)
 3. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> pspace_distinct' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>)
 4. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> no_0_obj' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>)
 5. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> valid_mdb' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>) proof (prove)
goal (1 subgoal):
 1. pspace_aligned' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>) proof (prove)
using this:
pspace_distinct' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (2 ^ gbits * n) ptr val) (ksPSpace s)\<rparr>)
pspace_aligned' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (2 ^ gbits * n) ptr val) (ksPSpace s)\<rparr>)
unat (word_of_nat n << gbits) = n * 2 ^ gbits

goal (1 subgoal):
 1. pspace_aligned' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>) proof (state)
this:
pspace_aligned' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>)

goal (4 subgoals):
 1. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> valid_objs' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>)
 2. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> pspace_distinct' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>)
 3. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> no_0_obj' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>)
 4. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> valid_mdb' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>) proof (prove)
goal (1 subgoal):
 1. pspace_distinct' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>) proof (prove)
using this:
pspace_distinct' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (2 ^ gbits * n) ptr val) (ksPSpace s)\<rparr>)
pspace_aligned' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (2 ^ gbits * n) ptr val) (ksPSpace s)\<rparr>)
unat (word_of_nat n << gbits) = n * 2 ^ gbits

goal (1 subgoal):
 1. pspace_distinct' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>) proof (state)
this:
pspace_distinct' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>)

goal (3 subgoals):
 1. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> valid_objs' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>)
 2. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> no_0_obj' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>)
 3. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> valid_mdb' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>) proof (state)
this:
obj_at' ?P ?p (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (2 ^ gbits * n) ptr val) (ksPSpace s)\<rparr>) = (obj_at' ?P ?p s \<or> ?p \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<and> (\<exists>ko. projectKO_opt val = Some ko \<and> ?P ko))

goal (3 subgoals):
 1. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> valid_objs' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>)
 2. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> no_0_obj' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>)
 3. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> valid_mdb' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>) proof (state)
this:
obj_at' ?P ?p (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>) = (obj_at' ?P ?p s \<or> ?p \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<and> (\<exists>ko. projectKO_opt val = Some ko \<and> ?P ko))

goal (3 subgoals):
 1. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> valid_objs' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>)
 2. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> no_0_obj' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>)
 3. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> valid_mdb' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>P x. x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<Longrightarrow> \<not> obj_at' P x s proof (prove)
goal (1 subgoal):
 1. \<And>P x ko obj. \<lbrakk>x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val); is_aligned x (objBitsKO ko); ksPSpace s x = Some ko; P obj; fst (projectKO ko s) = {(obj, s)}; ps_clear x (objBitsKO ko) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>P x ko obj. \<lbrakk>is_aligned x (objBitsKO ko); ksPSpace s x = Some ko; P obj; fst (projectKO ko s) = {(obj, s)}; ps_clear x (objBitsKO ko) s; x \<in> {ptr..ptr_add (ptr && ~~ mask sz) (2 ^ sz - 1)}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>P x ko obj. \<lbrakk>is_aligned x (objBitsKO ko); ksPSpace s x = Some ko; P obj; fst (projectKO ko s) = {(obj, s)}; ps_clear x (objBitsKO ko) s; x \<in> {ptr..ptr_add (ptr && ~~ mask sz) (2 ^ sz - 1)}; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>P x ko obj. \<lbrakk>is_aligned x (objBitsKO ko); P obj; fst (projectKO ko s) = {(obj, s)}; ps_clear x (objBitsKO ko) s; x \<in> {ptr..ptr_add (ptr && ~~ mask sz) (2 ^ sz - 1)}; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; x \<in> dom (ksPSpace s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>P x ko obj. \<lbrakk>is_aligned x (objBitsKO ko); P obj; fst (projectKO ko s) = {(obj, s)}; ps_clear x (objBitsKO ko) s; x \<in> {ptr..ptr_add (ptr && ~~ mask sz) (2 ^ sz - 1)}; x \<in> dom (ksPSpace s); x \<notin> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals! proof (state)
this:
?x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<Longrightarrow> \<not> obj_at' ?P ?x s

goal (3 subgoals):
 1. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> valid_objs' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>)
 2. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> no_0_obj' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>)
 3. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> valid_mdb' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>cap q. \<lbrakk>valid_cap' cap s; cte_wp_at' (\<lambda>cte. cteCap cte = cap) q s\<rbrakk> \<Longrightarrow> valid_cap' cap (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>) proof (prove)
goal (4 subgoals):
 1. \<And>cap q. \<lbrakk>valid_cap' cap s; cte_wp_at' (\<lambda>cte. cteCap cte = cap) q s\<rbrakk> \<Longrightarrow> valid_cap' cap s
 2. \<And>cap q. \<lbrakk>valid_cap' cap s; cte_wp_at' (\<lambda>cte. cteCap cte = cap) q s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>capa. cteCap capa = cap) (?q cap q) s
 3. \<And>cap q. \<lbrakk>valid_cap' cap s; cte_wp_at' (\<lambda>cte. cteCap cte = cap) q s\<rbrakk> \<Longrightarrow> range_cover ptr sz (objBitsKO val) (n * 2 ^ gbits)
 4. \<And>cap q. \<lbrakk>valid_cap' cap s; cte_wp_at' (\<lambda>cte. cteCap cte = cap) q s\<rbrakk> \<Longrightarrow> isUntypedCap cap \<longrightarrow> usableUntypedRange cap \<inter> {ptr..ptr + word_of_nat (n * 2 ^ gbits) * 2 ^ objBitsKO val - 1} = {} proof (prove)
goal (2 subgoals):
 1. \<And>cap q. \<lbrakk>valid_cap' cap s; cte_wp_at' (\<lambda>cte. cteCap cte = cap) q s\<rbrakk> \<Longrightarrow> range_cover ptr sz (objBitsKO val) (n * 2 ^ gbits)
 2. \<And>cap q. \<lbrakk>valid_cap' cap s; cte_wp_at' (\<lambda>cte. cteCap cte = cap) q s\<rbrakk> \<Longrightarrow> isUntypedCap cap \<longrightarrow> usableUntypedRange cap \<inter> {ptr..ptr + word_of_nat (n * 2 ^ gbits) * 2 ^ objBitsKO val - 1} = {} proof (prove)
goal (2 subgoals):
 1. \<And>cap q. \<lbrakk>valid_cap' cap s; cte_wp_at' (\<lambda>cte. cteCap cte = cap) q s\<rbrakk> \<Longrightarrow> range_cover ptr sz (objBitsKO val) (2 ^ gbits * n)
 2. \<And>cap q. \<lbrakk>valid_cap' cap s; cte_wp_at' (\<lambda>cte. cteCap cte = cap) q s\<rbrakk> \<Longrightarrow> isUntypedCap cap \<longrightarrow> usableUntypedRange cap \<inter> {ptr..ptr + word_of_nat (n * 2 ^ gbits) * 2 ^ objBitsKO val - 1} = {} proof (prove)
goal (1 subgoal):
 1. \<And>cap q. \<lbrakk>valid_cap' cap s; cte_wp_at' (\<lambda>cte. cteCap cte = cap) q s\<rbrakk> \<Longrightarrow> isUntypedCap cap \<longrightarrow> usableUntypedRange cap \<inter> {ptr..ptr + word_of_nat (n * 2 ^ gbits) * 2 ^ objBitsKO val - 1} = {} proof (prove)
using this:
caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s

goal (1 subgoal):
 1. \<And>cap q. \<lbrakk>valid_cap' cap s; cte_wp_at' (\<lambda>cte. cteCap cte = cap) q s\<rbrakk> \<Longrightarrow> isUntypedCap cap \<longrightarrow> usableUntypedRange cap \<inter> {ptr..ptr + word_of_nat (n * 2 ^ gbits) * 2 ^ objBitsKO val - 1} = {} proof (prove)
goal (1 subgoal):
 1. \<And>q cte. \<lbrakk>valid_cap' (cteCap cte) s; \<forall>cte\<in>ran (ctes_of s). isUntypedCap (cteCap cte) \<longrightarrow> usableUntypedRange (cteCap cte) \<inter> {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} = {}; ctes_of s q = Some cte; isUntypedCap (cteCap cte)\<rbrakk> \<Longrightarrow> usableUntypedRange (cteCap cte) \<inter> {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} = {} proof (prove)
goal (2 subgoals):
 1. \<And>q cte. \<lbrakk>valid_cap' (cteCap cte) s; ctes_of s q = Some cte; isUntypedCap (cteCap cte)\<rbrakk> \<Longrightarrow> cte \<in> ran (ctes_of s)
 2. \<And>q cte. \<lbrakk>valid_cap' (cteCap cte) s; ctes_of s q = Some cte; isUntypedCap (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> usableUntypedRange (cteCap cte) \<inter> {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} = {}\<rbrakk> \<Longrightarrow> usableUntypedRange (cteCap cte) \<inter> {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} = {} proof (prove)
goal (1 subgoal):
 1. \<And>q cte. \<lbrakk>valid_cap' (cteCap cte) s; ctes_of s q = Some cte; isUntypedCap (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> usableUntypedRange (cteCap cte) \<inter> {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} = {}\<rbrakk> \<Longrightarrow> usableUntypedRange (cteCap cte) \<inter> {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} = {} proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrakk>valid_cap' ?cap1 s; cte_wp_at' (\<lambda>cte. cteCap cte = ?cap1) ?q1 s\<rbrakk> \<Longrightarrow> valid_cap' ?cap1 (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>)

goal (3 subgoals):
 1. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> valid_objs' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>)
 2. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> no_0_obj' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>)
 3. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> valid_mdb' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>) proof (prove)
goal (1 subgoal):
 1. valid_objs' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>) proof (prove)
using this:
valid_objs' s

goal (1 subgoal):
 1. valid_objs' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>obj\<in>ran (ksPSpace s). valid_obj' obj s; x \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr val)\<rbrakk> \<Longrightarrow> valid_obj' val (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr val) then Some val else ksPSpace s x\<rparr>)
 2. \<And>obj x. \<lbrakk>\<forall>obj\<in>ran (ksPSpace s). valid_obj' obj s; x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some obj\<rbrakk> \<Longrightarrow> valid_obj' obj (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr val) then Some val else ksPSpace s x\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>obj\<in>ran (ksPSpace s). valid_obj' obj s; x \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr val); Some val = makeObjectKO dev ty\<rbrakk> \<Longrightarrow> valid_obj' val (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr val) then Some val else ksPSpace s x\<rparr>)
 2. \<And>obj x. \<lbrakk>\<forall>obj\<in>ran (ksPSpace s). valid_obj' obj s; x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some obj\<rbrakk> \<Longrightarrow> valid_obj' obj (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr val) then Some val else ksPSpace s x\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>obj x. \<lbrakk>\<forall>obj\<in>ran (ksPSpace s). valid_obj' obj s; x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some obj\<rbrakk> \<Longrightarrow> valid_obj' obj (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr val) then Some val else ksPSpace s x\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>obj x. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some obj; valid_obj' obj s\<rbrakk> \<Longrightarrow> valid_obj' obj (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr val) then Some val else ksPSpace s x\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>obj x. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some obj; valid_obj' obj s\<rbrakk> \<Longrightarrow> valid_obj' obj (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>) proof (prove)
goal (5 subgoals):
 1. \<And>obj x x1. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOEndpoint x1); valid_ep' x1 s; obj = KOEndpoint x1\<rbrakk> \<Longrightarrow> valid_ep' x1 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 2. \<And>obj x x2. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KONotification x2); valid_ntfn' x2 s; obj = KONotification x2\<rbrakk> \<Longrightarrow> valid_ntfn' x2 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 3. \<And>obj x x6. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOTCB x6); valid_tcb' x6 s; obj = KOTCB x6\<rbrakk> \<Longrightarrow> valid_tcb' x6 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 4. \<And>obj x x7. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOCTE x7); valid_cte' x7 s; obj = KOCTE x7\<rbrakk> \<Longrightarrow> valid_cte' x7 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 5. \<And>obj x x8. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOArch x8); valid_arch_obj' x8 s; obj = KOArch x8\<rbrakk> \<Longrightarrow> valid_arch_obj' x8 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>) proof (prove)
goal (5 subgoals):
 1. \<And>obj x endpoint. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOEndpoint endpoint); valid_ep' endpoint s; obj = KOEndpoint endpoint\<rbrakk> \<Longrightarrow> valid_ep' endpoint (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 2. \<And>obj x x2. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KONotification x2); valid_ntfn' x2 s; obj = KONotification x2\<rbrakk> \<Longrightarrow> valid_ntfn' x2 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 3. \<And>obj x x6. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOTCB x6); valid_tcb' x6 s; obj = KOTCB x6\<rbrakk> \<Longrightarrow> valid_tcb' x6 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 4. \<And>obj x x7. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOCTE x7); valid_cte' x7 s; obj = KOCTE x7\<rbrakk> \<Longrightarrow> valid_cte' x7 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 5. \<And>obj x x8. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOArch x8); valid_arch_obj' x8 s; obj = KOArch x8\<rbrakk> \<Longrightarrow> valid_arch_obj' x8 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>) proof (prove)
goal (4 subgoals):
 1. \<And>obj x x2. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KONotification x2); valid_ntfn' x2 s; obj = KONotification x2\<rbrakk> \<Longrightarrow> valid_ntfn' x2 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 2. \<And>obj x x6. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOTCB x6); valid_tcb' x6 s; obj = KOTCB x6\<rbrakk> \<Longrightarrow> valid_tcb' x6 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 3. \<And>obj x x7. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOCTE x7); valid_cte' x7 s; obj = KOCTE x7\<rbrakk> \<Longrightarrow> valid_cte' x7 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 4. \<And>obj x x8. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOArch x8); valid_arch_obj' x8 s; obj = KOArch x8\<rbrakk> \<Longrightarrow> valid_arch_obj' x8 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>) proof (prove)
goal (4 subgoals):
 1. \<And>obj x notification. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KONotification notification); valid_ntfn' notification s; obj = KONotification notification\<rbrakk> \<Longrightarrow> valid_ntfn' notification (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 2. \<And>obj x x6. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOTCB x6); valid_tcb' x6 s; obj = KOTCB x6\<rbrakk> \<Longrightarrow> valid_tcb' x6 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 3. \<And>obj x x7. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOCTE x7); valid_cte' x7 s; obj = KOCTE x7\<rbrakk> \<Longrightarrow> valid_cte' x7 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 4. \<And>obj x x8. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOArch x8); valid_arch_obj' x8 s; obj = KOArch x8\<rbrakk> \<Longrightarrow> valid_arch_obj' x8 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>) proof (prove)
goal (4 subgoals):
 1. \<And>obj x notification x1 x2. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KONotification (NTFN x1 x2)); (case x1 of Structures_H.ntfn.WaitingNtfn ts \<Rightarrow> ts \<noteq> [] \<and> (\<forall>t\<in>set ts. tcb_at' t s) \<and> distinct ts \<and> (case ntfnBoundTCB (NTFN x1 x2) of None \<Rightarrow> True | Some tcb \<Rightarrow> ts = [tcb]) | _ \<Rightarrow> True) \<and> (case x2 of None \<Rightarrow> True | Some t \<Rightarrow> tcb_at' t s); obj = KONotification (NTFN x1 x2); notification = NTFN x1 x2\<rbrakk> \<Longrightarrow> (case x1 of Structures_H.ntfn.WaitingNtfn ts \<Rightarrow> ts \<noteq> [] \<and> (\<forall>t\<in>set ts. tcb_at' t (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)) \<and> distinct ts \<and> (case ntfnBoundTCB (NTFN x1 x2) of None \<Rightarrow> True | Some tcb \<Rightarrow> ts = [tcb]) | _ \<Rightarrow> True) \<and> (case x2 of None \<Rightarrow> True | Some t \<Rightarrow> tcb_at' t s \<or> t \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<and> (\<exists>ko. projectKO_opt val = Some ko))
 2. \<And>obj x x6. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOTCB x6); valid_tcb' x6 s; obj = KOTCB x6\<rbrakk> \<Longrightarrow> valid_tcb' x6 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 3. \<And>obj x x7. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOCTE x7); valid_cte' x7 s; obj = KOCTE x7\<rbrakk> \<Longrightarrow> valid_cte' x7 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 4. \<And>obj x x8. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOArch x8); valid_arch_obj' x8 s; obj = KOArch x8\<rbrakk> \<Longrightarrow> valid_arch_obj' x8 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>) proof (prove)
goal (4 subgoals):
 1. \<And>obj x notification ntfn xa. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KONotification (NTFN ntfn xa)); (case ntfn of Structures_H.ntfn.WaitingNtfn ts \<Rightarrow> ts \<noteq> [] \<and> (\<forall>t\<in>set ts. tcb_at' t s) \<and> distinct ts \<and> (case ntfnBoundTCB (NTFN ntfn xa) of None \<Rightarrow> True | Some tcb \<Rightarrow> ts = [tcb]) | _ \<Rightarrow> True) \<and> (case xa of None \<Rightarrow> True | Some t \<Rightarrow> tcb_at' t s); obj = KONotification (NTFN ntfn xa); notification = NTFN ntfn xa\<rbrakk> \<Longrightarrow> (case ntfn of Structures_H.ntfn.WaitingNtfn ts \<Rightarrow> ts \<noteq> [] \<and> (\<forall>t\<in>set ts. tcb_at' t (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)) \<and> distinct ts \<and> (case ntfnBoundTCB (NTFN ntfn xa) of None \<Rightarrow> True | Some tcb \<Rightarrow> ts = [tcb]) | _ \<Rightarrow> True) \<and> (case xa of None \<Rightarrow> True | Some t \<Rightarrow> tcb_at' t s \<or> t \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<and> (\<exists>ko. projectKO_opt val = Some ko))
 2. \<And>obj x x6. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOTCB x6); valid_tcb' x6 s; obj = KOTCB x6\<rbrakk> \<Longrightarrow> valid_tcb' x6 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 3. \<And>obj x x7. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOCTE x7); valid_cte' x7 s; obj = KOCTE x7\<rbrakk> \<Longrightarrow> valid_cte' x7 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 4. \<And>obj x x8. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOArch x8); valid_arch_obj' x8 s; obj = KOArch x8\<rbrakk> \<Longrightarrow> valid_arch_obj' x8 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>x x6. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOTCB x6); valid_tcb' x6 s\<rbrakk> \<Longrightarrow> valid_tcb' x6 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 2. \<And>obj x x7. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOCTE x7); valid_cte' x7 s; obj = KOCTE x7\<rbrakk> \<Longrightarrow> valid_cte' x7 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 3. \<And>obj x x8. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOArch x8); valid_arch_obj' x8 s; obj = KOArch x8\<rbrakk> \<Longrightarrow> valid_arch_obj' x8 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>x tcb. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOTCB tcb); valid_tcb' tcb s\<rbrakk> \<Longrightarrow> valid_tcb' tcb (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 2. \<And>obj x x7. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOCTE x7); valid_cte' x7 s; obj = KOCTE x7\<rbrakk> \<Longrightarrow> valid_cte' x7 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 3. \<And>obj x x8. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOArch x8); valid_arch_obj' x8 s; obj = KOArch x8\<rbrakk> \<Longrightarrow> valid_arch_obj' x8 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>x x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOTCB (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16)); \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> valid_cap' (cteCap (getF (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16))) s; valid_tcb_state' x7 s; is_aligned x14 msg_align_bits; valid_bound_ntfn' x15 s; x6 \<le> maxDomain; x9 \<le> maxPriority; x8 \<le> maxPriority\<rbrakk> \<Longrightarrow> (\<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> valid_cap' (cteCap (getF (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16))) (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)) \<and> valid_tcb_state' x7 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>) \<and> valid_bound_ntfn' x15 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 2. \<And>obj x x7. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOCTE x7); valid_cte' x7 s; obj = KOCTE x7\<rbrakk> \<Longrightarrow> valid_cte' x7 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 3. \<And>obj x x8. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOArch x8); valid_arch_obj' x8 s; obj = KOArch x8\<rbrakk> \<Longrightarrow> valid_arch_obj' x8 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>x x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOTCB (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16)); \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> valid_cap' (cteCap (getF (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16))) s; valid_tcb_state' x7 s; is_aligned x14 msg_align_bits; valid_bound_ntfn' x15 s; x6 \<le> maxDomain; x9 \<le> maxPriority; x8 \<le> maxPriority; is_aligned x (objBitsKO (KOTCB (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16)))\<rbrakk> \<Longrightarrow> (\<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> valid_cap' (cteCap (getF (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16))) (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)) \<and> valid_tcb_state' x7 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>) \<and> valid_bound_ntfn' x15 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 2. \<And>obj x x7. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOCTE x7); valid_cte' x7 s; obj = KOCTE x7\<rbrakk> \<Longrightarrow> valid_cte' x7 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 3. \<And>obj x x8. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOArch x8); valid_arch_obj' x8 s; obj = KOArch x8\<rbrakk> \<Longrightarrow> valid_arch_obj' x8 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>x x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOTCB (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16)); \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> valid_cap' (cteCap (getF (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16))) s; valid_tcb_state' x7 s; is_aligned x14 msg_align_bits; valid_bound_ntfn' x15 s; x6 \<le> maxDomain; x9 \<le> maxPriority; x8 \<le> maxPriority; is_aligned x (objBitsKO (KOTCB (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16))); ps_clear x (objBitsKO (KOTCB (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16))) s\<rbrakk> \<Longrightarrow> (\<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> valid_cap' (cteCap (getF (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16))) (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)) \<and> valid_tcb_state' x7 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>) \<and> valid_bound_ntfn' x15 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 2. \<And>obj x x7. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOCTE x7); valid_cte' x7 s; obj = KOCTE x7\<rbrakk> \<Longrightarrow> valid_cte' x7 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 3. \<And>obj x x8. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOArch x8); valid_arch_obj' x8 s; obj = KOArch x8\<rbrakk> \<Longrightarrow> valid_arch_obj' x8 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>x x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOTCB (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16)); \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> valid_cap' (cteCap (getF (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16))) s; valid_tcb_state' x7 s; is_aligned x14 msg_align_bits; valid_bound_ntfn' x15 s; x6 \<le> maxDomain; x9 \<le> maxPriority; x8 \<le> maxPriority; is_aligned x tcbBlockSizeBits; ps_clear x tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> (\<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> valid_cap' (cteCap (getF (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16))) (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)) \<and> valid_tcb_state' x7 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>) \<and> valid_bound_ntfn' x15 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 2. \<And>obj x x7. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOCTE x7); valid_cte' x7 s; obj = KOCTE x7\<rbrakk> \<Longrightarrow> valid_cte' x7 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 3. \<And>obj x x8. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOArch x8); valid_arch_obj' x8 s; obj = KOArch x8\<rbrakk> \<Longrightarrow> valid_arch_obj' x8 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>x x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOTCB (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16)); \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> valid_cap' (cteCap (getF (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16))) s; valid_tcb_state' x7 s; is_aligned x14 msg_align_bits; valid_bound_ntfn' x15 s; x6 \<le> maxDomain; x9 \<le> maxPriority; x8 \<le> maxPriority; is_aligned x tcbBlockSizeBits; ps_clear x tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> (\<forall>(getF, setF)\<in>ran tcb_cte_cases. valid_cap' (cteCap (getF (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16))) (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr val) then Some val else ksPSpace s x\<rparr>)) \<and> valid_tcb_state' x7 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>) \<and> valid_bound_ntfn' x15 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 2. \<And>obj x x7. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOCTE x7); valid_cte' x7 s; obj = KOCTE x7\<rbrakk> \<Longrightarrow> valid_cte' x7 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 3. \<And>obj x x8. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOArch x8); valid_arch_obj' x8 s; obj = KOArch x8\<rbrakk> \<Longrightarrow> valid_arch_obj' x8 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>) proof (prove)
goal (5 subgoals):
 1. \<And>x x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 xa. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOTCB (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16)); \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> valid_cap' (cteCap (getF (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16))) s; valid_tcb_state' x7 s; is_aligned x14 msg_align_bits; valid_bound_ntfn' x15 s; x6 \<le> maxDomain; x9 \<le> maxPriority; x8 \<le> maxPriority; is_aligned x tcbBlockSizeBits; ps_clear x tcbBlockSizeBits s; xa \<in> ran tcb_cte_cases\<rbrakk> \<Longrightarrow> case xa of (getF, setF) \<Rightarrow> valid_cap' (cteCap (getF (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16))) (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr val) then Some val else ksPSpace s x\<rparr>)
 2. \<And>x x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOTCB (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16)); \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> valid_cap' (cteCap (getF (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16))) s; valid_tcb_state' x7 s; is_aligned x14 msg_align_bits; valid_bound_ntfn' x15 s; x6 \<le> maxDomain; x9 \<le> maxPriority; x8 \<le> maxPriority; is_aligned x tcbBlockSizeBits; ps_clear x tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> valid_tcb_state' x7 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 3. \<And>x x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOTCB (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16)); \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> valid_cap' (cteCap (getF (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16))) s; valid_tcb_state' x7 s; is_aligned x14 msg_align_bits; valid_bound_ntfn' x15 s; x6 \<le> maxDomain; x9 \<le> maxPriority; x8 \<le> maxPriority; is_aligned x tcbBlockSizeBits; ps_clear x tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> valid_bound_ntfn' x15 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 4. \<And>obj x x7. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOCTE x7); valid_cte' x7 s; obj = KOCTE x7\<rbrakk> \<Longrightarrow> valid_cte' x7 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 5. \<And>obj x x8. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOArch x8); valid_arch_obj' x8 s; obj = KOArch x8\<rbrakk> \<Longrightarrow> valid_arch_obj' x8 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>) proof (prove)
goal (5 subgoals):
 1. \<And>x x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 a b xa. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOTCB (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16)); \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> valid_cap' (cteCap (getF (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16))) s; valid_tcb_state' x7 s; is_aligned x14 msg_align_bits; valid_bound_ntfn' x15 s; x6 \<le> maxDomain; x9 \<le> maxPriority; x8 \<le> maxPriority; is_aligned x tcbBlockSizeBits; ps_clear x tcbBlockSizeBits s; tcb_cte_cases xa = Some (a, b)\<rbrakk> \<Longrightarrow> valid_cap' (cteCap (a (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16))) (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr val) then Some val else ksPSpace s x\<rparr>)
 2. \<And>x x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOTCB (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16)); \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> valid_cap' (cteCap (getF (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16))) s; valid_tcb_state' x7 s; is_aligned x14 msg_align_bits; valid_bound_ntfn' x15 s; x6 \<le> maxDomain; x9 \<le> maxPriority; x8 \<le> maxPriority; is_aligned x tcbBlockSizeBits; ps_clear x tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> valid_tcb_state' x7 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 3. \<And>x x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOTCB (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16)); \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> valid_cap' (cteCap (getF (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16))) s; valid_tcb_state' x7 s; is_aligned x14 msg_align_bits; valid_bound_ntfn' x15 s; x6 \<le> maxDomain; x9 \<le> maxPriority; x8 \<le> maxPriority; is_aligned x tcbBlockSizeBits; ps_clear x tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> valid_bound_ntfn' x15 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 4. \<And>obj x x7. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOCTE x7); valid_cte' x7 s; obj = KOCTE x7\<rbrakk> \<Longrightarrow> valid_cte' x7 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 5. \<And>obj x x8. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOArch x8); valid_arch_obj' x8 s; obj = KOArch x8\<rbrakk> \<Longrightarrow> valid_arch_obj' x8 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>) proof (prove)
goal (6 subgoals):
 1. \<And>x x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 a b xa. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOTCB (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16)); \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> valid_cap' (cteCap (getF (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16))) s; valid_tcb_state' x7 s; is_aligned x14 msg_align_bits; valid_bound_ntfn' x15 s; x6 \<le> maxDomain; x9 \<le> maxPriority; x8 \<le> maxPriority; is_aligned x tcbBlockSizeBits; ps_clear x tcbBlockSizeBits s; tcb_cte_cases xa = Some (a, b)\<rbrakk> \<Longrightarrow> valid_cap' (cteCap (a (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16))) s
 2. \<And>x x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 a b xa. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOTCB (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16)); \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> valid_cap' (cteCap (getF (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16))) s; valid_tcb_state' x7 s; is_aligned x14 msg_align_bits; valid_bound_ntfn' x15 s; x6 \<le> maxDomain; x9 \<le> maxPriority; x8 \<le> maxPriority; is_aligned x tcbBlockSizeBits; ps_clear x tcbBlockSizeBits s; tcb_cte_cases xa = Some (a, b)\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = cteCap (a (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16))) (?q264 x x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 a b xa) s
 3. \<And>x x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOTCB (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16)); \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> valid_cap' (cteCap (getF (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16))) s; valid_tcb_state' x7 s; is_aligned x14 msg_align_bits; valid_bound_ntfn' x15 s; x6 \<le> maxDomain; x9 \<le> maxPriority; x8 \<le> maxPriority; is_aligned x tcbBlockSizeBits; ps_clear x tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> valid_tcb_state' x7 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 4. \<And>x x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOTCB (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16)); \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> valid_cap' (cteCap (getF (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16))) s; valid_tcb_state' x7 s; is_aligned x14 msg_align_bits; valid_bound_ntfn' x15 s; x6 \<le> maxDomain; x9 \<le> maxPriority; x8 \<le> maxPriority; is_aligned x tcbBlockSizeBits; ps_clear x tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> valid_bound_ntfn' x15 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 5. \<And>obj x x7. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOCTE x7); valid_cte' x7 s; obj = KOCTE x7\<rbrakk> \<Longrightarrow> valid_cte' x7 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 6. \<And>obj x x8. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOArch x8); valid_arch_obj' x8 s; obj = KOArch x8\<rbrakk> \<Longrightarrow> valid_arch_obj' x8 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>) proof (prove)
goal (5 subgoals):
 1. \<And>x x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 a b xa. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOTCB (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16)); \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> valid_cap' (cteCap (getF (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16))) s; valid_tcb_state' x7 s; is_aligned x14 msg_align_bits; valid_bound_ntfn' x15 s; x6 \<le> maxDomain; x9 \<le> maxPriority; x8 \<le> maxPriority; is_aligned x tcbBlockSizeBits; ps_clear x tcbBlockSizeBits s; tcb_cte_cases xa = Some (a, b)\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = cteCap (a (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16))) (?q264 x x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 a b xa) s
 2. \<And>x x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOTCB (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16)); \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> valid_cap' (cteCap (getF (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16))) s; valid_tcb_state' x7 s; is_aligned x14 msg_align_bits; valid_bound_ntfn' x15 s; x6 \<le> maxDomain; x9 \<le> maxPriority; x8 \<le> maxPriority; is_aligned x tcbBlockSizeBits; ps_clear x tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> valid_tcb_state' x7 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 3. \<And>x x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOTCB (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16)); \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> valid_cap' (cteCap (getF (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16))) s; valid_tcb_state' x7 s; is_aligned x14 msg_align_bits; valid_bound_ntfn' x15 s; x6 \<le> maxDomain; x9 \<le> maxPriority; x8 \<le> maxPriority; is_aligned x tcbBlockSizeBits; ps_clear x tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> valid_bound_ntfn' x15 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 4. \<And>obj x x7. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOCTE x7); valid_cte' x7 s; obj = KOCTE x7\<rbrakk> \<Longrightarrow> valid_cte' x7 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 5. \<And>obj x x8. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOArch x8); valid_arch_obj' x8 s; obj = KOArch x8\<rbrakk> \<Longrightarrow> valid_arch_obj' x8 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>) proof (prove)
goal (6 subgoals):
 1. \<And>x x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 a b xa. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOTCB (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16)); \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> valid_cap' (cteCap (getF (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16))) s; valid_tcb_state' x7 s; is_aligned x14 msg_align_bits; valid_bound_ntfn' x15 s; x6 \<le> maxDomain; x9 \<le> maxPriority; x8 \<le> maxPriority; is_aligned x tcbBlockSizeBits; ps_clear x tcbBlockSizeBits s; tcb_cte_cases xa = Some (a, b)\<rbrakk> \<Longrightarrow> tcb_cte_cases (x + xa - x) = Some (?getF328 x x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 a b xa, ?setF328 x x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 a b xa)
 2. \<And>x x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 a b xa. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOTCB (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16)); \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> valid_cap' (cteCap (getF (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16))) s; valid_tcb_state' x7 s; is_aligned x14 msg_align_bits; valid_bound_ntfn' x15 s; x6 \<le> maxDomain; x9 \<le> maxPriority; x8 \<le> maxPriority; is_aligned x tcbBlockSizeBits; ps_clear x tcbBlockSizeBits s; tcb_cte_cases xa = Some (a, b)\<rbrakk> \<Longrightarrow> cteCap (?getF328 x x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 a b xa (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16)) = cteCap (a (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16))
 3. \<And>x x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOTCB (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16)); \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> valid_cap' (cteCap (getF (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16))) s; valid_tcb_state' x7 s; is_aligned x14 msg_align_bits; valid_bound_ntfn' x15 s; x6 \<le> maxDomain; x9 \<le> maxPriority; x8 \<le> maxPriority; is_aligned x tcbBlockSizeBits; ps_clear x tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> valid_tcb_state' x7 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 4. \<And>x x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOTCB (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16)); \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> valid_cap' (cteCap (getF (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16))) s; valid_tcb_state' x7 s; is_aligned x14 msg_align_bits; valid_bound_ntfn' x15 s; x6 \<le> maxDomain; x9 \<le> maxPriority; x8 \<le> maxPriority; is_aligned x tcbBlockSizeBits; ps_clear x tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> valid_bound_ntfn' x15 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 5. \<And>obj x x7. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOCTE x7); valid_cte' x7 s; obj = KOCTE x7\<rbrakk> \<Longrightarrow> valid_cte' x7 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 6. \<And>obj x x8. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOArch x8); valid_arch_obj' x8 s; obj = KOArch x8\<rbrakk> \<Longrightarrow> valid_arch_obj' x8 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>) proof (prove)
goal (5 subgoals):
 1. \<And>x x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 a b xa. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOTCB (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16)); \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> valid_cap' (cteCap (getF (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16))) s; valid_tcb_state' x7 s; is_aligned x14 msg_align_bits; valid_bound_ntfn' x15 s; x6 \<le> maxDomain; x9 \<le> maxPriority; x8 \<le> maxPriority; is_aligned x tcbBlockSizeBits; ps_clear x tcbBlockSizeBits s; tcb_cte_cases xa = Some (a, b)\<rbrakk> \<Longrightarrow> cteCap (a (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16)) = cteCap (a (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16))
 2. \<And>x x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOTCB (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16)); \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> valid_cap' (cteCap (getF (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16))) s; valid_tcb_state' x7 s; is_aligned x14 msg_align_bits; valid_bound_ntfn' x15 s; x6 \<le> maxDomain; x9 \<le> maxPriority; x8 \<le> maxPriority; is_aligned x tcbBlockSizeBits; ps_clear x tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> valid_tcb_state' x7 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 3. \<And>x x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOTCB (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16)); \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> valid_cap' (cteCap (getF (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16))) s; valid_tcb_state' x7 s; is_aligned x14 msg_align_bits; valid_bound_ntfn' x15 s; x6 \<le> maxDomain; x9 \<le> maxPriority; x8 \<le> maxPriority; is_aligned x tcbBlockSizeBits; ps_clear x tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> valid_bound_ntfn' x15 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 4. \<And>obj x x7. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOCTE x7); valid_cte' x7 s; obj = KOCTE x7\<rbrakk> \<Longrightarrow> valid_cte' x7 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 5. \<And>obj x x8. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOArch x8); valid_arch_obj' x8 s; obj = KOArch x8\<rbrakk> \<Longrightarrow> valid_arch_obj' x8 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>) proof (prove)
goal (4 subgoals):
 1. \<And>x x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOTCB (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16)); \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> valid_cap' (cteCap (getF (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16))) s; valid_tcb_state' x7 s; is_aligned x14 msg_align_bits; valid_bound_ntfn' x15 s; x6 \<le> maxDomain; x9 \<le> maxPriority; x8 \<le> maxPriority; is_aligned x tcbBlockSizeBits; ps_clear x tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> valid_tcb_state' x7 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 2. \<And>x x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOTCB (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16)); \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> valid_cap' (cteCap (getF (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16))) s; valid_tcb_state' x7 s; is_aligned x14 msg_align_bits; valid_bound_ntfn' x15 s; x6 \<le> maxDomain; x9 \<le> maxPriority; x8 \<le> maxPriority; is_aligned x tcbBlockSizeBits; ps_clear x tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> valid_bound_ntfn' x15 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 3. \<And>obj x x7. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOCTE x7); valid_cte' x7 s; obj = KOCTE x7\<rbrakk> \<Longrightarrow> valid_cte' x7 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 4. \<And>obj x x8. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOArch x8); valid_arch_obj' x8 s; obj = KOArch x8\<rbrakk> \<Longrightarrow> valid_arch_obj' x8 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>) proof (prove)
goal (4 subgoals):
 1. \<And>x x1 x2 x3 x4 x5 x6 thread_state mcp priority bool option nat cptr vptr bound user_context. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOTCB (Thread x1 x2 x3 x4 x5 x6 thread_state mcp priority bool option nat cptr vptr bound user_context)); \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> valid_cap' (cteCap (getF (Thread x1 x2 x3 x4 x5 x6 thread_state mcp priority bool option nat cptr vptr bound user_context))) s; valid_tcb_state' thread_state s; is_aligned vptr msg_align_bits; valid_bound_ntfn' bound s; x6 \<le> maxDomain; priority \<le> maxPriority; mcp \<le> maxPriority; is_aligned x tcbBlockSizeBits; ps_clear x tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> valid_tcb_state' thread_state (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 2. \<And>x x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOTCB (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16)); \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> valid_cap' (cteCap (getF (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16))) s; valid_tcb_state' x7 s; is_aligned x14 msg_align_bits; valid_bound_ntfn' x15 s; x6 \<le> maxDomain; x9 \<le> maxPriority; x8 \<le> maxPriority; is_aligned x tcbBlockSizeBits; ps_clear x tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> valid_bound_ntfn' x15 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 3. \<And>obj x x7. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOCTE x7); valid_cte' x7 s; obj = KOCTE x7\<rbrakk> \<Longrightarrow> valid_cte' x7 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 4. \<And>obj x x8. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOArch x8); valid_arch_obj' x8 s; obj = KOArch x8\<rbrakk> \<Longrightarrow> valid_arch_obj' x8 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>obj x x7. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOCTE x7); valid_cte' x7 s; obj = KOCTE x7\<rbrakk> \<Longrightarrow> valid_cte' x7 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 2. \<And>obj x x8. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOArch x8); valid_arch_obj' x8 s; obj = KOArch x8\<rbrakk> \<Longrightarrow> valid_arch_obj' x8 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>obj x x7. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOCTE x7); valid_cap' (cteCap x7) s; obj = KOCTE x7\<rbrakk> \<Longrightarrow> valid_cap' (cteCap x7) (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 2. \<And>obj x x8. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOArch x8); valid_arch_obj' x8 s; obj = KOArch x8\<rbrakk> \<Longrightarrow> valid_arch_obj' x8 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>obj x x7. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOCTE x7); valid_cap' (cteCap x7) s; obj = KOCTE x7; is_aligned x (objBitsKO (KOCTE x7))\<rbrakk> \<Longrightarrow> valid_cap' (cteCap x7) (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 2. \<And>obj x x8. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOArch x8); valid_arch_obj' x8 s; obj = KOArch x8\<rbrakk> \<Longrightarrow> valid_arch_obj' x8 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>obj x x7. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOCTE x7); valid_cap' (cteCap x7) s; obj = KOCTE x7; is_aligned x (objBitsKO (KOCTE x7)); ps_clear x (objBitsKO (KOCTE x7)) s\<rbrakk> \<Longrightarrow> valid_cap' (cteCap x7) (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 2. \<And>obj x x8. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOArch x8); valid_arch_obj' x8 s; obj = KOArch x8\<rbrakk> \<Longrightarrow> valid_arch_obj' x8 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>obj x x7. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOCTE x7); valid_cap' (cteCap x7) s; obj = KOCTE x7; is_aligned x 4; ps_clear x 4 s\<rbrakk> \<Longrightarrow> valid_cap' (cteCap x7) (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 2. \<And>obj x x8. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOArch x8); valid_arch_obj' x8 s; obj = KOArch x8\<rbrakk> \<Longrightarrow> valid_arch_obj' x8 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>obj x x7. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOCTE x7); valid_cap' (cteCap x7) s; obj = KOCTE x7; is_aligned x 4; ps_clear x 4 s\<rbrakk> \<Longrightarrow> valid_cap' (cteCap x7) (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr val) then Some val else ksPSpace s x\<rparr>)
 2. \<And>obj x x8. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOArch x8); valid_arch_obj' x8 s; obj = KOArch x8\<rbrakk> \<Longrightarrow> valid_arch_obj' x8 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>obj x x7. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOCTE x7); obj = KOCTE x7; is_aligned x 4; ps_clear x 4 s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = cteCap x7) (?q345 obj x x7) s
 2. \<And>obj x x8. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOArch x8); valid_arch_obj' x8 s; obj = KOArch x8\<rbrakk> \<Longrightarrow> valid_arch_obj' x8 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>obj x x7. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); obj = KOCTE x7; is_aligned x 4; ps_clear x 4 s\<rbrakk> \<Longrightarrow> cteCap x7 = cteCap x7
 2. \<And>obj x x8. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOArch x8); valid_arch_obj' x8 s; obj = KOArch x8\<rbrakk> \<Longrightarrow> valid_arch_obj' x8 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>obj x x8. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOArch x8); valid_arch_obj' x8 s; obj = KOArch x8\<rbrakk> \<Longrightarrow> valid_arch_obj' x8 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>obj x arch_kernel_object. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOArch arch_kernel_object); valid_arch_obj' arch_kernel_object s; obj = KOArch arch_kernel_object\<rbrakk> \<Longrightarrow> valid_arch_obj' arch_kernel_object (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>obj x arch_kernel_object x1. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOArch (KOASIDPool x1)); valid_asid_pool' x1 s; obj = KOArch (KOASIDPool x1); arch_kernel_object = KOASIDPool x1\<rbrakk> \<Longrightarrow> valid_asid_pool' x1 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 2. \<And>obj x arch_kernel_object x2. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOArch (KOPTE x2)); valid_pte' x2 s; obj = KOArch (KOPTE x2); arch_kernel_object = KOPTE x2\<rbrakk> \<Longrightarrow> valid_pte' x2 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 3. \<And>obj x arch_kernel_object x3. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOArch (KOPDE x3)); valid_pde' x3 s; obj = KOArch (KOPDE x3); arch_kernel_object = KOPDE x3\<rbrakk> \<Longrightarrow> valid_pde' x3 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>obj x arch_kernel_object asidpool. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOArch (KOASIDPool asidpool)); valid_asid_pool' asidpool s; obj = KOArch (KOASIDPool asidpool); arch_kernel_object = KOASIDPool asidpool\<rbrakk> \<Longrightarrow> valid_asid_pool' asidpool (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 2. \<And>obj x arch_kernel_object x2. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOArch (KOPTE x2)); valid_pte' x2 s; obj = KOArch (KOPTE x2); arch_kernel_object = KOPTE x2\<rbrakk> \<Longrightarrow> valid_pte' x2 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 3. \<And>obj x arch_kernel_object x3. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOArch (KOPDE x3)); valid_pde' x3 s; obj = KOArch (KOPDE x3); arch_kernel_object = KOPDE x3\<rbrakk> \<Longrightarrow> valid_pde' x3 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>obj x arch_kernel_object x2. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOArch (KOPTE x2)); valid_pte' x2 s; obj = KOArch (KOPTE x2); arch_kernel_object = KOPTE x2\<rbrakk> \<Longrightarrow> valid_pte' x2 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 2. \<And>obj x arch_kernel_object x3. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOArch (KOPDE x3)); valid_pde' x3 s; obj = KOArch (KOPDE x3); arch_kernel_object = KOPDE x3\<rbrakk> \<Longrightarrow> valid_pde' x3 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>obj x arch_kernel_object pte. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOArch (KOPTE pte)); valid_pte' pte s; obj = KOArch (KOPTE pte); arch_kernel_object = KOPTE pte\<rbrakk> \<Longrightarrow> valid_pte' pte (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>)
 2. \<And>obj x arch_kernel_object x3. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOArch (KOPDE x3)); valid_pde' x3 s; obj = KOArch (KOPDE x3); arch_kernel_object = KOPDE x3\<rbrakk> \<Longrightarrow> valid_pde' x3 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>obj x arch_kernel_object x3. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOArch (KOPDE x3)); valid_pde' x3 s; obj = KOArch (KOPDE x3); arch_kernel_object = KOPDE x3\<rbrakk> \<Longrightarrow> valid_pde' x3 (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>obj x arch_kernel_object pde. \<lbrakk>x \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr val); ksPSpace s x = Some (KOArch (KOPDE pde)); valid_pde' pde s; obj = KOArch (KOPDE pde); arch_kernel_object = KOPDE pde\<rbrakk> \<Longrightarrow> valid_pde' pde (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x\<rparr>) proof (prove)
goal:
No subgoals! proof (state)
this:
valid_objs' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>)

goal (2 subgoals):
 1. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> no_0_obj' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>)
 2. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> valid_mdb' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>) proof (prove)
goal (1 subgoal):
 1. 0 \<notin> set (new_cap_addrs (2 ^ gbits * n) ptr val) proof (prove)
using this:
ptr \<noteq> 0

goal (1 subgoal):
 1. 0 \<notin> set (new_cap_addrs (2 ^ gbits * n) ptr val) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptr \<noteq> 0; 0 \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptr \<noteq> 0; 0 \<in> {ptr..ptr_add (ptr && ~~ mask sz) (2 ^ sz - 1)}\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals! proof (state)
this:
0 \<notin> set (new_cap_addrs (2 ^ gbits * n) ptr val)

goal (2 subgoals):
 1. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> no_0_obj' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>)
 2. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> valid_mdb' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>) proof (prove)
goal (1 subgoal):
 1. valid_mdb' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>) proof (prove)
goal (1 subgoal):
 1. valid_mdb_ctes (map_to_ctes (\<lambda>x. if x \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr val) then Some val else ksPSpace s x)) proof (prove)
goal (1 subgoal):
 1. valid_mdb_ctes (map_to_ctes (\<lambda>x. if x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s x)) proof (prove)
goal (5 subgoals):
 1. pspace_aligned' (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s xa\<rparr>)
 2. pspace_distinct' (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) then Some val else ksPSpace s xa\<rparr>)
 3. \<forall>x\<in>set (new_cap_addrs (2 ^ gbits * n) ptr val). is_aligned x (objBitsKO val)
 4. \<forall>x\<in>set (new_cap_addrs (2 ^ gbits * n) ptr val). ksPSpace s x = None
 5. valid_mdb_ctes (\<lambda>x. if ty = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<or> ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> x && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<and> x && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then Some (CTE capability.NullCap nullMDBNode) else ctes_of s x) proof (prove)
goal (3 subgoals):
 1. \<forall>x\<in>set (new_cap_addrs (2 ^ gbits * n) ptr val). is_aligned x (objBitsKO val)
 2. \<forall>x\<in>set (new_cap_addrs (2 ^ gbits * n) ptr val). ksPSpace s x = None
 3. valid_mdb_ctes (\<lambda>x. if ty = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<or> ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> x && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<and> x && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then Some (CTE capability.NullCap nullMDBNode) else ctes_of s x) proof (prove)
goal (2 subgoals):
 1. \<forall>x\<in>set (new_cap_addrs (2 ^ gbits * n) ptr val). ksPSpace s x = None
 2. valid_mdb_ctes (\<lambda>x. if ty = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<or> ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> x && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<and> x && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then Some (CTE capability.NullCap nullMDBNode) else ctes_of s x) proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> {ptr..ptr_add (ptr && ~~ mask sz) (2 ^ sz - 1)} \<Longrightarrow> ksPSpace s x = None
 2. valid_mdb_ctes (\<lambda>x. if ty = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<or> ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> x && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<and> x && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then Some (CTE capability.NullCap nullMDBNode) else ctes_of s x) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>x \<in> {ptr..ptr_add (ptr && ~~ mask sz) (2 ^ sz - 1)}; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}\<rbrakk> \<Longrightarrow> ksPSpace s x = None
 2. {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {} \<Longrightarrow> valid_mdb_ctes (\<lambda>x. if ty = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<or> ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> x && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<and> x && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then Some (CTE capability.NullCap nullMDBNode) else ctes_of s x) proof (prove)
goal (3 subgoals):
 1. \<And>x. x \<in> {ptr..ptr_add (ptr && ~~ mask sz) (2 ^ sz - 1)} \<Longrightarrow> x \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}
 2. \<And>x. \<lbrakk>x \<in> {ptr..ptr_add (ptr && ~~ mask sz) (2 ^ sz - 1)}; x \<notin> dom (ksPSpace s)\<rbrakk> \<Longrightarrow> ksPSpace s x = None
 3. {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {} \<Longrightarrow> valid_mdb_ctes (\<lambda>x. if ty = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<or> ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> x && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<and> x && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then Some (CTE capability.NullCap nullMDBNode) else ctes_of s x) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>x \<in> {ptr..ptr_add (ptr && ~~ mask sz) (2 ^ sz - 1)}; x \<notin> dom (ksPSpace s)\<rbrakk> \<Longrightarrow> ksPSpace s x = None
 2. {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {} \<Longrightarrow> valid_mdb_ctes (\<lambda>x. if ty = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<or> ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> x && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<and> x && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then Some (CTE capability.NullCap nullMDBNode) else ctes_of s x) proof (prove)
goal (1 subgoal):
 1. {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {} \<Longrightarrow> valid_mdb_ctes (\<lambda>x. if ty = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<or> ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> x && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<and> x && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then Some (CTE capability.NullCap nullMDBNode) else ctes_of s x) proof (prove)
goal (1 subgoal):
 1. {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {} \<Longrightarrow> valid_mdb_ctes (\<lambda>x. if ty = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<or> ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> x && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<and> x && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then Some makeObject else ctes_of s x) proof (prove)
goal (1 subgoal):
 1. {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {} \<Longrightarrow> retype_mdb (ctes_of s) (\<lambda>p. ty = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> p \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<or> ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> p && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases) proof (prove)
goal (3 subgoals):
 1. {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {} \<Longrightarrow> valid_mdb_ctes (ctes_of s)
 2. \<And>p. \<lbrakk>{ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ty = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> p \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<or> ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> p && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases\<rbrakk> \<Longrightarrow> ctes_of s p = None
 3. {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {} \<Longrightarrow> \<not> (ty = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> 0 \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<or> ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> 0 && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<and> 0 && mask tcbBlockSizeBits \<in> dom tcb_cte_cases) proof (prove)
goal (2 subgoals):
 1. \<And>p. \<lbrakk>{ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ty = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> p \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<or> ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> p && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases\<rbrakk> \<Longrightarrow> ctes_of s p = None
 2. {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {} \<Longrightarrow> \<not> (ty = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> 0 \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<or> ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> 0 && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<and> 0 && mask tcbBlockSizeBits \<in> dom tcb_cte_cases) proof (prove)
goal (2 subgoals):
 1. \<And>p. \<lbrakk>{ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ty = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> p \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<or> ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> p && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases\<rbrakk> \<Longrightarrow> \<not> (real_cte_at' p s \<or> (\<exists>n\<in>dom tcb_cte_cases. obj_at' ((\<lambda>_. True) \<circ> fst (the (tcb_cte_cases n))) (p - n) s))
 2. {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {} \<Longrightarrow> \<not> (ty = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> 0 \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<or> ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> 0 && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<and> 0 && mask tcbBlockSizeBits \<in> dom tcb_cte_cases) proof (prove)
goal (2 subgoals):
 1. \<And>p. \<lbrakk>{ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ty = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> p \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<or> ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> p && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases; real_cte_at' p s \<or> (\<exists>n\<in>dom tcb_cte_cases. obj_at' ((\<lambda>_. True) \<circ> fst (the (tcb_cte_cases n))) (p - n) s)\<rbrakk> \<Longrightarrow> False
 2. {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {} \<Longrightarrow> \<not> (ty = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> 0 \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<or> ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> 0 && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<and> 0 && mask tcbBlockSizeBits \<in> dom tcb_cte_cases) proof (prove)
goal (4 subgoals):
 1. \<And>p. \<lbrakk>{ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; \<exists>n\<in>dom tcb_cte_cases. tcb_at' (p - n) s; ty = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject); p \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val)\<rbrakk> \<Longrightarrow> False
 2. \<And>p. \<lbrakk>{ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; real_cte_at' p s; ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); p && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val); p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases\<rbrakk> \<Longrightarrow> False
 3. \<And>p. \<lbrakk>{ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; \<exists>n\<in>dom tcb_cte_cases. tcb_at' (p - n) s; ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); p && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val); p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases\<rbrakk> \<Longrightarrow> False
 4. {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {} \<Longrightarrow> \<not> (ty = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> 0 \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<or> ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> 0 && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<and> 0 && mask tcbBlockSizeBits \<in> dom tcb_cte_cases) proof (prove)
goal (4 subgoals):
 1. \<And>p. \<lbrakk>\<exists>n\<in>dom tcb_cte_cases. tcb_at' (p - n) s; ty = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject); p \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val)\<rbrakk> \<Longrightarrow> False
 2. \<And>p. \<lbrakk>{ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; real_cte_at' p s; ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); p && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val); p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases\<rbrakk> \<Longrightarrow> False
 3. \<And>p. \<lbrakk>{ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; \<exists>n\<in>dom tcb_cte_cases. tcb_at' (p - n) s; ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); p && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val); p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases\<rbrakk> \<Longrightarrow> False
 4. {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {} \<Longrightarrow> \<not> (ty = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> 0 \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<or> ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> 0 && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<and> 0 && mask tcbBlockSizeBits \<in> dom tcb_cte_cases) proof (prove)
goal (4 subgoals):
 1. \<And>p na a b obj. \<lbrakk>ty = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject); p \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val); tcb_cte_cases na = Some (a, b); ksPSpace s (p - na) = Some (KOTCB obj); is_aligned (p - na) tcbBlockSizeBits; ps_clear (p - na) tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> False
 2. \<And>p. \<lbrakk>{ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; real_cte_at' p s; ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); p && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val); p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases\<rbrakk> \<Longrightarrow> False
 3. \<And>p. \<lbrakk>{ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; \<exists>n\<in>dom tcb_cte_cases. tcb_at' (p - n) s; ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); p && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val); p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases\<rbrakk> \<Longrightarrow> False
 4. {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {} \<Longrightarrow> \<not> (ty = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> 0 \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<or> ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> 0 && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<and> 0 && mask tcbBlockSizeBits \<in> dom tcb_cte_cases) proof (prove)
goal (4 subgoals):
 1. \<And>p na a b obj. \<lbrakk>ty = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject); p \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val); tcb_cte_cases na = Some (a, b); is_aligned (p - na) tcbBlockSizeBits; ps_clear (p - na) tcbBlockSizeBits s; {p - na..p - na + 2 ^ objBitsKO (KOTCB obj) - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>p. \<lbrakk>{ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; real_cte_at' p s; ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); p && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val); p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases\<rbrakk> \<Longrightarrow> False
 3. \<And>p. \<lbrakk>{ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; \<exists>n\<in>dom tcb_cte_cases. tcb_at' (p - n) s; ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); p && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val); p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases\<rbrakk> \<Longrightarrow> False
 4. {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {} \<Longrightarrow> \<not> (ty = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> 0 \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<or> ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> 0 && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<and> 0 && mask tcbBlockSizeBits \<in> dom tcb_cte_cases) proof (prove)
goal (4 subgoals):
 1. \<And>p n a b obj. \<lbrakk>ty = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject); tcb_cte_cases n = Some (a, b); is_aligned (p - n) tcbBlockSizeBits; ps_clear (p - n) tcbBlockSizeBits s; {p - n..p - n + 2 ^ objBitsKO (KOTCB obj) - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; p \<in> {ptr..ptr_add (ptr && ~~ mask sz) (2 ^ sz - 1)}\<rbrakk> \<Longrightarrow> False
 2. \<And>p. \<lbrakk>{ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; real_cte_at' p s; ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); p && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val); p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases\<rbrakk> \<Longrightarrow> False
 3. \<And>p. \<lbrakk>{ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; \<exists>n\<in>dom tcb_cte_cases. tcb_at' (p - n) s; ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); p && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val); p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases\<rbrakk> \<Longrightarrow> False
 4. {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {} \<Longrightarrow> \<not> (ty = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> 0 \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<or> ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> 0 && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<and> 0 && mask tcbBlockSizeBits \<in> dom tcb_cte_cases) proof (prove)
goal (4 subgoals):
 1. \<And>p n a b obj. \<lbrakk>ty = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject); tcb_cte_cases n = Some (a, b); is_aligned (p - n) tcbBlockSizeBits; ps_clear (p - n) tcbBlockSizeBits s; {p - n..p - n + 2 ^ objBitsKO (KOTCB obj) - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; p \<in> {ptr..ptr_add (ptr && ~~ mask sz) (2 ^ sz - 1)}; (p && ~~ mask tcbBlockSizeBits = p - n) = (p \<in> {p - n..p - n + 2 ^ tcbBlockSizeBits - 1})\<rbrakk> \<Longrightarrow> False
 2. \<And>p. \<lbrakk>{ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; real_cte_at' p s; ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); p && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val); p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases\<rbrakk> \<Longrightarrow> False
 3. \<And>p. \<lbrakk>{ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; \<exists>n\<in>dom tcb_cte_cases. tcb_at' (p - n) s; ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); p && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val); p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases\<rbrakk> \<Longrightarrow> False
 4. {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {} \<Longrightarrow> \<not> (ty = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> 0 \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<or> ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> 0 && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<and> 0 && mask tcbBlockSizeBits \<in> dom tcb_cte_cases) proof (prove)
goal (4 subgoals):
 1. \<And>p n a b obj. \<lbrakk>ty = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject); tcb_cte_cases n = Some (a, b); ps_clear (p - n) tcbBlockSizeBits s; {p - n..p - n + 2 ^ objBitsKO (KOTCB obj) - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; p \<in> {ptr..ptr_add (ptr && ~~ mask sz) (2 ^ sz - 1)}; (p && ~~ mask tcbBlockSizeBits = p - n) = (p \<in> {p - n..p - n + 2 ^ tcbBlockSizeBits - 1}); p - n + n && mask tcbBlockSizeBits = n \<and> p - n + n && ~~ mask tcbBlockSizeBits = p - n\<rbrakk> \<Longrightarrow> False
 2. \<And>p. \<lbrakk>{ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; real_cte_at' p s; ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); p && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val); p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases\<rbrakk> \<Longrightarrow> False
 3. \<And>p. \<lbrakk>{ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; \<exists>n\<in>dom tcb_cte_cases. tcb_at' (p - n) s; ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); p && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val); p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases\<rbrakk> \<Longrightarrow> False
 4. {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {} \<Longrightarrow> \<not> (ty = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> 0 \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<or> ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> 0 && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<and> 0 && mask tcbBlockSizeBits \<in> dom tcb_cte_cases) proof (prove)
goal (5 subgoals):
 1. \<And>p n a b obj. \<lbrakk>ty = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject); tcb_cte_cases n = Some (a, b); ps_clear (p - n) tcbBlockSizeBits s; p \<in> {ptr..ptr_add (ptr && ~~ mask sz) (2 ^ sz - 1)}; (p && ~~ mask tcbBlockSizeBits = p - n) = (p \<in> {p - n..p - n + 2 ^ tcbBlockSizeBits - 1}); p - n + n && mask tcbBlockSizeBits = n \<and> p - n + n && ~~ mask tcbBlockSizeBits = p - n\<rbrakk> \<Longrightarrow> p \<in> {p - n..p - n + 2 ^ objBitsKO (KOTCB obj) - 1}
 2. \<And>p n a b obj. \<lbrakk>ty = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject); tcb_cte_cases n = Some (a, b); ps_clear (p - n) tcbBlockSizeBits s; p \<in> {ptr..ptr_add (ptr && ~~ mask sz) (2 ^ sz - 1)}; (p && ~~ mask tcbBlockSizeBits = p - n) = (p \<in> {p - n..p - n + 2 ^ tcbBlockSizeBits - 1}); p - n + n && mask tcbBlockSizeBits = n \<and> p - n + n && ~~ mask tcbBlockSizeBits = p - n; p \<notin> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> False
 3. \<And>p. \<lbrakk>{ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; real_cte_at' p s; ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); p && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val); p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases\<rbrakk> \<Longrightarrow> False
 4. \<And>p. \<lbrakk>{ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; \<exists>n\<in>dom tcb_cte_cases. tcb_at' (p - n) s; ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); p && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val); p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases\<rbrakk> \<Longrightarrow> False
 5. {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {} \<Longrightarrow> \<not> (ty = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> 0 \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<or> ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> 0 && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<and> 0 && mask tcbBlockSizeBits \<in> dom tcb_cte_cases) proof (prove)
goal (4 subgoals):
 1. \<And>p n a b obj. \<lbrakk>ty = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject); tcb_cte_cases n = Some (a, b); ps_clear (p - n) tcbBlockSizeBits s; p \<in> {ptr..ptr_add (ptr && ~~ mask sz) (2 ^ sz - 1)}; (p && ~~ mask tcbBlockSizeBits = p - n) = (p \<in> {p - n..p - n + 2 ^ tcbBlockSizeBits - 1}); p - n + n && mask tcbBlockSizeBits = n \<and> p - n + n && ~~ mask tcbBlockSizeBits = p - n; p \<notin> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> False
 2. \<And>p. \<lbrakk>{ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; real_cte_at' p s; ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); p && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val); p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases\<rbrakk> \<Longrightarrow> False
 3. \<And>p. \<lbrakk>{ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; \<exists>n\<in>dom tcb_cte_cases. tcb_at' (p - n) s; ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); p && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val); p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases\<rbrakk> \<Longrightarrow> False
 4. {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {} \<Longrightarrow> \<not> (ty = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> 0 \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<or> ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> 0 && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<and> 0 && mask tcbBlockSizeBits \<in> dom tcb_cte_cases) proof (prove)
goal (3 subgoals):
 1. \<And>p. \<lbrakk>{ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; real_cte_at' p s; ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); p && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val); p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases\<rbrakk> \<Longrightarrow> False
 2. \<And>p. \<lbrakk>{ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; \<exists>n\<in>dom tcb_cte_cases. tcb_at' (p - n) s; ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); p && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val); p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases\<rbrakk> \<Longrightarrow> False
 3. {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {} \<Longrightarrow> \<not> (ty = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> 0 \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<or> ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> 0 && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<and> 0 && mask tcbBlockSizeBits \<in> dom tcb_cte_cases) proof (prove)
goal (3 subgoals):
 1. \<And>p. \<lbrakk>{ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; real_cte_at' p s; ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); p && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val); p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases; {p && ~~ mask tcbBlockSizeBits..(p && ~~ mask tcbBlockSizeBits) + 2 ^ objBitsKO val - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> False
 2. \<And>p. \<lbrakk>{ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; \<exists>n\<in>dom tcb_cte_cases. tcb_at' (p - n) s; ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); p && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val); p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases\<rbrakk> \<Longrightarrow> False
 3. {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {} \<Longrightarrow> \<not> (ty = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> 0 \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<or> ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> 0 && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<and> 0 && mask tcbBlockSizeBits \<in> dom tcb_cte_cases) proof (prove)
goal (3 subgoals):
 1. \<And>p. \<lbrakk>{ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; real_cte_at' p s; ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases; {p && ~~ mask tcbBlockSizeBits..(p && ~~ mask tcbBlockSizeBits) + 2 ^ objBitsKO val - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; is_aligned (p && ~~ mask tcbBlockSizeBits) (objBitsKO val)\<rbrakk> \<Longrightarrow> False
 2. \<And>p. \<lbrakk>{ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; \<exists>n\<in>dom tcb_cte_cases. tcb_at' (p - n) s; ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); p && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val); p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases\<rbrakk> \<Longrightarrow> False
 3. {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {} \<Longrightarrow> \<not> (ty = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> 0 \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<or> ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> 0 && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<and> 0 && mask tcbBlockSizeBits \<in> dom tcb_cte_cases) proof (prove)
goal (3 subgoals):
 1. \<And>p. \<lbrakk>real_cte_at' p s; ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases; {p && ~~ mask tcbBlockSizeBits..(p && ~~ mask tcbBlockSizeBits) + 2 ^ objBitsKO val - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; is_aligned (p && ~~ mask tcbBlockSizeBits) (objBitsKO val); {p && ~~ mask tcbBlockSizeBits..(p && ~~ mask tcbBlockSizeBits) + 2 ^ objBitsKO val - 1} \<inter> dom (ksPSpace s) = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>p. \<lbrakk>{ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; \<exists>n\<in>dom tcb_cte_cases. tcb_at' (p - n) s; ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); p && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val); p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases\<rbrakk> \<Longrightarrow> False
 3. {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {} \<Longrightarrow> \<not> (ty = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> 0 \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<or> ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> 0 && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<and> 0 && mask tcbBlockSizeBits \<in> dom tcb_cte_cases) proof (prove)
goal (3 subgoals):
 1. \<And>p. \<lbrakk>real_cte_at' p s; ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases; {p && ~~ mask tcbBlockSizeBits..(p && ~~ mask tcbBlockSizeBits) + 2 ^ objBitsKO val - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; is_aligned (p && ~~ mask tcbBlockSizeBits) (objBitsKO val); p \<notin> {p && ~~ mask tcbBlockSizeBits..(p && ~~ mask tcbBlockSizeBits) + 2 ^ objBitsKO val - 1} \<inter> dom (ksPSpace s)\<rbrakk> \<Longrightarrow> False
 2. \<And>p. \<lbrakk>{ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; \<exists>n\<in>dom tcb_cte_cases. tcb_at' (p - n) s; ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); p && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val); p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases\<rbrakk> \<Longrightarrow> False
 3. {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {} \<Longrightarrow> \<not> (ty = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> 0 \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<or> ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> 0 && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<and> 0 && mask tcbBlockSizeBits \<in> dom tcb_cte_cases) proof (prove)
goal (3 subgoals):
 1. \<And>p. \<lbrakk>real_cte_at' p s; ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases; {p && ~~ mask tcbBlockSizeBits..(p && ~~ mask tcbBlockSizeBits) + 2 ^ objBitsKO val - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; is_aligned (p && ~~ mask tcbBlockSizeBits) (objBitsKO val); p \<notin> {p && ~~ mask tcbBlockSizeBits..(p && ~~ mask tcbBlockSizeBits) + 2 ^ objBitsKO val - 1} \<inter> dom (ksPSpace s); (p && ~~ mask (objBitsKO val) = p && ~~ mask tcbBlockSizeBits) = (p \<in> {p && ~~ mask tcbBlockSizeBits..(p && ~~ mask tcbBlockSizeBits) + 2 ^ objBitsKO val - 1})\<rbrakk> \<Longrightarrow> False
 2. \<And>p. \<lbrakk>{ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; \<exists>n\<in>dom tcb_cte_cases. tcb_at' (p - n) s; ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); p && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val); p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases\<rbrakk> \<Longrightarrow> False
 3. {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {} \<Longrightarrow> \<not> (ty = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> 0 \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<or> ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> 0 && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<and> 0 && mask tcbBlockSizeBits \<in> dom tcb_cte_cases) proof (prove)
goal (2 subgoals):
 1. \<And>p. \<lbrakk>{ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; \<exists>n\<in>dom tcb_cte_cases. tcb_at' (p - n) s; ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); p && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val); p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases\<rbrakk> \<Longrightarrow> False
 2. {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {} \<Longrightarrow> \<not> (ty = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> 0 \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<or> ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> 0 && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<and> 0 && mask tcbBlockSizeBits \<in> dom tcb_cte_cases) proof (prove)
goal (2 subgoals):
 1. \<And>p na a b aa ba obj. \<lbrakk>{ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); p && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr (KOTCB makeObject)); val = KOTCB makeObject; range_cover ptr sz tcbBlockSizeBits (2 ^ gbits * n); tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); tcb_cte_cases na = Some (aa, ba); ksPSpace s (p - na) = Some (KOTCB obj); is_aligned (p - na) tcbBlockSizeBits; ps_clear (p - na) tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> False
 2. {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {} \<Longrightarrow> \<not> (ty = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> 0 \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<or> ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> 0 && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<and> 0 && mask tcbBlockSizeBits \<in> dom tcb_cte_cases) proof (prove)
goal (2 subgoals):
 1. \<And>p na a b aa ba obj. \<lbrakk>{ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); p && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr (KOTCB makeObject)); val = KOTCB makeObject; range_cover ptr sz tcbBlockSizeBits (2 ^ gbits * n); tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); tcb_cte_cases na = Some (aa, ba); ksPSpace s (p - na) = Some (KOTCB obj); ps_clear (p - na) tcbBlockSizeBits s; p && mask tcbBlockSizeBits = na \<and> p && ~~ mask tcbBlockSizeBits = p - na\<rbrakk> \<Longrightarrow> False
 2. {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {} \<Longrightarrow> \<not> (ty = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> 0 \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<or> ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> 0 && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<and> 0 && mask tcbBlockSizeBits \<in> dom tcb_cte_cases) proof (prove)
goal (2 subgoals):
 1. \<And>p a b obj. \<lbrakk>{ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); p - (p && mask tcbBlockSizeBits) \<in> set (new_cap_addrs (2 ^ gbits * n) ptr (KOTCB makeObject)); val = KOTCB makeObject; range_cover ptr sz tcbBlockSizeBits (2 ^ gbits * n); tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace s (p - (p && mask tcbBlockSizeBits)) = Some (KOTCB obj); ps_clear (p - (p && mask tcbBlockSizeBits)) tcbBlockSizeBits s; p && ~~ mask tcbBlockSizeBits = p - (p && mask tcbBlockSizeBits)\<rbrakk> \<Longrightarrow> False
 2. {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {} \<Longrightarrow> \<not> (ty = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> 0 \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<or> ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> 0 && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<and> 0 && mask tcbBlockSizeBits \<in> dom tcb_cte_cases) proof (prove)
goal (3 subgoals):
 1. \<And>p a b obj. \<lbrakk>{ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); val = KOTCB makeObject; range_cover ptr sz tcbBlockSizeBits (2 ^ gbits * n); tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace s (p - (p && mask tcbBlockSizeBits)) = Some (KOTCB obj); ps_clear (p - (p && mask tcbBlockSizeBits)) tcbBlockSizeBits s; p && ~~ mask tcbBlockSizeBits = p - (p && mask tcbBlockSizeBits)\<rbrakk> \<Longrightarrow> range_cover ptr (?sz128 p a b obj) (objBitsKO (KOTCB makeObject)) (2 ^ gbits * n)
 2. \<And>p a b obj. \<lbrakk>{ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); val = KOTCB makeObject; range_cover ptr sz tcbBlockSizeBits (2 ^ gbits * n); tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace s (p - (p && mask tcbBlockSizeBits)) = Some (KOTCB obj); ps_clear (p - (p && mask tcbBlockSizeBits)) tcbBlockSizeBits s; p && ~~ mask tcbBlockSizeBits = p - (p && mask tcbBlockSizeBits); p - (p && mask tcbBlockSizeBits) \<in> {ptr..ptr_add (ptr && ~~ mask (?sz128 p a b obj)) (2 ^ ?sz128 p a b obj - 1)}\<rbrakk> \<Longrightarrow> False
 3. {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {} \<Longrightarrow> \<not> (ty = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> 0 \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<or> ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> 0 && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<and> 0 && mask tcbBlockSizeBits \<in> dom tcb_cte_cases) proof (prove)
goal (2 subgoals):
 1. \<And>p a b obj. \<lbrakk>{ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); val = KOTCB makeObject; range_cover ptr sz tcbBlockSizeBits (2 ^ gbits * n); tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace s (p - (p && mask tcbBlockSizeBits)) = Some (KOTCB obj); ps_clear (p - (p && mask tcbBlockSizeBits)) tcbBlockSizeBits s; p && ~~ mask tcbBlockSizeBits = p - (p && mask tcbBlockSizeBits); p - (p && mask tcbBlockSizeBits) \<in> {ptr..ptr_add (ptr && ~~ mask sz) (2 ^ sz - 1)}\<rbrakk> \<Longrightarrow> False
 2. {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {} \<Longrightarrow> \<not> (ty = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> 0 \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<or> ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> 0 && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<and> 0 && mask tcbBlockSizeBits \<in> dom tcb_cte_cases) proof (prove)
goal (3 subgoals):
 1. \<And>p a b obj. \<lbrakk>ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); val = KOTCB makeObject; range_cover ptr sz tcbBlockSizeBits (2 ^ gbits * n); tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace s (p - (p && mask tcbBlockSizeBits)) = Some (KOTCB obj); ps_clear (p - (p && mask tcbBlockSizeBits)) tcbBlockSizeBits s; p && ~~ mask tcbBlockSizeBits = p - (p && mask tcbBlockSizeBits); p - (p && mask tcbBlockSizeBits) \<in> {ptr..ptr_add (ptr && ~~ mask sz) (2 ^ sz - 1)}\<rbrakk> \<Longrightarrow> ?x131 p a b obj \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}
 2. \<And>p a b obj. \<lbrakk>ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); val = KOTCB makeObject; range_cover ptr sz tcbBlockSizeBits (2 ^ gbits * n); tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace s (p - (p && mask tcbBlockSizeBits)) = Some (KOTCB obj); ps_clear (p - (p && mask tcbBlockSizeBits)) tcbBlockSizeBits s; p && ~~ mask tcbBlockSizeBits = p - (p && mask tcbBlockSizeBits); p - (p && mask tcbBlockSizeBits) \<in> {ptr..ptr_add (ptr && ~~ mask sz) (2 ^ sz - 1)}; ?x131 p a b obj \<notin> dom (ksPSpace s)\<rbrakk> \<Longrightarrow> False
 3. {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {} \<Longrightarrow> \<not> (ty = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> 0 \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<or> ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> 0 && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<and> 0 && mask tcbBlockSizeBits \<in> dom tcb_cte_cases) proof (prove)
goal (2 subgoals):
 1. \<And>p a b obj. \<lbrakk>ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); val = KOTCB makeObject; range_cover ptr sz tcbBlockSizeBits (2 ^ gbits * n); tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace s (p - (p && mask tcbBlockSizeBits)) = Some (KOTCB obj); ps_clear (p - (p && mask tcbBlockSizeBits)) tcbBlockSizeBits s; p && ~~ mask tcbBlockSizeBits = p - (p && mask tcbBlockSizeBits); p - (p && mask tcbBlockSizeBits) \<in> {ptr..ptr_add (ptr && ~~ mask sz) (2 ^ sz - 1)}; p - (p && mask tcbBlockSizeBits) \<notin> dom (ksPSpace s)\<rbrakk> \<Longrightarrow> False
 2. {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {} \<Longrightarrow> \<not> (ty = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> 0 \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<or> ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> 0 && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<and> 0 && mask tcbBlockSizeBits \<in> dom tcb_cte_cases) proof (prove)
goal (1 subgoal):
 1. {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {} \<Longrightarrow> \<not> (ty = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> 0 \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<or> ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> 0 && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) \<and> 0 && mask tcbBlockSizeBits \<in> dom tcb_cte_cases) proof (prove)
goal:
No subgoals! proof (state)
this:
valid_mdb' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>)

goal (1 subgoal):
 1. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> no_0_obj' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>x y. data_map_insert x y = (\<lambda>m. m(x \<mapsto> y)) proof (state)
this:
data_map_insert ?x1 ?y1 = (\<lambda>m. m(?x1 \<mapsto> ?y1))

goal (1 subgoal):
 1. \<And>s. \<lbrakk>0 < n; ptr && mask (objBitsKO val + gbits) = 0; pspace_no_overlap' ptr sz s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; ptr \<noteq> 0; fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<or> (\<exists>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<and> a < ptr)\<rbrakk> \<Longrightarrow> no_0_obj' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>) proof (prove)
goal (1 subgoal):
 1. no_0_obj' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>) proof (prove)
using this:
0 \<notin> set (new_cap_addrs (2 ^ gbits * n) ptr val)
no_0_obj' s

goal (1 subgoal):
 1. no_0_obj' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>) proof (state)
this:
no_0_obj' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (n * 2 ^ gbits) ptr val) (ksPSpace s)\<rparr>)

goal:
No subgoals!