theory Retype_R

lemma corres_retype':
  assumes    not_zero: "n \<noteq> 0"
  and         aligned: "is_aligned ptr (objBitsKO ko + gbits)"
  and    obj_bits_api: "obj_bits_api (APIType_map2 ty) us =
                        objBitsKO ko + gbits"
  and           check: "(sz < obj_bits_api (APIType_map2 ty)  us)
                           = (sz < objBitsKO ko + gbits)"
  and             usv: "APIType_map2 ty = Structures_A.CapTableObject \<Longrightarrow> 0 < us"
  and              ko: "makeObjectKO dev ty = Some ko"
  and             orr: "obj_bits_api (APIType_map2 ty) us \<le> sz \<Longrightarrow>
                        obj_relation_retype
                          (default_object (APIType_map2 ty) dev us) ko"
  and           cover: "range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n"
  shows "corres (\<lambda>rv rv'. rv' = g rv)
  (\<lambda>s. valid_pspace s \<and> pspace_no_overlap_range_cover ptr sz s
     \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s)
  (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s)
  (retype_region2 ptr n us (APIType_map2 ty) dev)
  (do addrs \<leftarrow> createObjects ptr n ko gbits;
      _ \<leftarrow> modify (update_gs (APIType_map2 ty) us (set addrs));
      return (g addrs) od)"
  (is "corres ?r ?P ?P' ?C ?A") proof - note data_map_insert_def[simp del] have not_zero':"((of_nat n)::word32) \<noteq> 0" by (rule range_cover_not_zero[OF not_zero cover]) have shiftr_not_zero:" ((of_nat n)::word32) << gbits \<noteq> 0" apply (rule range_cover_not_zero_shift[OF not_zero cover]) apply (simp add:obj_bits_api) done have unat_of_nat_shift:"unat (((of_nat n)::word32) << gbits) =
                          (n * 2^ gbits)" apply (rule range_cover.unat_of_nat_n_shift[OF cover]) using obj_bits_api apply simp done have unat_of_nat_shift':
    "unat (((of_nat n)::word32) * 2^(gbits + objBitsKO ko)) =
     n * 2^(gbits + objBitsKO ko)" apply (subst mult.commute) apply (simp add:shiftl_t2n[symmetric]) apply (rule range_cover.unat_of_nat_n_shift[OF cover]) using obj_bits_api apply simp done have unat_of_nat_n':
    "unat (((of_nat n)::word32) * 2 ^ (gbits + objBitsKO ko)) \<noteq> 0" by (simp add:unat_of_nat_shift' not_zero) have bound:"obj_bits_api (APIType_map2 ty) us \<le> sz" using cover by (simp add:range_cover_def) have n_estimate: "n < 2 ^ (word_bits - (objBitsKO ko + gbits))" apply (rule le_less_trans) apply (rule range_cover.range_cover_n_le(2)[OF cover]) apply (rule power_strict_increasing) apply (simp add:obj_bits_api ko) apply (rule diff_less_mono) using cover obj_bits_api apply (simp_all add:range_cover_def ko word_bits_def) done have set_retype_addrs_fold:
    "image (\<lambda>n. ptr + 2 ^ obj_bits_api (APIType_map2 ty) us * n)
           {x. x \<le> of_nat n - 1} =
     set (retype_addrs ptr (APIType_map2 ty) n us)" apply (clarsimp simp: retype_addrs_def image_def Bex_def ptr_add_def
                          Collect_eq) apply (rule iffI) apply (clarsimp simp: field_simps word_le_nat_alt) apply (rule_tac x="unat x" in exI) apply (simp add: unat_sub_if_size range_cover.unat_of_nat_n[OF cover]
                      not_le not_zero
               split: if_split_asm) apply (clarsimp simp: field_simps word_le_nat_alt) apply (rule_tac x="of_nat x" in exI) apply (simp add: unat_sub_if_size range_cover.unat_of_nat_n[OF cover]) apply (rule nat_le_Suc_less_imp) apply (metis le_unat_uoi nat_less_le not_le_imp_less) done have new_caps_adds_fold:
    "map (\<lambda>n. ptr + 2 ^ objBitsKO ko * n) [0.e.2 ^ gbits * of_nat n - 1] =
     new_cap_addrs (2 ^ gbits * n) ptr ko" apply (simp add: new_cap_addrs_def shiftl_t2n) apply (subgoal_tac "1 \<le> (2::word32) ^ gbits * of_nat n") apply (simp add: upto_enum_red' o_def) apply (rule arg_cong2[where f=map, OF refl]) apply (rule arg_cong2[where f=upt, OF refl]) apply (metis mult.commute shiftl_t2n unat_of_nat_shift) using shiftr_not_zero apply (simp add: shiftl_t2n) apply (metis word_less_1 word_not_le) done from aligned have al': "is_aligned ptr (obj_bits_api (APIType_map2 ty) us)" by (simp add: obj_bits_api ko) show ?thesis apply (simp add: when_def retype_region2_def createObjects'_def
                   createObjects_def aligned obj_bits_api[symmetric]
                   ko[symmetric] al' shiftl_t2n data_map_insert_def[symmetric]
                   is_aligned_mask[symmetric] split_def unless_def
                   lookupAround2_pspace_no check
        split del: if_split) apply (subst retype_addrs_fold)+ apply (subst if_P) using ko apply (clarsimp simp: makeObjectKO_def) apply (simp add: bind_assoc retype_region2_ext_def) apply (rule corres_guard_imp) apply (subst modify_ekheap_update_ekheap) apply (simp only: bind_assoc) apply (rule kheap_ekheap_double_gets) apply (rule corres_symb_exec_r) apply (simp add: not_less modify_modify bind_assoc[symmetric]
                          obj_bits_api[symmetric] shiftl_t2n upto_enum_red'
                           range_cover.unat_of_nat_n[OF cover]) apply (rule corres_split_nor[OF _ corres_trivial]) apply (rename_tac x eps ps) apply (rule_tac P="\<lambda>s. x = kheap s \<and> eps = ekheap (s) \<and> ?P s" and
                          P'="\<lambda>s. ps = ksPSpace s \<and> ?P' s" in corres_modify) apply (simp add: set_retype_addrs_fold new_caps_adds_fold) apply (erule retype_state_relation[OF _ _ _ _ _ _ _ _ _ cover _ _ orr],
                 simp_all add: ko not_zero obj_bits_api
                               bound[simplified obj_bits_api ko])[1] apply (clarsimp simp: retype_addrs_fold[symmetric] ptr_add_def upto_enum_red' not_zero'
                               range_cover.unat_of_nat_n[OF cover] word_le_sub1
                         simp del: word_of_nat_eq_0_iff) apply (rule_tac f=g in arg_cong) apply clarsimp apply wp+ apply (clarsimp split: option.splits) apply (intro conjI impI) apply (clarsimp|wp)+ apply (clarsimp split: option.splits) apply wpsimp apply (clarsimp split: option.splits) apply (intro conjI impI) apply wp apply (clarsimp simp:lookupAround2_char1) apply wp apply (clarsimp simp: obj_bits_api ko) apply (drule(1) pspace_no_overlap_disjoint') apply (rule_tac x1 = a in ccontr[OF in_empty_interE]) apply simp apply (clarsimp simp: not_less shiftL_nat) apply (erule order_trans) apply (subst p_assoc_help) apply (subst word_plus_and_or_coroll2[symmetric,where w = "mask sz"]) apply (subst add.commute) apply (subst add.assoc) apply (rule word_plus_mono_right) using cover apply - apply (rule iffD2[OF word_le_nat_alt]) apply (subst word_of_nat_minus) using not_zero apply simp apply (rule le_trans[OF unat_plus_gt]) apply simp apply (subst unat_minus_one) apply (subst mult.commute) apply (rule word_power_nonzero_32) apply (rule of_nat_less_pow_32[OF n_estimate]) apply (simp add:word_bits_def objBitsKO_gt_0 ko) apply (simp add:range_cover_def obj_bits_api ko word_bits_def) apply (cut_tac not_zero',clarsimp simp:ko) apply(clarsimp simp:field_simps ko) apply (subst unat_sub[OF word_1_le_power]) apply (simp add:range_cover_def) apply (subst diff_add_assoc[symmetric]) apply (cut_tac unat_of_nat_n',simp add:ko) apply (clarsimp simp: obj_bits_api ko) apply (rule diff_le_mono) apply (frule range_cover.range_cover_compare_bound) apply (cut_tac obj_bits_api unat_of_nat_shift') apply (clarsimp simp:add.commute range_cover_def ko) apply (rule is_aligned_no_wrap'[OF is_aligned_neg_mask,OF le_refl ]) apply (simp add:range_cover_def domI)+ done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (\<lambda>rv rv'. rv' = g rv) (\<lambda>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s) (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) (retype_region2 ptr n us (APIType_map2 ty) dev) (do addrs <- createObjects ptr n ko gbits;
_ <- modify (update_gs (APIType_map2 ty) us (set addrs));
return (g addrs)
od) proof (state)
goal (1 subgoal):
 1. corres (\<lambda>rv rv'. rv' = g rv) (\<lambda>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s) (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) (retype_region2 ptr n us (APIType_map2 ty) dev) (do addrs <- createObjects ptr n ko gbits;
_ <- modify (update_gs (APIType_map2 ty) us (set addrs));
return (g addrs)
od) proof (state)
this:
data_map_insert ?x ?y ?m \<equiv> ?m(?x \<mapsto> ?y)

goal (1 subgoal):
 1. corres (\<lambda>rv rv'. rv' = g rv) (\<lambda>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s) (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) (retype_region2 ptr n us (APIType_map2 ty) dev) (do addrs <- createObjects ptr n ko gbits;
_ <- modify (update_gs (APIType_map2 ty) us (set addrs));
return (g addrs)
od) proof (prove)
goal (1 subgoal):
 1. word_of_nat n \<noteq> 0 proof (state)
this:
word_of_nat n \<noteq> 0

goal (1 subgoal):
 1. corres (\<lambda>rv rv'. rv' = g rv) (\<lambda>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s) (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) (retype_region2 ptr n us (APIType_map2 ty) dev) (do addrs <- createObjects ptr n ko gbits;
_ <- modify (update_gs (APIType_map2 ty) us (set addrs));
return (g addrs)
od) proof (prove)
goal (1 subgoal):
 1. word_of_nat n << gbits \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. gbits \<le> obj_bits_api (APIType_map2 ty) us proof (prove)
goal:
No subgoals! proof (state)
this:
word_of_nat n << gbits \<noteq> 0

goal (1 subgoal):
 1. corres (\<lambda>rv rv'. rv' = g rv) (\<lambda>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s) (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) (retype_region2 ptr n us (APIType_map2 ty) dev) (do addrs <- createObjects ptr n ko gbits;
_ <- modify (update_gs (APIType_map2 ty) us (set addrs));
return (g addrs)
od) proof (prove)
goal (1 subgoal):
 1. unat (word_of_nat n << gbits) = n * 2 ^ gbits proof (prove)
goal (1 subgoal):
 1. gbits \<le> obj_bits_api (APIType_map2 ty) us proof (prove)
using this:
obj_bits_api (APIType_map2 ty) us = objBitsKO ko + gbits

goal (1 subgoal):
 1. gbits \<le> obj_bits_api (APIType_map2 ty) us proof (prove)
goal:
No subgoals! proof (state)
this:
unat (word_of_nat n << gbits) = n * 2 ^ gbits

goal (1 subgoal):
 1. corres (\<lambda>rv rv'. rv' = g rv) (\<lambda>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s) (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) (retype_region2 ptr n us (APIType_map2 ty) dev) (do addrs <- createObjects ptr n ko gbits;
_ <- modify (update_gs (APIType_map2 ty) us (set addrs));
return (g addrs)
od) proof (prove)
goal (1 subgoal):
 1. unat (word_of_nat n * 2 ^ (gbits + objBitsKO ko)) = n * 2 ^ (gbits + objBitsKO ko) proof (prove)
goal (1 subgoal):
 1. unat (2 ^ (gbits + objBitsKO ko) * word_of_nat n) = n * 2 ^ (gbits + objBitsKO ko) proof (prove)
goal (1 subgoal):
 1. unat (word_of_nat n << gbits + objBitsKO ko) = n * 2 ^ (gbits + objBitsKO ko) proof (prove)
goal (1 subgoal):
 1. gbits + objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us proof (prove)
using this:
obj_bits_api (APIType_map2 ty) us = objBitsKO ko + gbits

goal (1 subgoal):
 1. gbits + objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us proof (prove)
goal:
No subgoals! proof (state)
this:
unat (word_of_nat n * 2 ^ (gbits + objBitsKO ko)) = n * 2 ^ (gbits + objBitsKO ko)

goal (1 subgoal):
 1. corres (\<lambda>rv rv'. rv' = g rv) (\<lambda>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s) (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) (retype_region2 ptr n us (APIType_map2 ty) dev) (do addrs <- createObjects ptr n ko gbits;
_ <- modify (update_gs (APIType_map2 ty) us (set addrs));
return (g addrs)
od) proof (prove)
goal (1 subgoal):
 1. unat (word_of_nat n * 2 ^ (gbits + objBitsKO ko)) \<noteq> 0 proof (state)
this:
unat (word_of_nat n * 2 ^ (gbits + objBitsKO ko)) \<noteq> 0

goal (1 subgoal):
 1. corres (\<lambda>rv rv'. rv' = g rv) (\<lambda>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s) (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) (retype_region2 ptr n us (APIType_map2 ty) dev) (do addrs <- createObjects ptr n ko gbits;
_ <- modify (update_gs (APIType_map2 ty) us (set addrs));
return (g addrs)
od) proof (prove)
goal (1 subgoal):
 1. obj_bits_api (APIType_map2 ty) us \<le> sz proof (prove)
using this:
range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n

goal (1 subgoal):
 1. obj_bits_api (APIType_map2 ty) us \<le> sz proof (state)
this:
obj_bits_api (APIType_map2 ty) us \<le> sz

goal (1 subgoal):
 1. corres (\<lambda>rv rv'. rv' = g rv) (\<lambda>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s) (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) (retype_region2 ptr n us (APIType_map2 ty) dev) (do addrs <- createObjects ptr n ko gbits;
_ <- modify (update_gs (APIType_map2 ty) us (set addrs));
return (g addrs)
od) proof (prove)
goal (1 subgoal):
 1. n < 2 ^ (word_bits - (objBitsKO ko + gbits)) proof (prove)
goal (2 subgoals):
 1. n \<le> ?y
 2. ?y < 2 ^ (word_bits - (objBitsKO ko + gbits)) proof (prove)
goal (1 subgoal):
 1. 2 ^ (sz - obj_bits_api (APIType_map2 ty) us) < 2 ^ (word_bits - (objBitsKO ko + gbits)) proof (prove)
goal (2 subgoals):
 1. sz - obj_bits_api (APIType_map2 ty) us < word_bits - (objBitsKO ko + gbits)
 2. 1 < 2 proof (prove)
goal (2 subgoals):
 1. sz - (objBitsKO ko + gbits) < word_bits - (objBitsKO ko + gbits)
 2. 1 < 2 proof (prove)
goal (3 subgoals):
 1. sz < word_bits
 2. objBitsKO ko + gbits \<le> sz
 3. 1 < 2 proof (prove)
using this:
range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n
obj_bits_api (APIType_map2 ty) us = objBitsKO ko + gbits

goal (3 subgoals):
 1. sz < word_bits
 2. objBitsKO ko + gbits \<le> sz
 3. 1 < 2 proof (prove)
goal:
No subgoals! proof (state)
this:
n < 2 ^ (word_bits - (objBitsKO ko + gbits))

goal (1 subgoal):
 1. corres (\<lambda>rv rv'. rv' = g rv) (\<lambda>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s) (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) (retype_region2 ptr n us (APIType_map2 ty) dev) (do addrs <- createObjects ptr n ko gbits;
_ <- modify (update_gs (APIType_map2 ty) us (set addrs));
return (g addrs)
od) proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. ptr + 2 ^ obj_bits_api (APIType_map2 ty) us * n) ` {x. x \<le> word_of_nat n - 1} = set (retype_addrs ptr (APIType_map2 ty) n us) proof (prove)
goal (1 subgoal):
 1. \<And>y. (\<exists>x\<le>word_of_nat n - 1. y = ptr + 2 ^ obj_bits_api (APIType_map2 ty) us * x) = (\<exists>x<n. y = ptr + word_of_nat x * 2 ^ obj_bits_api (APIType_map2 ty) us) proof (prove)
goal (2 subgoals):
 1. \<And>y. \<exists>x\<le>word_of_nat n - 1. y = ptr + 2 ^ obj_bits_api (APIType_map2 ty) us * x \<Longrightarrow> \<exists>x<n. y = ptr + word_of_nat x * 2 ^ obj_bits_api (APIType_map2 ty) us
 2. \<And>y. \<exists>x<n. y = ptr + word_of_nat x * 2 ^ obj_bits_api (APIType_map2 ty) us \<Longrightarrow> \<exists>x\<le>word_of_nat n - 1. y = ptr + 2 ^ obj_bits_api (APIType_map2 ty) us * x proof (prove)
goal (2 subgoals):
 1. \<And>x. unat x \<le> unat (word_of_nat n - 1) \<Longrightarrow> \<exists>xa<n. x * 2 ^ obj_bits_api (APIType_map2 ty) us = word_of_nat xa * 2 ^ obj_bits_api (APIType_map2 ty) us
 2. \<And>y. \<exists>x<n. y = ptr + word_of_nat x * 2 ^ obj_bits_api (APIType_map2 ty) us \<Longrightarrow> \<exists>x\<le>word_of_nat n - 1. y = ptr + 2 ^ obj_bits_api (APIType_map2 ty) us * x proof (prove)
goal (2 subgoals):
 1. \<And>x. unat x \<le> unat (word_of_nat n - 1) \<Longrightarrow> unat x < n \<and> x * 2 ^ obj_bits_api (APIType_map2 ty) us = word_of_nat (unat x) * 2 ^ obj_bits_api (APIType_map2 ty) us
 2. \<And>y. \<exists>x<n. y = ptr + word_of_nat x * 2 ^ obj_bits_api (APIType_map2 ty) us \<Longrightarrow> \<exists>x\<le>word_of_nat n - 1. y = ptr + 2 ^ obj_bits_api (APIType_map2 ty) us * x proof (prove)
goal (1 subgoal):
 1. \<And>y. \<exists>x<n. y = ptr + word_of_nat x * 2 ^ obj_bits_api (APIType_map2 ty) us \<Longrightarrow> \<exists>x\<le>word_of_nat n - 1. y = ptr + 2 ^ obj_bits_api (APIType_map2 ty) us * x proof (prove)
goal (1 subgoal):
 1. \<And>x. x < n \<Longrightarrow> \<exists>xa. unat xa \<le> unat (word_of_nat n - 1) \<and> word_of_nat x * 2 ^ obj_bits_api (APIType_map2 ty) us = xa * 2 ^ obj_bits_api (APIType_map2 ty) us proof (prove)
goal (1 subgoal):
 1. \<And>x. x < n \<Longrightarrow> unat (word_of_nat x) \<le> unat (word_of_nat n - 1) \<and> word_of_nat x * 2 ^ obj_bits_api (APIType_map2 ty) us = word_of_nat x * 2 ^ obj_bits_api (APIType_map2 ty) us proof (prove)
goal (1 subgoal):
 1. \<And>x. x < n \<Longrightarrow> unat (word_of_nat x) \<le> n - Suc 0 proof (prove)
goal (1 subgoal):
 1. \<And>x. x < n \<Longrightarrow> unat (word_of_nat x) < n proof (prove)
goal:
No subgoals! proof (state)
this:
(\<lambda>n. ptr + 2 ^ obj_bits_api (APIType_map2 ty) us * n) ` {x. x \<le> word_of_nat n - 1} = set (retype_addrs ptr (APIType_map2 ty) n us)

goal (1 subgoal):
 1. corres (\<lambda>rv rv'. rv' = g rv) (\<lambda>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s) (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) (retype_region2 ptr n us (APIType_map2 ty) dev) (do addrs <- createObjects ptr n ko gbits;
_ <- modify (update_gs (APIType_map2 ty) us (set addrs));
return (g addrs)
od) proof (prove)
goal (1 subgoal):
 1. map (\<lambda>n. ptr + 2 ^ objBitsKO ko * n) [0 .e. 2 ^ gbits * word_of_nat n - 1] = new_cap_addrs (2 ^ gbits * n) ptr ko proof (prove)
goal (1 subgoal):
 1. map (\<lambda>n. ptr + 2 ^ objBitsKO ko * n) [0 .e. 2 ^ gbits * word_of_nat n - 1] = map (\<lambda>p. ptr + 2 ^ objBitsKO ko * word_of_nat p) [0..<2 ^ gbits * n] proof (prove)
goal (2 subgoals):
 1. 1 \<le> 2 ^ gbits * word_of_nat n \<Longrightarrow> map (\<lambda>n. ptr + 2 ^ objBitsKO ko * n) [0 .e. 2 ^ gbits * word_of_nat n - 1] = map (\<lambda>p. ptr + 2 ^ objBitsKO ko * word_of_nat p) [0..<2 ^ gbits * n]
 2. 1 \<le> 2 ^ gbits * word_of_nat n proof (prove)
goal (2 subgoals):
 1. 1 \<le> 2 ^ gbits * word_of_nat n \<Longrightarrow> map (\<lambda>x. ptr + 2 ^ objBitsKO ko * word_of_nat x) [0..<unat (2 ^ gbits * word_of_nat n)] = map (\<lambda>p. ptr + 2 ^ objBitsKO ko * word_of_nat p) [0..<2 ^ gbits * n]
 2. 1 \<le> 2 ^ gbits * word_of_nat n proof (prove)
goal (2 subgoals):
 1. 1 \<le> 2 ^ gbits * word_of_nat n \<Longrightarrow> [0..<unat (2 ^ gbits * word_of_nat n)] = [0..<2 ^ gbits * n]
 2. 1 \<le> 2 ^ gbits * word_of_nat n proof (prove)
goal (2 subgoals):
 1. 1 \<le> 2 ^ gbits * word_of_nat n \<Longrightarrow> unat (2 ^ gbits * word_of_nat n) = 2 ^ gbits * n
 2. 1 \<le> 2 ^ gbits * word_of_nat n proof (prove)
goal (1 subgoal):
 1. 1 \<le> 2 ^ gbits * word_of_nat n proof (prove)
using this:
word_of_nat n << gbits \<noteq> 0

goal (1 subgoal):
 1. 1 \<le> 2 ^ gbits * word_of_nat n proof (prove)
goal (1 subgoal):
 1. 2 ^ gbits * word_of_nat n \<noteq> 0 \<Longrightarrow> 1 \<le> 2 ^ gbits * word_of_nat n proof (prove)
goal:
No subgoals! proof (state)
this:
map (\<lambda>n. ptr + 2 ^ objBitsKO ko * n) [0 .e. 2 ^ gbits * word_of_nat n - 1] = new_cap_addrs (2 ^ gbits * n) ptr ko

goal (1 subgoal):
 1. corres (\<lambda>rv rv'. rv' = g rv) (\<lambda>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s) (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) (retype_region2 ptr n us (APIType_map2 ty) dev) (do addrs <- createObjects ptr n ko gbits;
_ <- modify (update_gs (APIType_map2 ty) us (set addrs));
return (g addrs)
od) proof (chain)
picking this:
is_aligned ptr (objBitsKO ko + gbits) proof (prove)
using this:
is_aligned ptr (objBitsKO ko + gbits)

goal (1 subgoal):
 1. is_aligned ptr (obj_bits_api (APIType_map2 ty) us) proof (state)
this:
is_aligned ptr (obj_bits_api (APIType_map2 ty) us)

goal (1 subgoal):
 1. corres (\<lambda>rv rv'. rv' = g rv) (\<lambda>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s) (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) (retype_region2 ptr n us (APIType_map2 ty) dev) (do addrs <- createObjects ptr n ko gbits;
_ <- modify (update_gs (APIType_map2 ty) us (set addrs));
return (g addrs)
od) proof (prove)
goal (1 subgoal):
 1. corres (\<lambda>rv rv'. rv' = g rv) (\<lambda>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s) (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) (retype_region2 ptr n us (APIType_map2 ty) dev) (do addrs <- createObjects ptr n ko gbits;
_ <- modify (update_gs (APIType_map2 ty) us (set addrs));
return (g addrs)
od) proof (prove)
goal (1 subgoal):
 1. corres (\<lambda>rv rv'. rv' = g rv) (\<lambda>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s) (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) (do y <- if ty \<noteq> Inr (APIObjectType ArchTypes_H.apiobject_type.Untyped) then do kh <- gets kheap;
y <- retype_region2_ext (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api (APIType_map2 ty) us)) [0..<n]) (APIType_map2 ty);
modify (kheap_update (\<lambda>y. foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api (APIType_map2 ty) us)) [0..<n]) kh))
od else return ();
return (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api (APIType_map2 ty) us)) [0..<n])
od) (do y <- do ps <- gets ksPSpace;
y <- case fst (lookupAround2 (ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0)) ps) of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr);
modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr. data_map_insert addr ko) (map (\<lambda>n. ptr + 2 ^ objBitsKO ko * n) [0 .e. 2 ^ gbits * word_of_nat n - 1]) ps))
od;
_ <- modify (update_gs (APIType_map2 ty) us ((\<lambda>x. ptr + 2 ^ obj_bits_api (APIType_map2 ty) us * x) ` {x. x \<le> word_of_nat n - 1}));
return (g (map (\<lambda>n. ptr + 2 ^ obj_bits_api (APIType_map2 ty) us * n) [0 .e. word_of_nat n - 1]))
od) proof (prove)
goal (1 subgoal):
 1. corres (\<lambda>rv rv'. rv' = g rv) (\<lambda>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s) (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) (do y <- if ty \<noteq> Inr (APIObjectType ArchTypes_H.apiobject_type.Untyped) then do kh <- gets kheap;
y <- retype_region2_ext (retype_addrs ptr (APIType_map2 ty) n us) (APIType_map2 ty);
modify (kheap_update (\<lambda>y. foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) kh))
od else return ();
return (retype_addrs ptr (APIType_map2 ty) n us)
od) (do y <- do ps <- gets ksPSpace;
y <- case fst (lookupAround2 (ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0)) ps) of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr);
modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr. data_map_insert addr ko) (map (\<lambda>n. ptr + 2 ^ objBitsKO ko * n) [0 .e. 2 ^ gbits * word_of_nat n - 1]) ps))
od;
_ <- modify (update_gs (APIType_map2 ty) us ((\<lambda>x. ptr + 2 ^ obj_bits_api (APIType_map2 ty) us * x) ` {x. x \<le> word_of_nat n - 1}));
return (g (map (\<lambda>n. ptr + 2 ^ obj_bits_api (APIType_map2 ty) us * n) [0 .e. word_of_nat n - 1]))
od) proof (prove)
goal (2 subgoals):
 1. ty \<noteq> Inr (APIObjectType ArchTypes_H.apiobject_type.Untyped)
 2. corres (\<lambda>rv rv'. rv' = g rv) (\<lambda>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s) (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) (do y <- do kh <- gets kheap;
y <- retype_region2_ext (retype_addrs ptr (APIType_map2 ty) n us) (APIType_map2 ty);
modify (kheap_update (\<lambda>y. foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) kh))
od;
return (retype_addrs ptr (APIType_map2 ty) n us)
od) (do y <- do ps <- gets ksPSpace;
y <- case fst (lookupAround2 (ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0)) ps) of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr);
modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr. data_map_insert addr ko) (map (\<lambda>n. ptr + 2 ^ objBitsKO ko * n) [0 .e. 2 ^ gbits * word_of_nat n - 1]) ps))
od;
_ <- modify (update_gs (APIType_map2 ty) us ((\<lambda>x. ptr + 2 ^ obj_bits_api (APIType_map2 ty) us * x) ` {x. x \<le> word_of_nat n - 1}));
return (g (map (\<lambda>n. ptr + 2 ^ obj_bits_api (APIType_map2 ty) us * n) [0 .e. word_of_nat n - 1]))
od) proof (prove)
using this:
makeObjectKO dev ty = Some ko

goal (2 subgoals):
 1. ty \<noteq> Inr (APIObjectType ArchTypes_H.apiobject_type.Untyped)
 2. corres (\<lambda>rv rv'. rv' = g rv) (\<lambda>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s) (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) (do y <- do kh <- gets kheap;
y <- retype_region2_ext (retype_addrs ptr (APIType_map2 ty) n us) (APIType_map2 ty);
modify (kheap_update (\<lambda>y. foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) kh))
od;
return (retype_addrs ptr (APIType_map2 ty) n us)
od) (do y <- do ps <- gets ksPSpace;
y <- case fst (lookupAround2 (ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0)) ps) of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr);
modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr. data_map_insert addr ko) (map (\<lambda>n. ptr + 2 ^ objBitsKO ko * n) [0 .e. 2 ^ gbits * word_of_nat n - 1]) ps))
od;
_ <- modify (update_gs (APIType_map2 ty) us ((\<lambda>x. ptr + 2 ^ obj_bits_api (APIType_map2 ty) us * x) ` {x. x \<le> word_of_nat n - 1}));
return (g (map (\<lambda>n. ptr + 2 ^ obj_bits_api (APIType_map2 ty) us * n) [0 .e. word_of_nat n - 1]))
od) proof (prove)
goal (1 subgoal):
 1. corres (\<lambda>rv rv'. rv' = g rv) (\<lambda>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s) (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) (do y <- do kh <- gets kheap;
y <- retype_region2_ext (retype_addrs ptr (APIType_map2 ty) n us) (APIType_map2 ty);
modify (kheap_update (\<lambda>y. foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) kh))
od;
return (retype_addrs ptr (APIType_map2 ty) n us)
od) (do y <- do ps <- gets ksPSpace;
y <- case fst (lookupAround2 (ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0)) ps) of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr);
modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr. data_map_insert addr ko) (map (\<lambda>n. ptr + 2 ^ objBitsKO ko * n) [0 .e. 2 ^ gbits * word_of_nat n - 1]) ps))
od;
_ <- modify (update_gs (APIType_map2 ty) us ((\<lambda>x. ptr + 2 ^ obj_bits_api (APIType_map2 ty) us * x) ` {x. x \<le> word_of_nat n - 1}));
return (g (map (\<lambda>n. ptr + 2 ^ obj_bits_api (APIType_map2 ty) us * n) [0 .e. word_of_nat n - 1]))
od) proof (prove)
goal (1 subgoal):
 1. corres (\<lambda>rv rv'. rv' = g rv) (\<lambda>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s) (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) (do x <- gets kheap;
xa <- modify (ekheap_update (foldr (\<lambda>p ekh. ekh(p := default_ext (APIType_map2 ty) default_domain)) (retype_addrs ptr (APIType_map2 ty) n us)));
y <- modify (kheap_update (\<lambda>y. foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) x));
return (retype_addrs ptr (APIType_map2 ty) n us)
od) (do x <- gets ksPSpace;
xa <- case fst (lookupAround2 (ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0)) x) of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr);
y <- modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr. data_map_insert addr ko) (map (\<lambda>n. ptr + 2 ^ objBitsKO ko * n) [0 .e. 2 ^ gbits * word_of_nat n - 1]) x));
_ <- modify (update_gs (APIType_map2 ty) us ((\<lambda>x. ptr + 2 ^ obj_bits_api (APIType_map2 ty) us * x) ` {x. x \<le> word_of_nat n - 1}));
return (g (map (\<lambda>n. ptr + 2 ^ obj_bits_api (APIType_map2 ty) us * n) [0 .e. word_of_nat n - 1]))
od) proof (prove)
goal (3 subgoals):
 1. corres (\<lambda>rv rv'. rv' = g rv) ?Q16 ?Q'16 (do x <- gets kheap;
xa <- modify (ekheap_update (foldr (\<lambda>p ekh. ekh(p := default_ext (APIType_map2 ty) default_domain)) (retype_addrs ptr (APIType_map2 ty) n us)));
y <- modify (kheap_update (\<lambda>y. foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) x));
return (retype_addrs ptr (APIType_map2 ty) n us)
od) (do x <- gets ksPSpace;
xa <- case fst (lookupAround2 (ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0)) x) of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr);
y <- modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr. data_map_insert addr ko) (map (\<lambda>n. ptr + 2 ^ objBitsKO ko * n) [0 .e. 2 ^ gbits * word_of_nat n - 1]) x));
_ <- modify (update_gs (APIType_map2 ty) us ((\<lambda>x. ptr + 2 ^ obj_bits_api (APIType_map2 ty) us * x) ` {x. x \<le> word_of_nat n - 1}));
return (g (map (\<lambda>n. ptr + 2 ^ obj_bits_api (APIType_map2 ty) us * n) [0 .e. word_of_nat n - 1]))
od)
 2. \<And>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s \<Longrightarrow> ?Q16 s
 3. \<And>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<Longrightarrow> ?Q'16 s proof (prove)
goal (3 subgoals):
 1. corres (\<lambda>rv rv'. rv' = g rv) ?Q16 ?Q'16 (do x <- gets kheap;
xa <- do s <- gets ekheap;
modify (ekheap_update (\<lambda>_. foldr (\<lambda>p ekh. ekh(p := default_ext (APIType_map2 ty) default_domain)) (retype_addrs ptr (APIType_map2 ty) n us) s))
od;
y <- modify (kheap_update (\<lambda>y. foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) x));
return (retype_addrs ptr (APIType_map2 ty) n us)
od) (do x <- gets ksPSpace;
xa <- case fst (lookupAround2 (ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0)) x) of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr);
y <- modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr. data_map_insert addr ko) (map (\<lambda>n. ptr + 2 ^ objBitsKO ko * n) [0 .e. 2 ^ gbits * word_of_nat n - 1]) x));
_ <- modify (update_gs (APIType_map2 ty) us ((\<lambda>x. ptr + 2 ^ obj_bits_api (APIType_map2 ty) us * x) ` {x. x \<le> word_of_nat n - 1}));
return (g (map (\<lambda>n. ptr + 2 ^ obj_bits_api (APIType_map2 ty) us * n) [0 .e. word_of_nat n - 1]))
od)
 2. \<And>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s \<Longrightarrow> ?Q16 s
 3. \<And>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<Longrightarrow> ?Q'16 s proof (prove)
goal (3 subgoals):
 1. corres (\<lambda>rv rv'. rv' = g rv) ?Q16 ?Q'16 (do x <- gets kheap;
xa <- gets ekheap;
xa <- modify (ekheap_update (\<lambda>_. foldr (\<lambda>p ekh. ekh(p := default_ext (APIType_map2 ty) default_domain)) (retype_addrs ptr (APIType_map2 ty) n us) xa));
y <- modify (kheap_update (\<lambda>y. foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) x));
return (retype_addrs ptr (APIType_map2 ty) n us)
od) (do x <- gets ksPSpace;
xa <- case fst (lookupAround2 (ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0)) x) of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr);
y <- modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr. data_map_insert addr ko) (map (\<lambda>n. ptr + 2 ^ objBitsKO ko * n) [0 .e. 2 ^ gbits * word_of_nat n - 1]) x));
_ <- modify (update_gs (APIType_map2 ty) us ((\<lambda>x. ptr + 2 ^ obj_bits_api (APIType_map2 ty) us * x) ` {x. x \<le> word_of_nat n - 1}));
return (g (map (\<lambda>n. ptr + 2 ^ obj_bits_api (APIType_map2 ty) us * n) [0 .e. word_of_nat n - 1]))
od)
 2. \<And>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s \<Longrightarrow> ?Q16 s
 3. \<And>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<Longrightarrow> ?Q'16 s proof (prove)
goal (3 subgoals):
 1. \<And>rv erv rv'. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'\<rbrakk> \<Longrightarrow> corres (\<lambda>rv rv'. rv' = g rv) (?R23 rv erv) (?R'23 rv') (do x <- modify (ekheap_update (\<lambda>_. foldr (\<lambda>p ekh. ekh(p := default_ext (APIType_map2 ty) default_domain)) (retype_addrs ptr (APIType_map2 ty) n us) erv));
y <- modify (kheap_update (\<lambda>y. foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) rv));
return (retype_addrs ptr (APIType_map2 ty) n us)
od) (do x <- case fst (lookupAround2 (ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0)) rv') of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr);
y <- modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr. data_map_insert addr ko) (map (\<lambda>n. ptr + 2 ^ objBitsKO ko * n) [0 .e. 2 ^ gbits * word_of_nat n - 1]) rv'));
_ <- modify (update_gs (APIType_map2 ty) us ((\<lambda>x. ptr + 2 ^ obj_bits_api (APIType_map2 ty) us * x) ` {x. x \<le> word_of_nat n - 1}));
return (g (map (\<lambda>n. ptr + 2 ^ obj_bits_api (APIType_map2 ty) us * n) [0 .e. word_of_nat n - 1]))
od)
 2. \<And>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s \<Longrightarrow> ?R23 (kheap s) (ekheap s) s
 3. \<And>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<Longrightarrow> ?R'23 (ksPSpace s) s proof (prove)
goal (6 subgoals):
 1. \<And>rv erv rv' rva. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'\<rbrakk> \<Longrightarrow> corres (\<lambda>rv rv'. rv' = g rv) (?R23 rv erv) (?Q'32 rv erv rv' rva) (do x <- modify (ekheap_update (\<lambda>_. foldr (\<lambda>p ekh. ekh(p := default_ext (APIType_map2 ty) default_domain)) (retype_addrs ptr (APIType_map2 ty) n us) erv));
y <- modify (kheap_update (\<lambda>y. foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) rv));
return (retype_addrs ptr (APIType_map2 ty) n us)
od) (do y <- modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr. data_map_insert addr ko) (map (\<lambda>n. ptr + 2 ^ objBitsKO ko * n) [0 .e. 2 ^ gbits * word_of_nat n - 1]) rv'));
_ <- modify (update_gs (APIType_map2 ty) us ((\<lambda>x. ptr + 2 ^ obj_bits_api (APIType_map2 ty) us * x) ` {x. x \<le> word_of_nat n - 1}));
return (g (map (\<lambda>n. ptr + 2 ^ obj_bits_api (APIType_map2 ty) us * n) [0 .e. word_of_nat n - 1]))
od)
 2. \<And>rv erv rv'. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?R'23 rv'\<rbrace> case fst (lookupAround2 (ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0)) rv') of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr) \<lbrace>?Q'32 rv erv rv'\<rbrace>
 3. \<And>rv erv rv' s. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'; ?R'23 rv' s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case fst (lookupAround2 (ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0)) rv') of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr) \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>rv erv rv'. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'; True\<rbrakk> \<Longrightarrow> no_fail (?R'23 rv') (case fst (lookupAround2 (ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0)) rv') of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr))
 5. \<And>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s \<Longrightarrow> ?R23 (kheap s) (ekheap s) s
 6. \<And>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<Longrightarrow> ?R'23 (ksPSpace s) s proof (prove)
goal (6 subgoals):
 1. \<And>rv erv rv'. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'\<rbrakk> \<Longrightarrow> corres (\<lambda>rv rv'. rv' = g rv) (?R23 rv erv) (?Q'32 rv erv rv' ()) (do y <- modify (kheap_update (\<lambda>y. foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) rv) \<circ> ekheap_update (\<lambda>_. foldr (\<lambda>p ekh a. if a = p then default_ext (APIType_map2 ty) default_domain else ekh a) (retype_addrs ptr (APIType_map2 ty) n us) erv));
return (retype_addrs ptr (APIType_map2 ty) n us)
od) (do _ <- modify (update_gs (APIType_map2 ty) us ((\<lambda>x. ptr + 2 ^ obj_bits_api (APIType_map2 ty) us * x) ` {x. x \<le> word_of_nat n - 1}) \<circ> ksPSpace_update (\<lambda>_. foldr (\<lambda>addr. data_map_insert addr ko) (map (\<lambda>n. ptr + 2 ^ objBitsKO ko * n) [0 .e. 2 ^ gbits * word_of_nat n - 1]) rv'));
return (g (map (\<lambda>n. ptr + 2 ^ obj_bits_api (APIType_map2 ty) us * n) [0 .e. word_of_nat n - 1]))
od)
 2. \<And>rv erv rv'. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?R'23 rv'\<rbrace> case fst (lookupAround2 (ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0)) rv') of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr) \<lbrace>?Q'32 rv erv rv'\<rbrace>
 3. \<And>rv erv rv' s. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'; ?R'23 rv' s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case fst (lookupAround2 (ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0)) rv') of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr) \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>rv erv rv'. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'; True\<rbrakk> \<Longrightarrow> no_fail (?R'23 rv') (case fst (lookupAround2 (ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0)) rv') of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr))
 5. \<And>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s \<Longrightarrow> ?R23 (kheap s) (ekheap s) s
 6. \<And>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<Longrightarrow> ?R'23 (ksPSpace s) s proof (prove)
goal (9 subgoals):
 1. \<And>rv erv rv'. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'\<rbrakk> \<Longrightarrow> corres dc (?P55 rv erv) (?P'51 rv erv rv' ()) (modify (kheap_update (\<lambda>y. foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) rv) \<circ> ekheap_update (\<lambda>_. foldr (\<lambda>p ekh a. if a = p then default_ext (APIType_map2 ty) default_domain else ekh a) (retype_addrs ptr (APIType_map2 ty) n us) erv))) (modify (update_gs (APIType_map2 ty) us ((\<lambda>x. ptr + 2 ^ obj_bits_api (APIType_map2 ty) us * x) ` {x. x \<le> word_of_nat n - 1}) \<circ> ksPSpace_update (\<lambda>_. foldr (\<lambda>addr. data_map_insert addr ko) (map (\<lambda>n. ptr + 2 ^ objBitsKO ko * n) [0 .e. 2 ^ gbits * word_of_nat n - 1]) rv')))
 2. \<And>rv erv rv'. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'\<rbrakk> \<Longrightarrow> corres (\<lambda>rv rv'. rv' = g rv) (\<lambda>_. True) (\<lambda>_. True) (return (retype_addrs ptr (APIType_map2 ty) n us)) (return (g (map (\<lambda>n. ptr + 2 ^ obj_bits_api (APIType_map2 ty) us * n) [0 .e. word_of_nat n - 1])))
 3. \<And>rv erv rv'. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q53 rv erv\<rbrace> modify (kheap_update (\<lambda>y. foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) rv) \<circ> ekheap_update (\<lambda>_. foldr (\<lambda>p ekh a. if a = p then default_ext (APIType_map2 ty) default_domain else ekh a) (retype_addrs ptr (APIType_map2 ty) n us) erv)) \<lbrace>\<lambda>x _. True\<rbrace>
 4. \<And>rv erv rv'. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'50 rv erv rv' ()\<rbrace> modify (update_gs (APIType_map2 ty) us ((\<lambda>x. ptr + 2 ^ obj_bits_api (APIType_map2 ty) us * x) ` {x. x \<le> word_of_nat n - 1}) \<circ> ksPSpace_update (\<lambda>_. foldr (\<lambda>addr. data_map_insert addr ko) (map (\<lambda>n. ptr + 2 ^ objBitsKO ko * n) [0 .e. 2 ^ gbits * word_of_nat n - 1]) rv')) \<lbrace>\<lambda>x _. True\<rbrace>
 5. \<And>rv erv rv'. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?R'23 rv'\<rbrace> case fst (lookupAround2 (ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0)) rv') of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr) \<lbrace>\<lambda>a. ?P'51 rv erv rv' a and ?Q'50 rv erv rv' a\<rbrace>
 6. \<And>rv erv rv' s. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'; ?R'23 rv' s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case fst (lookupAround2 (ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0)) rv') of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr) \<lbrace>\<lambda>r. (=) s\<rbrace>
 7. \<And>rv erv rv'. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'; True\<rbrakk> \<Longrightarrow> no_fail (?R'23 rv') (case fst (lookupAround2 (ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0)) rv') of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr))
 8. \<And>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s \<Longrightarrow> (?P55 (kheap s) (ekheap s) and ?Q53 (kheap s) (ekheap s)) s
 9. \<And>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<Longrightarrow> ?R'23 (ksPSpace s) s proof (prove)
goal (9 subgoals):
 1. \<And>x eps ps. \<lbrakk>pspace_relation x ps; ekheap_relation eps ps\<rbrakk> \<Longrightarrow> corres dc (?P55 x eps) (?P'51 x eps ps ()) (modify (kheap_update (\<lambda>y. foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) x) \<circ> ekheap_update (\<lambda>_. foldr (\<lambda>p ekh a. if a = p then default_ext (APIType_map2 ty) default_domain else ekh a) (retype_addrs ptr (APIType_map2 ty) n us) eps))) (modify (update_gs (APIType_map2 ty) us ((\<lambda>x. ptr + 2 ^ obj_bits_api (APIType_map2 ty) us * x) ` {x. x \<le> word_of_nat n - 1}) \<circ> ksPSpace_update (\<lambda>_. foldr (\<lambda>addr. data_map_insert addr ko) (map (\<lambda>n. ptr + 2 ^ objBitsKO ko * n) [0 .e. 2 ^ gbits * word_of_nat n - 1]) ps)))
 2. \<And>rv erv rv'. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'\<rbrakk> \<Longrightarrow> corres (\<lambda>rv rv'. rv' = g rv) (\<lambda>_. True) (\<lambda>_. True) (return (retype_addrs ptr (APIType_map2 ty) n us)) (return (g (map (\<lambda>n. ptr + 2 ^ obj_bits_api (APIType_map2 ty) us * n) [0 .e. word_of_nat n - 1])))
 3. \<And>rv erv rv'. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q53 rv erv\<rbrace> modify (kheap_update (\<lambda>y. foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) rv) \<circ> ekheap_update (\<lambda>_. foldr (\<lambda>p ekh a. if a = p then default_ext (APIType_map2 ty) default_domain else ekh a) (retype_addrs ptr (APIType_map2 ty) n us) erv)) \<lbrace>\<lambda>x _. True\<rbrace>
 4. \<And>rv erv rv'. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'50 rv erv rv' ()\<rbrace> modify (update_gs (APIType_map2 ty) us ((\<lambda>x. ptr + 2 ^ obj_bits_api (APIType_map2 ty) us * x) ` {x. x \<le> word_of_nat n - 1}) \<circ> ksPSpace_update (\<lambda>_. foldr (\<lambda>addr. data_map_insert addr ko) (map (\<lambda>n. ptr + 2 ^ objBitsKO ko * n) [0 .e. 2 ^ gbits * word_of_nat n - 1]) rv')) \<lbrace>\<lambda>x _. True\<rbrace>
 5. \<And>rv erv rv'. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?R'23 rv'\<rbrace> case fst (lookupAround2 (ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0)) rv') of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr) \<lbrace>\<lambda>a. ?P'51 rv erv rv' a and ?Q'50 rv erv rv' a\<rbrace>
 6. \<And>rv erv rv' s. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'; ?R'23 rv' s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case fst (lookupAround2 (ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0)) rv') of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr) \<lbrace>\<lambda>r. (=) s\<rbrace>
 7. \<And>rv erv rv'. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'; True\<rbrakk> \<Longrightarrow> no_fail (?R'23 rv') (case fst (lookupAround2 (ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0)) rv') of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr))
 8. \<And>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s \<Longrightarrow> (?P55 (kheap s) (ekheap s) and ?Q53 (kheap s) (ekheap s)) s
 9. \<And>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<Longrightarrow> ?R'23 (ksPSpace s) s proof (prove)
goal (9 subgoals):
 1. \<And>x eps ps s s'. \<lbrakk>pspace_relation x ps; ekheap_relation eps ps; x = kheap s \<and> eps = ekheap s \<and> valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s; ps = ksPSpace s' \<and> pspace_aligned' s' \<and> pspace_distinct' s' \<and> pspace_no_overlap' ptr sz s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> ((kheap_update (\<lambda>y. foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) x) \<circ> ekheap_update (\<lambda>_. foldr (\<lambda>p ekh a. if a = p then default_ext (APIType_map2 ty) default_domain else ekh a) (retype_addrs ptr (APIType_map2 ty) n us) eps)) s, (update_gs (APIType_map2 ty) us ((\<lambda>x. ptr + 2 ^ obj_bits_api (APIType_map2 ty) us * x) ` {x. x \<le> word_of_nat n - 1}) \<circ> ksPSpace_update (\<lambda>_. foldr (\<lambda>addr. data_map_insert addr ko) (map (\<lambda>n. ptr + 2 ^ objBitsKO ko * n) [0 .e. 2 ^ gbits * word_of_nat n - 1]) ps)) s') \<in> state_relation
 2. \<And>rv erv rv'. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'\<rbrakk> \<Longrightarrow> corres (\<lambda>rv rv'. rv' = g rv) (\<lambda>_. True) (\<lambda>_. True) (return (retype_addrs ptr (APIType_map2 ty) n us)) (return (g (map (\<lambda>n. ptr + 2 ^ obj_bits_api (APIType_map2 ty) us * n) [0 .e. word_of_nat n - 1])))
 3. \<And>rv erv rv'. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q53 rv erv\<rbrace> modify (kheap_update (\<lambda>y. foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) rv) \<circ> ekheap_update (\<lambda>_. foldr (\<lambda>p ekh a. if a = p then default_ext (APIType_map2 ty) default_domain else ekh a) (retype_addrs ptr (APIType_map2 ty) n us) erv)) \<lbrace>\<lambda>x _. True\<rbrace>
 4. \<And>rv erv rv'. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'50 rv erv rv' ()\<rbrace> modify (update_gs (APIType_map2 ty) us ((\<lambda>x. ptr + 2 ^ obj_bits_api (APIType_map2 ty) us * x) ` {x. x \<le> word_of_nat n - 1}) \<circ> ksPSpace_update (\<lambda>_. foldr (\<lambda>addr. data_map_insert addr ko) (map (\<lambda>n. ptr + 2 ^ objBitsKO ko * n) [0 .e. 2 ^ gbits * word_of_nat n - 1]) rv')) \<lbrace>\<lambda>x _. True\<rbrace>
 5. \<And>rv erv rv'. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?R'23 rv'\<rbrace> case fst (lookupAround2 (ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0)) rv') of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr) \<lbrace>\<lambda>a. (\<lambda>a. rv' = ksPSpace a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> pspace_no_overlap' ptr sz a) and ?Q'50 rv erv rv' a\<rbrace>
 6. \<And>rv erv rv' s. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'; ?R'23 rv' s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case fst (lookupAround2 (ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0)) rv') of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr) \<lbrace>\<lambda>r. (=) s\<rbrace>
 7. \<And>rv erv rv'. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'; True\<rbrakk> \<Longrightarrow> no_fail (?R'23 rv') (case fst (lookupAround2 (ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0)) rv') of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr))
 8. \<And>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s \<Longrightarrow> ((\<lambda>a. kheap s = kheap a \<and> ekheap s = ekheap a \<and> valid_pspace a \<and> pspace_no_overlap (up_aligned_area ptr sz) a \<and> valid_mdb a \<and> valid_etcbs a \<and> valid_list a) and ?Q53 (kheap s) (ekheap s)) s
 9. \<And>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<Longrightarrow> ?R'23 (ksPSpace s) s proof (prove)
goal (9 subgoals):
 1. \<And>s s'. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s; pspace_aligned' s' \<and> pspace_distinct' s' \<and> pspace_no_overlap' ptr sz s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (s\<lparr>ekheap := foldr (\<lambda>p ekh a. if a = p then default_ext (APIType_map2 ty) default_domain else ekh a) (retype_addrs ptr (APIType_map2 ty) n us) (ekheap s), kheap := foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)\<rparr>, update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs (2 ^ gbits * n) ptr ko) (ksPSpace s')\<rparr>)) \<in> state_relation
 2. \<And>rv erv rv'. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'\<rbrakk> \<Longrightarrow> corres (\<lambda>rv rv'. rv' = g rv) (\<lambda>_. True) (\<lambda>_. True) (return (retype_addrs ptr (APIType_map2 ty) n us)) (return (g (map (\<lambda>n. ptr + 2 ^ obj_bits_api (APIType_map2 ty) us * n) [0 .e. word_of_nat n - 1])))
 3. \<And>rv erv rv'. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q53 rv erv\<rbrace> modify (kheap_update (\<lambda>y. foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) rv) \<circ> ekheap_update (\<lambda>_. foldr (\<lambda>p ekh a. if a = p then default_ext (APIType_map2 ty) default_domain else ekh a) (retype_addrs ptr (APIType_map2 ty) n us) erv)) \<lbrace>\<lambda>x _. True\<rbrace>
 4. \<And>rv erv rv'. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'50 rv erv rv' ()\<rbrace> modify (update_gs (APIType_map2 ty) us ((\<lambda>x. ptr + 2 ^ obj_bits_api (APIType_map2 ty) us * x) ` {x. x \<le> word_of_nat n - 1}) \<circ> ksPSpace_update (\<lambda>_. foldr (\<lambda>addr. data_map_insert addr ko) (map (\<lambda>n. ptr + 2 ^ objBitsKO ko * n) [0 .e. 2 ^ gbits * word_of_nat n - 1]) rv')) \<lbrace>\<lambda>x _. True\<rbrace>
 5. \<And>rv erv rv'. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?R'23 rv'\<rbrace> case fst (lookupAround2 (ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0)) rv') of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr) \<lbrace>\<lambda>a. (\<lambda>a. rv' = ksPSpace a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> pspace_no_overlap' ptr sz a) and ?Q'50 rv erv rv' a\<rbrace>
 6. \<And>rv erv rv' s. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'; ?R'23 rv' s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case fst (lookupAround2 (ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0)) rv') of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr) \<lbrace>\<lambda>r. (=) s\<rbrace>
 7. \<And>rv erv rv'. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'; True\<rbrakk> \<Longrightarrow> no_fail (?R'23 rv') (case fst (lookupAround2 (ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0)) rv') of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr))
 8. \<And>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s \<Longrightarrow> ((\<lambda>a. kheap s = kheap a \<and> ekheap s = ekheap a \<and> valid_pspace a \<and> pspace_no_overlap (up_aligned_area ptr sz) a \<and> valid_mdb a \<and> valid_etcbs a \<and> valid_list a) and ?Q53 (kheap s) (ekheap s)) s
 9. \<And>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<Longrightarrow> ?R'23 (ksPSpace s) s proof (prove)
goal (8 subgoals):
 1. \<And>rv erv rv'. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'\<rbrakk> \<Longrightarrow> corres (\<lambda>rv rv'. rv' = g rv) (\<lambda>_. True) (\<lambda>_. True) (return (retype_addrs ptr (APIType_map2 ty) n us)) (return (g (map (\<lambda>n. ptr + 2 ^ obj_bits_api (APIType_map2 ty) us * n) [0 .e. word_of_nat n - 1])))
 2. \<And>rv erv rv'. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q53 rv erv\<rbrace> modify (kheap_update (\<lambda>y. foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) rv) \<circ> ekheap_update (\<lambda>_. foldr (\<lambda>p ekh a. if a = p then default_ext (APIType_map2 ty) default_domain else ekh a) (retype_addrs ptr (APIType_map2 ty) n us) erv)) \<lbrace>\<lambda>x _. True\<rbrace>
 3. \<And>rv erv rv'. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'50 rv erv rv' ()\<rbrace> modify (update_gs (APIType_map2 ty) us ((\<lambda>x. ptr + 2 ^ obj_bits_api (APIType_map2 ty) us * x) ` {x. x \<le> word_of_nat n - 1}) \<circ> ksPSpace_update (\<lambda>_. foldr (\<lambda>addr. data_map_insert addr ko) (map (\<lambda>n. ptr + 2 ^ objBitsKO ko * n) [0 .e. 2 ^ gbits * word_of_nat n - 1]) rv')) \<lbrace>\<lambda>x _. True\<rbrace>
 4. \<And>rv erv rv'. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?R'23 rv'\<rbrace> case fst (lookupAround2 (ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0)) rv') of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr) \<lbrace>\<lambda>a. (\<lambda>a. rv' = ksPSpace a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> pspace_no_overlap' ptr sz a) and ?Q'50 rv erv rv' a\<rbrace>
 5. \<And>rv erv rv' s. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'; ?R'23 rv' s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case fst (lookupAround2 (ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0)) rv') of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr) \<lbrace>\<lambda>r. (=) s\<rbrace>
 6. \<And>rv erv rv'. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'; True\<rbrakk> \<Longrightarrow> no_fail (?R'23 rv') (case fst (lookupAround2 (ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0)) rv') of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr))
 7. \<And>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s \<Longrightarrow> ((\<lambda>a. kheap s = kheap a \<and> ekheap s = ekheap a \<and> valid_pspace a \<and> pspace_no_overlap (up_aligned_area ptr sz) a \<and> valid_mdb a \<and> valid_etcbs a \<and> valid_list a) and ?Q53 (kheap s) (ekheap s)) s
 8. \<And>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<Longrightarrow> ?R'23 (ksPSpace s) s proof (prove)
goal (8 subgoals):
 1. \<And>rv erv rv' s s'. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> g (map ((\<lambda>n. ptr + 2 ^ obj_bits_api (APIType_map2 ty) us * n) \<circ> word_of_nat) [0..<n]) = g (map (\<lambda>p. ptr + word_of_nat p * 2 ^ obj_bits_api (APIType_map2 ty) us) [0..<n])
 2. \<And>rv erv rv'. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q53 rv erv\<rbrace> modify (kheap_update (\<lambda>y. foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) rv) \<circ> ekheap_update (\<lambda>_. foldr (\<lambda>p ekh a. if a = p then default_ext (APIType_map2 ty) default_domain else ekh a) (retype_addrs ptr (APIType_map2 ty) n us) erv)) \<lbrace>\<lambda>x _. True\<rbrace>
 3. \<And>rv erv rv'. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'50 rv erv rv' ()\<rbrace> modify (update_gs (APIType_map2 ty) us ((\<lambda>x. ptr + 2 ^ obj_bits_api (APIType_map2 ty) us * x) ` {x. x \<le> word_of_nat n - 1}) \<circ> ksPSpace_update (\<lambda>_. foldr (\<lambda>addr. data_map_insert addr ko) (map (\<lambda>n. ptr + 2 ^ objBitsKO ko * n) [0 .e. 2 ^ gbits * word_of_nat n - 1]) rv')) \<lbrace>\<lambda>x _. True\<rbrace>
 4. \<And>rv erv rv'. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?R'23 rv'\<rbrace> case fst (lookupAround2 (ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0)) rv') of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr) \<lbrace>\<lambda>a. (\<lambda>a. rv' = ksPSpace a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> pspace_no_overlap' ptr sz a) and ?Q'50 rv erv rv' a\<rbrace>
 5. \<And>rv erv rv' s. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'; ?R'23 rv' s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case fst (lookupAround2 (ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0)) rv') of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr) \<lbrace>\<lambda>r. (=) s\<rbrace>
 6. \<And>rv erv rv'. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'; True\<rbrakk> \<Longrightarrow> no_fail (?R'23 rv') (case fst (lookupAround2 (ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0)) rv') of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr))
 7. \<And>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s \<Longrightarrow> ((\<lambda>a. kheap s = kheap a \<and> ekheap s = ekheap a \<and> valid_pspace a \<and> pspace_no_overlap (up_aligned_area ptr sz) a \<and> valid_mdb a \<and> valid_etcbs a \<and> valid_list a) and ?Q53 (kheap s) (ekheap s)) s
 8. \<And>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<Longrightarrow> ?R'23 (ksPSpace s) s proof (prove)
goal (8 subgoals):
 1. \<And>rv erv rv' s s'. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> map ((\<lambda>n. ptr + 2 ^ obj_bits_api (APIType_map2 ty) us * n) \<circ> word_of_nat) [0..<n] = map (\<lambda>p. ptr + word_of_nat p * 2 ^ obj_bits_api (APIType_map2 ty) us) [0..<n]
 2. \<And>rv erv rv'. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q53 rv erv\<rbrace> modify (kheap_update (\<lambda>y. foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) rv) \<circ> ekheap_update (\<lambda>_. foldr (\<lambda>p ekh a. if a = p then default_ext (APIType_map2 ty) default_domain else ekh a) (retype_addrs ptr (APIType_map2 ty) n us) erv)) \<lbrace>\<lambda>x _. True\<rbrace>
 3. \<And>rv erv rv'. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'50 rv erv rv' ()\<rbrace> modify (update_gs (APIType_map2 ty) us ((\<lambda>x. ptr + 2 ^ obj_bits_api (APIType_map2 ty) us * x) ` {x. x \<le> word_of_nat n - 1}) \<circ> ksPSpace_update (\<lambda>_. foldr (\<lambda>addr. data_map_insert addr ko) (map (\<lambda>n. ptr + 2 ^ objBitsKO ko * n) [0 .e. 2 ^ gbits * word_of_nat n - 1]) rv')) \<lbrace>\<lambda>x _. True\<rbrace>
 4. \<And>rv erv rv'. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?R'23 rv'\<rbrace> case fst (lookupAround2 (ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0)) rv') of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr) \<lbrace>\<lambda>a. (\<lambda>a. rv' = ksPSpace a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> pspace_no_overlap' ptr sz a) and ?Q'50 rv erv rv' a\<rbrace>
 5. \<And>rv erv rv' s. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'; ?R'23 rv' s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case fst (lookupAround2 (ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0)) rv') of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr) \<lbrace>\<lambda>r. (=) s\<rbrace>
 6. \<And>rv erv rv'. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'; True\<rbrakk> \<Longrightarrow> no_fail (?R'23 rv') (case fst (lookupAround2 (ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0)) rv') of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr))
 7. \<And>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s \<Longrightarrow> ((\<lambda>a. kheap s = kheap a \<and> ekheap s = ekheap a \<and> valid_pspace a \<and> pspace_no_overlap (up_aligned_area ptr sz) a \<and> valid_mdb a \<and> valid_etcbs a \<and> valid_list a) and ?Q53 (kheap s) (ekheap s)) s
 8. \<And>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<Longrightarrow> ?R'23 (ksPSpace s) s proof (prove)
goal (7 subgoals):
 1. \<And>rv erv rv'. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q53 rv erv\<rbrace> modify (kheap_update (\<lambda>y. foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) rv) \<circ> ekheap_update (\<lambda>_. foldr (\<lambda>p ekh a. if a = p then default_ext (APIType_map2 ty) default_domain else ekh a) (retype_addrs ptr (APIType_map2 ty) n us) erv)) \<lbrace>\<lambda>x _. True\<rbrace>
 2. \<And>rv erv rv'. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'50 rv erv rv' ()\<rbrace> modify (update_gs (APIType_map2 ty) us ((\<lambda>x. ptr + 2 ^ obj_bits_api (APIType_map2 ty) us * x) ` {x. x \<le> word_of_nat n - 1}) \<circ> ksPSpace_update (\<lambda>_. foldr (\<lambda>addr. data_map_insert addr ko) (map (\<lambda>n. ptr + 2 ^ objBitsKO ko * n) [0 .e. 2 ^ gbits * word_of_nat n - 1]) rv')) \<lbrace>\<lambda>x _. True\<rbrace>
 3. \<And>rv erv rv'. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?R'23 rv'\<rbrace> case fst (lookupAround2 (ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0)) rv') of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr) \<lbrace>\<lambda>a. (\<lambda>a. rv' = ksPSpace a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> pspace_no_overlap' ptr sz a) and ?Q'50 rv erv rv' a\<rbrace>
 4. \<And>rv erv rv' s. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'; ?R'23 rv' s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case fst (lookupAround2 (ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0)) rv') of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr) \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<And>rv erv rv'. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'; True\<rbrakk> \<Longrightarrow> no_fail (?R'23 rv') (case fst (lookupAround2 (ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0)) rv') of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr))
 6. \<And>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s \<Longrightarrow> ((\<lambda>a. kheap s = kheap a \<and> ekheap s = ekheap a \<and> valid_pspace a \<and> pspace_no_overlap (up_aligned_area ptr sz) a \<and> valid_mdb a \<and> valid_etcbs a \<and> valid_list a) and ?Q53 (kheap s) (ekheap s)) s
 7. \<And>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<Longrightarrow> ?R'23 (ksPSpace s) s proof (prove)
goal (5 subgoals):
 1. \<And>rv erv rv'. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?R'23 rv'\<rbrace> case fst (lookupAround2 (ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0)) rv') of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr) \<lbrace>\<lambda>rv s. rv' = ksPSpace s \<and> (pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) \<and> True\<rbrace>
 2. \<And>rv erv rv' s. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'; ?R'23 rv' s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case fst (lookupAround2 (ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0)) rv') of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr) \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>rv erv rv'. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'; True\<rbrakk> \<Longrightarrow> no_fail (?R'23 rv') (case fst (lookupAround2 (ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0)) rv') of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr))
 4. \<And>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s \<Longrightarrow> ((\<lambda>a. kheap s = kheap a \<and> ekheap s = ekheap a \<and> valid_pspace a \<and> pspace_no_overlap (up_aligned_area ptr sz) a \<and> valid_mdb a \<and> valid_etcbs a \<and> valid_list a) and (\<lambda>a. True)) s
 5. \<And>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<Longrightarrow> ?R'23 (ksPSpace s) s proof (prove)
goal (5 subgoals):
 1. \<And>rv erv rv'. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'\<rbrakk> \<Longrightarrow> (fst (lookupAround2 (ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0)) rv') = None \<longrightarrow> \<lbrace>?R'23 rv'\<rbrace> return () \<lbrace>\<lambda>rv s. rv' = ksPSpace s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s\<rbrace>) \<and> (\<forall>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0)) rv') = Some (a, b)) \<longrightarrow> \<lbrace>?R'23 rv'\<rbrace> assert (a < ptr) \<lbrace>\<lambda>rv s. rv' = ksPSpace s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s\<rbrace>)
 2. \<And>rv erv rv' s. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'; ?R'23 rv' s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case fst (lookupAround2 (ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0)) rv') of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr) \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>rv erv rv'. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'; True\<rbrakk> \<Longrightarrow> no_fail (?R'23 rv') (case fst (lookupAround2 (ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0)) rv') of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr))
 4. \<And>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s \<Longrightarrow> ((\<lambda>a. kheap s = kheap a \<and> ekheap s = ekheap a \<and> valid_pspace a \<and> pspace_no_overlap (up_aligned_area ptr sz) a \<and> valid_mdb a \<and> valid_etcbs a \<and> valid_list a) and (\<lambda>a. True)) s
 5. \<And>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<Longrightarrow> ?R'23 (ksPSpace s) s proof (prove)
goal (6 subgoals):
 1. \<And>rv erv rv'. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'; fst (lookupAround2 (ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0)) rv') = None\<rbrakk> \<Longrightarrow> \<lbrace>?R'23 rv'\<rbrace> return () \<lbrace>\<lambda>rv s. rv' = ksPSpace s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s\<rbrace>
 2. \<And>rv erv rv'. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'\<rbrakk> \<Longrightarrow> \<forall>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0)) rv') = Some (a, b)) \<longrightarrow> \<lbrace>?R'23 rv'\<rbrace> assert (a < ptr) \<lbrace>\<lambda>rv s. rv' = ksPSpace s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s\<rbrace>
 3. \<And>rv erv rv' s. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'; ?R'23 rv' s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case fst (lookupAround2 (ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0)) rv') of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr) \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>rv erv rv'. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'; True\<rbrakk> \<Longrightarrow> no_fail (?R'23 rv') (case fst (lookupAround2 (ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0)) rv') of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr))
 5. \<And>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s \<Longrightarrow> ((\<lambda>a. kheap s = kheap a \<and> ekheap s = ekheap a \<and> valid_pspace a \<and> pspace_no_overlap (up_aligned_area ptr sz) a \<and> valid_mdb a \<and> valid_etcbs a \<and> valid_list a) and (\<lambda>a. True)) s
 6. \<And>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<Longrightarrow> ?R'23 (ksPSpace s) s proof (prove)
goal (4 subgoals):
 1. \<And>rv erv s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case fst (lookupAround2 (ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0)) (ksPSpace s)) of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr) \<lbrace>\<lambda>r. (=) s\<rbrace>
 2. \<And>rv erv rv'. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'; True\<rbrakk> \<Longrightarrow> no_fail (\<lambda>a. rv' = ksPSpace a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> pspace_no_overlap' ptr sz a) (case fst (lookupAround2 (ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0)) rv') of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr))
 3. \<And>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s \<Longrightarrow> ((\<lambda>a. kheap s = kheap a \<and> ekheap s = ekheap a \<and> valid_pspace a \<and> pspace_no_overlap (up_aligned_area ptr sz) a \<and> valid_mdb a \<and> valid_etcbs a \<and> valid_list a) and (\<lambda>a. True)) s
 4. \<And>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<Longrightarrow> ksPSpace s = ksPSpace s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s proof (prove)
goal (4 subgoals):
 1. \<And>rv erv s a b. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; fst (lookupAround2 (ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0)) (ksPSpace s)) = Some (a, b)\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> assert (a < ptr) \<lbrace>\<lambda>r. (=) s\<rbrace>
 2. \<And>rv erv rv'. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'; True\<rbrakk> \<Longrightarrow> no_fail (\<lambda>a. rv' = ksPSpace a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> pspace_no_overlap' ptr sz a) (case fst (lookupAround2 (ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0)) rv') of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr))
 3. \<And>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s \<Longrightarrow> ((\<lambda>a. kheap s = kheap a \<and> ekheap s = ekheap a \<and> valid_pspace a \<and> pspace_no_overlap (up_aligned_area ptr sz) a \<and> valid_mdb a \<and> valid_etcbs a \<and> valid_list a) and (\<lambda>a. True)) s
 4. \<And>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<Longrightarrow> ksPSpace s = ksPSpace s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s proof (prove)
goal (3 subgoals):
 1. \<And>rv erv rv'. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'; True\<rbrakk> \<Longrightarrow> no_fail (\<lambda>a. rv' = ksPSpace a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> pspace_no_overlap' ptr sz a) (case fst (lookupAround2 (ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0)) rv') of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr))
 2. \<And>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s \<Longrightarrow> ((\<lambda>a. kheap s = kheap a \<and> ekheap s = ekheap a \<and> valid_pspace a \<and> pspace_no_overlap (up_aligned_area ptr sz) a \<and> valid_mdb a \<and> valid_etcbs a \<and> valid_list a) and (\<lambda>a. True)) s
 3. \<And>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<Longrightarrow> ksPSpace s = ksPSpace s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s proof (prove)
goal (3 subgoals):
 1. \<And>rv erv rv'. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'\<rbrakk> \<Longrightarrow> (fst (lookupAround2 (ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0)) rv') = None \<longrightarrow> no_fail (\<lambda>a. rv' = ksPSpace a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> pspace_no_overlap' ptr sz a) (return ())) \<and> (\<forall>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0)) rv') = Some (a, b)) \<longrightarrow> no_fail (\<lambda>a. rv' = ksPSpace a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> pspace_no_overlap' ptr sz a) (assert (a < ptr)))
 2. \<And>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s \<Longrightarrow> ((\<lambda>a. kheap s = kheap a \<and> ekheap s = ekheap a \<and> valid_pspace a \<and> pspace_no_overlap (up_aligned_area ptr sz) a \<and> valid_mdb a \<and> valid_etcbs a \<and> valid_list a) and (\<lambda>a. True)) s
 3. \<And>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<Longrightarrow> ksPSpace s = ksPSpace s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s proof (prove)
goal (4 subgoals):
 1. \<And>rv erv rv'. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'; fst (lookupAround2 (ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0)) rv') = None\<rbrakk> \<Longrightarrow> no_fail (\<lambda>a. rv' = ksPSpace a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> pspace_no_overlap' ptr sz a) (return ())
 2. \<And>rv erv rv'. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'\<rbrakk> \<Longrightarrow> \<forall>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0)) rv') = Some (a, b)) \<longrightarrow> no_fail (\<lambda>a. rv' = ksPSpace a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> pspace_no_overlap' ptr sz a) (assert (a < ptr))
 3. \<And>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s \<Longrightarrow> ((\<lambda>a. kheap s = kheap a \<and> ekheap s = ekheap a \<and> valid_pspace a \<and> pspace_no_overlap (up_aligned_area ptr sz) a \<and> valid_mdb a \<and> valid_etcbs a \<and> valid_list a) and (\<lambda>a. True)) s
 4. \<And>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<Longrightarrow> ksPSpace s = ksPSpace s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s proof (prove)
goal (3 subgoals):
 1. \<And>rv erv rv'. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'\<rbrakk> \<Longrightarrow> \<forall>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0)) rv') = Some (a, b)) \<longrightarrow> no_fail (\<lambda>a. rv' = ksPSpace a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> pspace_no_overlap' ptr sz a) (assert (a < ptr))
 2. \<And>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s \<Longrightarrow> ((\<lambda>a. kheap s = kheap a \<and> ekheap s = ekheap a \<and> valid_pspace a \<and> pspace_no_overlap (up_aligned_area ptr sz) a \<and> valid_mdb a \<and> valid_etcbs a \<and> valid_list a) and (\<lambda>a. True)) s
 3. \<And>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<Longrightarrow> ksPSpace s = ksPSpace s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s proof (prove)
goal (3 subgoals):
 1. \<And>rv erv rv' a b. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'; a \<le> ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0) \<longrightarrow> rv' z = None; rv' a = Some b\<rbrakk> \<Longrightarrow> no_fail (\<lambda>a. rv' = ksPSpace a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> pspace_no_overlap' ptr sz a) (assert (a < ptr))
 2. \<And>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s \<Longrightarrow> ((\<lambda>a. kheap s = kheap a \<and> ekheap s = ekheap a \<and> valid_pspace a \<and> pspace_no_overlap (up_aligned_area ptr sz) a \<and> valid_mdb a \<and> valid_etcbs a \<and> valid_list a) and (\<lambda>a. True)) s
 3. \<And>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<Longrightarrow> ksPSpace s = ksPSpace s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s proof (prove)
goal (3 subgoals):
 1. \<And>rv erv rv' a b s. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'; a \<le> ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n (obj_bits_api (APIType_map2 ty) us) - Suc 0) \<longrightarrow> rv' z = None; rv' a = Some b; rv' = ksPSpace s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s\<rbrakk> \<Longrightarrow> a < ptr
 2. \<And>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s \<Longrightarrow> ((\<lambda>a. kheap s = kheap a \<and> ekheap s = ekheap a \<and> valid_pspace a \<and> pspace_no_overlap (up_aligned_area ptr sz) a \<and> valid_mdb a \<and> valid_etcbs a \<and> valid_list a) and (\<lambda>a. True)) s
 3. \<And>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<Longrightarrow> ksPSpace s = ksPSpace s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s proof (prove)
goal (3 subgoals):
 1. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); a \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s\<rbrakk> \<Longrightarrow> a < ptr
 2. \<And>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s \<Longrightarrow> ((\<lambda>a. kheap s = kheap a \<and> ekheap s = ekheap a \<and> valid_pspace a \<and> pspace_no_overlap (up_aligned_area ptr sz) a \<and> valid_mdb a \<and> valid_etcbs a \<and> valid_list a) and (\<lambda>a. True)) s
 3. \<And>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<Longrightarrow> ksPSpace s = ksPSpace s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s proof (prove)
goal (3 subgoals):
 1. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); a \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}\<rbrakk> \<Longrightarrow> a < ptr
 2. \<And>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s \<Longrightarrow> ((\<lambda>a. kheap s = kheap a \<and> ekheap s = ekheap a \<and> valid_pspace a \<and> pspace_no_overlap (up_aligned_area ptr sz) a \<and> valid_mdb a \<and> valid_etcbs a \<and> valid_list a) and (\<lambda>a. True)) s
 3. \<And>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<Longrightarrow> ksPSpace s = ksPSpace s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s proof (prove)
goal (5 subgoals):
 1. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); a \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; \<not> a < ptr\<rbrakk> \<Longrightarrow> ?A188 rv erv a b s \<inter> ?B188 rv erv a b s = {}
 2. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); a \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; \<not> a < ptr\<rbrakk> \<Longrightarrow> a \<in> ?A188 rv erv a b s
 3. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); a \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; \<not> a < ptr\<rbrakk> \<Longrightarrow> a \<in> ?B188 rv erv a b s
 4. \<And>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s \<Longrightarrow> ((\<lambda>a. kheap s = kheap a \<and> ekheap s = ekheap a \<and> valid_pspace a \<and> pspace_no_overlap (up_aligned_area ptr sz) a \<and> valid_mdb a \<and> valid_etcbs a \<and> valid_list a) and (\<lambda>a. True)) s
 5. \<And>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<Longrightarrow> ksPSpace s = ksPSpace s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s proof (prove)
goal (4 subgoals):
 1. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); a \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; \<not> a < ptr\<rbrakk> \<Longrightarrow> a \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}
 2. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); a \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; \<not> a < ptr\<rbrakk> \<Longrightarrow> a \<in> dom (ksPSpace s)
 3. \<And>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s \<Longrightarrow> ((\<lambda>a. kheap s = kheap a \<and> ekheap s = ekheap a \<and> valid_pspace a \<and> pspace_no_overlap (up_aligned_area ptr sz) a \<and> valid_mdb a \<and> valid_etcbs a \<and> valid_list a) and (\<lambda>a. True)) s
 4. \<And>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<Longrightarrow> ksPSpace s = ksPSpace s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s proof (prove)
goal (4 subgoals):
 1. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); a \<le> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a\<rbrakk> \<Longrightarrow> a \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1
 2. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); a \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; \<not> a < ptr\<rbrakk> \<Longrightarrow> a \<in> dom (ksPSpace s)
 3. \<And>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s \<Longrightarrow> ((\<lambda>a. kheap s = kheap a \<and> ekheap s = ekheap a \<and> valid_pspace a \<and> pspace_no_overlap (up_aligned_area ptr sz) a \<and> valid_mdb a \<and> valid_etcbs a \<and> valid_list a) and (\<lambda>a. True)) s
 4. \<And>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<Longrightarrow> ksPSpace s = ksPSpace s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s proof (prove)
goal (4 subgoals):
 1. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a\<rbrakk> \<Longrightarrow> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1
 2. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); a \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; \<not> a < ptr\<rbrakk> \<Longrightarrow> a \<in> dom (ksPSpace s)
 3. \<And>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s \<Longrightarrow> ((\<lambda>a. kheap s = kheap a \<and> ekheap s = ekheap a \<and> valid_pspace a \<and> pspace_no_overlap (up_aligned_area ptr sz) a \<and> valid_mdb a \<and> valid_etcbs a \<and> valid_list a) and (\<lambda>a. True)) s
 4. \<And>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<Longrightarrow> ksPSpace s = ksPSpace s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s proof (prove)
goal (4 subgoals):
 1. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a\<rbrakk> \<Longrightarrow> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1)
 2. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); a \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; \<not> a < ptr\<rbrakk> \<Longrightarrow> a \<in> dom (ksPSpace s)
 3. \<And>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s \<Longrightarrow> ((\<lambda>a. kheap s = kheap a \<and> ekheap s = ekheap a \<and> valid_pspace a \<and> pspace_no_overlap (up_aligned_area ptr sz) a \<and> valid_mdb a \<and> valid_etcbs a \<and> valid_list a) and (\<lambda>a. True)) s
 4. \<And>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<Longrightarrow> ksPSpace s = ksPSpace s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s proof (prove)
goal (4 subgoals):
 1. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a\<rbrakk> \<Longrightarrow> (ptr && mask sz) + (ptr && ~~ mask sz) + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1)
 2. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); a \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; \<not> a < ptr\<rbrakk> \<Longrightarrow> a \<in> dom (ksPSpace s)
 3. \<And>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s \<Longrightarrow> ((\<lambda>a. kheap s = kheap a \<and> ekheap s = ekheap a \<and> valid_pspace a \<and> pspace_no_overlap (up_aligned_area ptr sz) a \<and> valid_mdb a \<and> valid_etcbs a \<and> valid_list a) and (\<lambda>a. True)) s
 4. \<And>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<Longrightarrow> ksPSpace s = ksPSpace s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s proof (prove)
goal (4 subgoals):
 1. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a\<rbrakk> \<Longrightarrow> (ptr && ~~ mask sz) + (ptr && mask sz) + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1)
 2. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); a \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; \<not> a < ptr\<rbrakk> \<Longrightarrow> a \<in> dom (ksPSpace s)
 3. \<And>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s \<Longrightarrow> ((\<lambda>a. kheap s = kheap a \<and> ekheap s = ekheap a \<and> valid_pspace a \<and> pspace_no_overlap (up_aligned_area ptr sz) a \<and> valid_mdb a \<and> valid_etcbs a \<and> valid_list a) and (\<lambda>a. True)) s
 4. \<And>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<Longrightarrow> ksPSpace s = ksPSpace s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s proof (prove)
goal (4 subgoals):
 1. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a\<rbrakk> \<Longrightarrow> (ptr && ~~ mask sz) + ((ptr && mask sz) + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0)) \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1)
 2. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); a \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; \<not> a < ptr\<rbrakk> \<Longrightarrow> a \<in> dom (ksPSpace s)
 3. \<And>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s \<Longrightarrow> ((\<lambda>a. kheap s = kheap a \<and> ekheap s = ekheap a \<and> valid_pspace a \<and> pspace_no_overlap (up_aligned_area ptr sz) a \<and> valid_mdb a \<and> valid_etcbs a \<and> valid_list a) and (\<lambda>a. True)) s
 4. \<And>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<Longrightarrow> ksPSpace s = ksPSpace s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s proof (prove)
goal (5 subgoals):
 1. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a\<rbrakk> \<Longrightarrow> (ptr && mask sz) + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<le> 2 ^ sz - 1
 2. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1)
 3. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); a \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; \<not> a < ptr\<rbrakk> \<Longrightarrow> a \<in> dom (ksPSpace s)
 4. \<And>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s \<Longrightarrow> ((\<lambda>a. kheap s = kheap a \<and> ekheap s = ekheap a \<and> valid_pspace a \<and> pspace_no_overlap (up_aligned_area ptr sz) a \<and> valid_mdb a \<and> valid_etcbs a \<and> valid_list a) and (\<lambda>a. True)) s
 5. \<And>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<Longrightarrow> ksPSpace s = ksPSpace s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s proof (prove)
using this:
range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n

goal (5 subgoals):
 1. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a\<rbrakk> \<Longrightarrow> (ptr && mask sz) + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<le> 2 ^ sz - 1
 2. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1)
 3. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); a \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; \<not> a < ptr\<rbrakk> \<Longrightarrow> a \<in> dom (ksPSpace s)
 4. \<And>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s \<Longrightarrow> ((\<lambda>a. kheap s = kheap a \<and> ekheap s = ekheap a \<and> valid_pspace a \<and> pspace_no_overlap (up_aligned_area ptr sz) a \<and> valid_mdb a \<and> valid_etcbs a \<and> valid_list a) and (\<lambda>a. True)) s
 5. \<And>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<Longrightarrow> ksPSpace s = ksPSpace s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s proof (prove)
goal (5 subgoals):
 1. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> (ptr && mask sz) + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<le> 2 ^ sz - 1
 2. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1)
 3. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); a \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; \<not> a < ptr; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> a \<in> dom (ksPSpace s)
 4. \<And>s. \<lbrakk>valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ((\<lambda>a. kheap s = kheap a \<and> ekheap s = ekheap a \<and> valid_pspace a \<and> pspace_no_overlap (up_aligned_area ptr sz) a \<and> valid_mdb a \<and> valid_etcbs a \<and> valid_list a) and (\<lambda>a. True)) s
 5. \<And>s. \<lbrakk>pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ksPSpace s = ksPSpace s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s proof (prove)
goal (5 subgoals):
 1. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> unat ((ptr && mask sz) + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0)) \<le> unat (2 ^ sz - 1)
 2. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1)
 3. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); a \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; \<not> a < ptr; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> a \<in> dom (ksPSpace s)
 4. \<And>s. \<lbrakk>valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ((\<lambda>a. kheap s = kheap a \<and> ekheap s = ekheap a \<and> valid_pspace a \<and> pspace_no_overlap (up_aligned_area ptr sz) a \<and> valid_mdb a \<and> valid_etcbs a \<and> valid_list a) and (\<lambda>a. True)) s
 5. \<And>s. \<lbrakk>pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ksPSpace s = ksPSpace s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s proof (prove)
goal (6 subgoals):
 1. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> Suc 0 \<le> 2 ^ (objBitsKO ko + gbits) * n
 2. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> unat ((ptr && mask sz) + (word_of_nat (2 ^ (objBitsKO ko + gbits) * n) - word_of_nat (Suc 0))) \<le> unat (2 ^ sz - 1)
 3. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1)
 4. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); a \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; \<not> a < ptr; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> a \<in> dom (ksPSpace s)
 5. \<And>s. \<lbrakk>valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ((\<lambda>a. kheap s = kheap a \<and> ekheap s = ekheap a \<and> valid_pspace a \<and> pspace_no_overlap (up_aligned_area ptr sz) a \<and> valid_mdb a \<and> valid_etcbs a \<and> valid_list a) and (\<lambda>a. True)) s
 6. \<And>s. \<lbrakk>pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ksPSpace s = ksPSpace s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s proof (prove)
using this:
n \<noteq> 0

goal (6 subgoals):
 1. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> Suc 0 \<le> 2 ^ (objBitsKO ko + gbits) * n
 2. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> unat ((ptr && mask sz) + (word_of_nat (2 ^ (objBitsKO ko + gbits) * n) - word_of_nat (Suc 0))) \<le> unat (2 ^ sz - 1)
 3. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1)
 4. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); a \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; \<not> a < ptr; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> a \<in> dom (ksPSpace s)
 5. \<And>s. \<lbrakk>valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ((\<lambda>a. kheap s = kheap a \<and> ekheap s = ekheap a \<and> valid_pspace a \<and> pspace_no_overlap (up_aligned_area ptr sz) a \<and> valid_mdb a \<and> valid_etcbs a \<and> valid_list a) and (\<lambda>a. True)) s
 6. \<And>s. \<lbrakk>pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ksPSpace s = ksPSpace s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s proof (prove)
goal (5 subgoals):
 1. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> unat ((ptr && mask sz) + (word_of_nat (2 ^ (objBitsKO ko + gbits) * n) - word_of_nat (Suc 0))) \<le> unat (2 ^ sz - 1)
 2. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1)
 3. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); a \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; \<not> a < ptr; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> a \<in> dom (ksPSpace s)
 4. \<And>s. \<lbrakk>valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ((\<lambda>a. kheap s = kheap a \<and> ekheap s = ekheap a \<and> valid_pspace a \<and> pspace_no_overlap (up_aligned_area ptr sz) a \<and> valid_mdb a \<and> valid_etcbs a \<and> valid_list a) and (\<lambda>a. True)) s
 5. \<And>s. \<lbrakk>pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ksPSpace s = ksPSpace s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s proof (prove)
goal (5 subgoals):
 1. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> unat (ptr && mask sz) + unat (word_of_nat (2 ^ (objBitsKO ko + gbits) * n) - word_of_nat (Suc 0)) \<le> unat (2 ^ sz - 1)
 2. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1)
 3. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); a \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; \<not> a < ptr; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> a \<in> dom (ksPSpace s)
 4. \<And>s. \<lbrakk>valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ((\<lambda>a. kheap s = kheap a \<and> ekheap s = ekheap a \<and> valid_pspace a \<and> pspace_no_overlap (up_aligned_area ptr sz) a \<and> valid_mdb a \<and> valid_etcbs a \<and> valid_list a) and (\<lambda>a. True)) s
 5. \<And>s. \<lbrakk>pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ksPSpace s = ksPSpace s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s proof (prove)
goal (5 subgoals):
 1. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> unat (ptr && mask sz) + unat (2 ^ (objBitsKO ko + gbits) * word_of_nat n - 1) \<le> unat (2 ^ sz - 1)
 2. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1)
 3. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); a \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; \<not> a < ptr; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> a \<in> dom (ksPSpace s)
 4. \<And>s. \<lbrakk>valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ((\<lambda>a. kheap s = kheap a \<and> ekheap s = ekheap a \<and> valid_pspace a \<and> pspace_no_overlap (up_aligned_area ptr sz) a \<and> valid_mdb a \<and> valid_etcbs a \<and> valid_list a) and (\<lambda>a. True)) s
 5. \<And>s. \<lbrakk>pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ksPSpace s = ksPSpace s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s proof (prove)
goal (6 subgoals):
 1. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> 2 ^ (objBitsKO ko + gbits) * word_of_nat n \<noteq> 0
 2. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> unat (ptr && mask sz) + (unat (2 ^ (objBitsKO ko + gbits) * word_of_nat n) - 1) \<le> unat (2 ^ sz - 1)
 3. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1)
 4. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); a \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; \<not> a < ptr; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> a \<in> dom (ksPSpace s)
 5. \<And>s. \<lbrakk>valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ((\<lambda>a. kheap s = kheap a \<and> ekheap s = ekheap a \<and> valid_pspace a \<and> pspace_no_overlap (up_aligned_area ptr sz) a \<and> valid_mdb a \<and> valid_etcbs a \<and> valid_list a) and (\<lambda>a. True)) s
 6. \<And>s. \<lbrakk>pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ksPSpace s = ksPSpace s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s proof (prove)
goal (6 subgoals):
 1. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> word_of_nat n * 2 ^ (objBitsKO ko + gbits) \<noteq> 0
 2. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> unat (ptr && mask sz) + (unat (2 ^ (objBitsKO ko + gbits) * word_of_nat n) - 1) \<le> unat (2 ^ sz - 1)
 3. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1)
 4. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); a \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; \<not> a < ptr; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> a \<in> dom (ksPSpace s)
 5. \<And>s. \<lbrakk>valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ((\<lambda>a. kheap s = kheap a \<and> ekheap s = ekheap a \<and> valid_pspace a \<and> pspace_no_overlap (up_aligned_area ptr sz) a \<and> valid_mdb a \<and> valid_etcbs a \<and> valid_list a) and (\<lambda>a. True)) s
 6. \<And>s. \<lbrakk>pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ksPSpace s = ksPSpace s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s proof (prove)
goal (8 subgoals):
 1. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> word_of_nat n < 2 ^ (word_bits - (objBitsKO ko + gbits))
 2. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> objBitsKO ko + gbits < word_bits
 3. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> word_of_nat n \<noteq> 0
 4. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> unat (ptr && mask sz) + (unat (2 ^ (objBitsKO ko + gbits) * word_of_nat n) - 1) \<le> unat (2 ^ sz - 1)
 5. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1)
 6. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); a \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; \<not> a < ptr; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> a \<in> dom (ksPSpace s)
 7. \<And>s. \<lbrakk>valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ((\<lambda>a. kheap s = kheap a \<and> ekheap s = ekheap a \<and> valid_pspace a \<and> pspace_no_overlap (up_aligned_area ptr sz) a \<and> valid_mdb a \<and> valid_etcbs a \<and> valid_list a) and (\<lambda>a. True)) s
 8. \<And>s. \<lbrakk>pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ksPSpace s = ksPSpace s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s proof (prove)
goal (8 subgoals):
 1. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> word_bits - (objBitsKO ko + gbits) < word_bits
 2. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> objBitsKO ko + gbits < word_bits
 3. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> word_of_nat n \<noteq> 0
 4. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> unat (ptr && mask sz) + (unat (2 ^ (objBitsKO ko + gbits) * word_of_nat n) - 1) \<le> unat (2 ^ sz - 1)
 5. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1)
 6. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); a \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; \<not> a < ptr; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> a \<in> dom (ksPSpace s)
 7. \<And>s. \<lbrakk>valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ((\<lambda>a. kheap s = kheap a \<and> ekheap s = ekheap a \<and> valid_pspace a \<and> pspace_no_overlap (up_aligned_area ptr sz) a \<and> valid_mdb a \<and> valid_etcbs a \<and> valid_list a) and (\<lambda>a. True)) s
 8. \<And>s. \<lbrakk>pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ksPSpace s = ksPSpace s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s proof (prove)
goal (7 subgoals):
 1. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> objBitsKO ko + gbits < word_bits
 2. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> word_of_nat n \<noteq> 0
 3. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> unat (ptr && mask sz) + (unat (2 ^ (objBitsKO ko + gbits) * word_of_nat n) - 1) \<le> unat (2 ^ sz - 1)
 4. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1)
 5. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); a \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; \<not> a < ptr; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> a \<in> dom (ksPSpace s)
 6. \<And>s. \<lbrakk>valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ((\<lambda>a. kheap s = kheap a \<and> ekheap s = ekheap a \<and> valid_pspace a \<and> pspace_no_overlap (up_aligned_area ptr sz) a \<and> valid_mdb a \<and> valid_etcbs a \<and> valid_list a) and (\<lambda>a. True)) s
 7. \<And>s. \<lbrakk>pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ksPSpace s = ksPSpace s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s proof (prove)
goal (6 subgoals):
 1. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> word_of_nat n \<noteq> 0
 2. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> unat (ptr && mask sz) + (unat (2 ^ (objBitsKO ko + gbits) * word_of_nat n) - 1) \<le> unat (2 ^ sz - 1)
 3. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1)
 4. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); a \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; \<not> a < ptr; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> a \<in> dom (ksPSpace s)
 5. \<And>s. \<lbrakk>valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ((\<lambda>a. kheap s = kheap a \<and> ekheap s = ekheap a \<and> valid_pspace a \<and> pspace_no_overlap (up_aligned_area ptr sz) a \<and> valid_mdb a \<and> valid_etcbs a \<and> valid_list a) and (\<lambda>a. True)) s
 6. \<And>s. \<lbrakk>pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ksPSpace s = ksPSpace s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s proof (prove)
goal (5 subgoals):
 1. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> unat (ptr && mask sz) + (unat (2 ^ (objBitsKO ko + gbits) * word_of_nat n) - 1) \<le> unat (2 ^ sz - 1)
 2. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1)
 3. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); a \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; \<not> a < ptr; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> a \<in> dom (ksPSpace s)
 4. \<And>s. \<lbrakk>valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ((\<lambda>a. kheap s = kheap a \<and> ekheap s = ekheap a \<and> valid_pspace a \<and> pspace_no_overlap (up_aligned_area ptr sz) a \<and> valid_mdb a \<and> valid_etcbs a \<and> valid_list a) and (\<lambda>a. True)) s
 5. \<And>s. \<lbrakk>pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ksPSpace s = ksPSpace s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s proof (prove)
goal (5 subgoals):
 1. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (n * 2 ^ (gbits + objBitsKO ko) - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> unat (ptr && mask sz) + (unat (word_of_nat n * 2 ^ (gbits + objBitsKO ko)) - Suc 0) \<le> unat (2 ^ sz - 1)
 2. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1)
 3. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); a \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; \<not> a < ptr; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> a \<in> dom (ksPSpace s)
 4. \<And>s. \<lbrakk>valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ((\<lambda>a. kheap s = kheap a \<and> ekheap s = ekheap a \<and> valid_pspace a \<and> pspace_no_overlap (up_aligned_area ptr sz) a \<and> valid_mdb a \<and> valid_etcbs a \<and> valid_list a) and (\<lambda>a. True)) s
 5. \<And>s. \<lbrakk>pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ksPSpace s = ksPSpace s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s proof (prove)
goal (6 subgoals):
 1. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (n * 2 ^ (gbits + objBitsKO ko) - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> sz < LENGTH(32)
 2. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (n * 2 ^ (gbits + objBitsKO ko) - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> unat (ptr && mask sz) + (unat (word_of_nat n * 2 ^ (gbits + objBitsKO ko)) - Suc 0) \<le> unat (2 ^ sz) - unat 1
 3. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1)
 4. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); a \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; \<not> a < ptr; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> a \<in> dom (ksPSpace s)
 5. \<And>s. \<lbrakk>valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ((\<lambda>a. kheap s = kheap a \<and> ekheap s = ekheap a \<and> valid_pspace a \<and> pspace_no_overlap (up_aligned_area ptr sz) a \<and> valid_mdb a \<and> valid_etcbs a \<and> valid_list a) and (\<lambda>a. True)) s
 6. \<And>s. \<lbrakk>pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ksPSpace s = ksPSpace s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s proof (prove)
goal (5 subgoals):
 1. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (n * 2 ^ (gbits + objBitsKO ko) - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> unat (ptr && mask sz) + (unat (word_of_nat n * 2 ^ (gbits + objBitsKO ko)) - Suc 0) \<le> unat (2 ^ sz) - unat 1
 2. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1)
 3. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); a \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; \<not> a < ptr; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> a \<in> dom (ksPSpace s)
 4. \<And>s. \<lbrakk>valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ((\<lambda>a. kheap s = kheap a \<and> ekheap s = ekheap a \<and> valid_pspace a \<and> pspace_no_overlap (up_aligned_area ptr sz) a \<and> valid_mdb a \<and> valid_etcbs a \<and> valid_list a) and (\<lambda>a. True)) s
 5. \<And>s. \<lbrakk>pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ksPSpace s = ksPSpace s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s proof (prove)
goal (6 subgoals):
 1. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (n * 2 ^ (gbits + objBitsKO ko) - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> Suc 0 \<le> unat (word_of_nat n * 2 ^ (gbits + objBitsKO ko))
 2. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (n * 2 ^ (gbits + objBitsKO ko) - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> unat (ptr && mask sz) + unat (word_of_nat n * 2 ^ (gbits + objBitsKO ko)) - Suc 0 \<le> unat (2 ^ sz) - unat 1
 3. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1)
 4. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); a \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; \<not> a < ptr; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> a \<in> dom (ksPSpace s)
 5. \<And>s. \<lbrakk>valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ((\<lambda>a. kheap s = kheap a \<and> ekheap s = ekheap a \<and> valid_pspace a \<and> pspace_no_overlap (up_aligned_area ptr sz) a \<and> valid_mdb a \<and> valid_etcbs a \<and> valid_list a) and (\<lambda>a. True)) s
 6. \<And>s. \<lbrakk>pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ksPSpace s = ksPSpace s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s proof (prove)
goal (5 subgoals):
 1. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (n * 2 ^ (gbits + objBitsKO ko) - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> unat (ptr && mask sz) + unat (word_of_nat n * 2 ^ (gbits + objBitsKO ko)) - Suc 0 \<le> unat (2 ^ sz) - unat 1
 2. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1)
 3. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); a \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; \<not> a < ptr; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> a \<in> dom (ksPSpace s)
 4. \<And>s. \<lbrakk>valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ((\<lambda>a. kheap s = kheap a \<and> ekheap s = ekheap a \<and> valid_pspace a \<and> pspace_no_overlap (up_aligned_area ptr sz) a \<and> valid_mdb a \<and> valid_etcbs a \<and> valid_list a) and (\<lambda>a. True)) s
 5. \<And>s. \<lbrakk>pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ksPSpace s = ksPSpace s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s proof (prove)
goal (5 subgoals):
 1. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (n * 2 ^ (gbits + objBitsKO ko) - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> unat (ptr && mask sz) + unat (word_of_nat n * 2 ^ (gbits + objBitsKO ko)) - Suc 0 \<le> unat (2 ^ sz) - Suc 0
 2. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1)
 3. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); a \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; \<not> a < ptr; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> a \<in> dom (ksPSpace s)
 4. \<And>s. \<lbrakk>valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ((\<lambda>a. kheap s = kheap a \<and> ekheap s = ekheap a \<and> valid_pspace a \<and> pspace_no_overlap (up_aligned_area ptr sz) a \<and> valid_mdb a \<and> valid_etcbs a \<and> valid_list a) and (\<lambda>a. True)) s
 5. \<And>s. \<lbrakk>pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ksPSpace s = ksPSpace s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s proof (prove)
goal (5 subgoals):
 1. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (n * 2 ^ (gbits + objBitsKO ko) - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> unat (ptr && mask sz) + unat (word_of_nat n * 2 ^ (gbits + objBitsKO ko)) \<le> unat (2 ^ sz)
 2. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1)
 3. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); a \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; \<not> a < ptr; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> a \<in> dom (ksPSpace s)
 4. \<And>s. \<lbrakk>valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ((\<lambda>a. kheap s = kheap a \<and> ekheap s = ekheap a \<and> valid_pspace a \<and> pspace_no_overlap (up_aligned_area ptr sz) a \<and> valid_mdb a \<and> valid_etcbs a \<and> valid_list a) and (\<lambda>a. True)) s
 5. \<And>s. \<lbrakk>pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ksPSpace s = ksPSpace s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s proof (prove)
goal (5 subgoals):
 1. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (n * 2 ^ (gbits + objBitsKO ko) - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a; range_cover ptr sz (objBitsKO ko + gbits) n; n * 2 ^ (objBitsKO ko + gbits) + unat (ptr && mask sz) \<le> 2 ^ sz\<rbrakk> \<Longrightarrow> unat (ptr && mask sz) + unat (word_of_nat n * 2 ^ (gbits + objBitsKO ko)) \<le> unat (2 ^ sz)
 2. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1)
 3. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); a \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; \<not> a < ptr; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> a \<in> dom (ksPSpace s)
 4. \<And>s. \<lbrakk>valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ((\<lambda>a. kheap s = kheap a \<and> ekheap s = ekheap a \<and> valid_pspace a \<and> pspace_no_overlap (up_aligned_area ptr sz) a \<and> valid_mdb a \<and> valid_etcbs a \<and> valid_list a) and (\<lambda>a. True)) s
 5. \<And>s. \<lbrakk>pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ksPSpace s = ksPSpace s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s proof (prove)
goal (5 subgoals):
 1. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (n * 2 ^ (gbits + objBitsKO ko) - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a; range_cover ptr sz (objBitsKO ko + gbits) n; n * 2 ^ (objBitsKO ko + gbits) + unat (ptr && mask sz) \<le> 2 ^ sz; obj_bits_api (APIType_map2 ty) us = objBitsKO ko + gbits; unat (word_of_nat n * 2 ^ (gbits + objBitsKO ko)) = n * 2 ^ (gbits + objBitsKO ko)\<rbrakk> \<Longrightarrow> unat (ptr && mask sz) + unat (word_of_nat n * 2 ^ (gbits + objBitsKO ko)) \<le> unat (2 ^ sz)
 2. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1)
 3. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); a \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; \<not> a < ptr; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> a \<in> dom (ksPSpace s)
 4. \<And>s. \<lbrakk>valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ((\<lambda>a. kheap s = kheap a \<and> ekheap s = ekheap a \<and> valid_pspace a \<and> pspace_no_overlap (up_aligned_area ptr sz) a \<and> valid_mdb a \<and> valid_etcbs a \<and> valid_list a) and (\<lambda>a. True)) s
 5. \<And>s. \<lbrakk>pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ksPSpace s = ksPSpace s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s proof (prove)
goal (4 subgoals):
 1. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1)
 2. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); a \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; \<not> a < ptr; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> a \<in> dom (ksPSpace s)
 3. \<And>s. \<lbrakk>valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ((\<lambda>a. kheap s = kheap a \<and> ekheap s = ekheap a \<and> valid_pspace a \<and> pspace_no_overlap (up_aligned_area ptr sz) a \<and> valid_mdb a \<and> valid_etcbs a \<and> valid_list a) and (\<lambda>a. True)) s
 4. \<And>s. \<lbrakk>pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ksPSpace s = ksPSpace s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s proof (prove)
goal (4 subgoals):
 1. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (2 ^ (objBitsKO ko + gbits) * n - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> a; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> 2 ^ sz - 1 < 2 ^ sz
 2. \<And>rv erv a b s. \<lbrakk>pspace_relation rv (ksPSpace s); ekheap_relation erv (ksPSpace s); a \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; pspace_no_overlap' ptr sz s; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; \<not> a < ptr; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> a \<in> dom (ksPSpace s)
 3. \<And>s. \<lbrakk>valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ((\<lambda>a. kheap s = kheap a \<and> ekheap s = ekheap a \<and> valid_pspace a \<and> pspace_no_overlap (up_aligned_area ptr sz) a \<and> valid_mdb a \<and> valid_etcbs a \<and> valid_list a) and (\<lambda>a. True)) s
 4. \<And>s. \<lbrakk>pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s; range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n\<rbrakk> \<Longrightarrow> ksPSpace s = ksPSpace s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s proof (prove)
goal:
No subgoals! proof (state)
this:
corres (\<lambda>rv rv'. rv' = g rv) (\<lambda>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s) (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) (retype_region2 ptr n us (APIType_map2 ty) dev) (do addrs <- createObjects ptr n ko gbits;
_ <- modify (update_gs (APIType_map2 ty) us (set addrs));
return (g addrs)
od)

goal:
No subgoals!