theory Arch_C

lemma createObjects_asidpool_ccorres:
  shows "ccorres dc xfdc
   ((\<lambda>s. \<exists>p. cte_wp_at' (\<lambda>cte. cteCap cte = UntypedCap isdev frame pageBits idx ) p s)
    and pspace_aligned' and pspace_distinct' and valid_objs'
    and ret_zero frame (2 ^ pageBits)
    and valid_global_refs' and pspace_no_overlap' frame pageBits)
   ({s. region_actually_is_bytes frame (2^pageBits) s})
   hs
   (placeNewObject frame (makeObject::asidpool) 0)
   (CALL memzero(Ptr frame, (2 ^ unat ARMSmallPageBits));;
   (global_htd_update (\<lambda>_. ptr_retyp (ap_Ptr frame))))" proof - have helper: "\<forall>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> is_aligned frame pageBits \<and> frame \<noteq> 0
  \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma>
  \<and> pspace_no_overlap' frame pageBits \<sigma>
  \<and> ret_zero frame (2 ^ pageBits) \<sigma>
  \<and> region_actually_is_bytes frame (2 ^ pageBits) x
  \<and> {frame ..+ 2 ^ pageBits} \<inter> kernel_data_refs = {}
 \<longrightarrow>
  (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)\<rparr>,
   x\<lparr>globals := globals x
                 \<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False)
                       (hrs_mem_update
                         (heap_update_list frame (replicate (2 ^ pageBits) 0))
                         (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr"
    (is "\<forall>\<sigma> x. ?P \<sigma> x \<longrightarrow>
        (\<sigma>\<lparr>ksPSpace := ?ks \<sigma>\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := ?ks' x\<rparr>\<rparr>) \<in> rf_sr") proof (intro impI allI) fix \<sigma> x let ?thesis = "(\<sigma>\<lparr>ksPSpace := ?ks \<sigma>\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := ?ks' x\<rparr>\<rparr>) \<in> rf_sr" let ?ks = "?ks \<sigma>" let ?ks' = "?ks' x" let ?ptr = "ap_Ptr frame" assume "?P \<sigma> x" hence rf: "(\<sigma>, x) \<in> rf_sr" and al: "is_aligned frame pageBits" and ptr0: "frame \<noteq> 0"
    and pal: "pspace_aligned' \<sigma>" and pdst: "pspace_distinct' \<sigma>"
    and pno: "pspace_no_overlap' frame pageBits \<sigma>"
    and zro: "ret_zero frame (2 ^ pageBits) \<sigma>"
    and actually: "region_actually_is_bytes frame (2 ^ pageBits) x"
    and kdr: "{frame ..+ 2 ^ pageBits} \<inter> kernel_data_refs = {}" by simp_all note empty = region_actually_is_bytes[OF actually] have relrl:
    "casid_pool_relation makeObject (from_bytes (replicate (size_of TYPE(asid_pool_C)) 0))" unfolding casid_pool_relation_def apply (clarsimp simp: makeObject_asidpool split: asid_pool_C.splits) apply (clarsimp simp: array_relation_def option_to_ptr_def option_to_0_def) apply (simp add: from_bytes_def) apply (simp add: typ_info_simps asid_pool_C_tag_def
      size_td_lt_final_pad size_td_lt_ti_typ_pad_combine Let_def size_of_def) apply (simp add: final_pad_def Let_def size_td_lt_ti_typ_pad_combine) apply (simp add: padup_def align_td_array') apply (subst (asm) size_td_array) apply simp apply (simp add: size_td_array ti_typ_pad_combine_def ti_typ_combine_def
                     Let_def empty_typ_info_def update_ti_adjust_ti
               del: replicate_numeral Kernel_C.pde_C_size) apply (simp add: typ_info_array array_tag_def
                del: replicate_numeral) apply (drule ap_eq_D) apply (clarsimp simp del: replicate_numeral) apply (subst update_ti_t_array_tag_n_rep) apply (simp del: replicate_numeral) apply simp apply (simp del: replicate_numeral) apply (subst index_fold_update) apply simp apply auto[1] apply (simp add: asid_low_bits_def word_le_nat_alt) apply (simp split: if_split) apply (rule conjI) apply (clarsimp simp: update_ti_t_ptr_0s) apply (clarsimp simp: asid_low_bits_def word_le_nat_alt) done define ko where "ko \<equiv> KOArch (KOASIDPool makeObject)" have rc :"range_cover frame (objBitsKO ko) (objBitsKO ko) (Suc 0)" by (simp add:objBits_simps ko_def archObjSize_def al range_cover_full) have rc' :"range_cover frame (objBitsKO ko) (objBitsKO ko) (2 ^ 0)" by (simp add:objBits_simps ko_def archObjSize_def al range_cover_full range_cover_rel) have pno': "pspace_no_overlap' frame (objBitsKO ko) \<sigma>" by (simp add:objBits_simps pno ko_def archObjSize_def al) have al': "is_aligned frame (objBitsKO (ko::kernel_object))" by (simp add:objBits_simps ko_def archObjSize_def al) 

  (* s/obj/obj'/ *)
   have szo: "size_of TYPE(asid_pool_C) = 2 ^ objBitsKO ko" by (simp add: size_of_def objBits_simps ko_def archObjSize_def pageBits_def) have szko: "objBitsKO ko = pageBits" by (simp add: objBits_simps ko_def archObjSize_def) hence sz: "objBitsKO ko \<le> pageBits" by simp have szo': "2 ^ pageBits = 2 ^ (pageBits - objBitsKO ko) * size_of TYPE(asid_pool_C)" using szko apply (subst szo) apply (simp add: power_add [symmetric]) done have [simp]: "(2::nat) ^ (pageBits - objBitsKO ko) * 2 ^ objBitsKO ko = 2 ^ pageBits" by (clarsimp simp:pageBits_def objBits_simps ko_def archObjSize_def) have ptr_retyp:
    "hrs_htd_update (ptr_retyps (2 ^ (pageBits - objBitsKO ko)) (ap_Ptr frame)) = hrs_htd_update (ptr_retyp (ap_Ptr frame))" apply (simp add: szko hrs_htd_update_def) done note rl' = cslift_ptr_retyp_memset_other_inst [OF _ rc' _ szo,
     simplified, OF empty[folded szko] szo[symmetric], unfolded szko] have szb: "pageBits < word_bits" by simp have mko: "\<And>dev. makeObjectKO dev (Inl (KOArch (KOASIDPool f))) = Some ko" by (simp add: ko_def makeObjectKO_def) note rl = projectKO_opt_retyp_other [OF rc pal pno' ko_def] note cterl = retype_ctes_helper[OF pal pdst pno' al'
    le_refl range_cover_sz'[where 'a=32, folded word_bits_def, OF rc] mko rc,simplified] note ht_rl = clift_eq_h_t_valid_eq[OF rl', OF tag_disj_via_td_name, simplified] have guard:
    "\<forall>n<2 ^ (pageBits - objBitsKO ko). c_guard (CTypesDefs.ptr_add ?ptr (of_nat n))" apply (rule retype_guard_helper[where m = 2]) apply (rule range_cover_rel[OF rc]) apply fastforce apply simp apply (clarsimp simp:objBits_simps ko_def archObjSize_def) apply (simp add:ptr0) apply (simp add:szo) apply (simp add:align_of_def objBits_simps pageBits_def ko_def archObjSize_def)+ done have cslift_ptr_retyp_helper:
   "\<forall>x::asid_pool_C ptr\<in>dom (cslift x). is_aligned (ptr_val x) (objBitsKO ko)
   \<Longrightarrow> clift (hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False)
           (hrs_mem_update (heap_update_list frame (replicate ((2::nat) ^ pageBits) (0::word8)))
             (t_hrs_' (globals x)))) =
   (\<lambda>y::asid_pool_C ptr.
       if y \<in> (CTypesDefs.ptr_add (ap_Ptr frame) \<circ> of_nat) ` {k::nat. k < (2::nat) ^ (pageBits - objBitsKO ko)}
       then Some (from_bytes (replicate (size_of TYPE(asid_pool_C)) (0::word8))) else cslift x y)" using guard apply (subst clift_ptr_retyps_gen_memset_same, simp_all add: szo szko) apply (simp add: szo empty szko) done from rf have "cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x))" unfolding rf_sr_def cstate_relation_def by (simp add: Let_def) hence "cpspace_relation ?ks (underlying_memory (ksMachineState \<sigma>)) ?ks'" unfolding cpspace_relation_def apply - supply image_cong_simp [cong del] apply (clarsimp simp: rl' cterl[unfolded ko_def] tag_disj_via_td_name
                 foldr_upd_app_if [folded data_map_insert_def] cte_C_size tcb_C_size) apply (subst cslift_ptr_retyp_helper[simplified]) apply (erule pspace_aligned_to_C [OF pal]) apply (simp add: projectKOs ko_def) apply (simp add: ko_def projectKOs objBits_simps archObjSize_def) apply (simp add: ptr_add_to_new_cap_addrs [OF szo] ht_rl) apply (simp add: rl[unfolded ko_def] projectKO_opt_retyp_same ko_def projectKOs cong: if_cong) apply (simp add:objBits_simps archObjSize_def) apply (erule cmap_relation_retype) apply (rule relrl) done thus ?thesis using rf empty kdr zro apply (simp add: rf_sr_def cstate_relation_def Let_def rl' tag_disj_via_td_name
                     ko_def[symmetric]) apply (simp add: carch_state_relation_def cmachine_state_relation_def) apply (simp add: rl' cterl tag_disj_via_td_name h_t_valid_clift_Some_iff tcb_C_size) apply (clarsimp simp: hrs_htd_update ptr_retyps_htd_safe_neg szo szko
                          kernel_data_refs_domain_eq_rotate
                          cvariable_array_ptr_retyps[OF szo]
                          foldr_upd_app_if [folded data_map_insert_def]
                          zero_ranges_ptr_retyps
                          rl empty projectKOs) done qed have [simp]:
    "of_nat pageBits < (4::word32) = False" by (simp add: pageBits_def) show ?thesis apply (rule ccorres_from_vcg_nofail2, rule allI) apply (rule conseqPre) apply vcg apply (clarsimp simp: cte_wp_at_ctes_of split: if_split_asm) apply (frule(1) ctes_of_valid', clarsimp) apply (subst ghost_assertion_size_logic[unfolded o_def, rotated], assumption) apply (drule(1) valid_global_refsD_with_objSize) apply (simp add: ARMSmallPageBits_def pageBits_def) apply (erule valid_untyped_capE) apply (subst simpler_placeNewObject_def) apply ((simp add:word_bits_conv objBits_simps archObjSize_def
        capAligned_def)+)[4] apply (simp add:simpler_modify_def rf_sr_htd_safe) apply (subgoal_tac "{frame ..+ 2 ^ pageBits} \<inter> kernel_data_refs = {}") prefer 2 apply (drule(1) valid_global_refsD') apply (clarsimp simp:Int_commute pageBits_def ARMSmallPageBits_def
     intvl_range_conv[where bits = pageBits,unfolded pageBits_def word_bits_def,simplified]) apply (intro conjI impI) apply (erule is_aligned_no_wrap') apply (clarsimp simp:ARMSmallPageBits_def pageBits_def) apply (erule is_aligned_weaken,simp add:pageBits_def) apply (simp add:is_aligned_def ARMSmallPageBits_def) apply (simp add: region_actually_is_bytes_dom_s pageBits_def ARMSmallPageBits_def) apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def
                         kernel_data_refs_domain_eq_rotate
                         size_of_def pageBits_def
                         ptr_retyp_htd_safe_neg) apply clarsimp apply (cut_tac helper [rule_format]) prefer 2 apply fastforce apply (subst data_map_insert_def[symmetric]) apply (erule iffD1[OF rf_sr_upd,rotated -1 ]) apply simp_all apply (simp add: hrs_htd_update_def hrs_mem_update_def split_def) apply (simp add: pageBits_def ARMSmallPageBits_def ptr_retyps_gen_def
              del:replicate_numeral) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc ((\<lambda>s. \<exists>p. cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap isdev frame pageBits idx) p s) and pspace_aligned' and pspace_distinct' and valid_objs' and (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {frame..+2 ^ pageBits}) and valid_global_refs' and pspace_no_overlap' frame pageBits) {s. region_actually_is_bytes frame (2 ^ pageBits) s} hs (placeNewObject frame makeObject 0) (CALL memzero_'proc(PTR(unit) frame,2 ^ unat ARMSmallPageBits);;
Guard MemorySafety \<lbrace>htd_safe domain (hrs_htd \<acute>t_hrs) \<and> htd_safe domain (ptr_retyp (ap_Ptr frame) (hrs_htd \<acute>t_hrs))\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_htd_update (ptr_retyp (ap_Ptr frame))))) proof (state)
goal (1 subgoal):
 1. ccorres dc xfdc ((\<lambda>s. \<exists>p. cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap isdev frame pageBits idx) p s) and pspace_aligned' and pspace_distinct' and valid_objs' and (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {frame..+2 ^ pageBits}) and valid_global_refs' and pspace_no_overlap' frame pageBits) {s. region_actually_is_bytes frame (2 ^ pageBits) s} hs (placeNewObject frame makeObject 0) (CALL memzero_'proc(PTR(unit) frame,2 ^ unat ARMSmallPageBits);;
Guard MemorySafety \<lbrace>htd_safe domain (hrs_htd \<acute>t_hrs) \<and> htd_safe domain (ptr_retyp (ap_Ptr frame) (hrs_htd \<acute>t_hrs))\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_htd_update (ptr_retyp (ap_Ptr frame))))) proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> is_aligned frame pageBits \<and> frame \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' frame pageBits \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {frame..+2 ^ pageBits}) \<sigma> \<and> region_actually_is_bytes frame (2 ^ pageBits) x \<and> {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {} \<longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr proof (state)
goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> is_aligned frame pageBits \<and> frame \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' frame pageBits \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {frame..+2 ^ pageBits}) \<sigma> \<and> region_actually_is_bytes frame (2 ^ pageBits) x \<and> {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr proof (state)
goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> is_aligned frame pageBits \<and> frame \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' frame pageBits \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {frame..+2 ^ pageBits}) \<sigma> \<and> region_actually_is_bytes frame (2 ^ pageBits) x \<and> {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr proof (state)
goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> is_aligned frame pageBits \<and> frame \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' frame pageBits \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {frame..+2 ^ pageBits}) \<sigma> \<and> region_actually_is_bytes frame (2 ^ pageBits) x \<and> {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr proof (state)
goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> is_aligned frame pageBits \<and> frame \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' frame pageBits \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {frame..+2 ^ pageBits}) \<sigma> \<and> region_actually_is_bytes frame (2 ^ pageBits) x \<and> {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr proof (state)
goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> is_aligned frame pageBits \<and> frame \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' frame pageBits \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {frame..+2 ^ pageBits}) \<sigma> \<and> region_actually_is_bytes frame (2 ^ pageBits) x \<and> {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr proof (state)
goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> is_aligned frame pageBits \<and> frame \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' frame pageBits \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {frame..+2 ^ pageBits}) \<sigma> \<and> region_actually_is_bytes frame (2 ^ pageBits) x \<and> {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr proof (state)
this:
(\<sigma>, x) \<in> rf_sr \<and> is_aligned frame pageBits \<and> frame \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' frame pageBits \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {frame..+2 ^ pageBits}) \<sigma> \<and> region_actually_is_bytes frame (2 ^ pageBits) x \<and> {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {}

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> is_aligned frame pageBits \<and> frame \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' frame pageBits \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {frame..+2 ^ pageBits}) \<sigma> \<and> region_actually_is_bytes frame (2 ^ pageBits) x \<and> {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
using this:
(\<sigma>, x) \<in> rf_sr \<and> is_aligned frame pageBits \<and> frame \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' frame pageBits \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {frame..+2 ^ pageBits}) \<sigma> \<and> region_actually_is_bytes frame (2 ^ pageBits) x \<and> {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {}

goal (1 subgoal):
 1. (((\<sigma>, x) \<in> rf_sr &&& is_aligned frame pageBits) &&& frame \<noteq> 0 &&& pspace_aligned' \<sigma>) &&& (pspace_distinct' \<sigma> &&& pspace_no_overlap' frame pageBits \<sigma>) &&& (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {frame..+2 ^ pageBits}) \<sigma> &&& region_actually_is_bytes frame (2 ^ pageBits) x &&& {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {} proof (state)
this:
(\<sigma>, x) \<in> rf_sr
is_aligned frame pageBits
frame \<noteq> 0
pspace_aligned' \<sigma>
pspace_distinct' \<sigma>
pspace_no_overlap' frame pageBits \<sigma>
(valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {frame..+2 ^ pageBits}) \<sigma>
region_actually_is_bytes frame (2 ^ pageBits) x
{frame..+2 ^ pageBits} \<inter> kernel_data_refs = {}

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> is_aligned frame pageBits \<and> frame \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' frame pageBits \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {frame..+2 ^ pageBits}) \<sigma> \<and> region_actually_is_bytes frame (2 ^ pageBits) x \<and> {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr proof (state)
this:
region_is_bytes frame (2 ^ pageBits) x

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> is_aligned frame pageBits \<and> frame \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' frame pageBits \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {frame..+2 ^ pageBits}) \<sigma> \<and> region_actually_is_bytes frame (2 ^ pageBits) x \<and> {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. casid_pool_relation makeObject (from_bytes (replicate (size_of TYPE(asid_pool_C)) 0)) proof (prove)
goal (1 subgoal):
 1. case makeObject of asidpool.ASIDPool pool \<Rightarrow> case from_bytes (replicate (size_of TYPE(asid_pool_C)) 0) of asid_pool_C.asid_pool_C cpool \<Rightarrow> array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_low_bits - 1) pool cpool proof (prove)
goal (1 subgoal):
 1. \<And>x. from_bytes (replicate (size_of TYPE(asid_pool_C)) 0) = asid_pool_C.asid_pool_C x \<Longrightarrow> array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_low_bits - 1) (const None) x proof (prove)
goal (1 subgoal):
 1. \<And>x i. \<lbrakk>from_bytes (replicate (size_of TYPE(asid_pool_C)) 0) = asid_pool_C.asid_pool_C x; i \<le> 2 ^ local.asid_low_bits - 1\<rbrakk> \<Longrightarrow> NULL = x.[unat i] proof (prove)
goal (1 subgoal):
 1. \<And>x i. \<lbrakk>update_ti_t (typ_info_t TYPE(asid_pool_C)) (replicate (size_of TYPE(asid_pool_C)) 0) undefined = asid_pool_C.asid_pool_C x; i \<le> 2 ^ local.asid_low_bits - 1\<rbrakk> \<Longrightarrow> NULL = x.[unat i] proof (prove)
goal (1 subgoal):
 1. \<And>x i. \<lbrakk>update_ti_t (final_pad (ti_typ_pad_combine TYPE(pde_C ptr[1024]) array_C (array_C_update \<circ> (\<lambda>x _. x)) ''array_C'' (empty_typ_info ''asid_pool_C''))) (replicate (size_td (typ_info_t TYPE(pde_C ptr[1024])) + padup (2 ^ align_td (typ_info_t TYPE(pde_C ptr[1024]))) (size_td (typ_info_t TYPE(pde_C ptr[1024])))) 0) undefined = asid_pool_C.asid_pool_C x; i \<le> 2 ^ local.asid_low_bits - 1\<rbrakk> \<Longrightarrow> NULL = x.[unat i] proof (prove)
goal (1 subgoal):
 1. \<And>x i. \<lbrakk>update_ti_t (if 0 < padup (2 ^ align_td (typ_info_t TYPE(pde_C ptr[1024]))) (size_td (typ_info_t TYPE(pde_C ptr[1024]))) then ti_pad_combine (padup (2 ^ align_td (typ_info_t TYPE(pde_C ptr[1024]))) (size_td (typ_info_t TYPE(pde_C ptr[1024])))) (ti_typ_pad_combine TYPE(pde_C ptr[1024]) array_C (array_C_update \<circ> (\<lambda>x _. x)) ''array_C'' (empty_typ_info ''asid_pool_C'')) else ti_typ_pad_combine TYPE(pde_C ptr[1024]) array_C (array_C_update \<circ> (\<lambda>x _. x)) ''array_C'' (empty_typ_info ''asid_pool_C'')) (replicate (size_td (typ_info_t TYPE(pde_C ptr[1024])) + padup (2 ^ align_td (typ_info_t TYPE(pde_C ptr[1024]))) (size_td (typ_info_t TYPE(pde_C ptr[1024])))) 0) undefined = asid_pool_C.asid_pool_C x; i \<le> 2 ^ local.asid_low_bits - 1\<rbrakk> \<Longrightarrow> NULL = x.[unat i] proof (prove)
goal (1 subgoal):
 1. \<And>x i. \<lbrakk>update_ti_t (if 0 < (4 - size_td (typ_info_t TYPE(pde_C ptr[1024])) mod 4) mod 4 then ti_pad_combine (padup (2 ^ align_td (typ_info_t TYPE(pde_C ptr[1024]))) (size_td (typ_info_t TYPE(pde_C ptr[1024])))) (ti_typ_pad_combine TYPE(pde_C ptr[1024]) array_C (array_C_update \<circ> (\<lambda>x _. x)) ''array_C'' (empty_typ_info ''asid_pool_C'')) else ti_typ_pad_combine TYPE(pde_C ptr[1024]) array_C (array_C_update \<circ> (\<lambda>x _. x)) ''array_C'' (empty_typ_info ''asid_pool_C'')) (replicate (size_td (typ_info_t TYPE(pde_C ptr[1024])) + (4 - size_td (typ_info_t TYPE(pde_C ptr[1024])) mod 4) mod 4) 0) undefined = asid_pool_C.asid_pool_C x; i \<le> 2 ^ local.asid_low_bits - 1\<rbrakk> \<Longrightarrow> NULL = x.[unat i] proof (prove)
goal (1 subgoal):
 1. \<And>x i. \<lbrakk>update_ti_t (if 0 < (4 - CARD(1024) * size_of TYPE(pde_C ptr) mod 4) mod 4 then ti_pad_combine (padup (2 ^ align_td (typ_info_t TYPE(pde_C ptr[1024]))) (size_td (typ_info_t TYPE(pde_C ptr[1024])))) (ti_typ_pad_combine TYPE(pde_C ptr[1024]) array_C (array_C_update \<circ> (\<lambda>x _. x)) ''array_C'' (empty_typ_info ''asid_pool_C'')) else ti_typ_pad_combine TYPE(pde_C ptr[1024]) array_C (array_C_update \<circ> (\<lambda>x _. x)) ''array_C'' (empty_typ_info ''asid_pool_C'')) (replicate (size_td (typ_info_t TYPE(pde_C ptr[1024])) + (4 - size_td (typ_info_t TYPE(pde_C ptr[1024])) mod 4) mod 4) 0) undefined = asid_pool_C.asid_pool_C x; i \<le> 2 ^ local.asid_low_bits - 1\<rbrakk> \<Longrightarrow> NULL = x.[unat i] proof (prove)
goal (1 subgoal):
 1. \<And>x i. \<lbrakk>update_ti_t (ti_typ_pad_combine TYPE(pde_C ptr[1024]) array_C (array_C_update \<circ> (\<lambda>x _. x)) ''array_C'' (empty_typ_info ''asid_pool_C'')) (replicate (size_td (typ_info_t TYPE(pde_C ptr[1024])) + (4 - size_td (typ_info_t TYPE(pde_C ptr[1024])) mod 4) mod 4) 0) undefined = asid_pool_C.asid_pool_C x; i \<le> 2 ^ local.asid_low_bits - 1\<rbrakk> \<Longrightarrow> NULL = x.[unat i] proof (prove)
goal (1 subgoal):
 1. \<And>x i. \<lbrakk>array_C_update (\<lambda>_. update_ti_t (typ_info_t TYPE(pde_C ptr[1024])) (replicate 4096 0) (array_C undefined)) undefined = asid_pool_C.asid_pool_C x; i \<le> 2 ^ local.asid_low_bits - 1\<rbrakk> \<Longrightarrow> NULL = x.[unat i] proof (prove)
goal (1 subgoal):
 1. \<And>x i. \<lbrakk>array_C_update (\<lambda>_. update_ti_t (array_tag_n 1024) (replicate 4096 0) (array_C undefined)) undefined = asid_pool_C.asid_pool_C x; i \<le> 2 ^ local.asid_low_bits - 1\<rbrakk> \<Longrightarrow> NULL = x.[unat i] proof (prove)
goal (1 subgoal):
 1. \<And>x i. \<lbrakk>i \<le> 2 ^ local.asid_low_bits - 1; update_ti_t (array_tag_n 1024) (replicate 4096 0) (array_C undefined) = x\<rbrakk> \<Longrightarrow> NULL = x.[unat i] proof (prove)
goal (1 subgoal):
 1. \<And>i. i \<le> 2 ^ local.asid_low_bits - 1 \<Longrightarrow> NULL = update_ti_t (array_tag_n 1024) (replicate 4096 0) (array_C undefined).[unat i] proof (prove)
goal (3 subgoals):
 1. \<And>i. i \<le> 2 ^ local.asid_low_bits - 1 \<Longrightarrow> replicate 4096 0 = replicate (1024 * size_td (typ_info_t TYPE(pde_C ptr))) (?v14 i)
 2. \<And>i. i \<le> 2 ^ local.asid_low_bits - 1 \<Longrightarrow> 1024 \<le> CARD(1024)
 3. \<And>i. i \<le> 2 ^ local.asid_low_bits - 1 \<Longrightarrow> NULL = foldr (\<lambda>n arr. Arrays.update arr n (update_ti_t (typ_info_t TYPE(pde_C ptr)) (replicate (size_td (typ_info_t TYPE(pde_C ptr))) (?v14 i)) (arr.[n]))) [0..<1024] (array_C undefined).[unat i] proof (prove)
goal (2 subgoals):
 1. \<And>i. i \<le> 2 ^ local.asid_low_bits - 1 \<Longrightarrow> 1024 \<le> CARD(1024)
 2. \<And>i. i \<le> 2 ^ local.asid_low_bits - 1 \<Longrightarrow> NULL = foldr (\<lambda>n arr. Arrays.update arr n (update_ti_t (typ_info_t TYPE(pde_C ptr)) (replicate (size_td (typ_info_t TYPE(pde_C ptr))) 0) (arr.[n]))) [0..<1024] (array_C undefined).[unat i] proof (prove)
goal (1 subgoal):
 1. \<And>i. i \<le> 2 ^ local.asid_low_bits - 1 \<Longrightarrow> NULL = foldr (\<lambda>n arr. Arrays.update arr n (update_ti_t (typ_info_t TYPE(pde_C ptr)) (replicate (size_td (typ_info_t TYPE(pde_C ptr))) 0) (arr.[n]))) [0..<1024] (array_C undefined).[unat i] proof (prove)
goal (1 subgoal):
 1. \<And>i. i \<le> 2 ^ local.asid_low_bits - 1 \<Longrightarrow> NULL = foldr (\<lambda>n arr. Arrays.update arr n (update_ti_t (typ_info_t TYPE(pde_C ptr)) (replicate 4 0) (arr.[n]))) [0..<1024] (array_C undefined).[unat i] proof (prove)
goal (4 subgoals):
 1. \<And>i. i \<le> 2 ^ local.asid_low_bits - 1 \<Longrightarrow> distinct [0..<1024]
 2. \<And>i. i \<le> 2 ^ local.asid_low_bits - 1 \<Longrightarrow> set [0..<1024] \<subseteq> {..<CARD(1024)}
 3. \<And>i. i \<le> 2 ^ local.asid_low_bits - 1 \<Longrightarrow> unat i < CARD(1024)
 4. \<And>i. i \<le> 2 ^ local.asid_low_bits - 1 \<Longrightarrow> NULL = (if unat i \<in> set [0..<1024] then update_ti_t (typ_info_t TYPE(pde_C ptr)) (replicate 4 0) (array_C undefined.[unat i]) else array_C undefined.[unat i]) proof (prove)
goal (3 subgoals):
 1. \<And>i. i \<le> 2 ^ local.asid_low_bits - 1 \<Longrightarrow> set [0..<1024] \<subseteq> {..<CARD(1024)}
 2. \<And>i. i \<le> 2 ^ local.asid_low_bits - 1 \<Longrightarrow> unat i < CARD(1024)
 3. \<And>i. i \<le> 2 ^ local.asid_low_bits - 1 \<Longrightarrow> NULL = (if unat i \<in> set [0..<1024] then update_ti_t (typ_info_t TYPE(pde_C ptr)) (replicate 4 0) (array_C undefined.[unat i]) else array_C undefined.[unat i]) proof (prove)
goal (2 subgoals):
 1. \<And>i. i \<le> 2 ^ local.asid_low_bits - 1 \<Longrightarrow> unat i < CARD(1024)
 2. \<And>i. i \<le> 2 ^ local.asid_low_bits - 1 \<Longrightarrow> NULL = (if unat i \<in> set [0..<1024] then update_ti_t (typ_info_t TYPE(pde_C ptr)) (replicate 4 0) (array_C undefined.[unat i]) else array_C undefined.[unat i]) proof (prove)
goal (1 subgoal):
 1. \<And>i. i \<le> 2 ^ local.asid_low_bits - 1 \<Longrightarrow> NULL = (if unat i \<in> set [0..<1024] then update_ti_t (typ_info_t TYPE(pde_C ptr)) (replicate 4 0) (array_C undefined.[unat i]) else array_C undefined.[unat i]) proof (prove)
goal (1 subgoal):
 1. \<And>i. i \<le> 2 ^ local.asid_low_bits - 1 \<Longrightarrow> (unat i < 1024 \<longrightarrow> NULL = update_ti_t (typ_info_t TYPE(pde_C ptr)) [0, 0, 0, 0] (array_C undefined.[unat i])) \<and> (\<not> unat i < 1024 \<longrightarrow> NULL = array_C undefined.[unat i]) proof (prove)
goal (2 subgoals):
 1. \<And>i. i \<le> 2 ^ local.asid_low_bits - 1 \<Longrightarrow> unat i < 1024 \<longrightarrow> NULL = update_ti_t (typ_info_t TYPE(pde_C ptr)) [0, 0, 0, 0] (array_C undefined.[unat i])
 2. \<And>i. i \<le> 2 ^ local.asid_low_bits - 1 \<Longrightarrow> \<not> unat i < 1024 \<longrightarrow> NULL = array_C undefined.[unat i] proof (prove)
goal (1 subgoal):
 1. \<And>i. i \<le> 2 ^ local.asid_low_bits - 1 \<Longrightarrow> \<not> unat i < 1024 \<longrightarrow> NULL = array_C undefined.[unat i] proof (prove)
goal:
No subgoals! proof (state)
this:
casid_pool_relation makeObject (from_bytes (replicate (size_of TYPE(asid_pool_C)) 0))

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> is_aligned frame pageBits \<and> frame \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' frame pageBits \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {frame..+2 ^ pageBits}) \<sigma> \<and> region_actually_is_bytes frame (2 ^ pageBits) x \<and> {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr proof (state)
this:
ko \<equiv> KOArch (KOASIDPool makeObject)

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> is_aligned frame pageBits \<and> frame \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' frame pageBits \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {frame..+2 ^ pageBits}) \<sigma> \<and> region_actually_is_bytes frame (2 ^ pageBits) x \<and> {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. range_cover frame (objBitsKO ko) (objBitsKO ko) (Suc 0) proof (state)
this:
range_cover frame (objBitsKO ko) (objBitsKO ko) (Suc 0)

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> is_aligned frame pageBits \<and> frame \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' frame pageBits \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {frame..+2 ^ pageBits}) \<sigma> \<and> region_actually_is_bytes frame (2 ^ pageBits) x \<and> {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. range_cover frame (objBitsKO ko) (objBitsKO ko) (2 ^ 0) proof (state)
this:
range_cover frame (objBitsKO ko) (objBitsKO ko) (2 ^ 0)

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> is_aligned frame pageBits \<and> frame \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' frame pageBits \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {frame..+2 ^ pageBits}) \<sigma> \<and> region_actually_is_bytes frame (2 ^ pageBits) x \<and> {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. pspace_no_overlap' frame (objBitsKO ko) \<sigma> proof (state)
this:
pspace_no_overlap' frame (objBitsKO ko) \<sigma>

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> is_aligned frame pageBits \<and> frame \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' frame pageBits \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {frame..+2 ^ pageBits}) \<sigma> \<and> region_actually_is_bytes frame (2 ^ pageBits) x \<and> {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. is_aligned frame (objBitsKO ko) proof (state)
this:
is_aligned frame (objBitsKO ko)

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> is_aligned frame pageBits \<and> frame \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' frame pageBits \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {frame..+2 ^ pageBits}) \<sigma> \<and> region_actually_is_bytes frame (2 ^ pageBits) x \<and> {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr proof (state)
this:
is_aligned frame (objBitsKO ko)

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> is_aligned frame pageBits \<and> frame \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' frame pageBits \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {frame..+2 ^ pageBits}) \<sigma> \<and> region_actually_is_bytes frame (2 ^ pageBits) x \<and> {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. size_of TYPE(asid_pool_C) = 2 ^ objBitsKO ko proof (state)
this:
size_of TYPE(asid_pool_C) = 2 ^ objBitsKO ko

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> is_aligned frame pageBits \<and> frame \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' frame pageBits \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {frame..+2 ^ pageBits}) \<sigma> \<and> region_actually_is_bytes frame (2 ^ pageBits) x \<and> {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. objBitsKO ko = pageBits proof (state)
this:
objBitsKO ko = pageBits

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> is_aligned frame pageBits \<and> frame \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' frame pageBits \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {frame..+2 ^ pageBits}) \<sigma> \<and> region_actually_is_bytes frame (2 ^ pageBits) x \<and> {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
using this:
objBitsKO ko = pageBits

goal (1 subgoal):
 1. objBitsKO ko \<le> pageBits proof (state)
this:
objBitsKO ko \<le> pageBits

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> is_aligned frame pageBits \<and> frame \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' frame pageBits \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {frame..+2 ^ pageBits}) \<sigma> \<and> region_actually_is_bytes frame (2 ^ pageBits) x \<and> {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. 2 ^ pageBits = 2 ^ (pageBits - objBitsKO ko) * size_of TYPE(asid_pool_C) proof (prove)
using this:
objBitsKO ko = pageBits

goal (1 subgoal):
 1. 2 ^ pageBits = 2 ^ (pageBits - objBitsKO ko) * size_of TYPE(asid_pool_C) proof (prove)
goal (1 subgoal):
 1. objBitsKO ko = pageBits \<Longrightarrow> 2 ^ pageBits = 2 ^ (pageBits - objBitsKO ko) * 2 ^ objBitsKO ko proof (prove)
goal:
No subgoals! proof (state)
this:
2 ^ pageBits = 2 ^ (pageBits - objBitsKO ko) * size_of TYPE(asid_pool_C)

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> is_aligned frame pageBits \<and> frame \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' frame pageBits \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {frame..+2 ^ pageBits}) \<sigma> \<and> region_actually_is_bytes frame (2 ^ pageBits) x \<and> {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. 2 ^ (pageBits - objBitsKO ko) * 2 ^ objBitsKO ko = 2 ^ pageBits proof (state)
this:
2 ^ (pageBits - objBitsKO ko) * 2 ^ objBitsKO ko = 2 ^ pageBits

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> is_aligned frame pageBits \<and> frame \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' frame pageBits \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {frame..+2 ^ pageBits}) \<sigma> \<and> region_actually_is_bytes frame (2 ^ pageBits) x \<and> {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. hrs_htd_update (ptr_retyps (2 ^ (pageBits - objBitsKO ko)) (ap_Ptr frame)) = hrs_htd_update (ptr_retyp (ap_Ptr frame)) proof (prove)
goal:
No subgoals! proof (state)
this:
hrs_htd_update (ptr_retyps (2 ^ (pageBits - objBitsKO ko)) (ap_Ptr frame)) = hrs_htd_update (ptr_retyp (ap_Ptr frame))

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> is_aligned frame pageBits \<and> frame \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' frame pageBits \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {frame..+2 ^ pageBits}) \<sigma> \<and> region_actually_is_bytes frame (2 ^ pageBits) x \<and> {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr proof (state)
this:
\<lbrakk>typ_uinfo_t TYPE(?'b) \<bottom>\<^sub>t typ_uinfo_t TYPE(asid_pool_C); typ_uinfo_t TYPE(?'b) \<noteq> typ_uinfo_t TYPE(8 word)\<rbrakk> \<Longrightarrow> clift (hrs_htd_update (ptr_retyps_gen (Suc 0) (ap_Ptr frame) ?arr) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))) = cslift x

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> is_aligned frame pageBits \<and> frame \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' frame pageBits \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {frame..+2 ^ pageBits}) \<sigma> \<and> region_actually_is_bytes frame (2 ^ pageBits) x \<and> {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. pageBits < word_bits proof (state)
this:
pageBits < word_bits

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> is_aligned frame pageBits \<and> frame \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' frame pageBits \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {frame..+2 ^ pageBits}) \<sigma> \<and> region_actually_is_bytes frame (2 ^ pageBits) x \<and> {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>dev. makeObjectKO dev (Inl (KOArch (KOASIDPool f))) = Some ko proof (state)
this:
makeObjectKO ?dev2 (Inl (KOArch (KOASIDPool f))) = Some ko

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> is_aligned frame pageBits \<and> frame \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' frame pageBits \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {frame..+2 ^ pageBits}) \<sigma> \<and> region_actually_is_bytes frame (2 ^ pageBits) x \<and> {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr proof (state)
this:
\<forall>v. projectKO_opt (KOArch (KOASIDPool makeObject)) \<noteq> Some v \<Longrightarrow> projectKO_opt \<circ>\<^sub>m (\<lambda>x. if x \<in> set (new_cap_addrs (Suc 0) frame ko) then Some ko else ksPSpace \<sigma> x) = projectKO_opt \<circ>\<^sub>m ksPSpace \<sigma>

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> is_aligned frame pageBits \<and> frame \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' frame pageBits \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {frame..+2 ^ pageBits}) \<sigma> \<and> region_actually_is_bytes frame (2 ^ pageBits) x \<and> {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr proof (state)
this:
map_to_ctes (\<lambda>xa. if xa \<in> set (new_cap_addrs (Suc 0) frame ko) then Some ko else ksPSpace \<sigma> xa) = ctes_of \<sigma>

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> is_aligned frame pageBits \<and> frame \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' frame pageBits \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {frame..+2 ^ pageBits}) \<sigma> \<and> region_actually_is_bytes frame (2 ^ pageBits) x \<and> {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr proof (state)
this:
\<lbrakk>typ_name (typ_info_t TYPE(?'b1)) \<noteq> ''!pad_typ''; typ_name (typ_info_t TYPE(?'b1)) \<noteq> ''pde_C+ptr'' \<and> typ_name (typ_info_t TYPE(?'b1)) \<noteq> ''asid_pool_C'' \<and> typ_name (typ_info_t TYPE(?'b1)) \<noteq> ''pde_C+ptr_array_000000000010''; ''asid_pool_C'' \<notin> td_names (typ_info_t TYPE(?'b1)); typ_uinfo_t TYPE(?'b1) \<noteq> typ_uinfo_t TYPE(8 word)\<rbrakk> \<Longrightarrow> h_t_valid (hrs_htd (hrs_htd_update (ptr_retyps_gen (Suc 0) (ap_Ptr frame) ?arr1) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x))))) c_guard = c_h_t_valid x

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> is_aligned frame pageBits \<and> frame \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' frame pageBits \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {frame..+2 ^ pageBits}) \<sigma> \<and> region_actually_is_bytes frame (2 ^ pageBits) x \<and> {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<forall>n<2 ^ (pageBits - objBitsKO ko). c_guard (ap_Ptr frame +\<^sub>p int n) proof (prove)
goal (5 subgoals):
 1. range_cover frame ?sz (objBitsKO ?ko) (2 ^ (pageBits - objBitsKO ko))
 2. frame \<noteq> 0
 3. size_of TYPE(asid_pool_C) = 2 ^ objBitsKO ?ko
 4. 2 \<le> objBitsKO ?ko
 5. align_of TYPE(asid_pool_C) = 2\<^sup>2 proof (prove)
goal (6 subgoals):
 1. objBitsKO ?ko \<le> objBitsKO ko
 2. 2 ^ (pageBits - objBitsKO ko) = 2 ^ (objBitsKO ko - objBitsKO ?ko) * Suc 0
 3. frame \<noteq> 0
 4. size_of TYPE(asid_pool_C) = 2 ^ objBitsKO ?ko
 5. 2 \<le> objBitsKO ?ko
 6. align_of TYPE(asid_pool_C) = 2\<^sup>2 proof (prove)
goal (5 subgoals):
 1. 2 ^ (pageBits - objBitsKO ko) = 2 ^ (objBitsKO ko - objBitsKO ko) * Suc 0
 2. frame \<noteq> 0
 3. size_of TYPE(asid_pool_C) = 2 ^ objBitsKO ko
 4. 2 \<le> objBitsKO ko
 5. align_of TYPE(asid_pool_C) = 2\<^sup>2 proof (prove)
goal (5 subgoals):
 1. pageBits \<le> objBitsKO ko
 2. frame \<noteq> 0
 3. size_of TYPE(asid_pool_C) = 2 ^ objBitsKO ko
 4. 2 \<le> objBitsKO ko
 5. align_of TYPE(asid_pool_C) = 2\<^sup>2 proof (prove)
goal (4 subgoals):
 1. frame \<noteq> 0
 2. size_of TYPE(asid_pool_C) = 2 ^ objBitsKO ko
 3. 2 \<le> objBitsKO ko
 4. align_of TYPE(asid_pool_C) = 2\<^sup>2 proof (prove)
goal (3 subgoals):
 1. size_of TYPE(asid_pool_C) = 2 ^ objBitsKO ko
 2. 2 \<le> objBitsKO ko
 3. align_of TYPE(asid_pool_C) = 2\<^sup>2 proof (prove)
goal (2 subgoals):
 1. 2 \<le> objBitsKO ko
 2. align_of TYPE(asid_pool_C) = 2\<^sup>2 proof (prove)
goal:
No subgoals! proof (state)
this:
\<forall>n<2 ^ (pageBits - objBitsKO ko). c_guard (ap_Ptr frame +\<^sub>p int n)

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> is_aligned frame pageBits \<and> frame \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' frame pageBits \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {frame..+2 ^ pageBits}) \<sigma> \<and> region_actually_is_bytes frame (2 ^ pageBits) x \<and> {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>dom (cslift x). is_aligned (ptr_val x) (objBitsKO ko) \<Longrightarrow> clift (hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))) = (\<lambda>y. if y \<in> ((+\<^sub>p) (ap_Ptr frame) \<circ> int) ` {k. k < 2 ^ (pageBits - objBitsKO ko)} then Some (from_bytes (replicate (size_of TYPE(asid_pool_C)) 0)) else cslift x y) proof (prove)
using this:
\<forall>n<2 ^ (pageBits - objBitsKO ko). c_guard (ap_Ptr frame +\<^sub>p int n)

goal (1 subgoal):
 1. \<forall>x\<in>dom (cslift x). is_aligned (ptr_val x) (objBitsKO ko) \<Longrightarrow> clift (hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))) = (\<lambda>y. if y \<in> ((+\<^sub>p) (ap_Ptr frame) \<circ> int) ` {k. k < 2 ^ (pageBits - objBitsKO ko)} then Some (from_bytes (replicate (size_of TYPE(asid_pool_C)) 0)) else cslift x y) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>dom (cslift x). is_aligned (ptr_val x) pageBits; c_guard (ap_Ptr frame)\<rbrakk> \<Longrightarrow> region_is_bytes frame (2 ^ pageBits) x proof (prove)
goal:
No subgoals! proof (state)
this:
\<forall>x\<in>dom (cslift x). is_aligned (ptr_val x) (objBitsKO ko) \<Longrightarrow> clift (hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))) = (\<lambda>y. if y \<in> ((+\<^sub>p) (ap_Ptr frame) \<circ> int) ` {k. k < 2 ^ (pageBits - objBitsKO ko)} then Some (from_bytes (replicate (size_of TYPE(asid_pool_C)) 0)) else cslift x y)

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> is_aligned frame pageBits \<and> frame \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' frame pageBits \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {frame..+2 ^ pageBits}) \<sigma> \<and> region_actually_is_bytes frame (2 ^ pageBits) x \<and> {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr proof (chain)
picking this:
(\<sigma>, x) \<in> rf_sr proof (prove)
using this:
(\<sigma>, x) \<in> rf_sr

goal (1 subgoal):
 1. cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)) proof (prove)
using this:
(\<sigma>, x) \<in> {(s, s'). let cheap = t_hrs_' (globals s') in cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s)) cheap \<and> cready_queues_relation (clift cheap) (ksReadyQueues_' (globals s')) (ksReadyQueues s) \<and> zero_ranges_are_zero (gsUntypedZeroRanges s) cheap \<and> cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s) \<and> cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s) \<and> ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s) \<and> ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread s) \<and> cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')) \<and> cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s')) \<and> carch_state_relation (ksArchState s) (globals s') \<and> cmachine_state_relation (ksMachineState s) (globals s') \<and> cte_array_relation s (globals s') \<and> tcb_cte_array_relation s (globals s') \<and> apsnd fst (ghost'state_' (globals s')) = (gsUserPages s, gsCNodes s) \<and> ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s) \<and> ksWorkUnitsCompleted_' (globals s') = ksWorkUnitsCompleted s \<and> s' \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr \<and> ptr_span intStateIRQNode_array_Ptr \<subseteq> kernel_data_refs \<and> s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr \<and> ptr_span armKSGlobalPD_Ptr \<subseteq> kernel_data_refs \<and> htd_safe domain (hrs_htd (t_hrs_' (globals s'))) \<and> - domain \<subseteq> kernel_data_refs \<and> globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list \<and> cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule \<and> ksDomScheduleIdx_' (globals s') = word_of_nat (ksDomScheduleIdx s) \<and> ksCurDomain_' (globals s') = UCAST(8 \<rightarrow> 32) (ksCurDomain s) \<and> ksDomainTime_' (globals s') = ksDomainTime s}

goal (1 subgoal):
 1. cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)) proof (state)
this:
cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x))

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> is_aligned frame pageBits \<and> frame \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' frame pageBits \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {frame..+2 ^ pageBits}) \<sigma> \<and> region_actually_is_bytes frame (2 ^ pageBits) x \<and> {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
using this:
cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x))

goal (1 subgoal):
 1. cpspace_relation (foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))) proof (prove)
using this:
cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation \<and> cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation \<and> cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)) \<and> cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)) \<and> cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation \<and> cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation \<and> cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation \<and> cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation \<and> cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation \<and> carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr \<and> carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr

goal (1 subgoal):
 1. cmap_relation (map_to_ctes (foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x))))) cte_Ptr ccte_relation \<and> cpspace_tcb_relation (foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)) (hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))) \<and> cmap_relation (map_to_eps (foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x))))) ep_Ptr (cendpoint_relation (clift (hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))))) \<and> cmap_relation (map_to_ntfns (foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x))))) ntfn_Ptr (cnotification_relation (clift (hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))))) \<and> cmap_relation (map_to_pdes (foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x))))) pde_Ptr cpde_relation \<and> cmap_relation (map_to_ptes (foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x))))) pte_Ptr cpte_relation \<and> cmap_relation (map_to_asidpools (foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x))))) ap_Ptr casid_pool_relation \<and> cpspace_user_data_relation (foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))) \<and> cpspace_device_data_relation (foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))) \<and> cpspace_pde_array_relation (foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)) (hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))) \<and> cpspace_pte_array_relation (foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)) (hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))) proof (prove)
goal (1 subgoal):
 1. cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation \<and> cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation \<and> cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)) \<and> cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)) \<and> cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation \<and> cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation \<and> cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation \<and> cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation \<and> cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation \<and> carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr \<and> carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr \<Longrightarrow> cmap_relation (map_to_ctes (foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x))))) cte_Ptr ccte_relation \<and> cpspace_tcb_relation (foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)) (hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))) \<and> cmap_relation (map_to_eps (foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x))))) ep_Ptr (cendpoint_relation (clift (hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))))) \<and> cmap_relation (map_to_ntfns (foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x))))) ntfn_Ptr (cnotification_relation (clift (hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))))) \<and> cmap_relation (map_to_pdes (foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x))))) pde_Ptr cpde_relation \<and> cmap_relation (map_to_ptes (foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x))))) pte_Ptr cpte_relation \<and> cmap_relation (map_to_asidpools (foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x))))) ap_Ptr casid_pool_relation \<and> cpspace_user_data_relation (foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))) \<and> cpspace_device_data_relation (foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))) \<and> cpspace_pde_array_relation (foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)) (hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))) \<and> cpspace_pte_array_relation (foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)) (hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))) proof (prove)
goal (1 subgoal):
 1. cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation \<and> cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation \<and> cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)) \<and> cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)) \<and> cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation \<and> cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation \<and> cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation \<and> cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation \<and> cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation \<and> carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr \<and> carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr \<Longrightarrow> cmap_relation (map_to_ctes (foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x))))) cte_Ptr ccte_relation \<and> cpspace_tcb_relation (foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)) (hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))) \<and> cmap_relation (map_to_eps (foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x))))) ep_Ptr (cendpoint_relation (clift (hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))))) \<and> cmap_relation (map_to_ntfns (foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x))))) ntfn_Ptr (cnotification_relation (clift (hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))))) \<and> cmap_relation (map_to_pdes (foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x))))) pde_Ptr cpde_relation \<and> cmap_relation (map_to_ptes (foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x))))) pte_Ptr cpte_relation \<and> cmap_relation (map_to_asidpools (foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x))))) ap_Ptr casid_pool_relation \<and> cpspace_user_data_relation (foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))) \<and> cpspace_device_data_relation (foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))) \<and> cpspace_pde_array_relation (foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)) (hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))) \<and> cpspace_pte_array_relation (foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)) (hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr\<rbrakk> \<Longrightarrow> cmap_relation (map_to_tcbs (\<lambda>x. if x \<in> set (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) then Some (KOArch (KOASIDPool makeObject)) else ksPSpace \<sigma> x)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation \<and> cmap_relation (map_to_eps (\<lambda>x. if x \<in> set (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) then Some (KOArch (KOASIDPool makeObject)) else ksPSpace \<sigma> x)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)) \<and> cmap_relation (map_to_ntfns (\<lambda>x. if x \<in> set (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) then Some (KOArch (KOASIDPool makeObject)) else ksPSpace \<sigma> x)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)) \<and> cmap_relation (map_to_pdes (\<lambda>x. if x \<in> set (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) then Some (KOArch (KOASIDPool makeObject)) else ksPSpace \<sigma> x)) (cslift x) pde_Ptr cpde_relation \<and> cmap_relation (map_to_ptes (\<lambda>x. if x \<in> set (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) then Some (KOArch (KOASIDPool makeObject)) else ksPSpace \<sigma> x)) (cslift x) pte_Ptr cpte_relation \<and> cmap_relation (map_to_asidpools (\<lambda>x. if x \<in> set (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) then Some (KOArch (KOASIDPool makeObject)) else ksPSpace \<sigma> x)) (clift (hrs_htd_update (ptr_retyps_gen (Suc 0) (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x))))) ap_Ptr casid_pool_relation \<and> cmap_relation (heap_to_user_data (\<lambda>x. if x \<in> set (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) then Some (KOArch (KOASIDPool makeObject)) else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation \<and> cmap_relation (heap_to_device_data (\<lambda>x. if x \<in> set (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) then Some (KOArch (KOASIDPool makeObject)) else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation \<and> cpspace_pde_array_relation (\<lambda>x. if x \<in> set (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) then Some (KOArch (KOASIDPool makeObject)) else ksPSpace \<sigma> x) (hrs_htd_update (ptr_retyps_gen (Suc 0) (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))) \<and> cpspace_pte_array_relation (\<lambda>x. if x \<in> set (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) then Some (KOArch (KOASIDPool makeObject)) else ksPSpace \<sigma> x) (hrs_htd_update (ptr_retyps_gen (Suc 0) (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr\<rbrakk> \<Longrightarrow> \<forall>x\<in>dom (cslift x). is_aligned (ptr_val x) (objBitsKO ko)
 2. \<lbrakk>cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr\<rbrakk> \<Longrightarrow> cmap_relation (map_to_tcbs (\<lambda>x. if x \<in> set (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) then Some (KOArch (KOASIDPool makeObject)) else ksPSpace \<sigma> x)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation \<and> cmap_relation (map_to_eps (\<lambda>x. if x \<in> set (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) then Some (KOArch (KOASIDPool makeObject)) else ksPSpace \<sigma> x)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)) \<and> cmap_relation (map_to_ntfns (\<lambda>x. if x \<in> set (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) then Some (KOArch (KOASIDPool makeObject)) else ksPSpace \<sigma> x)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)) \<and> cmap_relation (map_to_pdes (\<lambda>x. if x \<in> set (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) then Some (KOArch (KOASIDPool makeObject)) else ksPSpace \<sigma> x)) (cslift x) pde_Ptr cpde_relation \<and> cmap_relation (map_to_ptes (\<lambda>x. if x \<in> set (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) then Some (KOArch (KOASIDPool makeObject)) else ksPSpace \<sigma> x)) (cslift x) pte_Ptr cpte_relation \<and> cmap_relation (map_to_asidpools (\<lambda>x. if x \<in> set (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) then Some (KOArch (KOASIDPool makeObject)) else ksPSpace \<sigma> x)) (\<lambda>y. if y \<in> ((+\<^sub>p) (ap_Ptr frame) \<circ> int) ` {k. k < 2 ^ (pageBits - objBitsKO ko)} then Some (from_bytes (replicate (size_of TYPE(asid_pool_C)) 0)) else cslift x y) ap_Ptr casid_pool_relation \<and> cmap_relation (heap_to_user_data (\<lambda>x. if x \<in> set (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) then Some (KOArch (KOASIDPool makeObject)) else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation \<and> cmap_relation (heap_to_device_data (\<lambda>x. if x \<in> set (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) then Some (KOArch (KOASIDPool makeObject)) else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation \<and> cpspace_pde_array_relation (\<lambda>x. if x \<in> set (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) then Some (KOArch (KOASIDPool makeObject)) else ksPSpace \<sigma> x) (hrs_htd_update (ptr_retyps_gen (Suc 0) (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))) \<and> cpspace_pte_array_relation (\<lambda>x. if x \<in> set (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) then Some (KOArch (KOASIDPool makeObject)) else ksPSpace \<sigma> x) (hrs_htd_update (ptr_retyps_gen (Suc 0) (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr\<rbrakk> \<Longrightarrow> projectKO_opt ko = Some ?v17
 2. \<And>ko' v'. \<lbrakk>cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr; projectKO_opt ko' = Some v'\<rbrakk> \<Longrightarrow> objBitsKO ko = objBitsKO ko'
 3. \<lbrakk>cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr\<rbrakk> \<Longrightarrow> cmap_relation (map_to_tcbs (\<lambda>x. if x \<in> set (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) then Some (KOArch (KOASIDPool makeObject)) else ksPSpace \<sigma> x)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation \<and> cmap_relation (map_to_eps (\<lambda>x. if x \<in> set (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) then Some (KOArch (KOASIDPool makeObject)) else ksPSpace \<sigma> x)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)) \<and> cmap_relation (map_to_ntfns (\<lambda>x. if x \<in> set (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) then Some (KOArch (KOASIDPool makeObject)) else ksPSpace \<sigma> x)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)) \<and> cmap_relation (map_to_pdes (\<lambda>x. if x \<in> set (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) then Some (KOArch (KOASIDPool makeObject)) else ksPSpace \<sigma> x)) (cslift x) pde_Ptr cpde_relation \<and> cmap_relation (map_to_ptes (\<lambda>x. if x \<in> set (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) then Some (KOArch (KOASIDPool makeObject)) else ksPSpace \<sigma> x)) (cslift x) pte_Ptr cpte_relation \<and> cmap_relation (map_to_asidpools (\<lambda>x. if x \<in> set (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) then Some (KOArch (KOASIDPool makeObject)) else ksPSpace \<sigma> x)) (\<lambda>y. if y \<in> ((+\<^sub>p) (ap_Ptr frame) \<circ> int) ` {k. k < 2 ^ (pageBits - objBitsKO ko)} then Some (from_bytes (replicate (size_of TYPE(asid_pool_C)) 0)) else cslift x y) ap_Ptr casid_pool_relation \<and> cmap_relation (heap_to_user_data (\<lambda>x. if x \<in> set (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) then Some (KOArch (KOASIDPool makeObject)) else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation \<and> cmap_relation (heap_to_device_data (\<lambda>x. if x \<in> set (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) then Some (KOArch (KOASIDPool makeObject)) else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation \<and> cpspace_pde_array_relation (\<lambda>x. if x \<in> set (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) then Some (KOArch (KOASIDPool makeObject)) else ksPSpace \<sigma> x) (hrs_htd_update (ptr_retyps_gen (Suc 0) (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))) \<and> cpspace_pte_array_relation (\<lambda>x. if x \<in> set (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) then Some (KOArch (KOASIDPool makeObject)) else ksPSpace \<sigma> x) (hrs_htd_update (ptr_retyps_gen (Suc 0) (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))) proof (prove)
goal (2 subgoals):
 1. \<And>ko' v'. \<lbrakk>cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr; projectKO_opt ko' = Some v'\<rbrakk> \<Longrightarrow> objBitsKO ko = objBitsKO ko'
 2. \<lbrakk>cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr\<rbrakk> \<Longrightarrow> cmap_relation (map_to_tcbs (\<lambda>x. if x \<in> set (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) then Some (KOArch (KOASIDPool makeObject)) else ksPSpace \<sigma> x)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation \<and> cmap_relation (map_to_eps (\<lambda>x. if x \<in> set (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) then Some (KOArch (KOASIDPool makeObject)) else ksPSpace \<sigma> x)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)) \<and> cmap_relation (map_to_ntfns (\<lambda>x. if x \<in> set (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) then Some (KOArch (KOASIDPool makeObject)) else ksPSpace \<sigma> x)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)) \<and> cmap_relation (map_to_pdes (\<lambda>x. if x \<in> set (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) then Some (KOArch (KOASIDPool makeObject)) else ksPSpace \<sigma> x)) (cslift x) pde_Ptr cpde_relation \<and> cmap_relation (map_to_ptes (\<lambda>x. if x \<in> set (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) then Some (KOArch (KOASIDPool makeObject)) else ksPSpace \<sigma> x)) (cslift x) pte_Ptr cpte_relation \<and> cmap_relation (map_to_asidpools (\<lambda>x. if x \<in> set (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) then Some (KOArch (KOASIDPool makeObject)) else ksPSpace \<sigma> x)) (\<lambda>y. if y \<in> ((+\<^sub>p) (ap_Ptr frame) \<circ> int) ` {k. k < 2 ^ (pageBits - objBitsKO ko)} then Some (from_bytes (replicate (size_of TYPE(asid_pool_C)) 0)) else cslift x y) ap_Ptr casid_pool_relation \<and> cmap_relation (heap_to_user_data (\<lambda>x. if x \<in> set (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) then Some (KOArch (KOASIDPool makeObject)) else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation \<and> cmap_relation (heap_to_device_data (\<lambda>x. if x \<in> set (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) then Some (KOArch (KOASIDPool makeObject)) else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation \<and> cpspace_pde_array_relation (\<lambda>x. if x \<in> set (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) then Some (KOArch (KOASIDPool makeObject)) else ksPSpace \<sigma> x) (hrs_htd_update (ptr_retyps_gen (Suc 0) (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))) \<and> cpspace_pte_array_relation (\<lambda>x. if x \<in> set (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) then Some (KOArch (KOASIDPool makeObject)) else ksPSpace \<sigma> x) (hrs_htd_update (ptr_retyps_gen (Suc 0) (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr\<rbrakk> \<Longrightarrow> cmap_relation (map_to_tcbs (\<lambda>x. if x \<in> set (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) then Some (KOArch (KOASIDPool makeObject)) else ksPSpace \<sigma> x)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation \<and> cmap_relation (map_to_eps (\<lambda>x. if x \<in> set (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) then Some (KOArch (KOASIDPool makeObject)) else ksPSpace \<sigma> x)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)) \<and> cmap_relation (map_to_ntfns (\<lambda>x. if x \<in> set (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) then Some (KOArch (KOASIDPool makeObject)) else ksPSpace \<sigma> x)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)) \<and> cmap_relation (map_to_pdes (\<lambda>x. if x \<in> set (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) then Some (KOArch (KOASIDPool makeObject)) else ksPSpace \<sigma> x)) (cslift x) pde_Ptr cpde_relation \<and> cmap_relation (map_to_ptes (\<lambda>x. if x \<in> set (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) then Some (KOArch (KOASIDPool makeObject)) else ksPSpace \<sigma> x)) (cslift x) pte_Ptr cpte_relation \<and> cmap_relation (map_to_asidpools (\<lambda>x. if x \<in> set (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) then Some (KOArch (KOASIDPool makeObject)) else ksPSpace \<sigma> x)) (\<lambda>y. if y \<in> ((+\<^sub>p) (ap_Ptr frame) \<circ> int) ` {k. k < 2 ^ (pageBits - objBitsKO ko)} then Some (from_bytes (replicate (size_of TYPE(asid_pool_C)) 0)) else cslift x y) ap_Ptr casid_pool_relation \<and> cmap_relation (heap_to_user_data (\<lambda>x. if x \<in> set (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) then Some (KOArch (KOASIDPool makeObject)) else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation \<and> cmap_relation (heap_to_device_data (\<lambda>x. if x \<in> set (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) then Some (KOArch (KOASIDPool makeObject)) else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation \<and> cpspace_pde_array_relation (\<lambda>x. if x \<in> set (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) then Some (KOArch (KOASIDPool makeObject)) else ksPSpace \<sigma> x) (hrs_htd_update (ptr_retyps_gen (Suc 0) (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))) \<and> cpspace_pte_array_relation (\<lambda>x. if x \<in> set (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) then Some (KOArch (KOASIDPool makeObject)) else ksPSpace \<sigma> x) (hrs_htd_update (ptr_retyps_gen (Suc 0) (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr\<rbrakk> \<Longrightarrow> cmap_relation (map_to_tcbs (\<lambda>x. if x \<in> set (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) then Some (KOArch (KOASIDPool makeObject)) else ksPSpace \<sigma> x)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation \<and> cmap_relation (map_to_eps (\<lambda>x. if x \<in> set (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) then Some (KOArch (KOASIDPool makeObject)) else ksPSpace \<sigma> x)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)) \<and> cmap_relation (map_to_ntfns (\<lambda>x. if x \<in> set (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) then Some (KOArch (KOASIDPool makeObject)) else ksPSpace \<sigma> x)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)) \<and> cmap_relation (map_to_pdes (\<lambda>x. if x \<in> set (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) then Some (KOArch (KOASIDPool makeObject)) else ksPSpace \<sigma> x)) (cslift x) pde_Ptr cpde_relation \<and> cmap_relation (map_to_ptes (\<lambda>x. if x \<in> set (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) then Some (KOArch (KOASIDPool makeObject)) else ksPSpace \<sigma> x)) (cslift x) pte_Ptr cpte_relation \<and> cmap_relation (map_to_asidpools (\<lambda>x. if x \<in> set (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) then Some (KOArch (KOASIDPool makeObject)) else ksPSpace \<sigma> x)) (\<lambda>y. if y \<in> ap_Ptr ` set (new_cap_addrs (2 ^ (pageBits - objBitsKO ko)) frame ko) then Some (from_bytes (replicate (size_of TYPE(asid_pool_C)) 0)) else cslift x y) ap_Ptr casid_pool_relation \<and> cmap_relation (heap_to_user_data (\<lambda>x. if x \<in> set (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) then Some (KOArch (KOASIDPool makeObject)) else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation \<and> cmap_relation (heap_to_device_data (\<lambda>x. if x \<in> set (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) then Some (KOArch (KOASIDPool makeObject)) else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation \<and> carray_map_relation pdBits (map_to_pdes (\<lambda>x. if x \<in> set (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) then Some (KOArch (KOASIDPool makeObject)) else ksPSpace \<sigma> x)) (c_h_t_valid x) pd_Ptr \<and> carray_map_relation ptBits (map_to_ptes (\<lambda>x. if x \<in> set (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) then Some (KOArch (KOASIDPool makeObject)) else ksPSpace \<sigma> x)) (c_h_t_valid x) pt_Ptr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr\<rbrakk> \<Longrightarrow> cmap_relation (\<lambda>x. if x \<in> set (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) then Some makeObject else map_to_asidpools (ksPSpace \<sigma>) x) (\<lambda>y. if y \<in> ap_Ptr ` set (new_cap_addrs (2 ^ (pageBits - objBitsKO (KOArch (KOASIDPool makeObject)))) frame (KOArch (KOASIDPool makeObject))) then Some (from_bytes (replicate (size_of TYPE(asid_pool_C)) 0)) else cslift x y) ap_Ptr casid_pool_relation proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr\<rbrakk> \<Longrightarrow> cmap_relation (\<lambda>x. if x \<in> set (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) then Some makeObject else map_to_asidpools (ksPSpace \<sigma>) x) (\<lambda>y. if y \<in> ap_Ptr ` set (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) then Some (from_bytes (replicate (size_of TYPE(asid_pool_C)) 0)) else cslift x y) ap_Ptr casid_pool_relation proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr\<rbrakk> \<Longrightarrow> casid_pool_relation makeObject (from_bytes (replicate (size_of TYPE(asid_pool_C)) 0)) proof (prove)
goal:
No subgoals! proof (state)
this:
cpspace_relation (foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x))))

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> is_aligned frame pageBits \<and> frame \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' frame pageBits \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {frame..+2 ^ pageBits}) \<sigma> \<and> region_actually_is_bytes frame (2 ^ pageBits) x \<and> {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
using this:
cpspace_relation (foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x))))

goal (1 subgoal):
 1. (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
using this:
cpspace_relation (foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x))))
(\<sigma>, x) \<in> rf_sr
region_is_bytes frame (2 ^ pageBits) x
{frame..+2 ^ pageBits} \<inter> kernel_data_refs = {}
(valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {frame..+2 ^ pageBits}) \<sigma>

goal (1 subgoal):
 1. (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cpspace_relation (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs (Suc 0) frame ko) (ksPSpace \<sigma>)) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen (Suc 0) (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))); cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)) \<and> cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>) \<and> zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)) \<and> cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>) \<and> cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>) \<and> ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>) \<and> ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>) \<and> cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)) \<and> cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)) \<and> carch_state_relation (ksArchState \<sigma>) (globals x) \<and> cmachine_state_relation (ksMachineState \<sigma>) (globals x) \<and> cte_array_relation \<sigma> (globals x) \<and> tcb_cte_array_relation \<sigma> (globals x) \<and> apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>) \<and> ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>) \<and> ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma> \<and> x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr \<and> {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs \<and> x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr \<and> {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs \<and> htd_safe domain (hrs_htd (t_hrs_' (globals x))) \<and> - domain \<subseteq> kernel_data_refs \<and> globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list \<and> cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule \<and> ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>) \<and> ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>) \<and> ksDomainTime_' (globals x) = ksDomainTime \<sigma>; region_is_bytes frame (2 ^ pageBits) x; {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {}; valid_objs' \<sigma> \<and> untyped_ranges_zero' \<sigma> \<and> caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>\<rbrakk> \<Longrightarrow> zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (hrs_htd_update (ptr_retyps_gen (Suc 0) (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))) \<and> carch_state_relation (ksArchState \<sigma>) (globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen (Suc 0) (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))\<rparr>) \<and> cmachine_state_relation (ksMachineState \<sigma>) (globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen (Suc 0) (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))\<rparr>) \<and> cvariable_array_map_relation (gsCNodes \<sigma>) ((^) 2) cte_Ptr (hrs_htd (hrs_htd_update (ptr_retyps_gen (Suc 0) (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x))))) \<and> cvariable_array_map_relation (map_to_tcbs (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs (Suc 0) frame ko) (ksPSpace \<sigma>))) (\<lambda>x. 5) cte_Ptr (hrs_htd (hrs_htd_update (ptr_retyps_gen (Suc 0) (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x))))) \<and> hrs_htd (hrs_htd_update (ptr_retyps_gen (Suc 0) (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr \<and> hrs_htd (hrs_htd_update (ptr_retyps_gen (Suc 0) (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr \<and> htd_safe domain (hrs_htd (hrs_htd_update (ptr_retyps_gen (Suc 0) (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x))))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cpspace_relation (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs (Suc 0) frame ko) (ksPSpace \<sigma>)) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen (Suc 0) (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))); cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)) \<and> cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>) \<and> zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)) \<and> cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>) \<and> cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>) \<and> ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>) \<and> ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>) \<and> cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)) \<and> cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)) \<and> armKSNextASID_' (globals x) = armKSNextASID (ksArchState \<sigma>) \<and> armKSKernelVSpace (ksArchState \<sigma>) = armKSKernelVSpace_C \<and> array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState \<sigma>)) (armKSHWASIDTable_' (globals x)) \<and> array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState \<sigma>)) (armKSASIDTable_' (globals x)) \<and> asid_map_pd_to_hwasids (armKSASIDMap (ksArchState \<sigma>)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift x \<circ>\<^sub>m pd_pointer_to_asid_slot) \<and> carch_globals (ksArchState \<sigma>) \<and> irq_masks (ksMachineState \<sigma>) = irq_masks (phantom_machine_state_' (globals x)) \<and> irq_state (ksMachineState \<sigma>) = irq_state (phantom_machine_state_' (globals x)) \<and> device_state (ksMachineState \<sigma>) = device_state (phantom_machine_state_' (globals x)) \<and> exclusive_state (ksMachineState \<sigma>) = exclusive_state (phantom_machine_state_' (globals x)) \<and> machine_state_rest (ksMachineState \<sigma>) = machine_state_rest (phantom_machine_state_' (globals x)) \<and> cte_array_relation \<sigma> (globals x) \<and> tcb_cte_array_relation \<sigma> (globals x) \<and> apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>) \<and> ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>) \<and> ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma> \<and> x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr \<and> {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs \<and> x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr \<and> {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs \<and> htd_safe domain (hrs_htd (t_hrs_' (globals x))) \<and> - domain \<subseteq> kernel_data_refs \<and> globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list \<and> cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule \<and> ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>) \<and> ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>) \<and> ksDomainTime_' (globals x) = ksDomainTime \<sigma>; region_is_bytes frame (2 ^ pageBits) x; {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {}; valid_objs' \<sigma> \<and> untyped_ranges_zero' \<sigma> \<and> caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>\<rbrakk> \<Longrightarrow> zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (hrs_htd_update (ptr_retyps_gen (Suc 0) (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))) \<and> set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift x \<circ>\<^sub>m pd_pointer_to_asid_slot) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (hrs_htd_update (ptr_retyps_gen (Suc 0) (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))) \<circ>\<^sub>m pd_pointer_to_asid_slot) \<and> cvariable_array_map_relation (gsCNodes \<sigma>) ((^) 2) cte_Ptr (hrs_htd (hrs_htd_update (ptr_retyps_gen (Suc 0) (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x))))) \<and> cvariable_array_map_relation (map_to_tcbs (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs (Suc 0) frame ko) (ksPSpace \<sigma>))) (\<lambda>x. 5) cte_Ptr (hrs_htd (hrs_htd_update (ptr_retyps_gen (Suc 0) (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x))))) \<and> hrs_htd (hrs_htd_update (ptr_retyps_gen (Suc 0) (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr \<and> hrs_htd (hrs_htd_update (ptr_retyps_gen (Suc 0) (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr \<and> htd_safe domain (hrs_htd (hrs_htd_update (ptr_retyps_gen (Suc 0) (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x))))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cpspace_relation (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs (Suc 0) frame ko) (ksPSpace \<sigma>)) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen (Suc 0) (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))); cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)) \<and> cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>) \<and> zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)) \<and> cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>) \<and> cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>) \<and> ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>) \<and> ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>) \<and> cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)) \<and> cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)) \<and> armKSNextASID_' (globals x) = armKSNextASID (ksArchState \<sigma>) \<and> armKSKernelVSpace (ksArchState \<sigma>) = armKSKernelVSpace_C \<and> array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState \<sigma>)) (armKSHWASIDTable_' (globals x)) \<and> array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState \<sigma>)) (armKSASIDTable_' (globals x)) \<and> asid_map_pd_to_hwasids (armKSASIDMap (ksArchState \<sigma>)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift x \<circ>\<^sub>m pd_pointer_to_asid_slot) \<and> carch_globals (ksArchState \<sigma>) \<and> irq_masks (ksMachineState \<sigma>) = irq_masks (phantom_machine_state_' (globals x)) \<and> irq_state (ksMachineState \<sigma>) = irq_state (phantom_machine_state_' (globals x)) \<and> device_state (ksMachineState \<sigma>) = device_state (phantom_machine_state_' (globals x)) \<and> exclusive_state (ksMachineState \<sigma>) = exclusive_state (phantom_machine_state_' (globals x)) \<and> machine_state_rest (ksMachineState \<sigma>) = machine_state_rest (phantom_machine_state_' (globals x)) \<and> cte_array_relation \<sigma> (globals x) \<and> tcb_cte_array_relation \<sigma> (globals x) \<and> apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>) \<and> ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>) \<and> ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma> \<and> (\<exists>v. cslift x intStateIRQNode_array_Ptr = Some v) \<and> {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs \<and> (\<exists>v. cslift x armKSGlobalPD_Ptr = Some v) \<and> {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs \<and> htd_safe domain (hrs_htd (t_hrs_' (globals x))) \<and> - domain \<subseteq> kernel_data_refs \<and> globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list \<and> cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule \<and> ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>) \<and> ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>) \<and> ksDomainTime_' (globals x) = ksDomainTime \<sigma>; region_is_bytes frame (2 ^ pageBits) x; {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {}; valid_objs' \<sigma> \<and> untyped_ranges_zero' \<sigma> \<and> caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>\<rbrakk> \<Longrightarrow> zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (hrs_htd_update (ptr_retyps_gen (Suc 0) (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))) \<and> cvariable_array_map_relation (gsCNodes \<sigma>) ((^) 2) cte_Ptr (hrs_htd (hrs_htd_update (ptr_retyps_gen (Suc 0) (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x))))) \<and> cvariable_array_map_relation (map_to_tcbs (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs (Suc 0) frame ko) (ksPSpace \<sigma>))) (\<lambda>x. 5) cte_Ptr (hrs_htd (hrs_htd_update (ptr_retyps_gen (Suc 0) (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x))))) \<and> htd_safe domain (hrs_htd (hrs_htd_update (ptr_retyps_gen (Suc 0) (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x))))) proof (prove)
goal:
No subgoals! proof (state)
this:
(\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr

goal:
No subgoals! proof (state)
this:
\<forall>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> is_aligned frame pageBits \<and> frame \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' frame pageBits \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {frame..+2 ^ pageBits}) \<sigma> \<and> region_actually_is_bytes frame (2 ^ pageBits) x \<and> {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {} \<longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr

goal (1 subgoal):
 1. ccorres dc xfdc ((\<lambda>s. \<exists>p. cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap isdev frame pageBits idx) p s) and pspace_aligned' and pspace_distinct' and valid_objs' and (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {frame..+2 ^ pageBits}) and valid_global_refs' and pspace_no_overlap' frame pageBits) {s. region_actually_is_bytes frame (2 ^ pageBits) s} hs (placeNewObject frame makeObject 0) (CALL memzero_'proc(PTR(unit) frame,2 ^ unat ARMSmallPageBits);;
Guard MemorySafety \<lbrace>htd_safe domain (hrs_htd \<acute>t_hrs) \<and> htd_safe domain (ptr_retyp (ap_Ptr frame) (hrs_htd \<acute>t_hrs))\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_htd_update (ptr_retyp (ap_Ptr frame))))) proof (prove)
goal (1 subgoal):
 1. (word_of_nat pageBits < 4) = False proof (state)
this:
(word_of_nat pageBits < 4) = False

goal (1 subgoal):
 1. ccorres dc xfdc ((\<lambda>s. \<exists>p. cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap isdev frame pageBits idx) p s) and pspace_aligned' and pspace_distinct' and valid_objs' and (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {frame..+2 ^ pageBits}) and valid_global_refs' and pspace_no_overlap' frame pageBits) {s. region_actually_is_bytes frame (2 ^ pageBits) s} hs (placeNewObject frame makeObject 0) (CALL memzero_'proc(PTR(unit) frame,2 ^ unat ARMSmallPageBits);;
Guard MemorySafety \<lbrace>htd_safe domain (hrs_htd \<acute>t_hrs) \<and> htd_safe domain (ptr_retyp (ap_Ptr frame) (hrs_htd \<acute>t_hrs))\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_htd_update (ptr_retyp (ap_Ptr frame))))) proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc ((\<lambda>s. \<exists>p. cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap isdev frame pageBits idx) p s) and pspace_aligned' and pspace_distinct' and valid_objs' and (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {frame..+2 ^ pageBits}) and valid_global_refs' and pspace_no_overlap' frame pageBits) {s. region_actually_is_bytes frame (2 ^ pageBits) s} hs (placeNewObject frame makeObject 0) (CALL memzero_'proc(PTR(unit) frame,2 ^ unat ARMSmallPageBits);;
Guard MemorySafety \<lbrace>htd_safe domain (hrs_htd \<acute>t_hrs) \<and> htd_safe domain (ptr_retyp (ap_Ptr frame) (hrs_htd \<acute>t_hrs))\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_htd_update (ptr_retyp (ap_Ptr frame))))) proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma>. \<Gamma>\<turnstile> {s. ((\<lambda>s. \<exists>p. cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap isdev frame pageBits idx) p s) and pspace_aligned' and pspace_distinct' and valid_objs' and (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {frame..+2 ^ pageBits}) and valid_global_refs' and pspace_no_overlap' frame pageBits) \<sigma> \<and> s \<in> {s. region_actually_is_bytes frame (2 ^ pageBits) s} \<and> (\<sigma>, s) \<in> rf_sr \<and> \<not> snd (placeNewObject frame makeObject 0 \<sigma>)} CALL memzero_'proc(PTR(unit) frame,2 ^ unat ARMSmallPageBits);;
Guard MemorySafety \<lbrace>htd_safe domain (hrs_htd \<acute>t_hrs) \<and> htd_safe domain (ptr_retyp (ap_Ptr frame) (hrs_htd \<acute>t_hrs))\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_htd_update (ptr_retyp (ap_Ptr frame)))) {s. \<exists>(rv, \<sigma>')\<in>fst (placeNewObject frame makeObject 0 \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)} proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma>. \<Gamma>\<turnstile> (?P'4 \<sigma>) CALL memzero_'proc(PTR(unit) frame,2 ^ unat ARMSmallPageBits);;
Guard MemorySafety \<lbrace>htd_safe domain (hrs_htd \<acute>t_hrs) \<and> htd_safe domain (ptr_retyp (ap_Ptr frame) (hrs_htd \<acute>t_hrs))\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_htd_update (ptr_retyp (ap_Ptr frame)))) {s. \<exists>(rv, \<sigma>')\<in>fst (placeNewObject frame makeObject 0 \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)}
 2. \<And>\<sigma>. {s. ((\<lambda>s. \<exists>p. cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap isdev frame pageBits idx) p s) and pspace_aligned' and pspace_distinct' and valid_objs' and (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {frame..+2 ^ pageBits}) and valid_global_refs' and pspace_no_overlap' frame pageBits) \<sigma> \<and> s \<in> {s. region_actually_is_bytes frame (2 ^ pageBits) s} \<and> (\<sigma>, s) \<in> rf_sr \<and> \<not> snd (placeNewObject frame makeObject 0 \<sigma>)} \<subseteq> ?P'4 \<sigma> proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma>. {s. ((\<lambda>s. \<exists>p. cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap isdev frame pageBits idx) p s) and pspace_aligned' and pspace_distinct' and valid_objs' and (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {frame..+2 ^ pageBits}) and valid_global_refs' and pspace_no_overlap' frame pageBits) \<sigma> \<and> s \<in> {s. region_actually_is_bytes frame (2 ^ pageBits) s} \<and> (\<sigma>, s) \<in> rf_sr \<and> \<not> snd (placeNewObject frame makeObject 0 \<sigma>)} \<subseteq> {s. ptr_val (PTR(unit) frame) \<noteq> 0 \<and> ptr_val (PTR(unit) frame) \<le> ptr_val (PTR(unit) frame) + (2 ^ unat ARMSmallPageBits - 1) \<and> is_aligned (ptr_val (PTR(unit) frame)) 2 \<and> is_aligned (2 ^ unat ARMSmallPageBits) 2 \<and> {ptr_val (PTR(unit) frame)..+unat (2 ^ unat ARMSmallPageBits)} \<times> insert SIndexVal {x. SIndexTyp 0 = x} \<subseteq> dom_s (hrs_htd (t_hrs_' (globals s))) \<and> ghost_assertion_data_get cap_get_capSizeBits_'proc (\<lambda>x. snd (snd x)) (ghost'state_' (globals s)) \<in> insert 0 {2 ^ unat ARMSmallPageBits..} \<and> (\<forall>t. t_hrs_' (globals t) = hrs_mem_update (heap_update_list (ptr_val (PTR(unit) frame)) (replicate (unat (2 ^ unat ARMSmallPageBits)) (UCAST(?'a25 \<rightarrow> 8) 0))) (t_hrs_' (globals s)) \<longrightarrow> htd_safe domain (hrs_htd (t_hrs_' (globals t))) \<and> htd_safe domain (ptr_retyp (ap_Ptr frame) (hrs_htd (t_hrs_' (globals t)))) \<and> (\<exists>(rv, \<sigma>')\<in>fst (placeNewObject frame makeObject 0 \<sigma>). (\<sigma>', s\<lparr>globals := globals s\<lparr>t_hrs_' := hrs_htd_update (ptr_retyp (ap_Ptr frame)) (t_hrs_' (globals t))\<rparr>\<rparr>) \<in> rf_sr \<and> dc rv (xfdc (s\<lparr>globals := globals s\<lparr>t_hrs_' := hrs_htd_update (ptr_retyp (ap_Ptr frame)) (t_hrs_' (globals t))\<rparr>\<rparr>))))} proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x p cte. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>)\<rbrakk> \<Longrightarrow> frame \<noteq> 0 \<and> frame \<le> frame + (2 ^ unat ARMSmallPageBits - 1) \<and> is_aligned frame 2 \<and> is_aligned (2 ^ unat ARMSmallPageBits) 2 \<and> {frame..+unat (2 ^ unat ARMSmallPageBits)} \<times> {SIndexVal, SIndexTyp 0} \<subseteq> dom_s (hrs_htd (t_hrs_' (globals x))) \<and> (ghost_assertion_data_get cap_get_capSizeBits_'proc (\<lambda>x. snd (snd x)) (ghost'state_' (globals x)) = 0 \<or> 2 ^ unat ARMSmallPageBits \<le> ghost_assertion_data_get cap_get_capSizeBits_'proc (\<lambda>x. snd (snd x)) (ghost'state_' (globals x))) \<and> ((\<exists>t. t_hrs_' (globals t) = hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x))) \<longrightarrow> htd_safe domain (hrs_htd (t_hrs_' (globals x))) \<and> htd_safe domain (ptr_retyp (ap_Ptr frame) (hrs_htd (t_hrs_' (globals x)))) \<and> (\<exists>xa\<in>fst (placeNewObject frame makeObject 0 \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyp (ap_Ptr frame)) (hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr)) proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x p cte. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); valid_cap' (capability.UntypedCap isdev frame pageBits idx) \<sigma>\<rbrakk> \<Longrightarrow> frame \<noteq> 0 \<and> frame \<le> frame + (2 ^ unat ARMSmallPageBits - 1) \<and> is_aligned frame 2 \<and> is_aligned (2 ^ unat ARMSmallPageBits) 2 \<and> {frame..+unat (2 ^ unat ARMSmallPageBits)} \<times> {SIndexVal, SIndexTyp 0} \<subseteq> dom_s (hrs_htd (t_hrs_' (globals x))) \<and> (ghost_assertion_data_get cap_get_capSizeBits_'proc (\<lambda>x. snd (snd x)) (ghost'state_' (globals x)) = 0 \<or> 2 ^ unat ARMSmallPageBits \<le> ghost_assertion_data_get cap_get_capSizeBits_'proc (\<lambda>x. snd (snd x)) (ghost'state_' (globals x))) \<and> ((\<exists>t. t_hrs_' (globals t) = hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x))) \<longrightarrow> htd_safe domain (hrs_htd (t_hrs_' (globals x))) \<and> htd_safe domain (ptr_retyp (ap_Ptr frame) (hrs_htd (t_hrs_' (globals x)))) \<and> (\<exists>xa\<in>fst (placeNewObject frame makeObject 0 \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyp (ap_Ptr frame)) (hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr)) proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x p cte. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); valid_cap' (capability.UntypedCap isdev frame pageBits idx) \<sigma>\<rbrakk> \<Longrightarrow> unat (2 ^ unat ARMSmallPageBits) \<le> gsMaxObjectSize \<sigma>
 2. \<And>\<sigma> x p cte. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); valid_cap' (capability.UntypedCap isdev frame pageBits idx) \<sigma>\<rbrakk> \<Longrightarrow> frame \<noteq> 0 \<and> frame \<le> frame + (2 ^ unat ARMSmallPageBits - 1) \<and> is_aligned frame 2 \<and> is_aligned (2 ^ unat ARMSmallPageBits) 2 \<and> {frame..+unat (2 ^ unat ARMSmallPageBits)} \<times> {SIndexVal, SIndexTyp 0} \<subseteq> dom_s (hrs_htd (t_hrs_' (globals x))) \<and> True \<and> ((\<exists>t. t_hrs_' (globals t) = hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x))) \<longrightarrow> htd_safe domain (hrs_htd (t_hrs_' (globals x))) \<and> htd_safe domain (ptr_retyp (ap_Ptr frame) (hrs_htd (t_hrs_' (globals x)))) \<and> (\<exists>(rv, \<sigma>')\<in>fst (placeNewObject frame makeObject 0 \<sigma>). (\<sigma>', x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyp (ap_Ptr frame)) (hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr)) proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x p cte. \<lbrakk>pspace_aligned' \<sigma>; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); valid_cap' (capability.UntypedCap isdev frame pageBits idx) \<sigma>; kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' \<sigma> \<subseteq> kernel_data_refs \<and> 2 ^ capBits (cteCap cte) \<le> gsMaxObjectSize \<sigma>\<rbrakk> \<Longrightarrow> unat (2 ^ unat ARMSmallPageBits) \<le> gsMaxObjectSize \<sigma>
 2. \<And>\<sigma> x p cte. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); valid_cap' (capability.UntypedCap isdev frame pageBits idx) \<sigma>\<rbrakk> \<Longrightarrow> frame \<noteq> 0 \<and> frame \<le> frame + (2 ^ unat ARMSmallPageBits - 1) \<and> is_aligned frame 2 \<and> is_aligned (2 ^ unat ARMSmallPageBits) 2 \<and> {frame..+unat (2 ^ unat ARMSmallPageBits)} \<times> {SIndexVal, SIndexTyp 0} \<subseteq> dom_s (hrs_htd (t_hrs_' (globals x))) \<and> True \<and> ((\<exists>t. t_hrs_' (globals t) = hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x))) \<longrightarrow> htd_safe domain (hrs_htd (t_hrs_' (globals x))) \<and> htd_safe domain (ptr_retyp (ap_Ptr frame) (hrs_htd (t_hrs_' (globals x)))) \<and> (\<exists>(rv, \<sigma>')\<in>fst (placeNewObject frame makeObject 0 \<sigma>). (\<sigma>', x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyp (ap_Ptr frame)) (hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr)) proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x p cte. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); valid_cap' (capability.UntypedCap isdev frame pageBits idx) \<sigma>\<rbrakk> \<Longrightarrow> frame \<noteq> 0 \<and> frame \<le> frame + (2 ^ unat ARMSmallPageBits - 1) \<and> is_aligned frame 2 \<and> is_aligned (2 ^ unat ARMSmallPageBits) 2 \<and> {frame..+unat (2 ^ unat ARMSmallPageBits)} \<times> {SIndexVal, SIndexTyp 0} \<subseteq> dom_s (hrs_htd (t_hrs_' (globals x))) \<and> True \<and> ((\<exists>t. t_hrs_' (globals t) = hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x))) \<longrightarrow> htd_safe domain (hrs_htd (t_hrs_' (globals x))) \<and> htd_safe domain (ptr_retyp (ap_Ptr frame) (hrs_htd (t_hrs_' (globals x)))) \<and> (\<exists>(rv, \<sigma>')\<in>fst (placeNewObject frame makeObject 0 \<sigma>). (\<sigma>', x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyp (ap_Ptr frame)) (hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr)) proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x p cte. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); is_aligned frame pageBits; valid_untyped' isdev frame pageBits idx \<sigma>; frame \<noteq> 0; pageBits < word_bits\<rbrakk> \<Longrightarrow> frame \<noteq> 0 \<and> frame \<le> frame + (2 ^ unat ARMSmallPageBits - 1) \<and> is_aligned frame 2 \<and> is_aligned (2 ^ unat ARMSmallPageBits) 2 \<and> {frame..+unat (2 ^ unat ARMSmallPageBits)} \<times> {SIndexVal, SIndexTyp 0} \<subseteq> dom_s (hrs_htd (t_hrs_' (globals x))) \<and> True \<and> ((\<exists>t. t_hrs_' (globals t) = hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x))) \<longrightarrow> htd_safe domain (hrs_htd (t_hrs_' (globals x))) \<and> htd_safe domain (ptr_retyp (ap_Ptr frame) (hrs_htd (t_hrs_' (globals x)))) \<and> (\<exists>(rv, \<sigma>')\<in>fst (placeNewObject frame makeObject 0 \<sigma>). (\<sigma>', x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyp (ap_Ptr frame)) (hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr)) proof (prove)
goal (5 subgoals):
 1. \<And>\<sigma> x p cte. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); is_aligned frame pageBits; valid_untyped' isdev frame pageBits idx \<sigma>; frame \<noteq> 0; pageBits < word_bits\<rbrakk> \<Longrightarrow> 0 < word_bits
 2. \<And>\<sigma> x p cte. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); is_aligned frame pageBits; valid_untyped' isdev frame pageBits idx \<sigma>; frame \<noteq> 0; pageBits < word_bits\<rbrakk> \<Longrightarrow> is_aligned frame (objBitsKO (injectKOS makeObject) + 0)
 3. \<And>\<sigma> x p cte. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); is_aligned frame pageBits; valid_untyped' isdev frame pageBits idx \<sigma>; frame \<noteq> 0; pageBits < word_bits\<rbrakk> \<Longrightarrow> pspace_no_overlap' frame (objBitsKO (injectKOS makeObject) + 0) \<sigma>
 4. \<And>\<sigma> x p cte. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); is_aligned frame pageBits; valid_untyped' isdev frame pageBits idx \<sigma>; frame \<noteq> 0; pageBits < word_bits\<rbrakk> \<Longrightarrow> pspace_aligned' \<sigma>
 5. \<And>\<sigma> x p cte. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); is_aligned frame pageBits; valid_untyped' isdev frame pageBits idx \<sigma>; frame \<noteq> 0; pageBits < word_bits\<rbrakk> \<Longrightarrow> frame \<noteq> 0 \<and> frame \<le> frame + (2 ^ unat ARMSmallPageBits - 1) \<and> is_aligned frame 2 \<and> is_aligned (2 ^ unat ARMSmallPageBits) 2 \<and> {frame..+unat (2 ^ unat ARMSmallPageBits)} \<times> {SIndexVal, SIndexTyp 0} \<subseteq> dom_s (hrs_htd (t_hrs_' (globals x))) \<and> True \<and> ((\<exists>t. t_hrs_' (globals t) = hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x))) \<longrightarrow> htd_safe domain (hrs_htd (t_hrs_' (globals x))) \<and> htd_safe domain (ptr_retyp (ap_Ptr frame) (hrs_htd (t_hrs_' (globals x)))) \<and> (\<exists>(rv, \<sigma>')\<in>fst (modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS makeObject)) (new_cap_addrs (2 ^ 0) frame (injectKOS makeObject)) (ksPSpace \<sigma>))) \<sigma>). (\<sigma>', x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyp (ap_Ptr frame)) (hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr)) proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x p cte. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); is_aligned frame pageBits; valid_untyped' isdev frame pageBits idx \<sigma>; frame \<noteq> 0; pageBits < word_bits\<rbrakk> \<Longrightarrow> frame \<noteq> 0 \<and> frame \<le> frame + (2 ^ unat ARMSmallPageBits - 1) \<and> is_aligned frame 2 \<and> is_aligned (2 ^ unat ARMSmallPageBits) 2 \<and> {frame..+unat (2 ^ unat ARMSmallPageBits)} \<times> {SIndexVal, SIndexTyp 0} \<subseteq> dom_s (hrs_htd (t_hrs_' (globals x))) \<and> True \<and> ((\<exists>t. t_hrs_' (globals t) = hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x))) \<longrightarrow> htd_safe domain (hrs_htd (t_hrs_' (globals x))) \<and> htd_safe domain (ptr_retyp (ap_Ptr frame) (hrs_htd (t_hrs_' (globals x)))) \<and> (\<exists>(rv, \<sigma>')\<in>fst (modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS makeObject)) (new_cap_addrs (2 ^ 0) frame (injectKOS makeObject)) (ksPSpace \<sigma>))) \<sigma>). (\<sigma>', x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyp (ap_Ptr frame)) (hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr)) proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x p cte. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); is_aligned frame pageBits; valid_untyped' isdev frame pageBits idx \<sigma>; frame \<noteq> 0\<rbrakk> \<Longrightarrow> frame \<le> frame + (2 ^ unat ARMSmallPageBits - 1) \<and> is_aligned frame 2 \<and> is_aligned (2 ^ unat ARMSmallPageBits) 2 \<and> {frame..+unat (2 ^ unat ARMSmallPageBits)} \<times> {SIndexVal, SIndexTyp 0} \<subseteq> dom_s (hrs_htd (t_hrs_' (globals x))) \<and> ((\<exists>t. t_hrs_' (globals t) = hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x))) \<longrightarrow> htd_safe domain (ptr_retyp (ap_Ptr frame) (hrs_htd (t_hrs_' (globals x)))) \<and> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyp (ap_Ptr frame)) (hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr) proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x p cte. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); is_aligned frame pageBits; valid_untyped' isdev frame pageBits idx \<sigma>; frame \<noteq> 0; {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {}\<rbrakk> \<Longrightarrow> frame \<le> frame + (2 ^ unat ARMSmallPageBits - 1) \<and> is_aligned frame 2 \<and> is_aligned (2 ^ unat ARMSmallPageBits) 2 \<and> {frame..+unat (2 ^ unat ARMSmallPageBits)} \<times> {SIndexVal, SIndexTyp 0} \<subseteq> dom_s (hrs_htd (t_hrs_' (globals x))) \<and> ((\<exists>t. t_hrs_' (globals t) = hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x))) \<longrightarrow> htd_safe domain (ptr_retyp (ap_Ptr frame) (hrs_htd (t_hrs_' (globals x)))) \<and> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyp (ap_Ptr frame)) (hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr)
 2. \<And>\<sigma> x p cte. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); is_aligned frame pageBits; valid_untyped' isdev frame pageBits idx \<sigma>; frame \<noteq> 0\<rbrakk> \<Longrightarrow> {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {} proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x p cte. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); is_aligned frame pageBits; valid_untyped' isdev frame pageBits idx \<sigma>; frame \<noteq> 0\<rbrakk> \<Longrightarrow> {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {}
 2. \<And>\<sigma> x p cte. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); is_aligned frame pageBits; valid_untyped' isdev frame pageBits idx \<sigma>; frame \<noteq> 0; {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {}\<rbrakk> \<Longrightarrow> frame \<le> frame + (2 ^ unat ARMSmallPageBits - 1) \<and> is_aligned frame 2 \<and> is_aligned (2 ^ unat ARMSmallPageBits) 2 \<and> {frame..+unat (2 ^ unat ARMSmallPageBits)} \<times> {SIndexVal, SIndexTyp 0} \<subseteq> dom_s (hrs_htd (t_hrs_' (globals x))) \<and> ((\<exists>t. t_hrs_' (globals t) = hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x))) \<longrightarrow> htd_safe domain (ptr_retyp (ap_Ptr frame) (hrs_htd (t_hrs_' (globals x)))) \<and> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyp (ap_Ptr frame)) (hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr) proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x p cte. \<lbrakk>pspace_aligned' \<sigma>; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); is_aligned frame pageBits; valid_untyped' isdev frame pageBits idx \<sigma>; frame \<noteq> 0; kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' \<sigma> \<subseteq> kernel_data_refs\<rbrakk> \<Longrightarrow> {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {}
 2. \<And>\<sigma> x p cte. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); is_aligned frame pageBits; valid_untyped' isdev frame pageBits idx \<sigma>; frame \<noteq> 0; {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {}\<rbrakk> \<Longrightarrow> frame \<le> frame + (2 ^ unat ARMSmallPageBits - 1) \<and> is_aligned frame 2 \<and> is_aligned (2 ^ unat ARMSmallPageBits) 2 \<and> {frame..+unat (2 ^ unat ARMSmallPageBits)} \<times> {SIndexVal, SIndexTyp 0} \<subseteq> dom_s (hrs_htd (t_hrs_' (globals x))) \<and> ((\<exists>t. t_hrs_' (globals t) = hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x))) \<longrightarrow> htd_safe domain (ptr_retyp (ap_Ptr frame) (hrs_htd (t_hrs_' (globals x)))) \<and> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyp (ap_Ptr frame)) (hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr) proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x p cte. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); is_aligned frame pageBits; valid_untyped' isdev frame pageBits idx \<sigma>; frame \<noteq> 0; {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {}\<rbrakk> \<Longrightarrow> frame \<le> frame + (2 ^ unat ARMSmallPageBits - 1) \<and> is_aligned frame 2 \<and> is_aligned (2 ^ unat ARMSmallPageBits) 2 \<and> {frame..+unat (2 ^ unat ARMSmallPageBits)} \<times> {SIndexVal, SIndexTyp 0} \<subseteq> dom_s (hrs_htd (t_hrs_' (globals x))) \<and> ((\<exists>t. t_hrs_' (globals t) = hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x))) \<longrightarrow> htd_safe domain (ptr_retyp (ap_Ptr frame) (hrs_htd (t_hrs_' (globals x)))) \<and> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyp (ap_Ptr frame)) (hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr) proof (prove)
goal (6 subgoals):
 1. \<And>\<sigma> x p cte. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); is_aligned frame pageBits; valid_untyped' isdev frame pageBits idx \<sigma>; frame \<noteq> 0; {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {}\<rbrakk> \<Longrightarrow> frame \<le> frame + (2 ^ unat ARMSmallPageBits - 1)
 2. \<And>\<sigma> x p cte. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); is_aligned frame pageBits; valid_untyped' isdev frame pageBits idx \<sigma>; frame \<noteq> 0; {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {}\<rbrakk> \<Longrightarrow> is_aligned frame 2
 3. \<And>\<sigma> x p cte. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); is_aligned frame pageBits; valid_untyped' isdev frame pageBits idx \<sigma>; frame \<noteq> 0; {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {}\<rbrakk> \<Longrightarrow> is_aligned (2 ^ unat ARMSmallPageBits) 2
 4. \<And>\<sigma> x p cte. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); is_aligned frame pageBits; valid_untyped' isdev frame pageBits idx \<sigma>; frame \<noteq> 0; {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {}\<rbrakk> \<Longrightarrow> {frame..+unat (2 ^ unat ARMSmallPageBits)} \<times> {SIndexVal, SIndexTyp 0} \<subseteq> dom_s (hrs_htd (t_hrs_' (globals x)))
 5. \<And>\<sigma> x p cte. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); is_aligned frame pageBits; valid_untyped' isdev frame pageBits idx \<sigma>; frame \<noteq> 0; {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {}; \<exists>t. t_hrs_' (globals t) = hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> htd_safe domain (ptr_retyp (ap_Ptr frame) (hrs_htd (t_hrs_' (globals x))))
 6. \<And>\<sigma> x p cte. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); is_aligned frame pageBits; valid_untyped' isdev frame pageBits idx \<sigma>; frame \<noteq> 0; {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {}; \<exists>t. t_hrs_' (globals t) = hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyp (ap_Ptr frame)) (hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (6 subgoals):
 1. \<And>\<sigma> x p cte. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); valid_untyped' isdev frame pageBits idx \<sigma>; frame \<noteq> 0; {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {}\<rbrakk> \<Longrightarrow> 2 ^ unat ARMSmallPageBits - 1 < 2 ^ pageBits
 2. \<And>\<sigma> x p cte. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); is_aligned frame pageBits; valid_untyped' isdev frame pageBits idx \<sigma>; frame \<noteq> 0; {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {}\<rbrakk> \<Longrightarrow> is_aligned frame 2
 3. \<And>\<sigma> x p cte. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); is_aligned frame pageBits; valid_untyped' isdev frame pageBits idx \<sigma>; frame \<noteq> 0; {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {}\<rbrakk> \<Longrightarrow> is_aligned (2 ^ unat ARMSmallPageBits) 2
 4. \<And>\<sigma> x p cte. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); is_aligned frame pageBits; valid_untyped' isdev frame pageBits idx \<sigma>; frame \<noteq> 0; {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {}\<rbrakk> \<Longrightarrow> {frame..+unat (2 ^ unat ARMSmallPageBits)} \<times> {SIndexVal, SIndexTyp 0} \<subseteq> dom_s (hrs_htd (t_hrs_' (globals x)))
 5. \<And>\<sigma> x p cte. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); is_aligned frame pageBits; valid_untyped' isdev frame pageBits idx \<sigma>; frame \<noteq> 0; {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {}; \<exists>t. t_hrs_' (globals t) = hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> htd_safe domain (ptr_retyp (ap_Ptr frame) (hrs_htd (t_hrs_' (globals x))))
 6. \<And>\<sigma> x p cte. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); is_aligned frame pageBits; valid_untyped' isdev frame pageBits idx \<sigma>; frame \<noteq> 0; {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {}; \<exists>t. t_hrs_' (globals t) = hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyp (ap_Ptr frame)) (hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (5 subgoals):
 1. \<And>\<sigma> x p cte. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); is_aligned frame pageBits; valid_untyped' isdev frame pageBits idx \<sigma>; frame \<noteq> 0; {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {}\<rbrakk> \<Longrightarrow> is_aligned frame 2
 2. \<And>\<sigma> x p cte. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); is_aligned frame pageBits; valid_untyped' isdev frame pageBits idx \<sigma>; frame \<noteq> 0; {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {}\<rbrakk> \<Longrightarrow> is_aligned (2 ^ unat ARMSmallPageBits) 2
 3. \<And>\<sigma> x p cte. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); is_aligned frame pageBits; valid_untyped' isdev frame pageBits idx \<sigma>; frame \<noteq> 0; {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {}\<rbrakk> \<Longrightarrow> {frame..+unat (2 ^ unat ARMSmallPageBits)} \<times> {SIndexVal, SIndexTyp 0} \<subseteq> dom_s (hrs_htd (t_hrs_' (globals x)))
 4. \<And>\<sigma> x p cte. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); is_aligned frame pageBits; valid_untyped' isdev frame pageBits idx \<sigma>; frame \<noteq> 0; {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {}; \<exists>t. t_hrs_' (globals t) = hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> htd_safe domain (ptr_retyp (ap_Ptr frame) (hrs_htd (t_hrs_' (globals x))))
 5. \<And>\<sigma> x p cte. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); is_aligned frame pageBits; valid_untyped' isdev frame pageBits idx \<sigma>; frame \<noteq> 0; {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {}; \<exists>t. t_hrs_' (globals t) = hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyp (ap_Ptr frame)) (hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (4 subgoals):
 1. \<And>\<sigma> x p cte. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); is_aligned frame pageBits; valid_untyped' isdev frame pageBits idx \<sigma>; frame \<noteq> 0; {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {}\<rbrakk> \<Longrightarrow> is_aligned (2 ^ unat ARMSmallPageBits) 2
 2. \<And>\<sigma> x p cte. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); is_aligned frame pageBits; valid_untyped' isdev frame pageBits idx \<sigma>; frame \<noteq> 0; {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {}\<rbrakk> \<Longrightarrow> {frame..+unat (2 ^ unat ARMSmallPageBits)} \<times> {SIndexVal, SIndexTyp 0} \<subseteq> dom_s (hrs_htd (t_hrs_' (globals x)))
 3. \<And>\<sigma> x p cte. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); is_aligned frame pageBits; valid_untyped' isdev frame pageBits idx \<sigma>; frame \<noteq> 0; {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {}; \<exists>t. t_hrs_' (globals t) = hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> htd_safe domain (ptr_retyp (ap_Ptr frame) (hrs_htd (t_hrs_' (globals x))))
 4. \<And>\<sigma> x p cte. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); is_aligned frame pageBits; valid_untyped' isdev frame pageBits idx \<sigma>; frame \<noteq> 0; {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {}; \<exists>t. t_hrs_' (globals t) = hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyp (ap_Ptr frame)) (hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (3 subgoals):
 1. \<And>\<sigma> x p cte. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); is_aligned frame pageBits; valid_untyped' isdev frame pageBits idx \<sigma>; frame \<noteq> 0; {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {}\<rbrakk> \<Longrightarrow> {frame..+unat (2 ^ unat ARMSmallPageBits)} \<times> {SIndexVal, SIndexTyp 0} \<subseteq> dom_s (hrs_htd (t_hrs_' (globals x)))
 2. \<And>\<sigma> x p cte. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); is_aligned frame pageBits; valid_untyped' isdev frame pageBits idx \<sigma>; frame \<noteq> 0; {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {}; \<exists>t. t_hrs_' (globals t) = hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> htd_safe domain (ptr_retyp (ap_Ptr frame) (hrs_htd (t_hrs_' (globals x))))
 3. \<And>\<sigma> x p cte. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); is_aligned frame pageBits; valid_untyped' isdev frame pageBits idx \<sigma>; frame \<noteq> 0; {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {}; \<exists>t. t_hrs_' (globals t) = hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyp (ap_Ptr frame)) (hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x p cte. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); is_aligned frame pageBits; valid_untyped' isdev frame pageBits idx \<sigma>; frame \<noteq> 0; {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {}; \<exists>t. t_hrs_' (globals t) = hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> htd_safe domain (ptr_retyp (ap_Ptr frame) (hrs_htd (t_hrs_' (globals x))))
 2. \<And>\<sigma> x p cte. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); is_aligned frame pageBits; valid_untyped' isdev frame pageBits idx \<sigma>; frame \<noteq> 0; {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {}; \<exists>t. t_hrs_' (globals t) = hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyp (ap_Ptr frame)) (hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x p cte. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); is_aligned frame pageBits; valid_untyped' isdev frame pageBits idx \<sigma>; frame \<noteq> 0; {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {}; \<exists>t. t_hrs_' (globals t) = hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyp (ap_Ptr frame)) (hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x p cte t. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); is_aligned frame pageBits; valid_untyped' isdev frame pageBits idx \<sigma>; frame \<noteq> 0; {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {}; t_hrs_' (globals t) = hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyp (ap_Ptr frame)) (hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x p cte t. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); is_aligned frame pageBits; valid_untyped' isdev frame pageBits idx \<sigma>; frame \<noteq> 0; {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {}; t_hrs_' (globals t) = hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x)); (?\<sigma>80 \<sigma> x p cte t\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace (?\<sigma>80 \<sigma> x p cte t))\<rparr>, ?x80 \<sigma> x p cte t\<lparr>globals := globals (?x80 \<sigma> x p cte t)\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals (?x80 \<sigma> x p cte t))))\<rparr>\<rparr>) \<in> rf_sr\<rbrakk> \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyp (ap_Ptr frame)) (hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr
 2. \<And>\<sigma> x p cte t. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); is_aligned frame pageBits; valid_untyped' isdev frame pageBits idx \<sigma>; frame \<noteq> 0; {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {}; t_hrs_' (globals t) = hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> (?\<sigma>80 \<sigma> x p cte t, ?x80 \<sigma> x p cte t) \<in> rf_sr \<and> is_aligned frame pageBits \<and> frame \<noteq> 0 \<and> pspace_aligned' (?\<sigma>80 \<sigma> x p cte t) \<and> pspace_distinct' (?\<sigma>80 \<sigma> x p cte t) \<and> pspace_no_overlap' frame pageBits (?\<sigma>80 \<sigma> x p cte t) \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {frame..+2 ^ pageBits}) (?\<sigma>80 \<sigma> x p cte t) \<and> region_actually_is_bytes frame (2 ^ pageBits) (?x80 \<sigma> x p cte t) \<and> {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {} proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x p cte t. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); is_aligned frame pageBits; valid_untyped' isdev frame pageBits idx \<sigma>; frame \<noteq> 0; {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {}; t_hrs_' (globals t) = hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> (?\<sigma>80 \<sigma> x p cte t, ?x80 \<sigma> x p cte t) \<in> rf_sr \<and> is_aligned frame pageBits \<and> frame \<noteq> 0 \<and> pspace_aligned' (?\<sigma>80 \<sigma> x p cte t) \<and> pspace_distinct' (?\<sigma>80 \<sigma> x p cte t) \<and> pspace_no_overlap' frame pageBits (?\<sigma>80 \<sigma> x p cte t) \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {frame..+2 ^ pageBits}) (?\<sigma>80 \<sigma> x p cte t) \<and> region_actually_is_bytes frame (2 ^ pageBits) (?x80 \<sigma> x p cte t) \<and> {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {}
 2. \<And>\<sigma> x p cte t. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); is_aligned frame pageBits; valid_untyped' isdev frame pageBits idx \<sigma>; frame \<noteq> 0; {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {}; t_hrs_' (globals t) = hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x)); (?\<sigma>80 \<sigma> x p cte t\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace (?\<sigma>80 \<sigma> x p cte t))\<rparr>, ?x80 \<sigma> x p cte t\<lparr>globals := globals (?x80 \<sigma> x p cte t)\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals (?x80 \<sigma> x p cte t))))\<rparr>\<rparr>) \<in> rf_sr\<rbrakk> \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyp (ap_Ptr frame)) (hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x p cte t. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); is_aligned frame pageBits; valid_untyped' isdev frame pageBits idx \<sigma>; frame \<noteq> 0; {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {}; t_hrs_' (globals t) = hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x)); (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr\<rbrakk> \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyp (ap_Ptr frame)) (hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x p cte t. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); is_aligned frame pageBits; valid_untyped' isdev frame pageBits idx \<sigma>; frame \<noteq> 0; {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {}; t_hrs_' (globals t) = hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x)); (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr\<rbrakk> \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOArch (KOASIDPool makeObject))) (new_cap_addrs (Suc 0) frame (KOArch (KOASIDPool makeObject))) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyp (ap_Ptr frame)) (hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (18 subgoals):
 1. \<And>\<sigma> x p cte t. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); is_aligned frame pageBits; valid_untyped' isdev frame pageBits idx \<sigma>; frame \<noteq> 0; {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {}; t_hrs_' (globals t) = hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> t_hrs_' (globals (x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>)) = t_hrs_' (globals (x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyp (ap_Ptr frame)) (hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>))
 2. \<And>\<sigma> x p cte t. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); is_aligned frame pageBits; valid_untyped' isdev frame pageBits idx \<sigma>; frame \<noteq> 0; {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {}; t_hrs_' (globals t) = hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> ksReadyQueues_' (globals (x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>)) = ksReadyQueues_' (globals (x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyp (ap_Ptr frame)) (hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>))
 3. \<And>\<sigma> x p cte t. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); is_aligned frame pageBits; valid_untyped' isdev frame pageBits idx \<sigma>; frame \<noteq> 0; {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {}; t_hrs_' (globals t) = hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> ksReadyQueuesL1Bitmap_' (globals (x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>)) = ksReadyQueuesL1Bitmap_' (globals (x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyp (ap_Ptr frame)) (hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>))
 4. \<And>\<sigma> x p cte t. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); is_aligned frame pageBits; valid_untyped' isdev frame pageBits idx \<sigma>; frame \<noteq> 0; {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {}; t_hrs_' (globals t) = hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> ksReadyQueuesL2Bitmap_' (globals (x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>)) = ksReadyQueuesL2Bitmap_' (globals (x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyp (ap_Ptr frame)) (hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>))
 5. \<And>\<sigma> x p cte t. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); is_aligned frame pageBits; valid_untyped' isdev frame pageBits idx \<sigma>; frame \<noteq> 0; {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {}; t_hrs_' (globals t) = hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> ksSchedulerAction_' (globals (x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>)) = ksSchedulerAction_' (globals (x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyp (ap_Ptr frame)) (hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>))
 6. \<And>\<sigma> x p cte t. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); is_aligned frame pageBits; valid_untyped' isdev frame pageBits idx \<sigma>; frame \<noteq> 0; {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {}; t_hrs_' (globals t) = hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> ksCurThread_' (globals (x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>)) = ksCurThread_' (globals (x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyp (ap_Ptr frame)) (hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>))
 7. \<And>\<sigma> x p cte t. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); is_aligned frame pageBits; valid_untyped' isdev frame pageBits idx \<sigma>; frame \<noteq> 0; {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {}; t_hrs_' (globals t) = hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> ksIdleThread_' (globals (x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>)) = ksIdleThread_' (globals (x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyp (ap_Ptr frame)) (hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>))
 8. \<And>\<sigma> x p cte t. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); is_aligned frame pageBits; valid_untyped' isdev frame pageBits idx \<sigma>; frame \<noteq> 0; {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {}; t_hrs_' (globals t) = hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> ksWorkUnitsCompleted_' (globals (x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>)) = ksWorkUnitsCompleted_' (globals (x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyp (ap_Ptr frame)) (hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>))
 9. \<And>\<sigma> x p cte t. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); is_aligned frame pageBits; valid_untyped' isdev frame pageBits idx \<sigma>; frame \<noteq> 0; {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {}; t_hrs_' (globals t) = hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> ?intStateIRQNode_'95 \<sigma> x p cte t (globals (x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>)) = ?intStateIRQNode_'95 \<sigma> x p cte t (globals (x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyp (ap_Ptr frame)) (hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>))
 10. \<And>\<sigma> x p cte t. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); is_aligned frame pageBits; valid_untyped' isdev frame pageBits idx \<sigma>; frame \<noteq> 0; {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {}; t_hrs_' (globals t) = hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> intStateIRQTable_' (globals (x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>)) = intStateIRQTable_' (globals (x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyp (ap_Ptr frame)) (hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x)))\<rparr>\<rparr>))
A total of 18 subgoals... proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x p cte t. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); is_aligned frame pageBits; valid_untyped' isdev frame pageBits idx \<sigma>; frame \<noteq> 0; {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {}; t_hrs_' (globals t) = hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> hrs_htd_update (ptr_retyps_gen (Suc 0) (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x))) = hrs_htd_update (ptr_retyp (ap_Ptr frame)) (hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x)))
flex-flex pairs:
\<lambda>\<sigma> x p cte t. ?intStateIRQNode_'95 \<sigma> x p cte t (globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen (Suc 0) (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))\<rparr>) \<equiv>\<^sup>? \<lambda>\<sigma> x p cte t. ?intStateIRQNode_'95 \<sigma> x p cte t (globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyp (ap_Ptr frame)) (hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x)))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x p cte t. \<lbrakk>pspace_aligned' \<sigma>; ctes_of \<sigma> p = Some cte; cteCap cte = capability.UntypedCap isdev frame pageBits idx; pspace_distinct' \<sigma>; valid_objs' \<sigma>; untyped_ranges_zero' \<sigma>; caps_overlap_reserved' {frame..+2 ^ pageBits} \<sigma>; valid_global_refs' \<sigma>; pspace_no_overlap' frame pageBits \<sigma>; region_actually_is_bytes frame (2 ^ pageBits) x; (\<sigma>, x) \<in> rf_sr; \<not> snd (placeNewObject frame makeObject 0 \<sigma>); is_aligned frame pageBits; valid_untyped' isdev frame pageBits idx \<sigma>; frame \<noteq> 0; {frame..+2 ^ pageBits} \<inter> kernel_data_refs = {}; t_hrs_' (globals t) = (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0) (fst (t_hrs_' (globals x))), snd (t_hrs_' (globals x)))\<rbrakk> \<Longrightarrow> heap_update_list frame (replicate (2 ^ pageBits) 0) (fst (t_hrs_' (globals x))) = heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0) (fst (t_hrs_' (globals x))) \<and> ptr_retyps_gen (Suc 0) (ap_Ptr frame) False (snd (t_hrs_' (globals x))) = ptr_retyp (ap_Ptr frame) (snd (t_hrs_' (globals x)))
flex-flex pairs:
\<lambda>\<sigma> x p cte t. ?intStateIRQNode_'95 \<sigma> x p cte t (globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen (Suc 0) (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))\<rparr>) \<equiv>\<^sup>? \<lambda>\<sigma> x p cte t. ?intStateIRQNode_'95 \<sigma> x p cte t (globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyp (ap_Ptr frame)) (hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x)))\<rparr>) proof (prove)
goal:
No subgoals!
flex-flex pairs:
\<lambda>\<sigma> x p cte t. ?intStateIRQNode_'95 \<sigma> x p cte t (globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen (Suc 0) (ap_Ptr frame) False) (hrs_mem_update (heap_update_list frame (replicate (2 ^ pageBits) 0)) (t_hrs_' (globals x)))\<rparr>) \<equiv>\<^sup>? \<lambda>\<sigma> x p cte t. ?intStateIRQNode_'95 \<sigma> x p cte t (globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyp (ap_Ptr frame)) (hrs_mem_update (heap_update_list frame (replicate (unat (2 ^ unat ARMSmallPageBits)) 0)) (t_hrs_' (globals x)))\<rparr>) proof (state)
this:
ccorres dc xfdc ((\<lambda>s. \<exists>p. cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap isdev frame pageBits idx) p s) and pspace_aligned' and pspace_distinct' and valid_objs' and (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {frame..+2 ^ pageBits}) and valid_global_refs' and pspace_no_overlap' frame pageBits) {s. region_actually_is_bytes frame (2 ^ pageBits) s} hs (placeNewObject frame makeObject 0) (CALL memzero_'proc(PTR(unit) frame,2 ^ unat ARMSmallPageBits);;
Guard MemorySafety \<lbrace>htd_safe domain (hrs_htd \<acute>t_hrs) \<and> htd_safe domain (ptr_retyp (ap_Ptr frame) (hrs_htd \<acute>t_hrs))\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_htd_update (ptr_retyp (ap_Ptr frame)))))

goal:
No subgoals!