theory Retype_C

lemma ccorres_placeNewObject_endpoint:
  "ko = (makeObject :: endpoint)
   \<Longrightarrow> ccorresG rf_sr \<Gamma> dc xfdc
   (pspace_aligned' and pspace_distinct'
      and pspace_no_overlap' regionBase (objBits ko)
      and ret_zero regionBase (2 ^ objBits ko)
      and (\<lambda>s. 2 ^ (objBits ko) \<le> gsMaxObjectSize s)
      and K (regionBase \<noteq> 0 \<and> range_cover regionBase (objBits ko) (objBits ko) 1
      \<and> {regionBase..+ 2 ^ (objBits ko)} \<inter> kernel_data_refs = {}))
   ({s. region_actually_is_zero_bytes regionBase (2 ^ objBits ko) s})
    hs
    (placeNewObject regionBase ko 0)
    (global_htd_update (\<lambda>_. (ptr_retyp (ep_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
                         objBits_simps'
                         ptr_retyp_htd_safe_neg) apply (rule bexI [OF _ placeNewObject_eq]) apply (clarsimp simp: split_def) apply (clarsimp simp: new_cap_addrs_def) apply (cut_tac createObjects_ccorres_ep [where ptr=regionBase and n="1" and sz="objBitsKO (KOEndpoint 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 Let_def rf_sr_def new_cap_addrs_def
                           region_actually_is_bytes ptr_retyps_gen_def objBits_simps
                    elim!: rsubst[where P="cstate_relation s'" for s']) apply (clarsimp simp: word_bits_conv) apply (clarsimp simp: range_cover.aligned objBits_simps) apply (clarsimp simp: no_fail_def) done

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