theory Retype_C

lemma ccorres_placeNewObject_captable:
  "ccorresG rf_sr \<Gamma> dc xfdc
   (pspace_aligned' and pspace_distinct' and pspace_no_overlap' regionBase (unat userSize + cteSizeBits)
      and (\<lambda>s. 2 ^ (unat userSize + cteSizeBits) \<le> gsMaxObjectSize s)
      and ret_zero regionBase (2 ^ (unat userSize + cteSizeBits))
      and K (regionBase \<noteq> 0 \<and> range_cover regionBase (unat userSize + cteSizeBits) (unat userSize + cteSizeBits) 1
      \<and> ({regionBase..+2 ^ (unat userSize + cteSizeBits)} \<inter> kernel_data_refs = {})))
    ({s. region_actually_is_zero_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) s})
    hs
    (placeNewObject regionBase (makeObject :: cte) (unat (userSize::word32)))
    (global_htd_update (\<lambda>_. (ptr_arr_retyps (2 ^ (unat userSize)) (cte_Ptr regionBase))))" apply (rule ccorres_from_vcg_nofail) apply clarsimp apply (rule conseqPre) apply vcg apply (clarsimp simp: rf_sr_htd_safe) apply (intro conjI allI impI) apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def
                         kernel_data_refs_domain_eq_rotate
                         ptr_array_retyps_htd_safe_neg
                         size_of_def power_add objBits_defs) apply (frule range_cover_rel[where sbit' = cteSizeBits]) apply simp apply simp apply (frule range_cover.unat_of_nat_shift[where gbits = cteSizeBits, OF _ le_refl le_refl]) apply (subgoal_tac "region_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x") apply (rule bexI [OF _ placeNewObject_eq]) apply (clarsimp simp: split_def new_cap_addrs_def) apply (cut_tac createObjects_ccorres_cte
                       [where ptr=regionBase and n="2 ^ unat userSize"
                          and sz="unat userSize + objBitsKO (KOCTE makeObject)"]) apply (erule_tac x=\<sigma> in allE, erule_tac x=x in allE) apply (clarsimp elim!:is_aligned_weaken simp: objBitsKO_def word_bits_def)+ apply (clarsimp simp: split_def objBitsKO_def
                            Fun.comp_def rf_sr_def Let_def
                            new_cap_addrs_def field_simps power_add ptr_retyps_gen_def
                   elim!: rsubst[where P="cstate_relation s'" for s']) apply (clarsimp simp: word_bits_conv range_cover_def) apply (clarsimp simp: objBitsKO_def range_cover.aligned) apply (clarsimp simp: no_fail_def) apply (simp add: region_actually_is_bytes) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (pspace_aligned' and pspace_distinct' and pspace_no_overlap' regionBase (unat userSize + cteSizeBits) and (\<lambda>s. 2 ^ (unat userSize + cteSizeBits) \<le> gsMaxObjectSize s) and (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {regionBase..+2 ^ (unat userSize + cteSizeBits)}) and K (regionBase \<noteq> 0 \<and> range_cover regionBase (unat userSize + cteSizeBits) (unat userSize + cteSizeBits) 1 \<and> {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<inter> kernel_data_refs = {})) {s. region_actually_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (2 ^ (unat userSize + cteSizeBits)) regionBase = replicate (2 ^ (unat userSize + cteSizeBits)) 0} hs (placeNewObject regionBase makeObject (unat userSize)) (Guard MemorySafety \<lbrace>htd_safe domain (hrs_htd \<acute>t_hrs) \<and> htd_safe domain (ptr_arr_retyps (2 ^ unat userSize) (cte_Ptr regionBase) (hrs_htd \<acute>t_hrs))\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_htd_update (ptr_arr_retyps (2 ^ unat userSize) (cte_Ptr regionBase))))) proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma>. \<Gamma>\<turnstile> {s. (pspace_aligned' and pspace_distinct' and pspace_no_overlap' regionBase (unat userSize + cteSizeBits) and (\<lambda>s. 2 ^ (unat userSize + cteSizeBits) \<le> gsMaxObjectSize s) and (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {regionBase..+2 ^ (unat userSize + cteSizeBits)}) and K (regionBase \<noteq> 0 \<and> range_cover regionBase (unat userSize + cteSizeBits) (unat userSize + cteSizeBits) 1 \<and> {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<inter> kernel_data_refs = {})) \<sigma> \<and> s \<in> {s. region_actually_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (2 ^ (unat userSize + cteSizeBits)) regionBase = replicate (2 ^ (unat userSize + cteSizeBits)) 0} \<and> (\<sigma>, s) \<in> rf_sr} Guard MemorySafety \<lbrace>htd_safe domain (hrs_htd \<acute>t_hrs) \<and> htd_safe domain (ptr_arr_retyps (2 ^ unat userSize) (cte_Ptr regionBase) (hrs_htd \<acute>t_hrs))\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_htd_update (ptr_arr_retyps (2 ^ unat userSize) (cte_Ptr regionBase)))) {s. \<not> snd (placeNewObject regionBase makeObject (unat userSize) \<sigma>) \<longrightarrow> (\<exists>(rv, \<sigma>')\<in>fst (placeNewObject regionBase makeObject (unat userSize) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s))} proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma>. \<Gamma>\<turnstile> {s. pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' regionBase (unat userSize + cteSizeBits) \<sigma> \<and> 2 ^ (unat userSize + cteSizeBits) \<le> gsMaxObjectSize \<sigma> \<and> valid_objs' \<sigma> \<and> untyped_ranges_zero' \<sigma> \<and> caps_overlap_reserved' {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<sigma> \<and> regionBase \<noteq> 0 \<and> range_cover regionBase (unat userSize + cteSizeBits) (unat userSize + cteSizeBits) (Suc 0) \<and> {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<inter> kernel_data_refs = {} \<and> region_actually_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (2 ^ (unat userSize + cteSizeBits)) regionBase = replicate (2 ^ (unat userSize + cteSizeBits)) 0 \<and> (\<sigma>, s) \<in> rf_sr} Guard MemorySafety \<lbrace>htd_safe domain (hrs_htd \<acute>t_hrs) \<and> htd_safe domain (ptr_arr_retyps (2 ^ unat userSize) (cte_Ptr regionBase) (hrs_htd \<acute>t_hrs))\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_htd_update (ptr_arr_retyps (2 ^ unat userSize) (cte_Ptr regionBase)))) {s. \<not> snd (placeNewObject regionBase makeObject (unat userSize) \<sigma>) \<longrightarrow> (\<exists>x\<in>fst (placeNewObject regionBase makeObject (unat userSize) \<sigma>). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', s) \<in> rf_sr)} proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma>. \<Gamma>\<turnstile> (?P'9 \<sigma>) Guard MemorySafety \<lbrace>htd_safe domain (hrs_htd \<acute>t_hrs) \<and> htd_safe domain (ptr_arr_retyps (2 ^ unat userSize) (cte_Ptr regionBase) (hrs_htd \<acute>t_hrs))\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_htd_update (ptr_arr_retyps (2 ^ unat userSize) (cte_Ptr regionBase)))) {s. \<not> snd (placeNewObject regionBase makeObject (unat userSize) \<sigma>) \<longrightarrow> (\<exists>x\<in>fst (placeNewObject regionBase makeObject (unat userSize) \<sigma>). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', s) \<in> rf_sr)}
 2. \<And>\<sigma>. {s. pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' regionBase (unat userSize + cteSizeBits) \<sigma> \<and> 2 ^ (unat userSize + cteSizeBits) \<le> gsMaxObjectSize \<sigma> \<and> valid_objs' \<sigma> \<and> untyped_ranges_zero' \<sigma> \<and> caps_overlap_reserved' {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<sigma> \<and> regionBase \<noteq> 0 \<and> range_cover regionBase (unat userSize + cteSizeBits) (unat userSize + cteSizeBits) (Suc 0) \<and> {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<inter> kernel_data_refs = {} \<and> region_actually_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (2 ^ (unat userSize + cteSizeBits)) regionBase = replicate (2 ^ (unat userSize + cteSizeBits)) 0 \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> ?P'9 \<sigma> proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma>. {s. pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' regionBase (unat userSize + cteSizeBits) \<sigma> \<and> 2 ^ (unat userSize + cteSizeBits) \<le> gsMaxObjectSize \<sigma> \<and> valid_objs' \<sigma> \<and> untyped_ranges_zero' \<sigma> \<and> caps_overlap_reserved' {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<sigma> \<and> regionBase \<noteq> 0 \<and> range_cover regionBase (unat userSize + cteSizeBits) (unat userSize + cteSizeBits) (Suc 0) \<and> {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<inter> kernel_data_refs = {} \<and> region_actually_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (2 ^ (unat userSize + cteSizeBits)) regionBase = replicate (2 ^ (unat userSize + cteSizeBits)) 0 \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. htd_safe domain (hrs_htd (t_hrs_' (globals s))) \<and> htd_safe domain (ptr_arr_retyps (2 ^ unat userSize) (cte_Ptr regionBase) (hrs_htd (t_hrs_' (globals s)))) \<and> (\<not> snd (placeNewObject regionBase makeObject (unat userSize) \<sigma>) \<longrightarrow> (\<exists>(rv, \<sigma>')\<in>fst (placeNewObject regionBase makeObject (unat userSize) \<sigma>). (\<sigma>', globals_update (t_hrs_'_update (hrs_htd_update (ptr_arr_retyps (2 ^ unat userSize) (cte_Ptr regionBase)))) s) \<in> rf_sr))} proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (unat userSize + cteSizeBits) \<sigma>; 2 ^ (unat userSize + cteSizeBits) \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<sigma>; regionBase \<noteq> 0; range_cover regionBase (unat userSize + cteSizeBits) (unat userSize + cteSizeBits) (Suc 0); {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (unat userSize + cteSizeBits)) regionBase = replicate (2 ^ (unat userSize + cteSizeBits)) 0; (\<sigma>, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> htd_safe domain (ptr_arr_retyps (2 ^ unat userSize) (cte_Ptr regionBase) (hrs_htd (t_hrs_' (globals x)))) \<and> (\<not> snd (placeNewObject regionBase makeObject (unat userSize) \<sigma>) \<longrightarrow> (\<exists>xa\<in>fst (placeNewObject regionBase makeObject (unat userSize) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', globals_update (t_hrs_'_update (hrs_htd_update (ptr_arr_retyps (2 ^ unat userSize) (cte_Ptr regionBase)))) x) \<in> rf_sr)) proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (unat userSize + cteSizeBits) \<sigma>; 2 ^ (unat userSize + cteSizeBits) \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<sigma>; regionBase \<noteq> 0; range_cover regionBase (unat userSize + cteSizeBits) (unat userSize + cteSizeBits) (Suc 0); {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (unat userSize + cteSizeBits)) regionBase = replicate (2 ^ (unat userSize + cteSizeBits)) 0; (\<sigma>, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> htd_safe domain (ptr_arr_retyps (2 ^ unat userSize) (cte_Ptr regionBase) (hrs_htd (t_hrs_' (globals x))))
 2. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (unat userSize + cteSizeBits) \<sigma>; 2 ^ (unat userSize + cteSizeBits) \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<sigma>; regionBase \<noteq> 0; range_cover regionBase (unat userSize + cteSizeBits) (unat userSize + cteSizeBits) (Suc 0); {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (unat userSize + cteSizeBits)) regionBase = replicate (2 ^ (unat userSize + cteSizeBits)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject (unat userSize) \<sigma>)\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (placeNewObject regionBase makeObject (unat userSize) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', globals_update (t_hrs_'_update (hrs_htd_update (ptr_arr_retyps (2 ^ unat userSize) (cte_Ptr regionBase)))) x) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (unat userSize + cteSizeBits) \<sigma>; 2 ^ (unat userSize + cteSizeBits) \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<sigma>; regionBase \<noteq> 0; range_cover regionBase (unat userSize + cteSizeBits) (unat userSize + cteSizeBits) (Suc 0); {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (unat userSize + cteSizeBits)) regionBase = replicate (2 ^ (unat userSize + cteSizeBits)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject (unat userSize) \<sigma>)\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (placeNewObject regionBase makeObject (unat userSize) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', globals_update (t_hrs_'_update (hrs_htd_update (ptr_arr_retyps (2 ^ unat userSize) (cte_Ptr regionBase)))) x) \<in> rf_sr proof (prove)
goal (3 subgoals):
 1. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (unat userSize + cteSizeBits) \<sigma>; 2 ^ (unat userSize + cteSizeBits) \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<sigma>; regionBase \<noteq> 0; range_cover regionBase (unat userSize + cteSizeBits) (unat userSize + cteSizeBits) (Suc 0); {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (unat userSize + cteSizeBits)) regionBase = replicate (2 ^ (unat userSize + cteSizeBits)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject (unat userSize) \<sigma>)\<rbrakk> \<Longrightarrow> cteSizeBits \<le> unat userSize + cteSizeBits
 2. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (unat userSize + cteSizeBits) \<sigma>; 2 ^ (unat userSize + cteSizeBits) \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<sigma>; regionBase \<noteq> 0; range_cover regionBase (unat userSize + cteSizeBits) (unat userSize + cteSizeBits) (Suc 0); {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (unat userSize + cteSizeBits)) regionBase = replicate (2 ^ (unat userSize + cteSizeBits)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject (unat userSize) \<sigma>)\<rbrakk> \<Longrightarrow> ?m35 \<sigma> x = 2 ^ (unat userSize + cteSizeBits - cteSizeBits) * Suc 0
 3. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (unat userSize + cteSizeBits) \<sigma>; 2 ^ (unat userSize + cteSizeBits) \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<sigma>; regionBase \<noteq> 0; range_cover regionBase (unat userSize + cteSizeBits) (unat userSize + cteSizeBits) (Suc 0); {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (unat userSize + cteSizeBits)) regionBase = replicate (2 ^ (unat userSize + cteSizeBits)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject (unat userSize) \<sigma>); range_cover regionBase (unat userSize + cteSizeBits) cteSizeBits (?m35 \<sigma> x)\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (placeNewObject regionBase makeObject (unat userSize) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', globals_update (t_hrs_'_update (hrs_htd_update (ptr_arr_retyps (2 ^ unat userSize) (cte_Ptr regionBase)))) x) \<in> rf_sr proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (unat userSize + cteSizeBits) \<sigma>; 2 ^ (unat userSize + cteSizeBits) \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<sigma>; regionBase \<noteq> 0; range_cover regionBase (unat userSize + cteSizeBits) (unat userSize + cteSizeBits) (Suc 0); {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (unat userSize + cteSizeBits)) regionBase = replicate (2 ^ (unat userSize + cteSizeBits)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject (unat userSize) \<sigma>)\<rbrakk> \<Longrightarrow> ?m35 \<sigma> x = 2 ^ (unat userSize + cteSizeBits - cteSizeBits) * Suc 0
 2. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (unat userSize + cteSizeBits) \<sigma>; 2 ^ (unat userSize + cteSizeBits) \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<sigma>; regionBase \<noteq> 0; range_cover regionBase (unat userSize + cteSizeBits) (unat userSize + cteSizeBits) (Suc 0); {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (unat userSize + cteSizeBits)) regionBase = replicate (2 ^ (unat userSize + cteSizeBits)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject (unat userSize) \<sigma>); range_cover regionBase (unat userSize + cteSizeBits) cteSizeBits (?m35 \<sigma> x)\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (placeNewObject regionBase makeObject (unat userSize) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', globals_update (t_hrs_'_update (hrs_htd_update (ptr_arr_retyps (2 ^ unat userSize) (cte_Ptr regionBase)))) x) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (unat userSize + cteSizeBits) \<sigma>; 2 ^ (unat userSize + cteSizeBits) \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<sigma>; regionBase \<noteq> 0; range_cover regionBase (unat userSize + cteSizeBits) (unat userSize + cteSizeBits) (Suc 0); {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (unat userSize + cteSizeBits)) regionBase = replicate (2 ^ (unat userSize + cteSizeBits)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject (unat userSize) \<sigma>); range_cover regionBase (unat userSize + cteSizeBits) cteSizeBits (2 ^ unat userSize)\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (placeNewObject regionBase makeObject (unat userSize) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', globals_update (t_hrs_'_update (hrs_htd_update (ptr_arr_retyps (2 ^ unat userSize) (cte_Ptr regionBase)))) x) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (unat userSize + cteSizeBits) \<sigma>; 2 ^ (unat userSize + cteSizeBits) \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<sigma>; regionBase \<noteq> 0; range_cover regionBase (unat userSize + cteSizeBits) (unat userSize + cteSizeBits) (Suc 0); {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (unat userSize + cteSizeBits)) regionBase = replicate (2 ^ (unat userSize + cteSizeBits)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject (unat userSize) \<sigma>); range_cover regionBase (unat userSize + cteSizeBits) cteSizeBits (2 ^ unat userSize); unat (word_of_nat (2 ^ unat userSize) * 2 ^ cteSizeBits) = 2 ^ unat userSize * 2 ^ cteSizeBits\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (placeNewObject regionBase makeObject (unat userSize) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', globals_update (t_hrs_'_update (hrs_htd_update (ptr_arr_retyps (2 ^ unat userSize) (cte_Ptr regionBase)))) x) \<in> rf_sr proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (unat userSize + cteSizeBits) \<sigma>; 2 ^ (unat userSize + cteSizeBits) \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<sigma>; regionBase \<noteq> 0; range_cover regionBase (unat userSize + cteSizeBits) (unat userSize + cteSizeBits) (Suc 0); {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (unat userSize + cteSizeBits)) regionBase = replicate (2 ^ (unat userSize + cteSizeBits)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject (unat userSize) \<sigma>); range_cover regionBase (unat userSize + cteSizeBits) cteSizeBits (2 ^ unat userSize); unat (word_of_nat (2 ^ unat userSize) * 2 ^ cteSizeBits) = 2 ^ unat userSize * 2 ^ cteSizeBits; region_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (placeNewObject regionBase makeObject (unat userSize) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', globals_update (t_hrs_'_update (hrs_htd_update (ptr_arr_retyps (2 ^ unat userSize) (cte_Ptr regionBase)))) x) \<in> rf_sr
 2. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (unat userSize + cteSizeBits) \<sigma>; 2 ^ (unat userSize + cteSizeBits) \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<sigma>; regionBase \<noteq> 0; range_cover regionBase (unat userSize + cteSizeBits) (unat userSize + cteSizeBits) (Suc 0); {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (unat userSize + cteSizeBits)) regionBase = replicate (2 ^ (unat userSize + cteSizeBits)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject (unat userSize) \<sigma>); range_cover regionBase (unat userSize + cteSizeBits) cteSizeBits (2 ^ unat userSize); unat (word_of_nat (2 ^ unat userSize) * 2 ^ cteSizeBits) = 2 ^ unat userSize * 2 ^ cteSizeBits\<rbrakk> \<Longrightarrow> region_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x proof (prove)
goal (5 subgoals):
 1. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (unat userSize + cteSizeBits) \<sigma>; 2 ^ (unat userSize + cteSizeBits) \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<sigma>; regionBase \<noteq> 0; range_cover regionBase (unat userSize + cteSizeBits) (unat userSize + cteSizeBits) (Suc 0); {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (unat userSize + cteSizeBits)) regionBase = replicate (2 ^ (unat userSize + cteSizeBits)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject (unat userSize) \<sigma>); range_cover regionBase (unat userSize + cteSizeBits) cteSizeBits (2 ^ unat userSize); unat (word_of_nat (2 ^ unat userSize) * 2 ^ cteSizeBits) = 2 ^ unat userSize * 2 ^ cteSizeBits; region_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x\<rbrakk> \<Longrightarrow> case ((), \<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (injectKOS makeObject)) (new_cap_addrs (2 ^ unat userSize) regionBase (injectKOS makeObject)) (ksPSpace \<sigma>)\<rparr>) of (rv, \<sigma>') \<Rightarrow> (\<sigma>', globals_update (t_hrs_'_update (hrs_htd_update (ptr_arr_retyps (2 ^ unat userSize) (cte_Ptr regionBase)))) x) \<in> rf_sr
 2. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (unat userSize + cteSizeBits) \<sigma>; 2 ^ (unat userSize + cteSizeBits) \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<sigma>; regionBase \<noteq> 0; range_cover regionBase (unat userSize + cteSizeBits) (unat userSize + cteSizeBits) (Suc 0); {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (unat userSize + cteSizeBits)) regionBase = replicate (2 ^ (unat userSize + cteSizeBits)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject (unat userSize) \<sigma>); range_cover regionBase (unat userSize + cteSizeBits) cteSizeBits (2 ^ unat userSize); unat (word_of_nat (2 ^ unat userSize) * 2 ^ cteSizeBits) = 2 ^ unat userSize * 2 ^ cteSizeBits; region_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x\<rbrakk> \<Longrightarrow> unat userSize < word_bits
 3. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (unat userSize + cteSizeBits) \<sigma>; 2 ^ (unat userSize + cteSizeBits) \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<sigma>; regionBase \<noteq> 0; range_cover regionBase (unat userSize + cteSizeBits) (unat userSize + cteSizeBits) (Suc 0); {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (unat userSize + cteSizeBits)) regionBase = replicate (2 ^ (unat userSize + cteSizeBits)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject (unat userSize) \<sigma>); range_cover regionBase (unat userSize + cteSizeBits) cteSizeBits (2 ^ unat userSize); unat (word_of_nat (2 ^ unat userSize) * 2 ^ cteSizeBits) = 2 ^ unat userSize * 2 ^ cteSizeBits; region_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x\<rbrakk> \<Longrightarrow> is_aligned regionBase (unat userSize + objBitsKO (injectKOS makeObject))
 4. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (unat userSize + cteSizeBits) \<sigma>; 2 ^ (unat userSize + cteSizeBits) \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<sigma>; regionBase \<noteq> 0; range_cover regionBase (unat userSize + cteSizeBits) (unat userSize + cteSizeBits) (Suc 0); {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (unat userSize + cteSizeBits)) regionBase = replicate (2 ^ (unat userSize + cteSizeBits)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject (unat userSize) \<sigma>); range_cover regionBase (unat userSize + cteSizeBits) cteSizeBits (2 ^ unat userSize); unat (word_of_nat (2 ^ unat userSize) * 2 ^ cteSizeBits) = 2 ^ unat userSize * 2 ^ cteSizeBits; region_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x\<rbrakk> \<Longrightarrow> no_fail ((=) \<sigma>) (placeNewObject regionBase makeObject (unat userSize))
 5. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (unat userSize + cteSizeBits) \<sigma>; 2 ^ (unat userSize + cteSizeBits) \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<sigma>; regionBase \<noteq> 0; range_cover regionBase (unat userSize + cteSizeBits) (unat userSize + cteSizeBits) (Suc 0); {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (unat userSize + cteSizeBits)) regionBase = replicate (2 ^ (unat userSize + cteSizeBits)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject (unat userSize) \<sigma>); range_cover regionBase (unat userSize + cteSizeBits) cteSizeBits (2 ^ unat userSize); unat (word_of_nat (2 ^ unat userSize) * 2 ^ cteSizeBits) = 2 ^ unat userSize * 2 ^ cteSizeBits\<rbrakk> \<Longrightarrow> region_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x proof (prove)
goal (5 subgoals):
 1. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (unat userSize + cteSizeBits) \<sigma>; 2 ^ (unat userSize + cteSizeBits) \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<sigma>; regionBase \<noteq> 0; range_cover regionBase (unat userSize + cteSizeBits) (unat userSize + cteSizeBits) (Suc 0); {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (unat userSize + cteSizeBits)) regionBase = replicate (2 ^ (unat userSize + cteSizeBits)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject (unat userSize) \<sigma>); range_cover regionBase (unat userSize + cteSizeBits) cteSizeBits (2 ^ unat userSize); unat (2 ^ unat userSize * 2 ^ cteSizeBits) = 2 ^ unat userSize * 2 ^ cteSizeBits; region_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x\<rbrakk> \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOCTE makeObject)) (map (\<lambda>p. regionBase + (word_of_nat p << objBitsKO (KOCTE makeObject))) [0..<2 ^ unat userSize]) (ksPSpace \<sigma>)\<rparr>, globals_update (t_hrs_'_update (hrs_htd_update (ptr_arr_retyps (2 ^ unat userSize) (cte_Ptr regionBase)))) x) \<in> rf_sr
 2. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (unat userSize + cteSizeBits) \<sigma>; 2 ^ (unat userSize + cteSizeBits) \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<sigma>; regionBase \<noteq> 0; range_cover regionBase (unat userSize + cteSizeBits) (unat userSize + cteSizeBits) (Suc 0); {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (unat userSize + cteSizeBits)) regionBase = replicate (2 ^ (unat userSize + cteSizeBits)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject (unat userSize) \<sigma>); range_cover regionBase (unat userSize + cteSizeBits) cteSizeBits (2 ^ unat userSize); unat (word_of_nat (2 ^ unat userSize) * 2 ^ cteSizeBits) = 2 ^ unat userSize * 2 ^ cteSizeBits; region_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x\<rbrakk> \<Longrightarrow> unat userSize < word_bits
 3. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (unat userSize + cteSizeBits) \<sigma>; 2 ^ (unat userSize + cteSizeBits) \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<sigma>; regionBase \<noteq> 0; range_cover regionBase (unat userSize + cteSizeBits) (unat userSize + cteSizeBits) (Suc 0); {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (unat userSize + cteSizeBits)) regionBase = replicate (2 ^ (unat userSize + cteSizeBits)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject (unat userSize) \<sigma>); range_cover regionBase (unat userSize + cteSizeBits) cteSizeBits (2 ^ unat userSize); unat (word_of_nat (2 ^ unat userSize) * 2 ^ cteSizeBits) = 2 ^ unat userSize * 2 ^ cteSizeBits; region_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x\<rbrakk> \<Longrightarrow> is_aligned regionBase (unat userSize + objBitsKO (injectKOS makeObject))
 4. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (unat userSize + cteSizeBits) \<sigma>; 2 ^ (unat userSize + cteSizeBits) \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<sigma>; regionBase \<noteq> 0; range_cover regionBase (unat userSize + cteSizeBits) (unat userSize + cteSizeBits) (Suc 0); {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (unat userSize + cteSizeBits)) regionBase = replicate (2 ^ (unat userSize + cteSizeBits)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject (unat userSize) \<sigma>); range_cover regionBase (unat userSize + cteSizeBits) cteSizeBits (2 ^ unat userSize); unat (word_of_nat (2 ^ unat userSize) * 2 ^ cteSizeBits) = 2 ^ unat userSize * 2 ^ cteSizeBits; region_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x\<rbrakk> \<Longrightarrow> no_fail ((=) \<sigma>) (placeNewObject regionBase makeObject (unat userSize))
 5. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (unat userSize + cteSizeBits) \<sigma>; 2 ^ (unat userSize + cteSizeBits) \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<sigma>; regionBase \<noteq> 0; range_cover regionBase (unat userSize + cteSizeBits) (unat userSize + cteSizeBits) (Suc 0); {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (unat userSize + cteSizeBits)) regionBase = replicate (2 ^ (unat userSize + cteSizeBits)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject (unat userSize) \<sigma>); range_cover regionBase (unat userSize + cteSizeBits) cteSizeBits (2 ^ unat userSize); unat (word_of_nat (2 ^ unat userSize) * 2 ^ cteSizeBits) = 2 ^ unat userSize * 2 ^ cteSizeBits\<rbrakk> \<Longrightarrow> region_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x proof (prove)
goal (5 subgoals):
 1. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (unat userSize + cteSizeBits) \<sigma>; 2 ^ (unat userSize + cteSizeBits) \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<sigma>; regionBase \<noteq> 0; range_cover regionBase (unat userSize + cteSizeBits) (unat userSize + cteSizeBits) (Suc 0); {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (unat userSize + cteSizeBits)) regionBase = replicate (2 ^ (unat userSize + cteSizeBits)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject (unat userSize) \<sigma>); range_cover regionBase (unat userSize + cteSizeBits) cteSizeBits (2 ^ unat userSize); unat (2 ^ unat userSize * 2 ^ cteSizeBits) = 2 ^ unat userSize * 2 ^ cteSizeBits; region_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x; \<forall>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> regionBase \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' regionBase (unat userSize + objBitsKO (KOCTE makeObject)) \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {regionBase..+2 ^ unat userSize * 2 ^ objBitsKO (KOCTE makeObject)}) \<sigma> \<and> (region_is_bytes regionBase (2 ^ unat userSize * 2 ^ objBitsKO (KOCTE makeObject)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ unat userSize * 2 ^ objBitsKO (KOCTE makeObject)) regionBase = replicate (2 ^ unat userSize * 2 ^ objBitsKO (KOCTE makeObject)) 0) \<and> range_cover regionBase (unat userSize + objBitsKO (KOCTE makeObject)) (objBitsKO (KOCTE makeObject)) (2 ^ unat userSize) \<and> {regionBase..+2 ^ unat userSize * 2 ^ objBitsKO (KOCTE makeObject)} \<inter> kernel_data_refs = {} \<longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOCTE makeObject)) (new_cap_addrs (2 ^ unat userSize) regionBase (KOCTE makeObject)) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen (2 ^ unat userSize) (cte_Ptr regionBase) True) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr\<rbrakk> \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOCTE makeObject)) (map (\<lambda>p. regionBase + (word_of_nat p << objBitsKO (KOCTE makeObject))) [0..<2 ^ unat userSize]) (ksPSpace \<sigma>)\<rparr>, globals_update (t_hrs_'_update (hrs_htd_update (ptr_arr_retyps (2 ^ unat userSize) (cte_Ptr regionBase)))) x) \<in> rf_sr
 2. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (unat userSize + cteSizeBits) \<sigma>; 2 ^ (unat userSize + cteSizeBits) \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<sigma>; regionBase \<noteq> 0; range_cover regionBase (unat userSize + cteSizeBits) (unat userSize + cteSizeBits) (Suc 0); {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (unat userSize + cteSizeBits)) regionBase = replicate (2 ^ (unat userSize + cteSizeBits)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject (unat userSize) \<sigma>); range_cover regionBase (unat userSize + cteSizeBits) cteSizeBits (2 ^ unat userSize); unat (word_of_nat (2 ^ unat userSize) * 2 ^ cteSizeBits) = 2 ^ unat userSize * 2 ^ cteSizeBits; region_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x\<rbrakk> \<Longrightarrow> unat userSize < word_bits
 3. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (unat userSize + cteSizeBits) \<sigma>; 2 ^ (unat userSize + cteSizeBits) \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<sigma>; regionBase \<noteq> 0; range_cover regionBase (unat userSize + cteSizeBits) (unat userSize + cteSizeBits) (Suc 0); {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (unat userSize + cteSizeBits)) regionBase = replicate (2 ^ (unat userSize + cteSizeBits)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject (unat userSize) \<sigma>); range_cover regionBase (unat userSize + cteSizeBits) cteSizeBits (2 ^ unat userSize); unat (word_of_nat (2 ^ unat userSize) * 2 ^ cteSizeBits) = 2 ^ unat userSize * 2 ^ cteSizeBits; region_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x\<rbrakk> \<Longrightarrow> is_aligned regionBase (unat userSize + objBitsKO (injectKOS makeObject))
 4. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (unat userSize + cteSizeBits) \<sigma>; 2 ^ (unat userSize + cteSizeBits) \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<sigma>; regionBase \<noteq> 0; range_cover regionBase (unat userSize + cteSizeBits) (unat userSize + cteSizeBits) (Suc 0); {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (unat userSize + cteSizeBits)) regionBase = replicate (2 ^ (unat userSize + cteSizeBits)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject (unat userSize) \<sigma>); range_cover regionBase (unat userSize + cteSizeBits) cteSizeBits (2 ^ unat userSize); unat (word_of_nat (2 ^ unat userSize) * 2 ^ cteSizeBits) = 2 ^ unat userSize * 2 ^ cteSizeBits; region_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x\<rbrakk> \<Longrightarrow> no_fail ((=) \<sigma>) (placeNewObject regionBase makeObject (unat userSize))
 5. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (unat userSize + cteSizeBits) \<sigma>; 2 ^ (unat userSize + cteSizeBits) \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<sigma>; regionBase \<noteq> 0; range_cover regionBase (unat userSize + cteSizeBits) (unat userSize + cteSizeBits) (Suc 0); {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (unat userSize + cteSizeBits)) regionBase = replicate (2 ^ (unat userSize + cteSizeBits)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject (unat userSize) \<sigma>); range_cover regionBase (unat userSize + cteSizeBits) cteSizeBits (2 ^ unat userSize); unat (word_of_nat (2 ^ unat userSize) * 2 ^ cteSizeBits) = 2 ^ unat userSize * 2 ^ cteSizeBits\<rbrakk> \<Longrightarrow> region_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x proof (prove)
goal (5 subgoals):
 1. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (unat userSize + cteSizeBits) \<sigma>; 2 ^ (unat userSize + cteSizeBits) \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<sigma>; regionBase \<noteq> 0; range_cover regionBase (unat userSize + cteSizeBits) (unat userSize + cteSizeBits) (Suc 0); {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (unat userSize + cteSizeBits)) regionBase = replicate (2 ^ (unat userSize + cteSizeBits)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject (unat userSize) \<sigma>); range_cover regionBase (unat userSize + cteSizeBits) cteSizeBits (2 ^ unat userSize); unat (2 ^ unat userSize * 2 ^ cteSizeBits) = 2 ^ unat userSize * 2 ^ cteSizeBits; region_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x; (\<sigma>, x) \<in> rf_sr \<and> regionBase \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' regionBase (unat userSize + objBitsKO (KOCTE makeObject)) \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {regionBase..+2 ^ unat userSize * 2 ^ objBitsKO (KOCTE makeObject)}) \<sigma> \<and> (region_is_bytes regionBase (2 ^ unat userSize * 2 ^ objBitsKO (KOCTE makeObject)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ unat userSize * 2 ^ objBitsKO (KOCTE makeObject)) regionBase = replicate (2 ^ unat userSize * 2 ^ objBitsKO (KOCTE makeObject)) 0) \<and> range_cover regionBase (unat userSize + objBitsKO (KOCTE makeObject)) (objBitsKO (KOCTE makeObject)) (2 ^ unat userSize) \<and> {regionBase..+2 ^ unat userSize * 2 ^ objBitsKO (KOCTE makeObject)} \<inter> kernel_data_refs = {} \<longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOCTE makeObject)) (new_cap_addrs (2 ^ unat userSize) regionBase (KOCTE makeObject)) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen (2 ^ unat userSize) (cte_Ptr regionBase) True) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr\<rbrakk> \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOCTE makeObject)) (map (\<lambda>p. regionBase + (word_of_nat p << objBitsKO (KOCTE makeObject))) [0..<2 ^ unat userSize]) (ksPSpace \<sigma>)\<rparr>, globals_update (t_hrs_'_update (hrs_htd_update (ptr_arr_retyps (2 ^ unat userSize) (cte_Ptr regionBase)))) x) \<in> rf_sr
 2. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (unat userSize + cteSizeBits) \<sigma>; 2 ^ (unat userSize + cteSizeBits) \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<sigma>; regionBase \<noteq> 0; range_cover regionBase (unat userSize + cteSizeBits) (unat userSize + cteSizeBits) (Suc 0); {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (unat userSize + cteSizeBits)) regionBase = replicate (2 ^ (unat userSize + cteSizeBits)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject (unat userSize) \<sigma>); range_cover regionBase (unat userSize + cteSizeBits) cteSizeBits (2 ^ unat userSize); unat (word_of_nat (2 ^ unat userSize) * 2 ^ cteSizeBits) = 2 ^ unat userSize * 2 ^ cteSizeBits; region_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x\<rbrakk> \<Longrightarrow> unat userSize < word_bits
 3. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (unat userSize + cteSizeBits) \<sigma>; 2 ^ (unat userSize + cteSizeBits) \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<sigma>; regionBase \<noteq> 0; range_cover regionBase (unat userSize + cteSizeBits) (unat userSize + cteSizeBits) (Suc 0); {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (unat userSize + cteSizeBits)) regionBase = replicate (2 ^ (unat userSize + cteSizeBits)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject (unat userSize) \<sigma>); range_cover regionBase (unat userSize + cteSizeBits) cteSizeBits (2 ^ unat userSize); unat (word_of_nat (2 ^ unat userSize) * 2 ^ cteSizeBits) = 2 ^ unat userSize * 2 ^ cteSizeBits; region_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x\<rbrakk> \<Longrightarrow> is_aligned regionBase (unat userSize + objBitsKO (injectKOS makeObject))
 4. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (unat userSize + cteSizeBits) \<sigma>; 2 ^ (unat userSize + cteSizeBits) \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<sigma>; regionBase \<noteq> 0; range_cover regionBase (unat userSize + cteSizeBits) (unat userSize + cteSizeBits) (Suc 0); {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (unat userSize + cteSizeBits)) regionBase = replicate (2 ^ (unat userSize + cteSizeBits)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject (unat userSize) \<sigma>); range_cover regionBase (unat userSize + cteSizeBits) cteSizeBits (2 ^ unat userSize); unat (word_of_nat (2 ^ unat userSize) * 2 ^ cteSizeBits) = 2 ^ unat userSize * 2 ^ cteSizeBits; region_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x\<rbrakk> \<Longrightarrow> no_fail ((=) \<sigma>) (placeNewObject regionBase makeObject (unat userSize))
 5. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (unat userSize + cteSizeBits) \<sigma>; 2 ^ (unat userSize + cteSizeBits) \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<sigma>; regionBase \<noteq> 0; range_cover regionBase (unat userSize + cteSizeBits) (unat userSize + cteSizeBits) (Suc 0); {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (unat userSize + cteSizeBits)) regionBase = replicate (2 ^ (unat userSize + cteSizeBits)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject (unat userSize) \<sigma>); range_cover regionBase (unat userSize + cteSizeBits) cteSizeBits (2 ^ unat userSize); unat (word_of_nat (2 ^ unat userSize) * 2 ^ cteSizeBits) = 2 ^ unat userSize * 2 ^ cteSizeBits\<rbrakk> \<Longrightarrow> region_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x proof (prove)
goal (5 subgoals):
 1. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (unat userSize + cteSizeBits) \<sigma>; 2 ^ (unat userSize + cteSizeBits) \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<sigma>; regionBase \<noteq> 0; range_cover regionBase (unat userSize + cteSizeBits) (unat userSize + cteSizeBits) (Suc 0); {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (unat userSize + cteSizeBits)) regionBase = replicate (2 ^ (unat userSize + cteSizeBits)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject (unat userSize) \<sigma>); range_cover regionBase (unat userSize + cteSizeBits) cteSizeBits (2 ^ unat userSize); unat (2 ^ unat userSize * 2 ^ cteSizeBits) = 2 ^ unat userSize * 2 ^ cteSizeBits; region_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x; caps_overlap_reserved' {regionBase..+2 ^ unat userSize * 2 ^ cteSizeBits} \<sigma> \<and> region_is_bytes regionBase (2 ^ unat userSize * 2 ^ cteSizeBits) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ unat userSize * 2 ^ cteSizeBits) regionBase = replicate (2 ^ unat userSize * 2 ^ cteSizeBits) 0 \<and> {regionBase..+2 ^ unat userSize * 2 ^ cteSizeBits} \<inter> kernel_data_refs = {} \<longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOCTE makeObject)) (new_cap_addrs (2 ^ unat userSize) regionBase (KOCTE makeObject)) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen (2 ^ unat userSize) (cte_Ptr regionBase) True) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr\<rbrakk> \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOCTE makeObject)) (map (\<lambda>p. regionBase + (word_of_nat p << cteSizeBits)) [0..<2 ^ unat userSize]) (ksPSpace \<sigma>)\<rparr>, globals_update (t_hrs_'_update (hrs_htd_update (ptr_arr_retyps (2 ^ unat userSize) (cte_Ptr regionBase)))) x) \<in> rf_sr
 2. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (unat userSize + cteSizeBits) \<sigma>; 2 ^ (unat userSize + cteSizeBits) \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<sigma>; regionBase \<noteq> 0; range_cover regionBase (unat userSize + cteSizeBits) (unat userSize + cteSizeBits) (Suc 0); {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (unat userSize + cteSizeBits)) regionBase = replicate (2 ^ (unat userSize + cteSizeBits)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject (unat userSize) \<sigma>); range_cover regionBase (unat userSize + cteSizeBits) cteSizeBits (2 ^ unat userSize); unat (word_of_nat (2 ^ unat userSize) * 2 ^ cteSizeBits) = 2 ^ unat userSize * 2 ^ cteSizeBits; region_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x\<rbrakk> \<Longrightarrow> unat userSize < word_bits
 3. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (unat userSize + cteSizeBits) \<sigma>; 2 ^ (unat userSize + cteSizeBits) \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<sigma>; regionBase \<noteq> 0; range_cover regionBase (unat userSize + cteSizeBits) (unat userSize + cteSizeBits) (Suc 0); {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (unat userSize + cteSizeBits)) regionBase = replicate (2 ^ (unat userSize + cteSizeBits)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject (unat userSize) \<sigma>); range_cover regionBase (unat userSize + cteSizeBits) cteSizeBits (2 ^ unat userSize); unat (word_of_nat (2 ^ unat userSize) * 2 ^ cteSizeBits) = 2 ^ unat userSize * 2 ^ cteSizeBits; region_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x\<rbrakk> \<Longrightarrow> is_aligned regionBase (unat userSize + objBitsKO (injectKOS makeObject))
 4. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (unat userSize + cteSizeBits) \<sigma>; 2 ^ (unat userSize + cteSizeBits) \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<sigma>; regionBase \<noteq> 0; range_cover regionBase (unat userSize + cteSizeBits) (unat userSize + cteSizeBits) (Suc 0); {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (unat userSize + cteSizeBits)) regionBase = replicate (2 ^ (unat userSize + cteSizeBits)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject (unat userSize) \<sigma>); range_cover regionBase (unat userSize + cteSizeBits) cteSizeBits (2 ^ unat userSize); unat (word_of_nat (2 ^ unat userSize) * 2 ^ cteSizeBits) = 2 ^ unat userSize * 2 ^ cteSizeBits; region_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x\<rbrakk> \<Longrightarrow> no_fail ((=) \<sigma>) (placeNewObject regionBase makeObject (unat userSize))
 5. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (unat userSize + cteSizeBits) \<sigma>; 2 ^ (unat userSize + cteSizeBits) \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<sigma>; regionBase \<noteq> 0; range_cover regionBase (unat userSize + cteSizeBits) (unat userSize + cteSizeBits) (Suc 0); {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (unat userSize + cteSizeBits)) regionBase = replicate (2 ^ (unat userSize + cteSizeBits)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject (unat userSize) \<sigma>); range_cover regionBase (unat userSize + cteSizeBits) cteSizeBits (2 ^ unat userSize); unat (word_of_nat (2 ^ unat userSize) * 2 ^ cteSizeBits) = 2 ^ unat userSize * 2 ^ cteSizeBits\<rbrakk> \<Longrightarrow> region_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x proof (prove)
goal (4 subgoals):
 1. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (unat userSize + cteSizeBits) \<sigma>; 2 ^ (unat userSize + cteSizeBits) \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<sigma>; regionBase \<noteq> 0; range_cover regionBase (unat userSize + cteSizeBits) (unat userSize + cteSizeBits) (Suc 0); {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (unat userSize + cteSizeBits)) regionBase = replicate (2 ^ (unat userSize + cteSizeBits)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject (unat userSize) \<sigma>); range_cover regionBase (unat userSize + cteSizeBits) cteSizeBits (2 ^ unat userSize); unat (word_of_nat (2 ^ unat userSize) * 2 ^ cteSizeBits) = 2 ^ unat userSize * 2 ^ cteSizeBits; region_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x\<rbrakk> \<Longrightarrow> unat userSize < word_bits
 2. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (unat userSize + cteSizeBits) \<sigma>; 2 ^ (unat userSize + cteSizeBits) \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<sigma>; regionBase \<noteq> 0; range_cover regionBase (unat userSize + cteSizeBits) (unat userSize + cteSizeBits) (Suc 0); {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (unat userSize + cteSizeBits)) regionBase = replicate (2 ^ (unat userSize + cteSizeBits)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject (unat userSize) \<sigma>); range_cover regionBase (unat userSize + cteSizeBits) cteSizeBits (2 ^ unat userSize); unat (word_of_nat (2 ^ unat userSize) * 2 ^ cteSizeBits) = 2 ^ unat userSize * 2 ^ cteSizeBits; region_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x\<rbrakk> \<Longrightarrow> is_aligned regionBase (unat userSize + objBitsKO (injectKOS makeObject))
 3. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (unat userSize + cteSizeBits) \<sigma>; 2 ^ (unat userSize + cteSizeBits) \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<sigma>; regionBase \<noteq> 0; range_cover regionBase (unat userSize + cteSizeBits) (unat userSize + cteSizeBits) (Suc 0); {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (unat userSize + cteSizeBits)) regionBase = replicate (2 ^ (unat userSize + cteSizeBits)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject (unat userSize) \<sigma>); range_cover regionBase (unat userSize + cteSizeBits) cteSizeBits (2 ^ unat userSize); unat (word_of_nat (2 ^ unat userSize) * 2 ^ cteSizeBits) = 2 ^ unat userSize * 2 ^ cteSizeBits; region_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x\<rbrakk> \<Longrightarrow> no_fail ((=) \<sigma>) (placeNewObject regionBase makeObject (unat userSize))
 4. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (unat userSize + cteSizeBits) \<sigma>; 2 ^ (unat userSize + cteSizeBits) \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<sigma>; regionBase \<noteq> 0; range_cover regionBase (unat userSize + cteSizeBits) (unat userSize + cteSizeBits) (Suc 0); {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (unat userSize + cteSizeBits)) regionBase = replicate (2 ^ (unat userSize + cteSizeBits)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject (unat userSize) \<sigma>); range_cover regionBase (unat userSize + cteSizeBits) cteSizeBits (2 ^ unat userSize); unat (word_of_nat (2 ^ unat userSize) * 2 ^ cteSizeBits) = 2 ^ unat userSize * 2 ^ cteSizeBits\<rbrakk> \<Longrightarrow> region_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x proof (prove)
goal (3 subgoals):
 1. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (unat userSize + cteSizeBits) \<sigma>; 2 ^ (unat userSize + cteSizeBits) \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<sigma>; regionBase \<noteq> 0; range_cover regionBase (unat userSize + cteSizeBits) (unat userSize + cteSizeBits) (Suc 0); {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (unat userSize + cteSizeBits)) regionBase = replicate (2 ^ (unat userSize + cteSizeBits)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject (unat userSize) \<sigma>); range_cover regionBase (unat userSize + cteSizeBits) cteSizeBits (2 ^ unat userSize); unat (word_of_nat (2 ^ unat userSize) * 2 ^ cteSizeBits) = 2 ^ unat userSize * 2 ^ cteSizeBits; region_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x\<rbrakk> \<Longrightarrow> is_aligned regionBase (unat userSize + objBitsKO (injectKOS makeObject))
 2. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (unat userSize + cteSizeBits) \<sigma>; 2 ^ (unat userSize + cteSizeBits) \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<sigma>; regionBase \<noteq> 0; range_cover regionBase (unat userSize + cteSizeBits) (unat userSize + cteSizeBits) (Suc 0); {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (unat userSize + cteSizeBits)) regionBase = replicate (2 ^ (unat userSize + cteSizeBits)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject (unat userSize) \<sigma>); range_cover regionBase (unat userSize + cteSizeBits) cteSizeBits (2 ^ unat userSize); unat (word_of_nat (2 ^ unat userSize) * 2 ^ cteSizeBits) = 2 ^ unat userSize * 2 ^ cteSizeBits; region_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x\<rbrakk> \<Longrightarrow> no_fail ((=) \<sigma>) (placeNewObject regionBase makeObject (unat userSize))
 3. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (unat userSize + cteSizeBits) \<sigma>; 2 ^ (unat userSize + cteSizeBits) \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<sigma>; regionBase \<noteq> 0; range_cover regionBase (unat userSize + cteSizeBits) (unat userSize + cteSizeBits) (Suc 0); {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (unat userSize + cteSizeBits)) regionBase = replicate (2 ^ (unat userSize + cteSizeBits)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject (unat userSize) \<sigma>); range_cover regionBase (unat userSize + cteSizeBits) cteSizeBits (2 ^ unat userSize); unat (word_of_nat (2 ^ unat userSize) * 2 ^ cteSizeBits) = 2 ^ unat userSize * 2 ^ cteSizeBits\<rbrakk> \<Longrightarrow> region_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (unat userSize + cteSizeBits) \<sigma>; 2 ^ (unat userSize + cteSizeBits) \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<sigma>; regionBase \<noteq> 0; range_cover regionBase (unat userSize + cteSizeBits) (unat userSize + cteSizeBits) (Suc 0); {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (unat userSize + cteSizeBits)) regionBase = replicate (2 ^ (unat userSize + cteSizeBits)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject (unat userSize) \<sigma>); range_cover regionBase (unat userSize + cteSizeBits) cteSizeBits (2 ^ unat userSize); unat (word_of_nat (2 ^ unat userSize) * 2 ^ cteSizeBits) = 2 ^ unat userSize * 2 ^ cteSizeBits; region_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x\<rbrakk> \<Longrightarrow> no_fail ((=) \<sigma>) (placeNewObject regionBase makeObject (unat userSize))
 2. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (unat userSize + cteSizeBits) \<sigma>; 2 ^ (unat userSize + cteSizeBits) \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<sigma>; regionBase \<noteq> 0; range_cover regionBase (unat userSize + cteSizeBits) (unat userSize + cteSizeBits) (Suc 0); {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (unat userSize + cteSizeBits)) regionBase = replicate (2 ^ (unat userSize + cteSizeBits)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject (unat userSize) \<sigma>); range_cover regionBase (unat userSize + cteSizeBits) cteSizeBits (2 ^ unat userSize); unat (word_of_nat (2 ^ unat userSize) * 2 ^ cteSizeBits) = 2 ^ unat userSize * 2 ^ cteSizeBits\<rbrakk> \<Longrightarrow> region_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (unat userSize + cteSizeBits) \<sigma>; 2 ^ (unat userSize + cteSizeBits) \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<sigma>; regionBase \<noteq> 0; range_cover regionBase (unat userSize + cteSizeBits) (unat userSize + cteSizeBits) (Suc 0); {regionBase..+2 ^ (unat userSize + cteSizeBits)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (unat userSize + cteSizeBits)) regionBase = replicate (2 ^ (unat userSize + cteSizeBits)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject (unat userSize) \<sigma>); range_cover regionBase (unat userSize + cteSizeBits) cteSizeBits (2 ^ unat userSize); unat (word_of_nat (2 ^ unat userSize) * 2 ^ cteSizeBits) = 2 ^ unat userSize * 2 ^ cteSizeBits\<rbrakk> \<Longrightarrow> region_is_bytes regionBase (2 ^ (unat userSize + cteSizeBits)) x proof (prove)
goal:
No subgoals!