theory Retype_C

lemma ccorres_placeNewObject_notification:
  "ccorresG rf_sr \<Gamma> dc xfdc
   (pspace_aligned' and pspace_distinct' and pspace_no_overlap' regionBase 4
      and (\<lambda>s. 2^ntfnSizeBits \<le> gsMaxObjectSize s)
      and ret_zero regionBase (2^ntfnSizeBits)
      and K (regionBase \<noteq> 0
      \<and> {regionBase..+2^ntfnSizeBits} \<inter> kernel_data_refs = {}
      \<and> range_cover regionBase ntfnSizeBits ntfnSizeBits 1))
   ({s. region_actually_is_zero_bytes regionBase (2^ntfnSizeBits) s})
    hs
    (placeNewObject regionBase (makeObject :: Structures_H.notification) 0)
    (global_htd_update (\<lambda>_. (ptr_retyp (ntfn_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_defs
                         ptr_retyp_htd_safe_neg) apply (rule bexI [OF _ placeNewObject_eq]) apply (clarsimp simp: split_def new_cap_addrs_def) apply (cut_tac createObjects_ccorres_ntfn [where ptr=regionBase and n="1" and sz="objBitsKO (KONotification 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 Let_def
                           Fun.comp_def rf_sr_def new_cap_addrs_def) apply (clarsimp simp: cstate_relation_def carch_state_relation_def split_def
                           Let_def cmachine_state_relation_def cpspace_relation_def
                           region_actually_is_bytes ptr_retyps_gen_def objBits_defs) apply (clarsimp simp: word_bits_conv) apply (clarsimp simp: objBits_simps range_cover.aligned) apply (clarsimp simp: no_fail_def) done

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