theory Retype_C

lemma placeNewObject_user_data:
  "ccorresG rf_sr \<Gamma> dc xfdc
  (pspace_aligned' and pspace_distinct' and pspace_no_overlap' regionBase (pageBits+us)
  and valid_queues and valid_machine_state'
  and ret_zero regionBase (2 ^ (pageBits+us))
  and (\<lambda>s. sym_refs (state_refs_of' s))
  and (\<lambda>s. 2^(pageBits +  us) \<le> gsMaxObjectSize s)
  and K (regionBase \<noteq> 0 \<and> range_cover regionBase (pageBits + us) (pageBits+us) (Suc 0)
  \<and> us < word_bits
  \<and>  {regionBase..+2^(pageBits +  us)} \<inter> kernel_data_refs = {}))
  ({s. region_actually_is_zero_bytes regionBase (2^(pageBits+us)) s})
  hs
  (placeNewObject regionBase UserData us)
  (global_htd_update (\<lambda>s. (ptr_retyps (2^us) (Ptr regionBase :: user_data_C ptr))))" apply (rule ccorres_from_vcg_nofail) apply (clarsimp simp:) 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_retyps_htd_safe_neg[where arr=False, unfolded ptr_retyps_gen_def, simplified]
                         size_of_def pageBits_def power_add mult.commute mult.left_commute) apply (frule range_cover.unat_of_nat_shift[where gbits = "pageBits + us"]) apply simp apply (clarsimp simp:size_of_def power_add pageBits_def
     rf_sr_def cstate_relation_def Let_def field_simps) apply blast apply (frule range_cover.aligned) apply (rule bexI [OF _ placeNewObject_eq], simp_all) apply (cut_tac ptr=regionBase and sz="pageBits + us" and gbits=us and arr=False
                in createObjects_ccorres_user_data[rule_format]) apply (rule conjI, assumption, clarsimp) apply (fastforce simp: pageBits_def field_simps region_actually_is_bytes) apply (clarsimp elim!: rsubst[where P="\<lambda>x. (\<sigma>, x) \<in> rf_sr" for \<sigma>]
                     simp: field_simps objBitsKO_def ptr_retyps_gen_def) apply (simp add: objBitsKO_def field_simps) apply (rule no_fail_pre, rule no_fail_placeNewObject) apply (clarsimp simp: objBitsKO_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (pspace_aligned' and pspace_distinct' and pspace_no_overlap' regionBase (pageBits + us) and Invariants_H.valid_queues and valid_machine_state' and (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {regionBase..+2 ^ (pageBits + us)}) and (\<lambda>s. sym_refs (state_refs_of' s)) and (\<lambda>s. 2 ^ (pageBits + us) \<le> gsMaxObjectSize s) and K (regionBase \<noteq> 0 \<and> range_cover regionBase (pageBits + us) (pageBits + us) (Suc 0) \<and> us < word_bits \<and> {regionBase..+2 ^ (pageBits + us)} \<inter> kernel_data_refs = {})) {s. region_actually_is_bytes regionBase (2 ^ (pageBits + us)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (2 ^ (pageBits + us)) regionBase = replicate (2 ^ (pageBits + us)) 0} hs (placeNewObject regionBase UserData us) (Guard MemorySafety \<lbrace>htd_safe domain (hrs_htd \<acute>t_hrs) \<and> htd_safe domain (ptr_retyps (2 ^ us) (PTR(user_data_C) regionBase) (hrs_htd \<acute>t_hrs))\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_htd_update (ptr_retyps (2 ^ us) (PTR(user_data_C) regionBase))))) proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma>. \<Gamma>\<turnstile> {s. (pspace_aligned' and pspace_distinct' and pspace_no_overlap' regionBase (pageBits + us) and Invariants_H.valid_queues and valid_machine_state' and (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {regionBase..+2 ^ (pageBits + us)}) and (\<lambda>s. sym_refs (state_refs_of' s)) and (\<lambda>s. 2 ^ (pageBits + us) \<le> gsMaxObjectSize s) and K (regionBase \<noteq> 0 \<and> range_cover regionBase (pageBits + us) (pageBits + us) (Suc 0) \<and> us < word_bits \<and> {regionBase..+2 ^ (pageBits + us)} \<inter> kernel_data_refs = {})) \<sigma> \<and> s \<in> {s. region_actually_is_bytes regionBase (2 ^ (pageBits + us)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (2 ^ (pageBits + us)) regionBase = replicate (2 ^ (pageBits + us)) 0} \<and> (\<sigma>, s) \<in> rf_sr} Guard MemorySafety \<lbrace>htd_safe domain (hrs_htd \<acute>t_hrs) \<and> htd_safe domain (ptr_retyps (2 ^ us) (PTR(user_data_C) regionBase) (hrs_htd \<acute>t_hrs))\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_htd_update (ptr_retyps (2 ^ us) (PTR(user_data_C) regionBase)))) {s. \<not> snd (placeNewObject regionBase UserData us \<sigma>) \<longrightarrow> (\<exists>(rv, \<sigma>')\<in>fst (placeNewObject regionBase UserData us \<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 (pageBits + us) \<sigma> \<and> Invariants_H.valid_queues \<sigma> \<and> valid_machine_state' \<sigma> \<and> valid_objs' \<sigma> \<and> untyped_ranges_zero' \<sigma> \<and> caps_overlap_reserved' {regionBase..+2 ^ (pageBits + us)} \<sigma> \<and> sym_refs (state_refs_of' \<sigma>) \<and> 2 ^ (pageBits + us) \<le> gsMaxObjectSize \<sigma> \<and> regionBase \<noteq> 0 \<and> range_cover regionBase (pageBits + us) (pageBits + us) (Suc 0) \<and> us < word_bits \<and> {regionBase..+2 ^ (pageBits + us)} \<inter> kernel_data_refs = {} \<and> region_actually_is_bytes regionBase (2 ^ (pageBits + us)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (2 ^ (pageBits + us)) regionBase = replicate (2 ^ (pageBits + us)) 0 \<and> (\<sigma>, s) \<in> rf_sr} Guard MemorySafety \<lbrace>htd_safe domain (hrs_htd \<acute>t_hrs) \<and> htd_safe domain (ptr_retyps (2 ^ us) (PTR(user_data_C) regionBase) (hrs_htd \<acute>t_hrs))\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_htd_update (ptr_retyps (2 ^ us) (PTR(user_data_C) regionBase)))) {s. \<not> snd (placeNewObject regionBase UserData us \<sigma>) \<longrightarrow> (\<exists>x\<in>fst (placeNewObject regionBase UserData us \<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_retyps (2 ^ us) (PTR(user_data_C) regionBase) (hrs_htd \<acute>t_hrs))\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_htd_update (ptr_retyps (2 ^ us) (PTR(user_data_C) regionBase)))) {s. \<not> snd (placeNewObject regionBase UserData us \<sigma>) \<longrightarrow> (\<exists>x\<in>fst (placeNewObject regionBase UserData us \<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 (pageBits + us) \<sigma> \<and> Invariants_H.valid_queues \<sigma> \<and> valid_machine_state' \<sigma> \<and> valid_objs' \<sigma> \<and> untyped_ranges_zero' \<sigma> \<and> caps_overlap_reserved' {regionBase..+2 ^ (pageBits + us)} \<sigma> \<and> sym_refs (state_refs_of' \<sigma>) \<and> 2 ^ (pageBits + us) \<le> gsMaxObjectSize \<sigma> \<and> regionBase \<noteq> 0 \<and> range_cover regionBase (pageBits + us) (pageBits + us) (Suc 0) \<and> us < word_bits \<and> {regionBase..+2 ^ (pageBits + us)} \<inter> kernel_data_refs = {} \<and> region_actually_is_bytes regionBase (2 ^ (pageBits + us)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (2 ^ (pageBits + us)) regionBase = replicate (2 ^ (pageBits + us)) 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 (pageBits + us) \<sigma> \<and> Invariants_H.valid_queues \<sigma> \<and> valid_machine_state' \<sigma> \<and> valid_objs' \<sigma> \<and> untyped_ranges_zero' \<sigma> \<and> caps_overlap_reserved' {regionBase..+2 ^ (pageBits + us)} \<sigma> \<and> sym_refs (state_refs_of' \<sigma>) \<and> 2 ^ (pageBits + us) \<le> gsMaxObjectSize \<sigma> \<and> regionBase \<noteq> 0 \<and> range_cover regionBase (pageBits + us) (pageBits + us) (Suc 0) \<and> us < word_bits \<and> {regionBase..+2 ^ (pageBits + us)} \<inter> kernel_data_refs = {} \<and> region_actually_is_bytes regionBase (2 ^ (pageBits + us)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (2 ^ (pageBits + us)) regionBase = replicate (2 ^ (pageBits + us)) 0 \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. htd_safe domain (hrs_htd (t_hrs_' (globals s))) \<and> htd_safe domain (ptr_retyps (2 ^ us) (PTR(user_data_C) regionBase) (hrs_htd (t_hrs_' (globals s)))) \<and> (\<not> snd (placeNewObject regionBase UserData us \<sigma>) \<longrightarrow> (\<exists>(rv, \<sigma>')\<in>fst (placeNewObject regionBase UserData us \<sigma>). (\<sigma>', globals_update (t_hrs_'_update (hrs_htd_update (ptr_retyps (2 ^ us) (PTR(user_data_C) 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 (pageBits + us) \<sigma>; Invariants_H.valid_queues \<sigma>; valid_machine_state' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (pageBits + us)} \<sigma>; sym_refs (state_refs_of' \<sigma>); 2 ^ (pageBits + us) \<le> gsMaxObjectSize \<sigma>; regionBase \<noteq> 0; range_cover regionBase (pageBits + us) (pageBits + us) (Suc 0); us < word_bits; {regionBase..+2 ^ (pageBits + us)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (pageBits + us)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (pageBits + us)) regionBase = replicate (2 ^ (pageBits + us)) 0; (\<sigma>, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> htd_safe domain (ptr_retyps (2 ^ us) (PTR(user_data_C) regionBase) (hrs_htd (t_hrs_' (globals x)))) \<and> (\<not> snd (placeNewObject regionBase UserData us \<sigma>) \<longrightarrow> (\<exists>xa\<in>fst (placeNewObject regionBase UserData us \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', globals_update (t_hrs_'_update (hrs_htd_update (ptr_retyps (2 ^ us) (PTR(user_data_C) 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 (pageBits + us) \<sigma>; Invariants_H.valid_queues \<sigma>; valid_machine_state' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (pageBits + us)} \<sigma>; sym_refs (state_refs_of' \<sigma>); 2 ^ (pageBits + us) \<le> gsMaxObjectSize \<sigma>; regionBase \<noteq> 0; range_cover regionBase (pageBits + us) (pageBits + us) (Suc 0); us < word_bits; {regionBase..+2 ^ (pageBits + us)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (pageBits + us)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (pageBits + us)) regionBase = replicate (2 ^ (pageBits + us)) 0; (\<sigma>, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> htd_safe domain (ptr_retyps (2 ^ us) (PTR(user_data_C) regionBase) (hrs_htd (t_hrs_' (globals x))))
 2. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (pageBits + us) \<sigma>; Invariants_H.valid_queues \<sigma>; valid_machine_state' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (pageBits + us)} \<sigma>; sym_refs (state_refs_of' \<sigma>); 2 ^ (pageBits + us) \<le> gsMaxObjectSize \<sigma>; regionBase \<noteq> 0; range_cover regionBase (pageBits + us) (pageBits + us) (Suc 0); us < word_bits; {regionBase..+2 ^ (pageBits + us)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (pageBits + us)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (pageBits + us)) regionBase = replicate (2 ^ (pageBits + us)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase UserData us \<sigma>)\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (placeNewObject regionBase UserData us \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', globals_update (t_hrs_'_update (hrs_htd_update (ptr_retyps (2 ^ us) (PTR(user_data_C) 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 (pageBits + us) \<sigma>; Invariants_H.valid_queues \<sigma>; valid_machine_state' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (pageBits + us)} \<sigma>; sym_refs (state_refs_of' \<sigma>); 2 ^ (pageBits + us) \<le> gsMaxObjectSize \<sigma>; regionBase \<noteq> 0; range_cover regionBase (pageBits + us) (pageBits + us) (Suc 0); us < word_bits; {regionBase..+2 ^ (pageBits + us)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (pageBits + us)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (pageBits + us)) regionBase = replicate (2 ^ (pageBits + us)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase UserData us \<sigma>)\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (placeNewObject regionBase UserData us \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', globals_update (t_hrs_'_update (hrs_htd_update (ptr_retyps (2 ^ us) (PTR(user_data_C) regionBase)))) x) \<in> rf_sr proof (prove)
goal (3 subgoals):
 1. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (pageBits + us) \<sigma>; Invariants_H.valid_queues \<sigma>; valid_machine_state' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (pageBits + us)} \<sigma>; sym_refs (state_refs_of' \<sigma>); 2 ^ (pageBits + us) \<le> gsMaxObjectSize \<sigma>; regionBase \<noteq> 0; range_cover regionBase (pageBits + us) (pageBits + us) (Suc 0); us < word_bits; {regionBase..+2 ^ (pageBits + us)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (pageBits + us)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (pageBits + us)) regionBase = replicate (2 ^ (pageBits + us)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase UserData us \<sigma>)\<rbrakk> \<Longrightarrow> pageBits + us \<le> pageBits + us
 2. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (pageBits + us) \<sigma>; Invariants_H.valid_queues \<sigma>; valid_machine_state' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (pageBits + us)} \<sigma>; sym_refs (state_refs_of' \<sigma>); 2 ^ (pageBits + us) \<le> gsMaxObjectSize \<sigma>; regionBase \<noteq> 0; range_cover regionBase (pageBits + us) (pageBits + us) (Suc 0); us < word_bits; {regionBase..+2 ^ (pageBits + us)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (pageBits + us)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (pageBits + us)) regionBase = replicate (2 ^ (pageBits + us)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase UserData us \<sigma>)\<rbrakk> \<Longrightarrow> ?p39 \<sigma> x \<le> Suc 0
 3. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (pageBits + us) \<sigma>; Invariants_H.valid_queues \<sigma>; valid_machine_state' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (pageBits + us)} \<sigma>; sym_refs (state_refs_of' \<sigma>); 2 ^ (pageBits + us) \<le> gsMaxObjectSize \<sigma>; regionBase \<noteq> 0; range_cover regionBase (pageBits + us) (pageBits + us) (Suc 0); us < word_bits; {regionBase..+2 ^ (pageBits + us)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (pageBits + us)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (pageBits + us)) regionBase = replicate (2 ^ (pageBits + us)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase UserData us \<sigma>); unat (word_of_nat (?p39 \<sigma> x) * 2 ^ (pageBits + us)) = ?p39 \<sigma> x * 2 ^ (pageBits + us)\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (placeNewObject regionBase UserData us \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', globals_update (t_hrs_'_update (hrs_htd_update (ptr_retyps (2 ^ us) (PTR(user_data_C) 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 (pageBits + us) \<sigma>; Invariants_H.valid_queues \<sigma>; valid_machine_state' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (pageBits + us)} \<sigma>; sym_refs (state_refs_of' \<sigma>); 2 ^ (pageBits + us) \<le> gsMaxObjectSize \<sigma>; regionBase \<noteq> 0; range_cover regionBase (pageBits + us) (pageBits + us) (Suc 0); us < word_bits; {regionBase..+2 ^ (pageBits + us)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (pageBits + us)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (pageBits + us)) regionBase = replicate (2 ^ (pageBits + us)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase UserData us \<sigma>)\<rbrakk> \<Longrightarrow> ?p39 \<sigma> x \<le> Suc 0
 2. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (pageBits + us) \<sigma>; Invariants_H.valid_queues \<sigma>; valid_machine_state' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (pageBits + us)} \<sigma>; sym_refs (state_refs_of' \<sigma>); 2 ^ (pageBits + us) \<le> gsMaxObjectSize \<sigma>; regionBase \<noteq> 0; range_cover regionBase (pageBits + us) (pageBits + us) (Suc 0); us < word_bits; {regionBase..+2 ^ (pageBits + us)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (pageBits + us)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (pageBits + us)) regionBase = replicate (2 ^ (pageBits + us)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase UserData us \<sigma>); unat (word_of_nat (?p39 \<sigma> x) * 2 ^ (pageBits + us)) = ?p39 \<sigma> x * 2 ^ (pageBits + us)\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (placeNewObject regionBase UserData us \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', globals_update (t_hrs_'_update (hrs_htd_update (ptr_retyps (2 ^ us) (PTR(user_data_C) 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 (us + 12) \<sigma>; Invariants_H.valid_queues \<sigma>; valid_machine_state' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ us * 4096} \<sigma>; sym_refs (state_refs_of' \<sigma>); 2 ^ us * 4096 \<le> gsMaxObjectSize \<sigma>; regionBase \<noteq> 0; range_cover regionBase (us + 12) (us + 12) (Suc 0); us < word_bits; {regionBase..+2 ^ us * 4096} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ us * 4096) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ us * 4096) regionBase = replicate (2 ^ us * 4096) 0; \<not> snd (placeNewObject regionBase UserData us \<sigma>); cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)); cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); carch_state_relation (ksArchState \<sigma>) (globals x); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+size_td (typ_info_t TYPE(cte_C[256]))} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+size_td (typ_info_t TYPE(pde_C[4096]))} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> ?p39 \<sigma> x \<le> Suc 0
 2. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (pageBits + us) \<sigma>; Invariants_H.valid_queues \<sigma>; valid_machine_state' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (pageBits + us)} \<sigma>; sym_refs (state_refs_of' \<sigma>); 2 ^ (pageBits + us) \<le> gsMaxObjectSize \<sigma>; regionBase \<noteq> 0; range_cover regionBase (pageBits + us) (pageBits + us) (Suc 0); us < word_bits; {regionBase..+2 ^ (pageBits + us)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (pageBits + us)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (pageBits + us)) regionBase = replicate (2 ^ (pageBits + us)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase UserData us \<sigma>); unat (word_of_nat (?p39 \<sigma> x) * 2 ^ (pageBits + us)) = ?p39 \<sigma> x * 2 ^ (pageBits + us)\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (placeNewObject regionBase UserData us \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', globals_update (t_hrs_'_update (hrs_htd_update (ptr_retyps (2 ^ us) (PTR(user_data_C) 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 (pageBits + us) \<sigma>; Invariants_H.valid_queues \<sigma>; valid_machine_state' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (pageBits + us)} \<sigma>; sym_refs (state_refs_of' \<sigma>); 2 ^ (pageBits + us) \<le> gsMaxObjectSize \<sigma>; regionBase \<noteq> 0; range_cover regionBase (pageBits + us) (pageBits + us) (Suc 0); us < word_bits; {regionBase..+2 ^ (pageBits + us)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (pageBits + us)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (pageBits + us)) regionBase = replicate (2 ^ (pageBits + us)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase UserData us \<sigma>); unat (word_of_nat 0 * 2 ^ (pageBits + us)) = 0 * 2 ^ (pageBits + us)\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (placeNewObject regionBase UserData us \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', globals_update (t_hrs_'_update (hrs_htd_update (ptr_retyps (2 ^ us) (PTR(user_data_C) 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 (pageBits + us) \<sigma>; Invariants_H.valid_queues \<sigma>; valid_machine_state' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (pageBits + us)} \<sigma>; sym_refs (state_refs_of' \<sigma>); 2 ^ (pageBits + us) \<le> gsMaxObjectSize \<sigma>; regionBase \<noteq> 0; range_cover regionBase (pageBits + us) (pageBits + us) (Suc 0); us < word_bits; {regionBase..+2 ^ (pageBits + us)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (pageBits + us)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (pageBits + us)) regionBase = replicate (2 ^ (pageBits + us)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase UserData us \<sigma>); unat (word_of_nat 0 * 2 ^ (pageBits + us)) = 0 * 2 ^ (pageBits + us); is_aligned regionBase (pageBits + us)\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (placeNewObject regionBase UserData us \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', globals_update (t_hrs_'_update (hrs_htd_update (ptr_retyps (2 ^ us) (PTR(user_data_C) regionBase)))) x) \<in> rf_sr proof (prove)
goal (3 subgoals):
 1. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (pageBits + us) \<sigma>; Invariants_H.valid_queues \<sigma>; valid_machine_state' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (pageBits + us)} \<sigma>; sym_refs (state_refs_of' \<sigma>); 2 ^ (pageBits + us) \<le> gsMaxObjectSize \<sigma>; regionBase \<noteq> 0; range_cover regionBase (pageBits + us) (pageBits + us) (Suc 0); us < word_bits; {regionBase..+2 ^ (pageBits + us)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (pageBits + us)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (pageBits + us)) regionBase = replicate (2 ^ (pageBits + us)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase UserData us \<sigma>); is_aligned regionBase (pageBits + us)\<rbrakk> \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (2 ^ us) regionBase KOUserData) (ksPSpace \<sigma>)\<rparr>, globals_update (t_hrs_'_update (hrs_htd_update (ptr_retyps (2 ^ us) (PTR(user_data_C) regionBase)))) x) \<in> rf_sr
 2. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (pageBits + us) \<sigma>; Invariants_H.valid_queues \<sigma>; valid_machine_state' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (pageBits + us)} \<sigma>; sym_refs (state_refs_of' \<sigma>); 2 ^ (pageBits + us) \<le> gsMaxObjectSize \<sigma>; regionBase \<noteq> 0; range_cover regionBase (pageBits + us) (pageBits + us) (Suc 0); us < word_bits; {regionBase..+2 ^ (pageBits + us)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (pageBits + us)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (pageBits + us)) regionBase = replicate (2 ^ (pageBits + us)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase UserData us \<sigma>); is_aligned regionBase (pageBits + us)\<rbrakk> \<Longrightarrow> is_aligned regionBase (us + objBitsKO KOUserData)
 3. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (pageBits + us) \<sigma>; Invariants_H.valid_queues \<sigma>; valid_machine_state' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (pageBits + us)} \<sigma>; sym_refs (state_refs_of' \<sigma>); 2 ^ (pageBits + us) \<le> gsMaxObjectSize \<sigma>; regionBase \<noteq> 0; range_cover regionBase (pageBits + us) (pageBits + us) (Suc 0); us < word_bits; {regionBase..+2 ^ (pageBits + us)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (pageBits + us)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (pageBits + us)) regionBase = replicate (2 ^ (pageBits + us)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase UserData us \<sigma>); is_aligned regionBase (pageBits + us)\<rbrakk> \<Longrightarrow> no_fail ((=) \<sigma>) (placeNewObject regionBase UserData us) proof (prove)
goal (4 subgoals):
 1. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (pageBits + us) \<sigma>; Invariants_H.valid_queues \<sigma>; valid_machine_state' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (pageBits + us)} \<sigma>; sym_refs (state_refs_of' \<sigma>); 2 ^ (pageBits + us) \<le> gsMaxObjectSize \<sigma>; regionBase \<noteq> 0; range_cover regionBase (pageBits + us) (pageBits + us) (Suc 0); us < word_bits; {regionBase..+2 ^ (pageBits + us)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (pageBits + us)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (pageBits + us)) regionBase = replicate (2 ^ (pageBits + us)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase UserData us \<sigma>); is_aligned regionBase (pageBits + us)\<rbrakk> \<Longrightarrow> (?\<sigma>83 \<sigma> x, ?x83 \<sigma> x) \<in> rf_sr \<and> range_cover regionBase (pageBits + us) (us + pageBits) (?n83 \<sigma> x) \<and> regionBase \<noteq> 0 \<and> pspace_aligned' (?\<sigma>83 \<sigma> x) \<and> pspace_distinct' (?\<sigma>83 \<sigma> x) \<and> valid_machine_state' (?\<sigma>83 \<sigma> x) \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {regionBase..+?n83 \<sigma> x * 2 ^ (us + pageBits)}) (?\<sigma>83 \<sigma> x) \<and> pspace_no_overlap' regionBase (pageBits + us) (?\<sigma>83 \<sigma> x) \<and> (region_is_bytes regionBase (?n83 \<sigma> x * 2 ^ (us + pageBits)) (?x83 \<sigma> x) \<and> heap_list (hrs_mem (t_hrs_' (globals (?x83 \<sigma> x)))) (?n83 \<sigma> x * 2 ^ (us + pageBits)) regionBase = replicate (?n83 \<sigma> x * 2 ^ (us + pageBits)) 0) \<and> {regionBase..+?n83 \<sigma> x * 2 ^ (us + pageBits)} \<inter> kernel_data_refs = {}
 2. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (pageBits + us) \<sigma>; Invariants_H.valid_queues \<sigma>; valid_machine_state' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (pageBits + us)} \<sigma>; sym_refs (state_refs_of' \<sigma>); 2 ^ (pageBits + us) \<le> gsMaxObjectSize \<sigma>; regionBase \<noteq> 0; range_cover regionBase (pageBits + us) (pageBits + us) (Suc 0); us < word_bits; {regionBase..+2 ^ (pageBits + us)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (pageBits + us)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (pageBits + us)) regionBase = replicate (2 ^ (pageBits + us)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase UserData us \<sigma>); is_aligned regionBase (pageBits + us); (?\<sigma>83 \<sigma> x\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (?n83 \<sigma> x * 2 ^ us) regionBase KOUserData) (ksPSpace (?\<sigma>83 \<sigma> x))\<rparr>, ?x83 \<sigma> x\<lparr>globals := globals (?x83 \<sigma> x)\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen (?n83 \<sigma> x * 2 ^ us) (PTR(user_data_C) regionBase) False) (t_hrs_' (globals (?x83 \<sigma> x)))\<rparr>\<rparr>) \<in> rf_sr\<rbrakk> \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (2 ^ us) regionBase KOUserData) (ksPSpace \<sigma>)\<rparr>, globals_update (t_hrs_'_update (hrs_htd_update (ptr_retyps (2 ^ us) (PTR(user_data_C) regionBase)))) x) \<in> rf_sr
 3. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (pageBits + us) \<sigma>; Invariants_H.valid_queues \<sigma>; valid_machine_state' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (pageBits + us)} \<sigma>; sym_refs (state_refs_of' \<sigma>); 2 ^ (pageBits + us) \<le> gsMaxObjectSize \<sigma>; regionBase \<noteq> 0; range_cover regionBase (pageBits + us) (pageBits + us) (Suc 0); us < word_bits; {regionBase..+2 ^ (pageBits + us)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (pageBits + us)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (pageBits + us)) regionBase = replicate (2 ^ (pageBits + us)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase UserData us \<sigma>); is_aligned regionBase (pageBits + us)\<rbrakk> \<Longrightarrow> is_aligned regionBase (us + objBitsKO KOUserData)
 4. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (pageBits + us) \<sigma>; Invariants_H.valid_queues \<sigma>; valid_machine_state' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (pageBits + us)} \<sigma>; sym_refs (state_refs_of' \<sigma>); 2 ^ (pageBits + us) \<le> gsMaxObjectSize \<sigma>; regionBase \<noteq> 0; range_cover regionBase (pageBits + us) (pageBits + us) (Suc 0); us < word_bits; {regionBase..+2 ^ (pageBits + us)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (pageBits + us)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (pageBits + us)) regionBase = replicate (2 ^ (pageBits + us)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase UserData us \<sigma>); is_aligned regionBase (pageBits + us)\<rbrakk> \<Longrightarrow> no_fail ((=) \<sigma>) (placeNewObject regionBase UserData us) proof (prove)
goal (4 subgoals):
 1. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (pageBits + us) \<sigma>; Invariants_H.valid_queues \<sigma>; valid_machine_state' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (pageBits + us)} \<sigma>; sym_refs (state_refs_of' \<sigma>); 2 ^ (pageBits + us) \<le> gsMaxObjectSize \<sigma>; regionBase \<noteq> 0; range_cover regionBase (pageBits + us) (pageBits + us) (Suc 0); us < word_bits; {regionBase..+2 ^ (pageBits + us)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (pageBits + us)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (pageBits + us)) regionBase = replicate (2 ^ (pageBits + us)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase UserData us \<sigma>); is_aligned regionBase (pageBits + us)\<rbrakk> \<Longrightarrow> range_cover regionBase (pageBits + us) (us + pageBits) (?n83 \<sigma> x) \<and> caps_overlap_reserved' {regionBase..+?n83 \<sigma> x * 2 ^ (us + pageBits)} \<sigma> \<and> region_is_bytes regionBase (?n83 \<sigma> x * 2 ^ (us + pageBits)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (?n83 \<sigma> x * 2 ^ (us + pageBits)) regionBase = replicate (?n83 \<sigma> x * 2 ^ (us + pageBits)) 0 \<and> {regionBase..+?n83 \<sigma> x * 2 ^ (us + pageBits)} \<inter> kernel_data_refs = {}
 2. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (pageBits + us) \<sigma>; Invariants_H.valid_queues \<sigma>; valid_machine_state' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (pageBits + us)} \<sigma>; sym_refs (state_refs_of' \<sigma>); 2 ^ (pageBits + us) \<le> gsMaxObjectSize \<sigma>; regionBase \<noteq> 0; range_cover regionBase (pageBits + us) (pageBits + us) (Suc 0); us < word_bits; {regionBase..+2 ^ (pageBits + us)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (pageBits + us)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (pageBits + us)) regionBase = replicate (2 ^ (pageBits + us)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase UserData us \<sigma>); is_aligned regionBase (pageBits + us); (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (?n83 \<sigma> x * 2 ^ us) regionBase KOUserData) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen (?n83 \<sigma> x * 2 ^ us) (PTR(user_data_C) regionBase) False) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr\<rbrakk> \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (2 ^ us) regionBase KOUserData) (ksPSpace \<sigma>)\<rparr>, globals_update (t_hrs_'_update (hrs_htd_update (ptr_retyps (2 ^ us) (PTR(user_data_C) regionBase)))) x) \<in> rf_sr
 3. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (pageBits + us) \<sigma>; Invariants_H.valid_queues \<sigma>; valid_machine_state' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (pageBits + us)} \<sigma>; sym_refs (state_refs_of' \<sigma>); 2 ^ (pageBits + us) \<le> gsMaxObjectSize \<sigma>; regionBase \<noteq> 0; range_cover regionBase (pageBits + us) (pageBits + us) (Suc 0); us < word_bits; {regionBase..+2 ^ (pageBits + us)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (pageBits + us)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (pageBits + us)) regionBase = replicate (2 ^ (pageBits + us)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase UserData us \<sigma>); is_aligned regionBase (pageBits + us)\<rbrakk> \<Longrightarrow> is_aligned regionBase (us + objBitsKO KOUserData)
 4. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (pageBits + us) \<sigma>; Invariants_H.valid_queues \<sigma>; valid_machine_state' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (pageBits + us)} \<sigma>; sym_refs (state_refs_of' \<sigma>); 2 ^ (pageBits + us) \<le> gsMaxObjectSize \<sigma>; regionBase \<noteq> 0; range_cover regionBase (pageBits + us) (pageBits + us) (Suc 0); us < word_bits; {regionBase..+2 ^ (pageBits + us)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (pageBits + us)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (pageBits + us)) regionBase = replicate (2 ^ (pageBits + us)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase UserData us \<sigma>); is_aligned regionBase (pageBits + us)\<rbrakk> \<Longrightarrow> no_fail ((=) \<sigma>) (placeNewObject regionBase UserData us) proof (prove)
goal (3 subgoals):
 1. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (pageBits + us) \<sigma>; Invariants_H.valid_queues \<sigma>; valid_machine_state' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (pageBits + us)} \<sigma>; sym_refs (state_refs_of' \<sigma>); 2 ^ (pageBits + us) \<le> gsMaxObjectSize \<sigma>; regionBase \<noteq> 0; range_cover regionBase (pageBits + us) (pageBits + us) (Suc 0); us < word_bits; {regionBase..+2 ^ (pageBits + us)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (pageBits + us)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (pageBits + us)) regionBase = replicate (2 ^ (pageBits + us)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase UserData us \<sigma>); is_aligned regionBase (pageBits + us); (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (Suc 0 * 2 ^ us) regionBase KOUserData) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen (Suc 0 * 2 ^ us) (PTR(user_data_C) regionBase) False) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr\<rbrakk> \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (2 ^ us) regionBase KOUserData) (ksPSpace \<sigma>)\<rparr>, globals_update (t_hrs_'_update (hrs_htd_update (ptr_retyps (2 ^ us) (PTR(user_data_C) regionBase)))) x) \<in> rf_sr
 2. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (pageBits + us) \<sigma>; Invariants_H.valid_queues \<sigma>; valid_machine_state' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (pageBits + us)} \<sigma>; sym_refs (state_refs_of' \<sigma>); 2 ^ (pageBits + us) \<le> gsMaxObjectSize \<sigma>; regionBase \<noteq> 0; range_cover regionBase (pageBits + us) (pageBits + us) (Suc 0); us < word_bits; {regionBase..+2 ^ (pageBits + us)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (pageBits + us)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (pageBits + us)) regionBase = replicate (2 ^ (pageBits + us)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase UserData us \<sigma>); is_aligned regionBase (pageBits + us)\<rbrakk> \<Longrightarrow> is_aligned regionBase (us + objBitsKO KOUserData)
 3. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (pageBits + us) \<sigma>; Invariants_H.valid_queues \<sigma>; valid_machine_state' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (pageBits + us)} \<sigma>; sym_refs (state_refs_of' \<sigma>); 2 ^ (pageBits + us) \<le> gsMaxObjectSize \<sigma>; regionBase \<noteq> 0; range_cover regionBase (pageBits + us) (pageBits + us) (Suc 0); us < word_bits; {regionBase..+2 ^ (pageBits + us)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (pageBits + us)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (pageBits + us)) regionBase = replicate (2 ^ (pageBits + us)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase UserData us \<sigma>); is_aligned regionBase (pageBits + us)\<rbrakk> \<Longrightarrow> no_fail ((=) \<sigma>) (placeNewObject regionBase UserData us) proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (pageBits + us) \<sigma>; Invariants_H.valid_queues \<sigma>; valid_machine_state' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (pageBits + us)} \<sigma>; sym_refs (state_refs_of' \<sigma>); 2 ^ (pageBits + us) \<le> gsMaxObjectSize \<sigma>; regionBase \<noteq> 0; range_cover regionBase (pageBits + us) (pageBits + us) (Suc 0); us < word_bits; {regionBase..+2 ^ (pageBits + us)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (pageBits + us)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (pageBits + us)) regionBase = replicate (2 ^ (pageBits + us)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase UserData us \<sigma>); is_aligned regionBase (pageBits + us)\<rbrakk> \<Longrightarrow> is_aligned regionBase (us + objBitsKO KOUserData)
 2. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (pageBits + us) \<sigma>; Invariants_H.valid_queues \<sigma>; valid_machine_state' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (pageBits + us)} \<sigma>; sym_refs (state_refs_of' \<sigma>); 2 ^ (pageBits + us) \<le> gsMaxObjectSize \<sigma>; regionBase \<noteq> 0; range_cover regionBase (pageBits + us) (pageBits + us) (Suc 0); us < word_bits; {regionBase..+2 ^ (pageBits + us)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (pageBits + us)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (pageBits + us)) regionBase = replicate (2 ^ (pageBits + us)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase UserData us \<sigma>); is_aligned regionBase (pageBits + us)\<rbrakk> \<Longrightarrow> no_fail ((=) \<sigma>) (placeNewObject regionBase UserData us) proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (pageBits + us) \<sigma>; Invariants_H.valid_queues \<sigma>; valid_machine_state' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (pageBits + us)} \<sigma>; sym_refs (state_refs_of' \<sigma>); 2 ^ (pageBits + us) \<le> gsMaxObjectSize \<sigma>; regionBase \<noteq> 0; range_cover regionBase (pageBits + us) (pageBits + us) (Suc 0); us < word_bits; {regionBase..+2 ^ (pageBits + us)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (pageBits + us)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (pageBits + us)) regionBase = replicate (2 ^ (pageBits + us)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase UserData us \<sigma>); is_aligned regionBase (pageBits + us)\<rbrakk> \<Longrightarrow> no_fail ((=) \<sigma>) (placeNewObject regionBase UserData us) proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x s. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pspace_no_overlap' regionBase (pageBits + us) \<sigma>; Invariants_H.valid_queues \<sigma>; valid_machine_state' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {regionBase..+2 ^ (pageBits + us)} \<sigma>; sym_refs (state_refs_of' \<sigma>); 2 ^ (pageBits + us) \<le> gsMaxObjectSize \<sigma>; regionBase \<noteq> 0; range_cover regionBase (pageBits + us) (pageBits + us) (Suc 0); us < word_bits; {regionBase..+2 ^ (pageBits + us)} \<inter> kernel_data_refs = {}; region_actually_is_bytes regionBase (2 ^ (pageBits + us)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ (pageBits + us)) regionBase = replicate (2 ^ (pageBits + us)) 0; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject regionBase UserData us \<sigma>); is_aligned regionBase (pageBits + us); \<sigma> = s\<rbrakk> \<Longrightarrow> us < word_bits \<and> is_aligned regionBase (objBitsKO (injectKOS UserData) + us) \<and> pspace_no_overlap' regionBase (objBitsKO (injectKOS UserData) + us) s \<and> pspace_aligned' s proof (prove)
goal:
No subgoals!