theory Retype_C

lemma placeNewObject_pde:
  "ccorresG rf_sr \<Gamma> dc xfdc
   (valid_global_refs' and pspace_aligned' and pspace_distinct' and pspace_no_overlap' regionBase 14
      and (\<lambda>s. 2 ^ 14 \<le> gsMaxObjectSize s)
      and ret_zero regionBase (2 ^ 14)
      and K (regionBase \<noteq> 0 \<and> range_cover regionBase 14 14 1
      \<and> ({regionBase..+2 ^ 14}
          \<inter> kernel_data_refs = {})
      ))
    ({s. region_actually_is_zero_bytes regionBase (2 ^ 14) s})
    hs
    (placeNewObject regionBase (makeObject :: pde) 12)
    (global_htd_update (\<lambda>_. (ptr_retyp (pd_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_retyp_htd_safe_neg) apply (frule range_cover_rel[where sbit' = 2]) apply simp+ apply (frule range_cover.unat_of_nat_shift[where gbits = 2 ]) apply simp+ apply (rule le_refl) apply (subgoal_tac "region_is_bytes regionBase 16384 x") apply (rule bexI [OF _ placeNewObject_eq]) apply (clarsimp simp: split_def new_cap_addrs_def) apply (cut_tac s=\<sigma> in createObjects_ccorres_pde [where ptr=regionBase and sz=14]) 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 archObjSize_def
          Fun.comp_def rf_sr_def Let_def ptr_retyps_gen_def
          new_cap_addrs_def field_simps power_add
          cong: globals.unfold_congs) apply (simp add:Int_ac pdBits_def pageBits_def pdeBits_def) apply (clarsimp simp: word_bits_conv range_cover_def archObjSize_def) apply (clarsimp simp: objBitsKO_def range_cover.aligned archObjSize_def pdeBits_def) 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 (valid_global_refs' and pspace_aligned' and pspace_distinct' and pspace_no_overlap' regionBase 14 and (\<lambda>s. 2 ^ 14 \<le> gsMaxObjectSize s) and (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {regionBase..+2 ^ 14}) and K (regionBase \<noteq> 0 \<and> range_cover regionBase 14 14 1 \<and> {regionBase..+2 ^ 14} \<inter> kernel_data_refs = {})) {s. region_actually_is_bytes regionBase (2 ^ 14) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (2 ^ 14) regionBase = replicate (2 ^ 14) 0} hs (placeNewObject regionBase makeObject 12) (Guard MemorySafety \<lbrace>htd_safe domain (hrs_htd \<acute>t_hrs) \<and> htd_safe domain (ptr_retyp (pd_Ptr regionBase) (hrs_htd \<acute>t_hrs))\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_htd_update (ptr_retyp (pd_Ptr regionBase))))) proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma>. \<Gamma>\<turnstile> {s. (valid_global_refs' and pspace_aligned' and pspace_distinct' and pspace_no_overlap' regionBase 14 and (\<lambda>s. 2 ^ 14 \<le> gsMaxObjectSize s) and (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {regionBase..+2 ^ 14}) and K (regionBase \<noteq> 0 \<and> range_cover regionBase 14 14 1 \<and> {regionBase..+2 ^ 14} \<inter> kernel_data_refs = {})) \<sigma> \<and> s \<in> {s. region_actually_is_bytes regionBase (2 ^ 14) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (2 ^ 14) regionBase = replicate (2 ^ 14) 0} \<and> (\<sigma>, s) \<in> rf_sr} Guard MemorySafety \<lbrace>htd_safe domain (hrs_htd \<acute>t_hrs) \<and> htd_safe domain (ptr_retyp (pd_Ptr regionBase) (hrs_htd \<acute>t_hrs))\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_htd_update (ptr_retyp (pd_Ptr regionBase)))) {s. \<not> snd (placeNewObject regionBase makeObject 12 \<sigma>) \<longrightarrow> (\<exists>(rv, \<sigma>')\<in>fst (placeNewObject regionBase makeObject 12 \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s))} proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma>. \<Gamma>\<turnstile> {s. valid_global_refs' \<sigma> \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' regionBase 14 \<sigma> \<and> 16384 \<le> gsMaxObjectSize \<sigma> \<and> valid_objs' \<sigma> \<and> untyped_ranges_zero' \<sigma> \<and> caps_overlap_reserved' {regionBase..+16384} \<sigma> \<and> regionBase \<noteq> 0 \<and> range_cover regionBase 14 14 (Suc 0) \<and> {regionBase..+16384} \<inter> kernel_data_refs = {} \<and> region_actually_is_bytes regionBase 16384 s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) 16384 regionBase = replicate 16384 0 \<and> (\<sigma>, s) \<in> rf_sr} Guard MemorySafety \<lbrace>htd_safe domain (hrs_htd \<acute>t_hrs) \<and> htd_safe domain (ptr_retyp (pd_Ptr regionBase) (hrs_htd \<acute>t_hrs))\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_htd_update (ptr_retyp (pd_Ptr regionBase)))) {s. \<not> snd (placeNewObject regionBase makeObject 12 \<sigma>) \<longrightarrow> (\<exists>x\<in>fst (placeNewObject regionBase makeObject 12 \<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 (pd_Ptr regionBase) (hrs_htd \<acute>t_hrs))\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_htd_update (ptr_retyp (pd_Ptr regionBase)))) {s. \<not> snd (placeNewObject regionBase makeObject 12 \<sigma>) \<longrightarrow> (\<exists>x\<in>fst (placeNewObject regionBase makeObject 12 \<sigma>). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', s) \<in> rf_sr)}
 2. \<And>\<sigma>. {s. valid_global_refs' \<sigma> \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' regionBase 14 \<sigma> \<and> 16384 \<le> gsMaxObjectSize \<sigma> \<and> valid_objs' \<sigma> \<and> untyped_ranges_zero' \<sigma> \<and> caps_overlap_reserved' {regionBase..+16384} \<sigma> \<and> regionBase \<noteq> 0 \<and> range_cover regionBase 14 14 (Suc 0) \<and> {regionBase..+16384} \<inter> kernel_data_refs = {} \<and> region_actually_is_bytes regionBase 16384 s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) 16384 regionBase = replicate 16384 0 \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> ?P'9 \<sigma> proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma>. {s. valid_global_refs' \<sigma> \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' regionBase 14 \<sigma> \<and> 16384 \<le> gsMaxObjectSize \<sigma> \<and> valid_objs' \<sigma> \<and> untyped_ranges_zero' \<sigma> \<and> caps_overlap_reserved' {regionBase..+16384} \<sigma> \<and> regionBase \<noteq> 0 \<and> range_cover regionBase 14 14 (Suc 0) \<and> {regionBase..+16384} \<inter> kernel_data_refs = {} \<and> region_actually_is_bytes regionBase 16384 s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) 16384 regionBase = replicate 16384 0 \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. htd_safe domain (hrs_htd (t_hrs_' (globals s))) \<and> htd_safe domain (ptr_retyp (pd_Ptr regionBase) (hrs_htd (t_hrs_' (globals s)))) \<and> (\<not> snd (placeNewObject regionBase makeObject 12 \<sigma>) \<longrightarrow> (\<exists>(rv, \<sigma>')\<in>fst (placeNewObject regionBase makeObject 12 \<sigma>). (\<sigma>', globals_update (t_hrs_'_update (hrs_htd_update (ptr_retyp (pd_Ptr regionBase)))) s) \<in> rf_sr))} proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x. \<lbrakk>valid_global_refs' \<sigma>; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase 14 \<sigma>; 16384 \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+16384} \<sigma>; regionBase \<noteq> 0; range_cover regionBase 14 14 (Suc 0); {regionBase..+16384} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase 16384 x; heap_list (hrs_mem (t_hrs_' (globals x))) 16384 regionBase = replicate 16384 0; (\<sigma>, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> htd_safe domain (ptr_retyp (pd_Ptr regionBase) (hrs_htd (t_hrs_' (globals x)))) \<and> (\<not> snd (placeNewObject regionBase makeObject 12 \<sigma>) \<longrightarrow> (\<exists>xa\<in>fst (placeNewObject regionBase makeObject 12 \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', globals_update (t_hrs_'_update (hrs_htd_update (ptr_retyp (pd_Ptr regionBase)))) x) \<in> rf_sr)) proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x. \<lbrakk>valid_global_refs' \<sigma>; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase 14 \<sigma>; 16384 \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+16384} \<sigma>; regionBase \<noteq> 0; range_cover regionBase 14 14 (Suc 0); {regionBase..+16384} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase 16384 x; heap_list (hrs_mem (t_hrs_' (globals x))) 16384 regionBase = replicate 16384 0; (\<sigma>, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> htd_safe domain (ptr_retyp (pd_Ptr regionBase) (hrs_htd (t_hrs_' (globals x))))
 2. \<And>\<sigma> x. \<lbrakk>valid_global_refs' \<sigma>; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase 14 \<sigma>; 16384 \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+16384} \<sigma>; regionBase \<noteq> 0; range_cover regionBase 14 14 (Suc 0); {regionBase..+16384} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase 16384 x; heap_list (hrs_mem (t_hrs_' (globals x))) 16384 regionBase = replicate 16384 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject 12 \<sigma>)\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (placeNewObject regionBase makeObject 12 \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', globals_update (t_hrs_'_update (hrs_htd_update (ptr_retyp (pd_Ptr regionBase)))) x) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x. \<lbrakk>valid_global_refs' \<sigma>; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase 14 \<sigma>; 16384 \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+16384} \<sigma>; regionBase \<noteq> 0; range_cover regionBase 14 14 (Suc 0); {regionBase..+16384} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase 16384 x; heap_list (hrs_mem (t_hrs_' (globals x))) 16384 regionBase = replicate 16384 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject 12 \<sigma>)\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (placeNewObject regionBase makeObject 12 \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', globals_update (t_hrs_'_update (hrs_htd_update (ptr_retyp (pd_Ptr regionBase)))) x) \<in> rf_sr proof (prove)
goal (3 subgoals):
 1. \<And>\<sigma> x. \<lbrakk>valid_global_refs' \<sigma>; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase 14 \<sigma>; 16384 \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+16384} \<sigma>; regionBase \<noteq> 0; range_cover regionBase 14 14 (Suc 0); {regionBase..+16384} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase 16384 x; heap_list (hrs_mem (t_hrs_' (globals x))) 16384 regionBase = replicate 16384 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject 12 \<sigma>)\<rbrakk> \<Longrightarrow> 2 \<le> 14
 2. \<And>\<sigma> x. \<lbrakk>valid_global_refs' \<sigma>; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase 14 \<sigma>; 16384 \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+16384} \<sigma>; regionBase \<noteq> 0; range_cover regionBase 14 14 (Suc 0); {regionBase..+16384} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase 16384 x; heap_list (hrs_mem (t_hrs_' (globals x))) 16384 regionBase = replicate 16384 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject 12 \<sigma>)\<rbrakk> \<Longrightarrow> ?m36 \<sigma> x = 2 ^ (14 - 2) * Suc 0
 3. \<And>\<sigma> x. \<lbrakk>valid_global_refs' \<sigma>; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase 14 \<sigma>; 16384 \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+16384} \<sigma>; regionBase \<noteq> 0; range_cover regionBase 14 14 (Suc 0); {regionBase..+16384} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase 16384 x; heap_list (hrs_mem (t_hrs_' (globals x))) 16384 regionBase = replicate 16384 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject 12 \<sigma>); range_cover regionBase 14 2 (?m36 \<sigma> x)\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (placeNewObject regionBase makeObject 12 \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', globals_update (t_hrs_'_update (hrs_htd_update (ptr_retyp (pd_Ptr regionBase)))) x) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x. \<lbrakk>valid_global_refs' \<sigma>; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase 14 \<sigma>; 16384 \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+16384} \<sigma>; regionBase \<noteq> 0; range_cover regionBase 14 14 (Suc 0); {regionBase..+16384} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase 16384 x; heap_list (hrs_mem (t_hrs_' (globals x))) 16384 regionBase = replicate 16384 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject 12 \<sigma>); range_cover regionBase 14 2 4096\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (placeNewObject regionBase makeObject 12 \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', globals_update (t_hrs_'_update (hrs_htd_update (ptr_retyp (pd_Ptr regionBase)))) x) \<in> rf_sr proof (prove)
goal (3 subgoals):
 1. \<And>\<sigma> x. \<lbrakk>valid_global_refs' \<sigma>; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase 14 \<sigma>; 16384 \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+16384} \<sigma>; regionBase \<noteq> 0; range_cover regionBase 14 14 (Suc 0); {regionBase..+16384} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase 16384 x; heap_list (hrs_mem (t_hrs_' (globals x))) 16384 regionBase = replicate 16384 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject 12 \<sigma>); range_cover regionBase 14 2 4096\<rbrakk> \<Longrightarrow> 2 \<le> 14
 2. \<And>\<sigma> x. \<lbrakk>valid_global_refs' \<sigma>; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase 14 \<sigma>; 16384 \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+16384} \<sigma>; regionBase \<noteq> 0; range_cover regionBase 14 14 (Suc 0); {regionBase..+16384} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase 16384 x; heap_list (hrs_mem (t_hrs_' (globals x))) 16384 regionBase = replicate 16384 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject 12 \<sigma>); range_cover regionBase 14 2 4096\<rbrakk> \<Longrightarrow> ?p41 \<sigma> x \<le> Suc 0
 3. \<And>\<sigma> x. \<lbrakk>valid_global_refs' \<sigma>; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase 14 \<sigma>; 16384 \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+16384} \<sigma>; regionBase \<noteq> 0; range_cover regionBase 14 14 (Suc 0); {regionBase..+16384} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase 16384 x; heap_list (hrs_mem (t_hrs_' (globals x))) 16384 regionBase = replicate 16384 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject 12 \<sigma>); range_cover regionBase 14 2 4096; unat (word_of_nat (?p41 \<sigma> x) * 2\<^sup>2) = ?p41 \<sigma> x * 2\<^sup>2\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (placeNewObject regionBase makeObject 12 \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', globals_update (t_hrs_'_update (hrs_htd_update (ptr_retyp (pd_Ptr regionBase)))) x) \<in> rf_sr proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x. \<lbrakk>valid_global_refs' \<sigma>; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase 14 \<sigma>; 16384 \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+16384} \<sigma>; regionBase \<noteq> 0; range_cover regionBase 14 14 (Suc 0); {regionBase..+16384} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase 16384 x; heap_list (hrs_mem (t_hrs_' (globals x))) 16384 regionBase = replicate 16384 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject 12 \<sigma>); range_cover regionBase 14 2 4096\<rbrakk> \<Longrightarrow> ?p41 \<sigma> x \<le> Suc 0
 2. \<And>\<sigma> x. \<lbrakk>valid_global_refs' \<sigma>; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase 14 \<sigma>; 16384 \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+16384} \<sigma>; regionBase \<noteq> 0; range_cover regionBase 14 14 (Suc 0); {regionBase..+16384} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase 16384 x; heap_list (hrs_mem (t_hrs_' (globals x))) 16384 regionBase = replicate 16384 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject 12 \<sigma>); range_cover regionBase 14 2 4096; unat (word_of_nat (?p41 \<sigma> x) * 2\<^sup>2) = ?p41 \<sigma> x * 2\<^sup>2\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (placeNewObject regionBase makeObject 12 \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', globals_update (t_hrs_'_update (hrs_htd_update (ptr_retyp (pd_Ptr regionBase)))) x) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x. \<lbrakk>valid_global_refs' \<sigma>; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase 14 \<sigma>; 16384 \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+16384} \<sigma>; regionBase \<noteq> 0; range_cover regionBase 14 14 (Suc 0); {regionBase..+16384} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase 16384 x; heap_list (hrs_mem (t_hrs_' (globals x))) 16384 regionBase = replicate 16384 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject 12 \<sigma>); range_cover regionBase 14 2 4096; unat (word_of_nat (Suc 0) * 2\<^sup>2) = Suc 0 * 2\<^sup>2\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (placeNewObject regionBase makeObject 12 \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', globals_update (t_hrs_'_update (hrs_htd_update (ptr_retyp (pd_Ptr regionBase)))) x) \<in> rf_sr proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x. \<lbrakk>valid_global_refs' \<sigma>; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase 14 \<sigma>; 16384 \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+16384} \<sigma>; regionBase \<noteq> 0; range_cover regionBase 14 14 (Suc 0); {regionBase..+16384} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase 16384 x; heap_list (hrs_mem (t_hrs_' (globals x))) 16384 regionBase = replicate 16384 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject 12 \<sigma>); range_cover regionBase 14 2 4096; unat (word_of_nat (Suc 0) * 2\<^sup>2) = Suc 0 * 2\<^sup>2; region_is_bytes regionBase 16384 x\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (placeNewObject regionBase makeObject 12 \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', globals_update (t_hrs_'_update (hrs_htd_update (ptr_retyp (pd_Ptr regionBase)))) x) \<in> rf_sr
 2. \<And>\<sigma> x. \<lbrakk>valid_global_refs' \<sigma>; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase 14 \<sigma>; 16384 \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+16384} \<sigma>; regionBase \<noteq> 0; range_cover regionBase 14 14 (Suc 0); {regionBase..+16384} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase 16384 x; heap_list (hrs_mem (t_hrs_' (globals x))) 16384 regionBase = replicate 16384 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject 12 \<sigma>); range_cover regionBase 14 2 4096; unat (word_of_nat (Suc 0) * 2\<^sup>2) = Suc 0 * 2\<^sup>2\<rbrakk> \<Longrightarrow> region_is_bytes regionBase 16384 x proof (prove)
goal (5 subgoals):
 1. \<And>\<sigma> x. \<lbrakk>valid_global_refs' \<sigma>; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase 14 \<sigma>; 16384 \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+16384} \<sigma>; regionBase \<noteq> 0; range_cover regionBase 14 14 (Suc 0); {regionBase..+16384} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase 16384 x; heap_list (hrs_mem (t_hrs_' (globals x))) 16384 regionBase = replicate 16384 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject 12 \<sigma>); range_cover regionBase 14 2 4096; unat (word_of_nat (Suc 0) * 2\<^sup>2) = Suc 0 * 2\<^sup>2; region_is_bytes regionBase 16384 x\<rbrakk> \<Longrightarrow> case ((), \<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (injectKOS makeObject)) (new_cap_addrs (2 ^ 12) regionBase (injectKOS makeObject)) (ksPSpace \<sigma>)\<rparr>) of (rv, \<sigma>') \<Rightarrow> (\<sigma>', globals_update (t_hrs_'_update (hrs_htd_update (ptr_retyp (pd_Ptr regionBase)))) x) \<in> rf_sr
 2. \<And>\<sigma> x. \<lbrakk>valid_global_refs' \<sigma>; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase 14 \<sigma>; 16384 \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+16384} \<sigma>; regionBase \<noteq> 0; range_cover regionBase 14 14 (Suc 0); {regionBase..+16384} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase 16384 x; heap_list (hrs_mem (t_hrs_' (globals x))) 16384 regionBase = replicate 16384 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject 12 \<sigma>); range_cover regionBase 14 2 4096; unat (word_of_nat (Suc 0) * 2\<^sup>2) = Suc 0 * 2\<^sup>2; region_is_bytes regionBase 16384 x\<rbrakk> \<Longrightarrow> 12 < word_bits
 3. \<And>\<sigma> x. \<lbrakk>valid_global_refs' \<sigma>; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase 14 \<sigma>; 16384 \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+16384} \<sigma>; regionBase \<noteq> 0; range_cover regionBase 14 14 (Suc 0); {regionBase..+16384} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase 16384 x; heap_list (hrs_mem (t_hrs_' (globals x))) 16384 regionBase = replicate 16384 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject 12 \<sigma>); range_cover regionBase 14 2 4096; unat (word_of_nat (Suc 0) * 2\<^sup>2) = Suc 0 * 2\<^sup>2; region_is_bytes regionBase 16384 x\<rbrakk> \<Longrightarrow> is_aligned regionBase (12 + objBitsKO (injectKOS makeObject))
 4. \<And>\<sigma> x. \<lbrakk>valid_global_refs' \<sigma>; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase 14 \<sigma>; 16384 \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+16384} \<sigma>; regionBase \<noteq> 0; range_cover regionBase 14 14 (Suc 0); {regionBase..+16384} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase 16384 x; heap_list (hrs_mem (t_hrs_' (globals x))) 16384 regionBase = replicate 16384 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject 12 \<sigma>); range_cover regionBase 14 2 4096; unat (word_of_nat (Suc 0) * 2\<^sup>2) = Suc 0 * 2\<^sup>2; region_is_bytes regionBase 16384 x\<rbrakk> \<Longrightarrow> no_fail ((=) \<sigma>) (placeNewObject regionBase makeObject 12)
 5. \<And>\<sigma> x. \<lbrakk>valid_global_refs' \<sigma>; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase 14 \<sigma>; 16384 \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+16384} \<sigma>; regionBase \<noteq> 0; range_cover regionBase 14 14 (Suc 0); {regionBase..+16384} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase 16384 x; heap_list (hrs_mem (t_hrs_' (globals x))) 16384 regionBase = replicate 16384 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject 12 \<sigma>); range_cover regionBase 14 2 4096; unat (word_of_nat (Suc 0) * 2\<^sup>2) = Suc 0 * 2\<^sup>2\<rbrakk> \<Longrightarrow> region_is_bytes regionBase 16384 x proof (prove)
goal (5 subgoals):
 1. \<And>\<sigma> x. \<lbrakk>valid_global_refs' \<sigma>; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase 14 \<sigma>; 16384 \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+16384} \<sigma>; regionBase \<noteq> 0; range_cover regionBase 14 14 (Suc 0); {regionBase..+16384} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase 16384 x; heap_list (hrs_mem (t_hrs_' (globals x))) 16384 regionBase = replicate 16384 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject 12 \<sigma>); range_cover regionBase 14 2 4096; region_is_bytes regionBase 16384 x\<rbrakk> \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOArch (KOPDE makeObject))) (map (\<lambda>p. regionBase + (word_of_nat p << objBitsKO (KOArch (KOPDE makeObject)))) [0..<4096]) (ksPSpace \<sigma>)\<rparr>, globals_update (t_hrs_'_update (hrs_htd_update (ptr_retyp (pd_Ptr regionBase)))) x) \<in> rf_sr
 2. \<And>\<sigma> x. \<lbrakk>valid_global_refs' \<sigma>; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase 14 \<sigma>; 16384 \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+16384} \<sigma>; regionBase \<noteq> 0; range_cover regionBase 14 14 (Suc 0); {regionBase..+16384} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase 16384 x; heap_list (hrs_mem (t_hrs_' (globals x))) 16384 regionBase = replicate 16384 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject 12 \<sigma>); range_cover regionBase 14 2 4096; unat (word_of_nat (Suc 0) * 2\<^sup>2) = Suc 0 * 2\<^sup>2; region_is_bytes regionBase 16384 x\<rbrakk> \<Longrightarrow> 12 < word_bits
 3. \<And>\<sigma> x. \<lbrakk>valid_global_refs' \<sigma>; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase 14 \<sigma>; 16384 \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+16384} \<sigma>; regionBase \<noteq> 0; range_cover regionBase 14 14 (Suc 0); {regionBase..+16384} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase 16384 x; heap_list (hrs_mem (t_hrs_' (globals x))) 16384 regionBase = replicate 16384 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject 12 \<sigma>); range_cover regionBase 14 2 4096; unat (word_of_nat (Suc 0) * 2\<^sup>2) = Suc 0 * 2\<^sup>2; region_is_bytes regionBase 16384 x\<rbrakk> \<Longrightarrow> is_aligned regionBase (12 + objBitsKO (injectKOS makeObject))
 4. \<And>\<sigma> x. \<lbrakk>valid_global_refs' \<sigma>; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase 14 \<sigma>; 16384 \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+16384} \<sigma>; regionBase \<noteq> 0; range_cover regionBase 14 14 (Suc 0); {regionBase..+16384} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase 16384 x; heap_list (hrs_mem (t_hrs_' (globals x))) 16384 regionBase = replicate 16384 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject 12 \<sigma>); range_cover regionBase 14 2 4096; unat (word_of_nat (Suc 0) * 2\<^sup>2) = Suc 0 * 2\<^sup>2; region_is_bytes regionBase 16384 x\<rbrakk> \<Longrightarrow> no_fail ((=) \<sigma>) (placeNewObject regionBase makeObject 12)
 5. \<And>\<sigma> x. \<lbrakk>valid_global_refs' \<sigma>; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase 14 \<sigma>; 16384 \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+16384} \<sigma>; regionBase \<noteq> 0; range_cover regionBase 14 14 (Suc 0); {regionBase..+16384} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase 16384 x; heap_list (hrs_mem (t_hrs_' (globals x))) 16384 regionBase = replicate 16384 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject 12 \<sigma>); range_cover regionBase 14 2 4096; unat (word_of_nat (Suc 0) * 2\<^sup>2) = Suc 0 * 2\<^sup>2\<rbrakk> \<Longrightarrow> region_is_bytes regionBase 16384 x proof (prove)
goal (5 subgoals):
 1. \<And>\<sigma> x. \<lbrakk>valid_global_refs' \<sigma>; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase 14 \<sigma>; 16384 \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+16384} \<sigma>; regionBase \<noteq> 0; range_cover regionBase 14 14 (Suc 0); {regionBase..+16384} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase 16384 x; heap_list (hrs_mem (t_hrs_' (globals x))) 16384 regionBase = replicate 16384 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject 12 \<sigma>); range_cover regionBase 14 2 4096; region_is_bytes regionBase 16384 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 14 \<sigma>' \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {regionBase..+2 ^ pdBits}) \<sigma>' \<and> (region_is_bytes regionBase (2 ^ pdBits) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ pdBits) regionBase = replicate (2 ^ pdBits) 0) \<and> range_cover regionBase 14 pdBits 1 \<and> valid_global_refs' \<sigma> \<and> kernel_data_refs \<inter> {regionBase..+2 ^ pdBits} = {} \<longrightarrow> (\<sigma>'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOArch (KOPDE makeObject))) (new_cap_addrs 4096 regionBase (KOArch (KOPDE makeObject))) (ksPSpace \<sigma>')\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr regionBase) False) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr\<rbrakk> \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOArch (KOPDE makeObject))) (map (\<lambda>p. regionBase + (word_of_nat p << objBitsKO (KOArch (KOPDE makeObject)))) [0..<4096]) (ksPSpace \<sigma>)\<rparr>, globals_update (t_hrs_'_update (hrs_htd_update (ptr_retyp (pd_Ptr regionBase)))) x) \<in> rf_sr
 2. \<And>\<sigma> x. \<lbrakk>valid_global_refs' \<sigma>; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase 14 \<sigma>; 16384 \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+16384} \<sigma>; regionBase \<noteq> 0; range_cover regionBase 14 14 (Suc 0); {regionBase..+16384} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase 16384 x; heap_list (hrs_mem (t_hrs_' (globals x))) 16384 regionBase = replicate 16384 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject 12 \<sigma>); range_cover regionBase 14 2 4096; unat (word_of_nat (Suc 0) * 2\<^sup>2) = Suc 0 * 2\<^sup>2; region_is_bytes regionBase 16384 x\<rbrakk> \<Longrightarrow> 12 < word_bits
 3. \<And>\<sigma> x. \<lbrakk>valid_global_refs' \<sigma>; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase 14 \<sigma>; 16384 \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+16384} \<sigma>; regionBase \<noteq> 0; range_cover regionBase 14 14 (Suc 0); {regionBase..+16384} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase 16384 x; heap_list (hrs_mem (t_hrs_' (globals x))) 16384 regionBase = replicate 16384 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject 12 \<sigma>); range_cover regionBase 14 2 4096; unat (word_of_nat (Suc 0) * 2\<^sup>2) = Suc 0 * 2\<^sup>2; region_is_bytes regionBase 16384 x\<rbrakk> \<Longrightarrow> is_aligned regionBase (12 + objBitsKO (injectKOS makeObject))
 4. \<And>\<sigma> x. \<lbrakk>valid_global_refs' \<sigma>; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase 14 \<sigma>; 16384 \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+16384} \<sigma>; regionBase \<noteq> 0; range_cover regionBase 14 14 (Suc 0); {regionBase..+16384} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase 16384 x; heap_list (hrs_mem (t_hrs_' (globals x))) 16384 regionBase = replicate 16384 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject 12 \<sigma>); range_cover regionBase 14 2 4096; unat (word_of_nat (Suc 0) * 2\<^sup>2) = Suc 0 * 2\<^sup>2; region_is_bytes regionBase 16384 x\<rbrakk> \<Longrightarrow> no_fail ((=) \<sigma>) (placeNewObject regionBase makeObject 12)
 5. \<And>\<sigma> x. \<lbrakk>valid_global_refs' \<sigma>; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase 14 \<sigma>; 16384 \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+16384} \<sigma>; regionBase \<noteq> 0; range_cover regionBase 14 14 (Suc 0); {regionBase..+16384} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase 16384 x; heap_list (hrs_mem (t_hrs_' (globals x))) 16384 regionBase = replicate 16384 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject 12 \<sigma>); range_cover regionBase 14 2 4096; unat (word_of_nat (Suc 0) * 2\<^sup>2) = Suc 0 * 2\<^sup>2\<rbrakk> \<Longrightarrow> region_is_bytes regionBase 16384 x proof (prove)
goal (5 subgoals):
 1. \<And>\<sigma> x. \<lbrakk>valid_global_refs' \<sigma>; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase 14 \<sigma>; 16384 \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+16384} \<sigma>; regionBase \<noteq> 0; range_cover regionBase 14 14 (Suc 0); {regionBase..+16384} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase 16384 x; heap_list (hrs_mem (t_hrs_' (globals x))) 16384 regionBase = replicate 16384 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject 12 \<sigma>); range_cover regionBase 14 2 4096; region_is_bytes regionBase 16384 x; (\<sigma>, x) \<in> rf_sr \<and> regionBase \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' regionBase 14 \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {regionBase..+2 ^ pdBits}) \<sigma> \<and> (region_is_bytes regionBase (2 ^ pdBits) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ pdBits) regionBase = replicate (2 ^ pdBits) 0) \<and> range_cover regionBase 14 pdBits 1 \<and> valid_global_refs' \<sigma> \<and> kernel_data_refs \<inter> {regionBase..+2 ^ pdBits} = {} \<longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOArch (KOPDE makeObject))) (new_cap_addrs 4096 regionBase (KOArch (KOPDE makeObject))) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr regionBase) False) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr\<rbrakk> \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOArch (KOPDE makeObject))) (map (\<lambda>p. regionBase + (word_of_nat p << objBitsKO (KOArch (KOPDE makeObject)))) [0..<4096]) (ksPSpace \<sigma>)\<rparr>, globals_update (t_hrs_'_update (hrs_htd_update (ptr_retyp (pd_Ptr regionBase)))) x) \<in> rf_sr
 2. \<And>\<sigma> x. \<lbrakk>valid_global_refs' \<sigma>; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase 14 \<sigma>; 16384 \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+16384} \<sigma>; regionBase \<noteq> 0; range_cover regionBase 14 14 (Suc 0); {regionBase..+16384} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase 16384 x; heap_list (hrs_mem (t_hrs_' (globals x))) 16384 regionBase = replicate 16384 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject 12 \<sigma>); range_cover regionBase 14 2 4096; unat (word_of_nat (Suc 0) * 2\<^sup>2) = Suc 0 * 2\<^sup>2; region_is_bytes regionBase 16384 x\<rbrakk> \<Longrightarrow> 12 < word_bits
 3. \<And>\<sigma> x. \<lbrakk>valid_global_refs' \<sigma>; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase 14 \<sigma>; 16384 \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+16384} \<sigma>; regionBase \<noteq> 0; range_cover regionBase 14 14 (Suc 0); {regionBase..+16384} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase 16384 x; heap_list (hrs_mem (t_hrs_' (globals x))) 16384 regionBase = replicate 16384 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject 12 \<sigma>); range_cover regionBase 14 2 4096; unat (word_of_nat (Suc 0) * 2\<^sup>2) = Suc 0 * 2\<^sup>2; region_is_bytes regionBase 16384 x\<rbrakk> \<Longrightarrow> is_aligned regionBase (12 + objBitsKO (injectKOS makeObject))
 4. \<And>\<sigma> x. \<lbrakk>valid_global_refs' \<sigma>; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase 14 \<sigma>; 16384 \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+16384} \<sigma>; regionBase \<noteq> 0; range_cover regionBase 14 14 (Suc 0); {regionBase..+16384} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase 16384 x; heap_list (hrs_mem (t_hrs_' (globals x))) 16384 regionBase = replicate 16384 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject 12 \<sigma>); range_cover regionBase 14 2 4096; unat (word_of_nat (Suc 0) * 2\<^sup>2) = Suc 0 * 2\<^sup>2; region_is_bytes regionBase 16384 x\<rbrakk> \<Longrightarrow> no_fail ((=) \<sigma>) (placeNewObject regionBase makeObject 12)
 5. \<And>\<sigma> x. \<lbrakk>valid_global_refs' \<sigma>; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase 14 \<sigma>; 16384 \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+16384} \<sigma>; regionBase \<noteq> 0; range_cover regionBase 14 14 (Suc 0); {regionBase..+16384} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase 16384 x; heap_list (hrs_mem (t_hrs_' (globals x))) 16384 regionBase = replicate 16384 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject 12 \<sigma>); range_cover regionBase 14 2 4096; unat (word_of_nat (Suc 0) * 2\<^sup>2) = Suc 0 * 2\<^sup>2\<rbrakk> \<Longrightarrow> region_is_bytes regionBase 16384 x proof (prove)
goal (5 subgoals):
 1. \<And>\<sigma> x. \<lbrakk>valid_global_refs' \<sigma>; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase 14 \<sigma>; 16384 \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+16384} \<sigma>; regionBase \<noteq> 0; range_cover regionBase 14 14 (Suc 0); {regionBase..+16384} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase 16384 x; heap_list (hrs_mem (t_hrs_' (globals x))) 16384 regionBase = replicate 16384 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject 12 \<sigma>); range_cover regionBase 14 2 4096; region_is_bytes regionBase 16384 x; caps_overlap_reserved' {regionBase..+2 ^ pdBits} \<sigma> \<and> region_is_bytes regionBase (2 ^ pdBits) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ pdBits) regionBase = replicate (2 ^ pdBits) 0 \<and> range_cover regionBase 14 pdBits (Suc 0) \<and> kernel_data_refs \<inter> {regionBase..+2 ^ pdBits} = {} \<longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOArch (KOPDE makeObject))) (new_cap_addrs 4096 regionBase (KOArch (KOPDE makeObject))) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr regionBase) False) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr\<rbrakk> \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOArch (KOPDE makeObject))) (map (\<lambda>p. regionBase + (word_of_nat p << archObjSize (KOPDE makeObject))) [0..<4096]) (ksPSpace \<sigma>)\<rparr>, globals_update (t_hrs_'_update (hrs_htd_update (ptr_retyp (pd_Ptr regionBase)))) x) \<in> rf_sr
 2. \<And>\<sigma> x. \<lbrakk>valid_global_refs' \<sigma>; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase 14 \<sigma>; 16384 \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+16384} \<sigma>; regionBase \<noteq> 0; range_cover regionBase 14 14 (Suc 0); {regionBase..+16384} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase 16384 x; heap_list (hrs_mem (t_hrs_' (globals x))) 16384 regionBase = replicate 16384 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject 12 \<sigma>); range_cover regionBase 14 2 4096; unat (word_of_nat (Suc 0) * 2\<^sup>2) = Suc 0 * 2\<^sup>2; region_is_bytes regionBase 16384 x\<rbrakk> \<Longrightarrow> 12 < word_bits
 3. \<And>\<sigma> x. \<lbrakk>valid_global_refs' \<sigma>; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase 14 \<sigma>; 16384 \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+16384} \<sigma>; regionBase \<noteq> 0; range_cover regionBase 14 14 (Suc 0); {regionBase..+16384} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase 16384 x; heap_list (hrs_mem (t_hrs_' (globals x))) 16384 regionBase = replicate 16384 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject 12 \<sigma>); range_cover regionBase 14 2 4096; unat (word_of_nat (Suc 0) * 2\<^sup>2) = Suc 0 * 2\<^sup>2; region_is_bytes regionBase 16384 x\<rbrakk> \<Longrightarrow> is_aligned regionBase (12 + objBitsKO (injectKOS makeObject))
 4. \<And>\<sigma> x. \<lbrakk>valid_global_refs' \<sigma>; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase 14 \<sigma>; 16384 \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+16384} \<sigma>; regionBase \<noteq> 0; range_cover regionBase 14 14 (Suc 0); {regionBase..+16384} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase 16384 x; heap_list (hrs_mem (t_hrs_' (globals x))) 16384 regionBase = replicate 16384 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject 12 \<sigma>); range_cover regionBase 14 2 4096; unat (word_of_nat (Suc 0) * 2\<^sup>2) = Suc 0 * 2\<^sup>2; region_is_bytes regionBase 16384 x\<rbrakk> \<Longrightarrow> no_fail ((=) \<sigma>) (placeNewObject regionBase makeObject 12)
 5. \<And>\<sigma> x. \<lbrakk>valid_global_refs' \<sigma>; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase 14 \<sigma>; 16384 \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+16384} \<sigma>; regionBase \<noteq> 0; range_cover regionBase 14 14 (Suc 0); {regionBase..+16384} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase 16384 x; heap_list (hrs_mem (t_hrs_' (globals x))) 16384 regionBase = replicate 16384 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject 12 \<sigma>); range_cover regionBase 14 2 4096; unat (word_of_nat (Suc 0) * 2\<^sup>2) = Suc 0 * 2\<^sup>2\<rbrakk> \<Longrightarrow> region_is_bytes regionBase 16384 x proof (prove)
goal (5 subgoals):
 1. \<And>\<sigma> x. \<lbrakk>valid_global_refs' \<sigma>; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase 14 \<sigma>; 16384 \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+16384} \<sigma>; regionBase \<noteq> 0; range_cover regionBase 14 14 (Suc 0); {regionBase..+16384} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase 16384 x; heap_list (hrs_mem (t_hrs_' (globals x))) 16384 regionBase = replicate 16384 0; cstate_relation \<sigma> (globals x); \<not> snd (placeNewObject regionBase makeObject 12 \<sigma>); range_cover regionBase 14 2 4096; region_is_bytes regionBase 16384 x; range_cover regionBase 14 pdBits (Suc 0) \<longrightarrow> heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ pdBits) regionBase = replicate (2 ^ pdBits) 0 \<longrightarrow> region_is_bytes regionBase (2 ^ pdBits) x \<longrightarrow> caps_overlap_reserved' {regionBase..+2 ^ pdBits} \<sigma> \<longrightarrow> kernel_data_refs \<inter> {regionBase..+2 ^ pdBits} \<noteq> {}\<rbrakk> \<Longrightarrow> cstate_relation (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOArch (KOPDE makeObject))) (map (\<lambda>p. regionBase + (word_of_nat p << pdeBits)) [0..<4096]) (ksPSpace \<sigma>)\<rparr>) (t_hrs_'_update (hrs_htd_update (ptr_retyp (pd_Ptr regionBase))) (globals x))
 2. \<And>\<sigma> x. \<lbrakk>valid_global_refs' \<sigma>; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase 14 \<sigma>; 16384 \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+16384} \<sigma>; regionBase \<noteq> 0; range_cover regionBase 14 14 (Suc 0); {regionBase..+16384} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase 16384 x; heap_list (hrs_mem (t_hrs_' (globals x))) 16384 regionBase = replicate 16384 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject 12 \<sigma>); range_cover regionBase 14 2 4096; unat (word_of_nat (Suc 0) * 2\<^sup>2) = Suc 0 * 2\<^sup>2; region_is_bytes regionBase 16384 x\<rbrakk> \<Longrightarrow> 12 < word_bits
 3. \<And>\<sigma> x. \<lbrakk>valid_global_refs' \<sigma>; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase 14 \<sigma>; 16384 \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+16384} \<sigma>; regionBase \<noteq> 0; range_cover regionBase 14 14 (Suc 0); {regionBase..+16384} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase 16384 x; heap_list (hrs_mem (t_hrs_' (globals x))) 16384 regionBase = replicate 16384 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject 12 \<sigma>); range_cover regionBase 14 2 4096; unat (word_of_nat (Suc 0) * 2\<^sup>2) = Suc 0 * 2\<^sup>2; region_is_bytes regionBase 16384 x\<rbrakk> \<Longrightarrow> is_aligned regionBase (12 + objBitsKO (injectKOS makeObject))
 4. \<And>\<sigma> x. \<lbrakk>valid_global_refs' \<sigma>; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase 14 \<sigma>; 16384 \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+16384} \<sigma>; regionBase \<noteq> 0; range_cover regionBase 14 14 (Suc 0); {regionBase..+16384} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase 16384 x; heap_list (hrs_mem (t_hrs_' (globals x))) 16384 regionBase = replicate 16384 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject 12 \<sigma>); range_cover regionBase 14 2 4096; unat (word_of_nat (Suc 0) * 2\<^sup>2) = Suc 0 * 2\<^sup>2; region_is_bytes regionBase 16384 x\<rbrakk> \<Longrightarrow> no_fail ((=) \<sigma>) (placeNewObject regionBase makeObject 12)
 5. \<And>\<sigma> x. \<lbrakk>valid_global_refs' \<sigma>; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase 14 \<sigma>; 16384 \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+16384} \<sigma>; regionBase \<noteq> 0; range_cover regionBase 14 14 (Suc 0); {regionBase..+16384} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase 16384 x; heap_list (hrs_mem (t_hrs_' (globals x))) 16384 regionBase = replicate 16384 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject 12 \<sigma>); range_cover regionBase 14 2 4096; unat (word_of_nat (Suc 0) * 2\<^sup>2) = Suc 0 * 2\<^sup>2\<rbrakk> \<Longrightarrow> region_is_bytes regionBase 16384 x proof (prove)
goal (4 subgoals):
 1. \<And>\<sigma> x. \<lbrakk>valid_global_refs' \<sigma>; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase 14 \<sigma>; 16384 \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+16384} \<sigma>; regionBase \<noteq> 0; range_cover regionBase 14 14 (Suc 0); {regionBase..+16384} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase 16384 x; heap_list (hrs_mem (t_hrs_' (globals x))) 16384 regionBase = replicate 16384 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject 12 \<sigma>); range_cover regionBase 14 2 4096; unat (word_of_nat (Suc 0) * 2\<^sup>2) = Suc 0 * 2\<^sup>2; region_is_bytes regionBase 16384 x\<rbrakk> \<Longrightarrow> 12 < word_bits
 2. \<And>\<sigma> x. \<lbrakk>valid_global_refs' \<sigma>; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase 14 \<sigma>; 16384 \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+16384} \<sigma>; regionBase \<noteq> 0; range_cover regionBase 14 14 (Suc 0); {regionBase..+16384} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase 16384 x; heap_list (hrs_mem (t_hrs_' (globals x))) 16384 regionBase = replicate 16384 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject 12 \<sigma>); range_cover regionBase 14 2 4096; unat (word_of_nat (Suc 0) * 2\<^sup>2) = Suc 0 * 2\<^sup>2; region_is_bytes regionBase 16384 x\<rbrakk> \<Longrightarrow> is_aligned regionBase (12 + objBitsKO (injectKOS makeObject))
 3. \<And>\<sigma> x. \<lbrakk>valid_global_refs' \<sigma>; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase 14 \<sigma>; 16384 \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+16384} \<sigma>; regionBase \<noteq> 0; range_cover regionBase 14 14 (Suc 0); {regionBase..+16384} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase 16384 x; heap_list (hrs_mem (t_hrs_' (globals x))) 16384 regionBase = replicate 16384 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject 12 \<sigma>); range_cover regionBase 14 2 4096; unat (word_of_nat (Suc 0) * 2\<^sup>2) = Suc 0 * 2\<^sup>2; region_is_bytes regionBase 16384 x\<rbrakk> \<Longrightarrow> no_fail ((=) \<sigma>) (placeNewObject regionBase makeObject 12)
 4. \<And>\<sigma> x. \<lbrakk>valid_global_refs' \<sigma>; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase 14 \<sigma>; 16384 \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+16384} \<sigma>; regionBase \<noteq> 0; range_cover regionBase 14 14 (Suc 0); {regionBase..+16384} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase 16384 x; heap_list (hrs_mem (t_hrs_' (globals x))) 16384 regionBase = replicate 16384 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject 12 \<sigma>); range_cover regionBase 14 2 4096; unat (word_of_nat (Suc 0) * 2\<^sup>2) = Suc 0 * 2\<^sup>2\<rbrakk> \<Longrightarrow> region_is_bytes regionBase 16384 x proof (prove)
goal (3 subgoals):
 1. \<And>\<sigma> x. \<lbrakk>valid_global_refs' \<sigma>; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase 14 \<sigma>; 16384 \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+16384} \<sigma>; regionBase \<noteq> 0; range_cover regionBase 14 14 (Suc 0); {regionBase..+16384} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase 16384 x; heap_list (hrs_mem (t_hrs_' (globals x))) 16384 regionBase = replicate 16384 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject 12 \<sigma>); range_cover regionBase 14 2 4096; unat (word_of_nat (Suc 0) * 2\<^sup>2) = Suc 0 * 2\<^sup>2; region_is_bytes regionBase 16384 x\<rbrakk> \<Longrightarrow> is_aligned regionBase (12 + objBitsKO (injectKOS makeObject))
 2. \<And>\<sigma> x. \<lbrakk>valid_global_refs' \<sigma>; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase 14 \<sigma>; 16384 \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+16384} \<sigma>; regionBase \<noteq> 0; range_cover regionBase 14 14 (Suc 0); {regionBase..+16384} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase 16384 x; heap_list (hrs_mem (t_hrs_' (globals x))) 16384 regionBase = replicate 16384 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject 12 \<sigma>); range_cover regionBase 14 2 4096; unat (word_of_nat (Suc 0) * 2\<^sup>2) = Suc 0 * 2\<^sup>2; region_is_bytes regionBase 16384 x\<rbrakk> \<Longrightarrow> no_fail ((=) \<sigma>) (placeNewObject regionBase makeObject 12)
 3. \<And>\<sigma> x. \<lbrakk>valid_global_refs' \<sigma>; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase 14 \<sigma>; 16384 \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+16384} \<sigma>; regionBase \<noteq> 0; range_cover regionBase 14 14 (Suc 0); {regionBase..+16384} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase 16384 x; heap_list (hrs_mem (t_hrs_' (globals x))) 16384 regionBase = replicate 16384 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject 12 \<sigma>); range_cover regionBase 14 2 4096; unat (word_of_nat (Suc 0) * 2\<^sup>2) = Suc 0 * 2\<^sup>2\<rbrakk> \<Longrightarrow> region_is_bytes regionBase 16384 x proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x. \<lbrakk>valid_global_refs' \<sigma>; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase 14 \<sigma>; 16384 \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+16384} \<sigma>; regionBase \<noteq> 0; range_cover regionBase 14 14 (Suc 0); {regionBase..+16384} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase 16384 x; heap_list (hrs_mem (t_hrs_' (globals x))) 16384 regionBase = replicate 16384 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject 12 \<sigma>); range_cover regionBase 14 2 4096; unat (word_of_nat (Suc 0) * 2\<^sup>2) = Suc 0 * 2\<^sup>2; region_is_bytes regionBase 16384 x\<rbrakk> \<Longrightarrow> no_fail ((=) \<sigma>) (placeNewObject regionBase makeObject 12)
 2. \<And>\<sigma> x. \<lbrakk>valid_global_refs' \<sigma>; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase 14 \<sigma>; 16384 \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+16384} \<sigma>; regionBase \<noteq> 0; range_cover regionBase 14 14 (Suc 0); {regionBase..+16384} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase 16384 x; heap_list (hrs_mem (t_hrs_' (globals x))) 16384 regionBase = replicate 16384 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject 12 \<sigma>); range_cover regionBase 14 2 4096; unat (word_of_nat (Suc 0) * 2\<^sup>2) = Suc 0 * 2\<^sup>2\<rbrakk> \<Longrightarrow> region_is_bytes regionBase 16384 x proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x. \<lbrakk>valid_global_refs' \<sigma>; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase 14 \<sigma>; 16384 \<le> gsMaxObjectSize \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+16384} \<sigma>; regionBase \<noteq> 0; range_cover regionBase 14 14 (Suc 0); {regionBase..+16384} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase 16384 x; heap_list (hrs_mem (t_hrs_' (globals x))) 16384 regionBase = replicate 16384 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase makeObject 12 \<sigma>); range_cover regionBase 14 2 4096; unat (word_of_nat (Suc 0) * 2\<^sup>2) = Suc 0 * 2\<^sup>2\<rbrakk> \<Longrightarrow> region_is_bytes regionBase 16384 x proof (prove)
goal:
No subgoals!