theory Retype_C

lemma createObjects_ccorres_user_data:
  defines "ko \<equiv> KOUserData"
  shows "\<forall>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> range_cover ptr sz (gbits + pageBits) n
  \<and> ptr \<noteq> 0
  \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma>
  \<and> valid_machine_state' \<sigma>
  \<and> ret_zero ptr (n * 2 ^ (gbits + pageBits)) \<sigma>
  \<and> pspace_no_overlap' ptr sz \<sigma>
  \<and> region_is_zero_bytes ptr (n * 2 ^ (gbits + pageBits)) x
  \<and> {ptr ..+ n * (2 ^ (gbits + pageBits))} \<inter> kernel_data_refs = {}
  \<longrightarrow>
  (\<sigma>\<lparr>ksPSpace :=
               foldr (\<lambda>addr. data_map_insert addr KOUserData)
                  (new_cap_addrs (n * 2^gbits) ptr KOUserData) (ksPSpace \<sigma>)\<rparr>,
           x\<lparr>globals := globals x\<lparr>t_hrs_' :=
                      hrs_htd_update
                       (ptr_retyps_gen (n * 2 ^ gbits) (Ptr ptr :: user_data_C ptr) arr)
                       ((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 = "Ptr ptr :: user_data_C ptr" note Kernel_C.user_data_C_size [simp del] assume "?P \<sigma> x" hence rf: "(\<sigma>, x) \<in> rf_sr" and al: "is_aligned ptr (gbits + pageBits)"
    and ptr0: "ptr \<noteq> 0"
    and sz: "gbits + pageBits \<le> sz"
    and szb: "sz < word_bits"
    and pal: "pspace_aligned' \<sigma>" and pdst: "pspace_distinct' \<sigma>"
    and pno: "pspace_no_overlap' ptr sz \<sigma>"
    and vms: "valid_machine_state' \<sigma>"
    and rzo: "ret_zero ptr (n * 2 ^ (gbits + pageBits)) \<sigma>"
    and empty: "region_is_bytes ptr (n * 2 ^ (gbits + pageBits)) x"
    and zero: "heap_list_is_zero (hrs_mem (t_hrs_' (globals x))) ptr (n * 2 ^ (gbits + pageBits))"
    and rc: "range_cover ptr sz (gbits + pageBits) n"
    and rc': "range_cover ptr sz (objBitsKO ko) (n * 2^ gbits)"
    and kdr: "{ptr..+n * 2 ^ (gbits + pageBits)} \<inter> kernel_data_refs = {}" by (auto simp: range_cover.aligned objBits_simps  ko_def
                   range_cover_rel[where sbit' = pageBits]
                   range_cover.sz[where 'a=32, folded word_bits_def]) hence al': "is_aligned ptr (objBitsKO ko)" by (clarsimp dest!: is_aligned_weaken range_cover.aligned) 

  (* This is a hack *)
   have mko: "\<And>dev. makeObjectKO False (Inr object_type.SmallPageObject) = Some ko" by (simp add: makeObjectKO_def ko_def) from sz have "2 \<le> sz" by (simp add: objBits_simps pageBits_def ko_def) hence sz2: "2 ^ (sz - 2) * 4 = (2 :: nat) ^ sz" apply (subgoal_tac "(4 :: nat) = 2 ^ 2") apply (erule ssubst) apply (subst power_add [symmetric]) apply (rule arg_cong [where f = "\<lambda>n. 2 ^ n"]) apply simp apply simp done define big_0s where "big_0s \<equiv> (replicate (2^pageBits) 0) :: word8 list" have "length big_0s = 4096" unfolding big_0s_def by simp (simp add: pageBits_def) hence i1: "\<And>off :: 10 word. index (user_data_C.words_C (from_bytes big_0s)) (unat off) = 0" apply (simp add: from_bytes_def) apply (simp add: typ_info_simps user_data_C_tag_def) apply (simp add: ti_typ_pad_combine_empty_ti ti_typ_pad_combine_td align_of_def padup_def
      final_pad_def size_td_lt_ti_typ_pad_combine Let_def align_td_array' size_td_array size_of_def
      cong: if_cong) apply (simp add: update_ti_adjust_ti update_ti_t_word32_0s
      typ_info_simps update_ti_t_ptr_0s
      ti_typ_pad_combine_empty_ti ti_typ_pad_combine_td
      align_of_def padup_def
      final_pad_def size_td_lt_ti_typ_pad_combine Let_def
      align_td_array' size_td_array cong: if_cong) apply (subst update_ti_t_array_rep_word0) apply (unfold big_0s_def)[1] apply (rule arg_cong [where f = "\<lambda>x. replicate x 0"]) apply (simp (no_asm) add: size_of_def pageBits_def) apply (subst index_foldr_update) apply (rule order_less_le_trans [OF unat_lt2p]) apply simp apply simp apply simp done have p2dist: "n * (2::nat) ^ (gbits + pageBits) = n * 2 ^ gbits * 2 ^ pageBits" (is "?lhs = ?rhs") by (simp add:monoid_mult_class.power_add) have nca: "\<And>x p (off :: 10 word). \<lbrakk> p \<in> set (new_cap_addrs (n*2^gbits) ptr KOUserData); x < 4 \<rbrakk>
    \<Longrightarrow> p + ucast off * 4 + x \<in> {ptr..+ n * 2 ^ (gbits + pageBits) }" using sz apply (clarsimp simp: new_cap_addrs_def objBits_simps shiftl_t2n intvl_def) apply (rename_tac x off pa) apply (rule_tac x = "2 ^ pageBits * pa + unat off * 4 + unat x" in exI) apply (simp add: ucast_nat_def power_add) apply (subst mult.commute, subst add.assoc) apply (rule_tac y = "(pa + 1) * 2 ^ pageBits " in less_le_trans) apply (simp add:word_less_nat_alt) apply (rule_tac y="unat off * 4 + 4" in less_le_trans) apply simp apply (simp add:pageBits_def) apply (cut_tac x = off in unat_lt2p) apply simp apply (subst mult.assoc[symmetric]) apply (rule mult_right_mono) apply simp+ done have nca_neg: "\<And>x p (off :: 10 word).
    \<lbrakk>x < 4; {p..+2 ^ objBitsKO KOUserData } \<inter> {ptr..ptr + (of_nat n * 2 ^ (gbits + pageBits) - 1)} = {}\<rbrakk>
     \<Longrightarrow> p + ucast off * 4 + x \<notin> {ptr..+n * 2 ^ (gbits + pageBits)}" apply (case_tac "n = 0") apply simp apply (subst range_cover_intvl[OF rc]) apply simp apply (subgoal_tac " p + ucast off * 4 + x \<in>  {p..+2 ^ objBitsKO KOUserData}") apply blast apply (clarsimp simp:intvl_def) apply (rule_tac x = "unat off * 4 + unat x" in exI) apply (simp add: ucast_nat_def) apply (rule nat_add_offset_less [where n = 2, simplified]) apply (simp add: word_less_nat_alt) apply (rule unat_lt2p) apply (simp add: pageBits_def objBits_simps) done have zero_app: "\<And>x. x \<in> {ptr..+ n * 2 ^ (gbits + pageBits) }
    \<Longrightarrow> underlying_memory (ksMachineState \<sigma>) x = 0" apply (cases "n = 0") apply simp apply (rule pspace_no_overlap_underlying_zero[OF pno vms]) apply (erule subsetD[rotated]) apply (cases "n = 0") apply simp apply (subst range_cover_intvl[OF rc], simp) apply (rule order_trans[rotated], erule range_cover_subset'[OF rc]) apply (simp add: field_simps) done have cud: "\<And>p. p \<in> set (new_cap_addrs (n * 2^ gbits) ptr KOUserData) \<Longrightarrow>
              cuser_user_data_relation
                (byte_to_word_heap
                  (underlying_memory (ksMachineState \<sigma>)) p)
                (from_bytes big_0s)" unfolding cuser_user_data_relation_def apply - apply (rule allI) apply (subst i1) apply (simp add: byte_to_word_heap_def Let_def
                     zero_app nca nca [where x3 = 0, simplified]) apply (simp add: word_rcat_bl) done note blah[simp del] =  atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff
      Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex have cud2: "\<And>xa v y.
              \<lbrakk> heap_to_user_data
                     (\<lambda>x. if x \<in> set (new_cap_addrs (n*2^gbits) ptr KOUserData)
                           then Some KOUserData else ksPSpace \<sigma> x)
                     (underlying_memory (ksMachineState \<sigma>)) xa =
              Some v; xa \<notin> set (new_cap_addrs (n*2^gbits) ptr KOUserData);
              heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) xa = Some y \<rbrakk> \<Longrightarrow> y = v" using range_cover_intvl[OF rc] by (clarsimp simp add: heap_to_user_data_def Let_def sz2
      byte_to_word_heap_def[abs_def] map_comp_Some_iff projectKOs) have relrl: "cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)))
                             (cslift x) Ptr cuser_user_data_relation
    \<Longrightarrow> cmap_relation
        (heap_to_user_data
          (\<lambda>x. if x \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData)
               then Some KOUserData else ksPSpace \<sigma> x)
          (underlying_memory (ksMachineState \<sigma>)))
        (\<lambda>y. if y \<in> Ptr ` set (new_cap_addrs (n*2^gbits) ptr KOUserData)
             then Some
                   (from_bytes (replicate (2 ^ pageBits) 0))
             else cslift x y)
        Ptr cuser_user_data_relation" apply (rule cmap_relationI) apply (clarsimp simp: dom_heap_to_user_data cmap_relation_def dom_if image_Un
      projectKO_opt_retyp_same projectKOs) apply (case_tac "xa \<in> set (new_cap_addrs (n*2^gbits) ptr KOUserData)") apply (clarsimp simp: heap_to_user_data_def sz2) apply (erule cud [unfolded big_0s_def]) apply (subgoal_tac "(Ptr xa :: user_data_C ptr) \<notin> Ptr ` set (new_cap_addrs (n*2^gbits) ptr KOUserData)") apply simp apply (erule (1) cmap_relationE2) apply (drule (1) cud2) apply simp apply simp apply clarsimp done 

  (* /obj specific *)

  (* s/obj/obj'/ *)

   have szo: "size_of TYPE(user_data_C) = 2 ^ objBitsKO ko" by (simp add: size_of_def objBits_simps archObjSize_def ko_def pageBits_def) have szo': "n * 2 ^ (gbits + pageBits) = n * 2 ^ gbits * size_of TYPE(user_data_C)" using sz apply (subst szo) apply (clarsimp simp: power_add[symmetric] objBits_simps ko_def) done have rb': "region_is_bytes ptr (n * 2 ^ gbits * 2 ^ objBitsKO ko) x" using empty by (simp add: mult.commute mult.left_commute power_add objBits_simps ko_def) note rl' = cslift_ptr_retyp_other_inst[OF rb' rc' szo' szo, simplified] 

  (* rest is generic *)

   note rl = projectKO_opt_retyp_other [OF rc' pal pno,unfolded ko_def] note cterl = retype_ctes_helper[OF pal pdst pno al' range_cover.sz(2)[OF rc'] range_cover.sz(1)[OF rc', folded word_bits_def] mko rc'] note ht_rl = clift_eq_h_t_valid_eq[OF rl', OF tag_disj_via_td_name, simplified] have guard:
    "\<forall>t<n * 2 ^ gbits. c_guard (CTypesDefs.ptr_add ?ptr (of_nat t))" apply (rule retype_guard_helper[OF rc' ptr0 szo,where m = 2]) apply (clarsimp simp:align_of_def objBits_simps ko_def pageBits_def)+ 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 using empty rc' szo apply - supply image_cong_simp [cong del] apply (clarsimp simp: rl' tag_disj_via_td_name cte_C_size ht_rl
                          foldr_upd_app_if [folded data_map_insert_def]) apply (simp add: rl ko_def projectKOs p2dist
                     cterl[unfolded ko_def]) apply (subst clift_ptr_retyps_gen_prev_memset_same[OF guard]) apply (simp add: pageBits_def objBits_simps) apply simp apply (simp add: pageBits_def objBits_simps) apply (cut_tac range_cover.strong_times_32[OF rc], simp_all)[1] apply (simp add: p2dist objBits_simps) apply (cut_tac zero) apply (simp add: pageBits_def power_add field_simps) apply (simp add: objBits_simps ptr_add_to_new_cap_addrs[OF szo] ko_def
               cong: if_cong) apply (simp add: p2dist[symmetric]) apply (erule relrl[simplified]) done thus  ?thesis using rf empty kdr rzo apply (simp add: rf_sr_def cstate_relation_def Let_def rl' tag_disj_via_td_name ) apply (simp add: carch_state_relation_def cmachine_state_relation_def) apply (simp add: tag_disj_via_td_name rl' tcb_C_size h_t_valid_clift_Some_iff) apply (clarsimp simp: hrs_htd_update szo'[symmetric]) apply (simp add:szo hrs_htd_def p2dist objBits_simps ko_def ptr_retyps_htd_safe_neg
                    kernel_data_refs_domain_eq_rotate
                    rl foldr_upd_app_if [folded data_map_insert_def]
                    projectKOs cvariable_array_ptr_retyps
                    zero_ranges_ptr_retyps) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> range_cover ptr sz (gbits + pageBits) n \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> valid_machine_state' \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+n * 2 ^ (gbits + pageBits)}) \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ (gbits + pageBits)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ (gbits + pageBits)) ptr = replicate (n * 2 ^ (gbits + pageBits)) 0) \<and> {ptr..+n * 2 ^ (gbits + pageBits)} \<inter> kernel_data_refs = {} \<longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (state)
goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> range_cover ptr sz (gbits + pageBits) n \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> valid_machine_state' \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+n * 2 ^ (gbits + pageBits)}) \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ (gbits + pageBits)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ (gbits + pageBits)) ptr = replicate (n * 2 ^ (gbits + pageBits)) 0) \<and> {ptr..+n * 2 ^ (gbits + pageBits)} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (state)
goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> range_cover ptr sz (gbits + pageBits) n \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> valid_machine_state' \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+n * 2 ^ (gbits + pageBits)}) \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ (gbits + pageBits)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ (gbits + pageBits)) ptr = replicate (n * 2 ^ (gbits + pageBits)) 0) \<and> {ptr..+n * 2 ^ (gbits + pageBits)} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (state)
goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> range_cover ptr sz (gbits + pageBits) n \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> valid_machine_state' \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+n * 2 ^ (gbits + pageBits)}) \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ (gbits + pageBits)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ (gbits + pageBits)) ptr = replicate (n * 2 ^ (gbits + pageBits)) 0) \<and> {ptr..+n * 2 ^ (gbits + pageBits)} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (state)
goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> range_cover ptr sz (gbits + pageBits) n \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> valid_machine_state' \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+n * 2 ^ (gbits + pageBits)}) \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ (gbits + pageBits)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ (gbits + pageBits)) ptr = replicate (n * 2 ^ (gbits + pageBits)) 0) \<and> {ptr..+n * 2 ^ (gbits + pageBits)} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (state)
goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> range_cover ptr sz (gbits + pageBits) n \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> valid_machine_state' \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+n * 2 ^ (gbits + pageBits)}) \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ (gbits + pageBits)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ (gbits + pageBits)) ptr = replicate (n * 2 ^ (gbits + pageBits)) 0) \<and> {ptr..+n * 2 ^ (gbits + pageBits)} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (state)
goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> range_cover ptr sz (gbits + pageBits) n \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> valid_machine_state' \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+n * 2 ^ (gbits + pageBits)}) \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ (gbits + pageBits)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ (gbits + pageBits)) ptr = replicate (n * 2 ^ (gbits + pageBits)) 0) \<and> {ptr..+n * 2 ^ (gbits + pageBits)} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (state)
this:
size_of TYPE(user_data_C) \<equiv> 4096

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> range_cover ptr sz (gbits + pageBits) n \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> valid_machine_state' \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+n * 2 ^ (gbits + pageBits)}) \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ (gbits + pageBits)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ (gbits + pageBits)) ptr = replicate (n * 2 ^ (gbits + pageBits)) 0) \<and> {ptr..+n * 2 ^ (gbits + pageBits)} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (state)
this:
(\<sigma>, x) \<in> rf_sr \<and> range_cover ptr sz (gbits + pageBits) n \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> valid_machine_state' \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+n * 2 ^ (gbits + pageBits)}) \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ (gbits + pageBits)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ (gbits + pageBits)) ptr = replicate (n * 2 ^ (gbits + pageBits)) 0) \<and> {ptr..+n * 2 ^ (gbits + pageBits)} \<inter> kernel_data_refs = {}

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> range_cover ptr sz (gbits + pageBits) n \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> valid_machine_state' \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+n * 2 ^ (gbits + pageBits)}) \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ (gbits + pageBits)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ (gbits + pageBits)) ptr = replicate (n * 2 ^ (gbits + pageBits)) 0) \<and> {ptr..+n * 2 ^ (gbits + pageBits)} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
using this:
(\<sigma>, x) \<in> rf_sr \<and> range_cover ptr sz (gbits + pageBits) n \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> valid_machine_state' \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+n * 2 ^ (gbits + pageBits)}) \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ (gbits + pageBits)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ (gbits + pageBits)) ptr = replicate (n * 2 ^ (gbits + pageBits)) 0) \<and> {ptr..+n * 2 ^ (gbits + pageBits)} \<inter> kernel_data_refs = {}

goal (1 subgoal):
 1. (((\<sigma>, x) \<in> rf_sr &&& is_aligned ptr (gbits + pageBits) &&& ptr \<noteq> 0) &&& (gbits + pageBits \<le> sz &&& sz < word_bits) &&& pspace_aligned' \<sigma> &&& pspace_distinct' \<sigma>) &&& ((pspace_no_overlap' ptr sz \<sigma> &&& valid_machine_state' \<sigma>) &&& (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+n * 2 ^ (gbits + pageBits)}) \<sigma> &&& region_is_bytes ptr (n * 2 ^ (gbits + pageBits)) x) &&& (heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ (gbits + pageBits)) ptr = replicate (n * 2 ^ (gbits + pageBits)) 0 &&& range_cover ptr sz (gbits + pageBits) n) &&& range_cover ptr sz (objBitsKO ko) (n * 2 ^ gbits) &&& {ptr..+n * 2 ^ (gbits + pageBits)} \<inter> kernel_data_refs = {} proof (state)
this:
(\<sigma>, x) \<in> rf_sr
is_aligned ptr (gbits + pageBits)
ptr \<noteq> 0
gbits + pageBits \<le> sz
sz < word_bits
pspace_aligned' \<sigma>
pspace_distinct' \<sigma>
pspace_no_overlap' ptr sz \<sigma>
valid_machine_state' \<sigma>
(valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+n * 2 ^ (gbits + pageBits)}) \<sigma>
region_is_bytes ptr (n * 2 ^ (gbits + pageBits)) x
heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ (gbits + pageBits)) ptr = replicate (n * 2 ^ (gbits + pageBits)) 0
range_cover ptr sz (gbits + pageBits) n
range_cover ptr sz (objBitsKO ko) (n * 2 ^ gbits)
{ptr..+n * 2 ^ (gbits + pageBits)} \<inter> kernel_data_refs = {}

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> range_cover ptr sz (gbits + pageBits) n \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> valid_machine_state' \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+n * 2 ^ (gbits + pageBits)}) \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ (gbits + pageBits)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ (gbits + pageBits)) ptr = replicate (n * 2 ^ (gbits + pageBits)) 0) \<and> {ptr..+n * 2 ^ (gbits + pageBits)} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
using this:
(\<sigma>, x) \<in> rf_sr
is_aligned ptr (gbits + pageBits)
ptr \<noteq> 0
gbits + pageBits \<le> sz
sz < word_bits
pspace_aligned' \<sigma>
pspace_distinct' \<sigma>
pspace_no_overlap' ptr sz \<sigma>
valid_machine_state' \<sigma>
(valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+n * 2 ^ (gbits + pageBits)}) \<sigma>
region_is_bytes ptr (n * 2 ^ (gbits + pageBits)) x
heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ (gbits + pageBits)) ptr = replicate (n * 2 ^ (gbits + pageBits)) 0
range_cover ptr sz (gbits + pageBits) n
range_cover ptr sz (objBitsKO ko) (n * 2 ^ gbits)
{ptr..+n * 2 ^ (gbits + pageBits)} \<inter> kernel_data_refs = {}

goal (1 subgoal):
 1. is_aligned ptr (objBitsKO ko) proof (state)
this:
is_aligned ptr (objBitsKO ko)

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> range_cover ptr sz (gbits + pageBits) n \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> valid_machine_state' \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+n * 2 ^ (gbits + pageBits)}) \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ (gbits + pageBits)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ (gbits + pageBits)) ptr = replicate (n * 2 ^ (gbits + pageBits)) 0) \<and> {ptr..+n * 2 ^ (gbits + pageBits)} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (state)
this:
is_aligned ptr (objBitsKO ko)

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> range_cover ptr sz (gbits + pageBits) n \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> valid_machine_state' \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+n * 2 ^ (gbits + pageBits)}) \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ (gbits + pageBits)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ (gbits + pageBits)) ptr = replicate (n * 2 ^ (gbits + pageBits)) 0) \<and> {ptr..+n * 2 ^ (gbits + pageBits)} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>dev. makeObjectKO False (Inr object_type.SmallPageObject) = Some ko proof (state)
this:
makeObjectKO False (Inr object_type.SmallPageObject) = Some ko

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> range_cover ptr sz (gbits + pageBits) n \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> valid_machine_state' \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+n * 2 ^ (gbits + pageBits)}) \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ (gbits + pageBits)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ (gbits + pageBits)) ptr = replicate (n * 2 ^ (gbits + pageBits)) 0) \<and> {ptr..+n * 2 ^ (gbits + pageBits)} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (chain)
picking this:
gbits + pageBits \<le> sz proof (prove)
using this:
gbits + pageBits \<le> sz

goal (1 subgoal):
 1. 2 \<le> sz proof (state)
this:
2 \<le> sz

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> range_cover ptr sz (gbits + pageBits) n \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> valid_machine_state' \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+n * 2 ^ (gbits + pageBits)}) \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ (gbits + pageBits)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ (gbits + pageBits)) ptr = replicate (n * 2 ^ (gbits + pageBits)) 0) \<and> {ptr..+n * 2 ^ (gbits + pageBits)} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
using this:
2 \<le> sz

goal (1 subgoal):
 1. 2 ^ (sz - 2) * 4 = 2 ^ sz proof (prove)
goal (2 subgoals):
 1. \<lbrakk>2 \<le> sz; 4 = 2\<^sup>2\<rbrakk> \<Longrightarrow> 2 ^ (sz - 2) * 4 = 2 ^ sz
 2. 2 \<le> sz \<Longrightarrow> 4 = 2\<^sup>2 proof (prove)
goal (2 subgoals):
 1. 2 \<le> sz \<Longrightarrow> 2 ^ (sz - 2) * 2\<^sup>2 = 2 ^ sz
 2. 2 \<le> sz \<Longrightarrow> 4 = 2\<^sup>2 proof (prove)
goal (2 subgoals):
 1. 2 \<le> sz \<Longrightarrow> 2 ^ (sz - 2 + 2) = 2 ^ sz
 2. 2 \<le> sz \<Longrightarrow> 4 = 2\<^sup>2 proof (prove)
goal (2 subgoals):
 1. 2 \<le> sz \<Longrightarrow> sz - 2 + 2 = sz
 2. 2 \<le> sz \<Longrightarrow> 4 = 2\<^sup>2 proof (prove)
goal (1 subgoal):
 1. 2 \<le> sz \<Longrightarrow> 4 = 2\<^sup>2 proof (prove)
goal:
No subgoals! proof (state)
this:
2 ^ (sz - 2) * 4 = 2 ^ sz

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> range_cover ptr sz (gbits + pageBits) n \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> valid_machine_state' \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+n * 2 ^ (gbits + pageBits)}) \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ (gbits + pageBits)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ (gbits + pageBits)) ptr = replicate (n * 2 ^ (gbits + pageBits)) 0) \<and> {ptr..+n * 2 ^ (gbits + pageBits)} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (state)
this:
big_0s \<equiv> replicate (2 ^ pageBits) 0

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> range_cover ptr sz (gbits + pageBits) n \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> valid_machine_state' \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+n * 2 ^ (gbits + pageBits)}) \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ (gbits + pageBits)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ (gbits + pageBits)) ptr = replicate (n * 2 ^ (gbits + pageBits)) 0) \<and> {ptr..+n * 2 ^ (gbits + pageBits)} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. length big_0s = 4096 proof (prove)
goal (1 subgoal):
 1. length (replicate (2 ^ pageBits) 0) = 4096 proof (state)
this:
length big_0s = 4096

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> range_cover ptr sz (gbits + pageBits) n \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> valid_machine_state' \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+n * 2 ^ (gbits + pageBits)}) \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ (gbits + pageBits)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ (gbits + pageBits)) ptr = replicate (n * 2 ^ (gbits + pageBits)) 0) \<and> {ptr..+n * 2 ^ (gbits + pageBits)} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
using this:
length big_0s = 4096

goal (1 subgoal):
 1. \<And>off. user_data_C.words_C (from_bytes big_0s).[unat off] = 0 proof (prove)
goal (1 subgoal):
 1. \<And>off. length big_0s = 4096 \<Longrightarrow> user_data_C.words_C (update_ti_t (typ_info_t TYPE(user_data_C)) big_0s undefined).[unat off] = 0 proof (prove)
goal (1 subgoal):
 1. \<And>off. length big_0s = 4096 \<Longrightarrow> user_data_C.words_C (update_ti_t (final_pad (ti_typ_pad_combine TYPE(32 word[1024]) user_data_C.words_C (user_data_C.words_C_update \<circ> (\<lambda>x _. x)) ''words_C'' (empty_typ_info ''user_data_C''))) big_0s undefined).[unat off] = 0 proof (prove)
goal (1 subgoal):
 1. \<And>off. length big_0s = 4096 \<Longrightarrow> user_data_C.words_C (update_ti_t (adjust_ti (typ_info_t TYPE(32 word[1024])) user_data_C.words_C (user_data_C.words_C_update \<circ> (\<lambda>x _. x))) big_0s undefined).[unat off] = 0 proof (prove)
goal (1 subgoal):
 1. \<And>off. length big_0s = 4096 \<Longrightarrow> update_ti_t (typ_info_t TYPE(32 word[1024])) big_0s (user_data_C.words_C undefined).[unat off] = 0 proof (prove)
goal (2 subgoals):
 1. \<And>off. length big_0s = 4096 \<Longrightarrow> big_0s = replicate (CARD(1024) * 4) 0
 2. \<And>off. length big_0s = 4096 \<Longrightarrow> foldr (\<lambda>n arr. Arrays.update arr n 0) [0..<CARD(1024)] (user_data_C.words_C undefined).[unat off] = 0 proof (prove)
goal (2 subgoals):
 1. \<And>off. length (replicate (2 ^ pageBits) 0) = 4096 \<Longrightarrow> replicate (2 ^ pageBits) 0 = replicate (CARD(1024) * 4) 0
 2. \<And>off. length big_0s = 4096 \<Longrightarrow> foldr (\<lambda>n arr. Arrays.update arr n 0) [0..<CARD(1024)] (user_data_C.words_C undefined).[unat off] = 0 proof (prove)
goal (2 subgoals):
 1. \<And>off. length (replicate (2 ^ pageBits) 0) = 4096 \<Longrightarrow> 2 ^ pageBits = CARD(1024) * 4
 2. \<And>off. length big_0s = 4096 \<Longrightarrow> foldr (\<lambda>n arr. Arrays.update arr n 0) [0..<CARD(1024)] (user_data_C.words_C undefined).[unat off] = 0 proof (prove)
goal (1 subgoal):
 1. \<And>off. length big_0s = 4096 \<Longrightarrow> foldr (\<lambda>n arr. Arrays.update arr n 0) [0..<CARD(1024)] (user_data_C.words_C undefined).[unat off] = 0 proof (prove)
goal (3 subgoals):
 1. \<And>off. length big_0s = 4096 \<Longrightarrow> unat off < CARD(1024)
 2. \<And>off. length big_0s = 4096 \<Longrightarrow> CARD(1024) \<le> CARD(1024)
 3. \<And>off. length big_0s = 4096 \<Longrightarrow> 0 = 0 proof (prove)
goal (3 subgoals):
 1. \<And>off. length big_0s = 4096 \<Longrightarrow> 2 ^ LENGTH(10) \<le> CARD(1024)
 2. \<And>off. length big_0s = 4096 \<Longrightarrow> CARD(1024) \<le> CARD(1024)
 3. \<And>off. length big_0s = 4096 \<Longrightarrow> 0 = 0 proof (prove)
goal (2 subgoals):
 1. \<And>off. length big_0s = 4096 \<Longrightarrow> CARD(1024) \<le> CARD(1024)
 2. \<And>off. length big_0s = 4096 \<Longrightarrow> 0 = 0 proof (prove)
goal (1 subgoal):
 1. \<And>off. length big_0s = 4096 \<Longrightarrow> 0 = 0 proof (prove)
goal:
No subgoals! proof (state)
this:
user_data_C.words_C (from_bytes big_0s).[unat ?off3] = 0

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> range_cover ptr sz (gbits + pageBits) n \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> valid_machine_state' \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+n * 2 ^ (gbits + pageBits)}) \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ (gbits + pageBits)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ (gbits + pageBits)) ptr = replicate (n * 2 ^ (gbits + pageBits)) 0) \<and> {ptr..+n * 2 ^ (gbits + pageBits)} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. n * 2 ^ (gbits + pageBits) = n * 2 ^ gbits * 2 ^ pageBits proof (state)
this:
n * 2 ^ (gbits + pageBits) = n * 2 ^ gbits * 2 ^ pageBits

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> range_cover ptr sz (gbits + pageBits) n \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> valid_machine_state' \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+n * 2 ^ (gbits + pageBits)}) \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ (gbits + pageBits)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ (gbits + pageBits)) ptr = replicate (n * 2 ^ (gbits + pageBits)) 0) \<and> {ptr..+n * 2 ^ (gbits + pageBits)} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>x p off. \<lbrakk>p \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData); x < 4\<rbrakk> \<Longrightarrow> p + UCAST(10 \<rightarrow> 32) off * 4 + x \<in> {ptr..+n * 2 ^ (gbits + pageBits)} proof (prove)
using this:
gbits + pageBits \<le> sz

goal (1 subgoal):
 1. \<And>x p off. \<lbrakk>p \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData); x < 4\<rbrakk> \<Longrightarrow> p + UCAST(10 \<rightarrow> 32) off * 4 + x \<in> {ptr..+n * 2 ^ (gbits + pageBits)} proof (prove)
goal (1 subgoal):
 1. \<And>x off xa. \<lbrakk>x < 4; gbits + pageBits \<le> sz; xa < n * 2 ^ gbits\<rbrakk> \<Longrightarrow> \<exists>k. 2 ^ pageBits * word_of_nat xa + (UCAST(10 \<rightarrow> 32) off * 4 + x) = word_of_nat k \<and> k < n * 2 ^ (gbits + pageBits) proof (prove)
goal (1 subgoal):
 1. \<And>x off pa. \<lbrakk>x < 4; gbits + pageBits \<le> sz; pa < n * 2 ^ gbits\<rbrakk> \<Longrightarrow> \<exists>k. 2 ^ pageBits * word_of_nat pa + (UCAST(10 \<rightarrow> 32) off * 4 + x) = word_of_nat k \<and> k < n * 2 ^ (gbits + pageBits) proof (prove)
goal (1 subgoal):
 1. \<And>x off pa. \<lbrakk>x < 4; gbits + pageBits \<le> sz; pa < n * 2 ^ gbits\<rbrakk> \<Longrightarrow> 2 ^ pageBits * word_of_nat pa + (UCAST(10 \<rightarrow> 32) off * 4 + x) = word_of_nat (2 ^ pageBits * pa + unat off * 4 + unat x) \<and> 2 ^ pageBits * pa + unat off * 4 + unat x < n * 2 ^ (gbits + pageBits) proof (prove)
goal (1 subgoal):
 1. \<And>x off pa. \<lbrakk>x < 4; gbits + pageBits \<le> sz; pa < n * 2 ^ gbits\<rbrakk> \<Longrightarrow> 2 ^ pageBits * pa + unat off * 4 + unat x < n * (2 ^ gbits * 2 ^ pageBits) proof (prove)
goal (1 subgoal):
 1. \<And>x off pa. \<lbrakk>x < 4; gbits + pageBits \<le> sz; pa < n * 2 ^ gbits\<rbrakk> \<Longrightarrow> pa * 2 ^ pageBits + (unat off * 4 + unat x) < n * (2 ^ gbits * 2 ^ pageBits) proof (prove)
goal (2 subgoals):
 1. \<And>x off pa. \<lbrakk>x < 4; gbits + pageBits \<le> sz; pa < n * 2 ^ gbits\<rbrakk> \<Longrightarrow> pa * 2 ^ pageBits + (unat off * 4 + unat x) < (pa + 1) * 2 ^ pageBits
 2. \<And>x off pa. \<lbrakk>x < 4; gbits + pageBits \<le> sz; pa < n * 2 ^ gbits\<rbrakk> \<Longrightarrow> (pa + 1) * 2 ^ pageBits \<le> n * (2 ^ gbits * 2 ^ pageBits) proof (prove)
goal (2 subgoals):
 1. \<And>x off pa. \<lbrakk>unat x < 4; gbits + pageBits \<le> sz; pa < n * 2 ^ gbits\<rbrakk> \<Longrightarrow> unat off * 4 + unat x < 2 ^ pageBits
 2. \<And>x off pa. \<lbrakk>x < 4; gbits + pageBits \<le> sz; pa < n * 2 ^ gbits\<rbrakk> \<Longrightarrow> (pa + 1) * 2 ^ pageBits \<le> n * (2 ^ gbits * 2 ^ pageBits) proof (prove)
goal (3 subgoals):
 1. \<And>x off pa. \<lbrakk>unat x < 4; gbits + pageBits \<le> sz; pa < n * 2 ^ gbits\<rbrakk> \<Longrightarrow> unat off * 4 + unat x < unat off * 4 + 4
 2. \<And>x off pa. \<lbrakk>unat x < 4; gbits + pageBits \<le> sz; pa < n * 2 ^ gbits\<rbrakk> \<Longrightarrow> unat off * 4 + 4 \<le> 2 ^ pageBits
 3. \<And>x off pa. \<lbrakk>x < 4; gbits + pageBits \<le> sz; pa < n * 2 ^ gbits\<rbrakk> \<Longrightarrow> (pa + 1) * 2 ^ pageBits \<le> n * (2 ^ gbits * 2 ^ pageBits) proof (prove)
goal (2 subgoals):
 1. \<And>x off pa. \<lbrakk>unat x < 4; gbits + pageBits \<le> sz; pa < n * 2 ^ gbits\<rbrakk> \<Longrightarrow> unat off * 4 + 4 \<le> 2 ^ pageBits
 2. \<And>x off pa. \<lbrakk>x < 4; gbits + pageBits \<le> sz; pa < n * 2 ^ gbits\<rbrakk> \<Longrightarrow> (pa + 1) * 2 ^ pageBits \<le> n * (2 ^ gbits * 2 ^ pageBits) proof (prove)
goal (2 subgoals):
 1. \<And>x off pa. \<lbrakk>unat x < 4; gbits + 12 \<le> sz; pa < n * 2 ^ gbits\<rbrakk> \<Longrightarrow> unat off \<le> 1023
 2. \<And>x off pa. \<lbrakk>x < 4; gbits + pageBits \<le> sz; pa < n * 2 ^ gbits\<rbrakk> \<Longrightarrow> (pa + 1) * 2 ^ pageBits \<le> n * (2 ^ gbits * 2 ^ pageBits) proof (prove)
goal (2 subgoals):
 1. \<And>x off pa. \<lbrakk>unat x < 4; gbits + 12 \<le> sz; pa < n * 2 ^ gbits; unat off < 2 ^ LENGTH(10)\<rbrakk> \<Longrightarrow> unat off \<le> 1023
 2. \<And>x off pa. \<lbrakk>x < 4; gbits + pageBits \<le> sz; pa < n * 2 ^ gbits\<rbrakk> \<Longrightarrow> (pa + 1) * 2 ^ pageBits \<le> n * (2 ^ gbits * 2 ^ pageBits) proof (prove)
goal (1 subgoal):
 1. \<And>x off pa. \<lbrakk>x < 4; gbits + pageBits \<le> sz; pa < n * 2 ^ gbits\<rbrakk> \<Longrightarrow> (pa + 1) * 2 ^ pageBits \<le> n * (2 ^ gbits * 2 ^ pageBits) proof (prove)
goal (1 subgoal):
 1. \<And>x off pa. \<lbrakk>x < 4; gbits + pageBits \<le> sz; pa < n * 2 ^ gbits\<rbrakk> \<Longrightarrow> (pa + 1) * 2 ^ pageBits \<le> n * 2 ^ gbits * 2 ^ pageBits proof (prove)
goal (2 subgoals):
 1. \<And>x off pa. \<lbrakk>x < 4; gbits + pageBits \<le> sz; pa < n * 2 ^ gbits\<rbrakk> \<Longrightarrow> pa + 1 \<le> n * 2 ^ gbits
 2. \<And>x off pa. \<lbrakk>x < 4; gbits + pageBits \<le> sz; pa < n * 2 ^ gbits\<rbrakk> \<Longrightarrow> 0 \<le> 2 ^ pageBits proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrakk>?p3 \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData); ?x3 < 4\<rbrakk> \<Longrightarrow> ?p3 + UCAST(10 \<rightarrow> 32) ?off3 * 4 + ?x3 \<in> {ptr..+n * 2 ^ (gbits + pageBits)}

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> range_cover ptr sz (gbits + pageBits) n \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> valid_machine_state' \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+n * 2 ^ (gbits + pageBits)}) \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ (gbits + pageBits)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ (gbits + pageBits)) ptr = replicate (n * 2 ^ (gbits + pageBits)) 0) \<and> {ptr..+n * 2 ^ (gbits + pageBits)} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>x p off. \<lbrakk>x < 4; {p..+2 ^ objBitsKO KOUserData} \<inter> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)} = {}\<rbrakk> \<Longrightarrow> p + UCAST(10 \<rightarrow> 32) off * 4 + x \<notin> {ptr..+n * 2 ^ (gbits + pageBits)} proof (prove)
goal (2 subgoals):
 1. \<And>x p off. \<lbrakk>x < 4; {p..+2 ^ objBitsKO KOUserData} \<inter> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)} = {}; n = 0\<rbrakk> \<Longrightarrow> p + UCAST(10 \<rightarrow> 32) off * 4 + x \<notin> {ptr..+n * 2 ^ (gbits + pageBits)}
 2. \<And>x p off. \<lbrakk>x < 4; {p..+2 ^ objBitsKO KOUserData} \<inter> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)} = {}; n \<noteq> 0\<rbrakk> \<Longrightarrow> p + UCAST(10 \<rightarrow> 32) off * 4 + x \<notin> {ptr..+n * 2 ^ (gbits + pageBits)} proof (prove)
goal (1 subgoal):
 1. \<And>x p off. \<lbrakk>x < 4; {p..+2 ^ objBitsKO KOUserData} \<inter> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)} = {}; n \<noteq> 0\<rbrakk> \<Longrightarrow> p + UCAST(10 \<rightarrow> 32) off * 4 + x \<notin> {ptr..+n * 2 ^ (gbits + pageBits)} proof (prove)
goal (2 subgoals):
 1. \<And>x p off. \<lbrakk>x < 4; {p..+2 ^ objBitsKO KOUserData} \<inter> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)} = {}; n \<noteq> 0\<rbrakk> \<Longrightarrow> n \<noteq> 0
 2. \<And>x p off. \<lbrakk>x < 4; {p..+2 ^ objBitsKO KOUserData} \<inter> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)} = {}; n \<noteq> 0\<rbrakk> \<Longrightarrow> p + UCAST(10 \<rightarrow> 32) off * 4 + x \<notin> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)} proof (prove)
goal (1 subgoal):
 1. \<And>x p off. \<lbrakk>x < 4; {p..+2 ^ objBitsKO KOUserData} \<inter> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)} = {}; n \<noteq> 0\<rbrakk> \<Longrightarrow> p + UCAST(10 \<rightarrow> 32) off * 4 + x \<notin> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)} proof (prove)
goal (2 subgoals):
 1. \<And>x p off. \<lbrakk>x < 4; {p..+2 ^ objBitsKO KOUserData} \<inter> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)} = {}; n \<noteq> 0; p + UCAST(10 \<rightarrow> 32) off * 4 + x \<in> {p..+2 ^ objBitsKO KOUserData}\<rbrakk> \<Longrightarrow> p + UCAST(10 \<rightarrow> 32) off * 4 + x \<notin> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)}
 2. \<And>x p off. \<lbrakk>x < 4; {p..+2 ^ objBitsKO KOUserData} \<inter> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)} = {}; n \<noteq> 0\<rbrakk> \<Longrightarrow> p + UCAST(10 \<rightarrow> 32) off * 4 + x \<in> {p..+2 ^ objBitsKO KOUserData} proof (prove)
goal (1 subgoal):
 1. \<And>x p off. \<lbrakk>x < 4; {p..+2 ^ objBitsKO KOUserData} \<inter> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)} = {}; n \<noteq> 0\<rbrakk> \<Longrightarrow> p + UCAST(10 \<rightarrow> 32) off * 4 + x \<in> {p..+2 ^ objBitsKO KOUserData} proof (prove)
goal (1 subgoal):
 1. \<And>x p off. \<lbrakk>x < 4; {p + word_of_nat k |k. k < 2 ^ objBitsKO KOUserData} \<inter> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)} = {}; 0 < n\<rbrakk> \<Longrightarrow> \<exists>k. UCAST(10 \<rightarrow> 32) off * 4 + x = word_of_nat k \<and> k < 2 ^ objBitsKO KOUserData proof (prove)
goal (1 subgoal):
 1. \<And>x p off. \<lbrakk>x < 4; {p + word_of_nat k |k. k < 2 ^ objBitsKO KOUserData} \<inter> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)} = {}; 0 < n\<rbrakk> \<Longrightarrow> UCAST(10 \<rightarrow> 32) off * 4 + x = word_of_nat (unat off * 4 + unat x) \<and> unat off * 4 + unat x < 2 ^ objBitsKO KOUserData proof (prove)
goal (1 subgoal):
 1. \<And>x p off. \<lbrakk>x < 4; {p + word_of_nat k |k. k < 2 ^ objBitsKO KOUserData} \<inter> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)} = {}; 0 < n\<rbrakk> \<Longrightarrow> unat off * 4 + unat x < 2 ^ objBitsKO KOUserData proof (prove)
goal (3 subgoals):
 1. \<And>x p off. \<lbrakk>x < 4; {p + word_of_nat k |k. k < 2 ^ objBitsKO KOUserData} \<inter> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)} = {}; 0 < n\<rbrakk> \<Longrightarrow> unat x < 4
 2. \<And>x p off. \<lbrakk>x < 4; {p + word_of_nat k |k. k < 2 ^ objBitsKO KOUserData} \<inter> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)} = {}; 0 < n\<rbrakk> \<Longrightarrow> unat off < 2 ^ ?m16 x p off
 3. \<And>x p off. \<lbrakk>x < 4; {p + word_of_nat k |k. k < 2 ^ objBitsKO KOUserData} \<inter> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)} = {}; 0 < n\<rbrakk> \<Longrightarrow> objBitsKO KOUserData = Suc (Suc (?m16 x p off)) proof (prove)
goal (2 subgoals):
 1. \<And>x p off. \<lbrakk>x < 4; {p + word_of_nat k |k. k < 2 ^ objBitsKO KOUserData} \<inter> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)} = {}; 0 < n\<rbrakk> \<Longrightarrow> unat off < 2 ^ ?m16 x p off
 2. \<And>x p off. \<lbrakk>x < 4; {p + word_of_nat k |k. k < 2 ^ objBitsKO KOUserData} \<inter> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)} = {}; 0 < n\<rbrakk> \<Longrightarrow> objBitsKO KOUserData = Suc (Suc (?m16 x p off)) proof (prove)
goal (1 subgoal):
 1. \<And>x p off. \<lbrakk>x < 4; {p + word_of_nat k |k. k < 2 ^ objBitsKO KOUserData} \<inter> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)} = {}; 0 < n\<rbrakk> \<Longrightarrow> objBitsKO KOUserData = Suc (Suc LENGTH(10)) proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrakk>?x3 < 4; {?p3..+2 ^ objBitsKO KOUserData} \<inter> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)} = {}\<rbrakk> \<Longrightarrow> ?p3 + UCAST(10 \<rightarrow> 32) ?off3 * 4 + ?x3 \<notin> {ptr..+n * 2 ^ (gbits + pageBits)}

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> range_cover ptr sz (gbits + pageBits) n \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> valid_machine_state' \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+n * 2 ^ (gbits + pageBits)}) \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ (gbits + pageBits)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ (gbits + pageBits)) ptr = replicate (n * 2 ^ (gbits + pageBits)) 0) \<and> {ptr..+n * 2 ^ (gbits + pageBits)} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> {ptr..+n * 2 ^ (gbits + pageBits)} \<Longrightarrow> underlying_memory (ksMachineState \<sigma>) x = 0 proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>x \<in> {ptr..+n * 2 ^ (gbits + pageBits)}; n = 0\<rbrakk> \<Longrightarrow> underlying_memory (ksMachineState \<sigma>) x = 0
 2. \<And>x. \<lbrakk>x \<in> {ptr..+n * 2 ^ (gbits + pageBits)}; n \<noteq> 0\<rbrakk> \<Longrightarrow> underlying_memory (ksMachineState \<sigma>) x = 0 proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> {ptr..+n * 2 ^ (gbits + pageBits)}; n \<noteq> 0\<rbrakk> \<Longrightarrow> underlying_memory (ksMachineState \<sigma>) x = 0 proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> {ptr..+n * 2 ^ (gbits + pageBits)}; n \<noteq> 0\<rbrakk> \<Longrightarrow> x \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (1 subgoal):
 1. \<And>x. n \<noteq> 0 \<Longrightarrow> {ptr..+n * 2 ^ (gbits + pageBits)} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>n \<noteq> 0; n = 0\<rbrakk> \<Longrightarrow> {ptr..+n * 2 ^ (gbits + pageBits)} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}
 2. \<And>x. \<lbrakk>n \<noteq> 0; n \<noteq> 0\<rbrakk> \<Longrightarrow> {ptr..+n * 2 ^ (gbits + pageBits)} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>n \<noteq> 0; n \<noteq> 0\<rbrakk> \<Longrightarrow> {ptr..+n * 2 ^ (gbits + pageBits)} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>n \<noteq> 0; n \<noteq> 0\<rbrakk> \<Longrightarrow> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>n \<noteq> 0; n \<noteq> 0\<rbrakk> \<Longrightarrow> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)} \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ (gbits + pageBits) - 1} proof (prove)
goal:
No subgoals! proof (state)
this:
?x3 \<in> {ptr..+n * 2 ^ (gbits + pageBits)} \<Longrightarrow> underlying_memory (ksMachineState \<sigma>) ?x3 = 0

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> range_cover ptr sz (gbits + pageBits) n \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> valid_machine_state' \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+n * 2 ^ (gbits + pageBits)}) \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ (gbits + pageBits)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ (gbits + pageBits)) ptr = replicate (n * 2 ^ (gbits + pageBits)) 0) \<and> {ptr..+n * 2 ^ (gbits + pageBits)} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>p. p \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) \<Longrightarrow> cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) p) (from_bytes big_0s) proof (prove)
goal (1 subgoal):
 1. \<And>p. p \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) \<Longrightarrow> \<forall>off. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) p off = user_data_C.words_C (from_bytes big_0s).[unat off] proof (prove)
goal (1 subgoal):
 1. \<And>p. p \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) \<Longrightarrow> \<forall>off. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) p off = user_data_C.words_C (from_bytes big_0s).[unat off] proof (prove)
goal (1 subgoal):
 1. \<And>p off. p \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) \<Longrightarrow> byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) p off = user_data_C.words_C (from_bytes big_0s).[unat off] proof (prove)
goal (1 subgoal):
 1. \<And>p off. p \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) \<Longrightarrow> byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) p off = 0 proof (prove)
goal (1 subgoal):
 1. \<And>p. p \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) \<Longrightarrow> word_rcat [0, 0, 0, 0] = 0 proof (prove)
goal:
No subgoals! proof (state)
this:
?p3 \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) \<Longrightarrow> cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) ?p3) (from_bytes big_0s)

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> range_cover ptr sz (gbits + pageBits) n \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> valid_machine_state' \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+n * 2 ^ (gbits + pageBits)}) \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ (gbits + pageBits)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ (gbits + pageBits)) ptr = replicate (n * 2 ^ (gbits + pageBits)) 0) \<and> {ptr..+n * 2 ^ (gbits + pageBits)} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (state)
this:
(?i \<in> {?l..?u}) = (?l \<le> ?i \<and> ?i \<le> ?u)
({?a..?b} \<subseteq> {?c..?d}) = (\<not> ?a \<le> ?b \<or> ?c \<le> ?a \<and> ?b \<le> ?d)
(?i \<in> {?l..<?u}) = (?l \<le> ?i \<and> ?i < ?u)
{?a..?b} \<inter> {?c..?d} = {max ?a ?c..min ?b ?d}
({?a..?b} = {}) = (\<not> ?a \<le> ?b)
(\<exists>x. ?P x) = (\<exists>a b. ?P (a, b))

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> range_cover ptr sz (gbits + pageBits) n \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> valid_machine_state' \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+n * 2 ^ (gbits + pageBits)}) \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ (gbits + pageBits)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ (gbits + pageBits)) ptr = replicate (n * 2 ^ (gbits + pageBits)) 0) \<and> {ptr..+n * 2 ^ (gbits + pageBits)} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>xa v y. \<lbrakk>heap_to_user_data (\<lambda>x. if x \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) then Some KOUserData else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>)) xa = Some v; xa \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData); heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) xa = Some y\<rbrakk> \<Longrightarrow> y = v proof (prove)
using this:
n \<noteq> 0 \<Longrightarrow> {ptr..+n * 2 ^ (gbits + pageBits)} = {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)}

goal (1 subgoal):
 1. \<And>xa v y. \<lbrakk>heap_to_user_data (\<lambda>x. if x \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) then Some KOUserData else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>)) xa = Some v; xa \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData); heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) xa = Some y\<rbrakk> \<Longrightarrow> y = v proof (state)
this:
\<lbrakk>heap_to_user_data (\<lambda>x. if x \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) then Some KOUserData else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>)) ?xa3 = Some ?v3; ?xa3 \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData); heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) ?xa3 = Some ?y3\<rbrakk> \<Longrightarrow> ?y3 = ?v3

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> range_cover ptr sz (gbits + pageBits) n \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> valid_machine_state' \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+n * 2 ^ (gbits + pageBits)}) \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ (gbits + pageBits)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ (gbits + pageBits)) ptr = replicate (n * 2 ^ (gbits + pageBits)) 0) \<and> {ptr..+n * 2 ^ (gbits + pageBits)} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation \<Longrightarrow> cmap_relation (heap_to_user_data (\<lambda>x. if x \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) then Some KOUserData else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>))) (\<lambda>y. if y \<in> PTR(user_data_C) ` set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) then Some (from_bytes (replicate (2 ^ pageBits) 0)) else cslift x y) PTR(user_data_C) cuser_user_data_relation proof (prove)
goal (2 subgoals):
 1. cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation \<Longrightarrow> PTR(user_data_C) ` dom (heap_to_user_data (\<lambda>x. if x \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) then Some KOUserData else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>))) = dom (\<lambda>y. if y \<in> PTR(user_data_C) ` set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) then Some (from_bytes (replicate (2 ^ pageBits) 0)) else cslift x y)
 2. \<And>xa v v'. \<lbrakk>cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; heap_to_user_data (\<lambda>x. if x \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) then Some KOUserData else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>)) xa = Some v; (if PTR(user_data_C) xa \<in> PTR(user_data_C) ` set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) then Some (from_bytes (replicate (2 ^ pageBits) 0)) else cslift x (PTR(user_data_C) xa)) = Some v'\<rbrakk> \<Longrightarrow> cuser_user_data_relation v v' proof (prove)
goal (1 subgoal):
 1. \<And>xa v v'. \<lbrakk>cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; heap_to_user_data (\<lambda>x. if x \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) then Some KOUserData else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>)) xa = Some v; (if PTR(user_data_C) xa \<in> PTR(user_data_C) ` set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) then Some (from_bytes (replicate (2 ^ pageBits) 0)) else cslift x (PTR(user_data_C) xa)) = Some v'\<rbrakk> \<Longrightarrow> cuser_user_data_relation v v' proof (prove)
goal (2 subgoals):
 1. \<And>xa v v'. \<lbrakk>cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; heap_to_user_data (\<lambda>x. if x \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) then Some KOUserData else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>)) xa = Some v; (if PTR(user_data_C) xa \<in> PTR(user_data_C) ` set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) then Some (from_bytes (replicate (2 ^ pageBits) 0)) else cslift x (PTR(user_data_C) xa)) = Some v'; xa \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData)\<rbrakk> \<Longrightarrow> cuser_user_data_relation v v'
 2. \<And>xa v v'. \<lbrakk>cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; heap_to_user_data (\<lambda>x. if x \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) then Some KOUserData else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>)) xa = Some v; (if PTR(user_data_C) xa \<in> PTR(user_data_C) ` set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) then Some (from_bytes (replicate (2 ^ pageBits) 0)) else cslift x (PTR(user_data_C) xa)) = Some v'; xa \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData)\<rbrakk> \<Longrightarrow> cuser_user_data_relation v v' proof (prove)
goal (2 subgoals):
 1. \<And>xa z. \<lbrakk>cmap_relation (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) p) (map_to_user_data (ksPSpace \<sigma>) p)) (cslift x) PTR(user_data_C) cuser_user_data_relation; xa \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData); projectKO_opt KOUserData = Some z\<rbrakk> \<Longrightarrow> cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) xa) (from_bytes (replicate (2 ^ pageBits) 0))
 2. \<And>xa v v'. \<lbrakk>cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; heap_to_user_data (\<lambda>x. if x \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) then Some KOUserData else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>)) xa = Some v; (if PTR(user_data_C) xa \<in> PTR(user_data_C) ` set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) then Some (from_bytes (replicate (2 ^ pageBits) 0)) else cslift x (PTR(user_data_C) xa)) = Some v'; xa \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData)\<rbrakk> \<Longrightarrow> cuser_user_data_relation v v' proof (prove)
goal (1 subgoal):
 1. \<And>xa v v'. \<lbrakk>cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; heap_to_user_data (\<lambda>x. if x \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) then Some KOUserData else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>)) xa = Some v; (if PTR(user_data_C) xa \<in> PTR(user_data_C) ` set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) then Some (from_bytes (replicate (2 ^ pageBits) 0)) else cslift x (PTR(user_data_C) xa)) = Some v'; xa \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData)\<rbrakk> \<Longrightarrow> cuser_user_data_relation v v' proof (prove)
goal (2 subgoals):
 1. \<And>xa v v'. \<lbrakk>cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; heap_to_user_data (\<lambda>x. if x \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) then Some KOUserData else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>)) xa = Some v; (if PTR(user_data_C) xa \<in> PTR(user_data_C) ` set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) then Some (from_bytes (replicate (2 ^ pageBits) 0)) else cslift x (PTR(user_data_C) xa)) = Some v'; xa \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData); PTR(user_data_C) xa \<notin> PTR(user_data_C) ` set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData)\<rbrakk> \<Longrightarrow> cuser_user_data_relation v v'
 2. \<And>xa v v'. \<lbrakk>cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; heap_to_user_data (\<lambda>x. if x \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) then Some KOUserData else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>)) xa = Some v; (if PTR(user_data_C) xa \<in> PTR(user_data_C) ` set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) then Some (from_bytes (replicate (2 ^ pageBits) 0)) else cslift x (PTR(user_data_C) xa)) = Some v'; xa \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData)\<rbrakk> \<Longrightarrow> PTR(user_data_C) xa \<notin> PTR(user_data_C) ` set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) proof (prove)
goal (2 subgoals):
 1. \<And>xa v v'. \<lbrakk>cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; heap_to_user_data (\<lambda>x. if x \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) then Some KOUserData else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>)) xa = Some v; cslift x (PTR(user_data_C) xa) = Some v'; xa \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData); PTR(user_data_C) xa \<notin> PTR(user_data_C) ` set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData)\<rbrakk> \<Longrightarrow> cuser_user_data_relation v v'
 2. \<And>xa v v'. \<lbrakk>cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; heap_to_user_data (\<lambda>x. if x \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) then Some KOUserData else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>)) xa = Some v; (if PTR(user_data_C) xa \<in> PTR(user_data_C) ` set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) then Some (from_bytes (replicate (2 ^ pageBits) 0)) else cslift x (PTR(user_data_C) xa)) = Some v'; xa \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData)\<rbrakk> \<Longrightarrow> PTR(user_data_C) xa \<notin> PTR(user_data_C) ` set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) proof (prove)
goal (2 subgoals):
 1. \<And>xa v v' x' y. \<lbrakk>heap_to_user_data (\<lambda>x. if x \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) then Some KOUserData else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>)) xa = Some v; cslift x (PTR(user_data_C) xa) = Some v'; xa \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData); PTR(user_data_C) xa \<notin> PTR(user_data_C) ` set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData); PTR(user_data_C) xa = PTR(user_data_C) x'; cuser_user_data_relation y v'; heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) x' = Some y\<rbrakk> \<Longrightarrow> cuser_user_data_relation v v'
 2. \<And>xa v v'. \<lbrakk>cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; heap_to_user_data (\<lambda>x. if x \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) then Some KOUserData else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>)) xa = Some v; (if PTR(user_data_C) xa \<in> PTR(user_data_C) ` set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) then Some (from_bytes (replicate (2 ^ pageBits) 0)) else cslift x (PTR(user_data_C) xa)) = Some v'; xa \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData)\<rbrakk> \<Longrightarrow> PTR(user_data_C) xa \<notin> PTR(user_data_C) ` set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) proof (prove)
goal (3 subgoals):
 1. \<And>xa v v' x' y. \<lbrakk>cslift x (PTR(user_data_C) xa) = Some v'; xa \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData); PTR(user_data_C) xa \<notin> PTR(user_data_C) ` set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData); PTR(user_data_C) xa = PTR(user_data_C) x'; cuser_user_data_relation y v'; heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) x' = Some y\<rbrakk> \<Longrightarrow> heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) xa = Some (?y22 xa v v' x' y)
 2. \<And>xa v v' x' y. \<lbrakk>cslift x (PTR(user_data_C) xa) = Some v'; xa \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData); PTR(user_data_C) xa \<notin> PTR(user_data_C) ` set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData); PTR(user_data_C) xa = PTR(user_data_C) x'; cuser_user_data_relation y v'; heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) x' = Some y; ?y22 xa v v' x' y = v\<rbrakk> \<Longrightarrow> cuser_user_data_relation v v'
 3. \<And>xa v v'. \<lbrakk>cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; heap_to_user_data (\<lambda>x. if x \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) then Some KOUserData else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>)) xa = Some v; (if PTR(user_data_C) xa \<in> PTR(user_data_C) ` set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) then Some (from_bytes (replicate (2 ^ pageBits) 0)) else cslift x (PTR(user_data_C) xa)) = Some v'; xa \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData)\<rbrakk> \<Longrightarrow> PTR(user_data_C) xa \<notin> PTR(user_data_C) ` set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) proof (prove)
goal (2 subgoals):
 1. \<And>xa v v' x' y. \<lbrakk>cslift x (PTR(user_data_C) xa) = Some v'; xa \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData); PTR(user_data_C) xa \<notin> PTR(user_data_C) ` set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData); PTR(user_data_C) xa = PTR(user_data_C) x'; cuser_user_data_relation y v'; heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) x' = Some y; y = v\<rbrakk> \<Longrightarrow> cuser_user_data_relation v v'
 2. \<And>xa v v'. \<lbrakk>cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; heap_to_user_data (\<lambda>x. if x \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) then Some KOUserData else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>)) xa = Some v; (if PTR(user_data_C) xa \<in> PTR(user_data_C) ` set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) then Some (from_bytes (replicate (2 ^ pageBits) 0)) else cslift x (PTR(user_data_C) xa)) = Some v'; xa \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData)\<rbrakk> \<Longrightarrow> PTR(user_data_C) xa \<notin> PTR(user_data_C) ` set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) proof (prove)
goal (1 subgoal):
 1. \<And>xa v v'. \<lbrakk>cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; heap_to_user_data (\<lambda>x. if x \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) then Some KOUserData else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>)) xa = Some v; (if PTR(user_data_C) xa \<in> PTR(user_data_C) ` set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) then Some (from_bytes (replicate (2 ^ pageBits) 0)) else cslift x (PTR(user_data_C) xa)) = Some v'; xa \<notin> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData)\<rbrakk> \<Longrightarrow> PTR(user_data_C) xa \<notin> PTR(user_data_C) ` set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) proof (prove)
goal:
No subgoals! proof (state)
this:
cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation \<Longrightarrow> cmap_relation (heap_to_user_data (\<lambda>x. if x \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) then Some KOUserData else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>))) (\<lambda>y. if y \<in> PTR(user_data_C) ` set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) then Some (from_bytes (replicate (2 ^ pageBits) 0)) else cslift x y) PTR(user_data_C) cuser_user_data_relation

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> range_cover ptr sz (gbits + pageBits) n \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> valid_machine_state' \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+n * 2 ^ (gbits + pageBits)}) \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ (gbits + pageBits)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ (gbits + pageBits)) ptr = replicate (n * 2 ^ (gbits + pageBits)) 0) \<and> {ptr..+n * 2 ^ (gbits + pageBits)} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (state)
this:
cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation \<Longrightarrow> cmap_relation (heap_to_user_data (\<lambda>x. if x \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) then Some KOUserData else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>))) (\<lambda>y. if y \<in> PTR(user_data_C) ` set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) then Some (from_bytes (replicate (2 ^ pageBits) 0)) else cslift x y) PTR(user_data_C) cuser_user_data_relation

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> range_cover ptr sz (gbits + pageBits) n \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> valid_machine_state' \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+n * 2 ^ (gbits + pageBits)}) \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ (gbits + pageBits)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ (gbits + pageBits)) ptr = replicate (n * 2 ^ (gbits + pageBits)) 0) \<and> {ptr..+n * 2 ^ (gbits + pageBits)} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. size_of TYPE(user_data_C) = 2 ^ objBitsKO ko proof (state)
this:
size_of TYPE(user_data_C) = 2 ^ objBitsKO ko

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> range_cover ptr sz (gbits + pageBits) n \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> valid_machine_state' \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+n * 2 ^ (gbits + pageBits)}) \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ (gbits + pageBits)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ (gbits + pageBits)) ptr = replicate (n * 2 ^ (gbits + pageBits)) 0) \<and> {ptr..+n * 2 ^ (gbits + pageBits)} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. n * 2 ^ (gbits + pageBits) = n * 2 ^ gbits * size_of TYPE(user_data_C) proof (prove)
using this:
gbits + pageBits \<le> sz

goal (1 subgoal):
 1. n * 2 ^ (gbits + pageBits) = n * 2 ^ gbits * size_of TYPE(user_data_C) proof (prove)
goal (1 subgoal):
 1. gbits + pageBits \<le> sz \<Longrightarrow> n * 2 ^ (gbits + pageBits) = n * 2 ^ gbits * 2 ^ objBitsKO ko proof (prove)
goal:
No subgoals! proof (state)
this:
n * 2 ^ (gbits + pageBits) = n * 2 ^ gbits * size_of TYPE(user_data_C)

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> range_cover ptr sz (gbits + pageBits) n \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> valid_machine_state' \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+n * 2 ^ (gbits + pageBits)}) \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ (gbits + pageBits)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ (gbits + pageBits)) ptr = replicate (n * 2 ^ (gbits + pageBits)) 0) \<and> {ptr..+n * 2 ^ (gbits + pageBits)} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. region_is_bytes ptr (n * 2 ^ gbits * 2 ^ objBitsKO ko) x proof (prove)
using this:
region_is_bytes ptr (n * 2 ^ (gbits + pageBits)) x

goal (1 subgoal):
 1. region_is_bytes ptr (n * 2 ^ gbits * 2 ^ objBitsKO ko) x proof (state)
this:
region_is_bytes ptr (n * 2 ^ gbits * 2 ^ objBitsKO ko) x

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> range_cover ptr sz (gbits + pageBits) n \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> valid_machine_state' \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+n * 2 ^ (gbits + pageBits)}) \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ (gbits + pageBits)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ (gbits + pageBits)) ptr = replicate (n * 2 ^ (gbits + pageBits)) 0) \<and> {ptr..+n * 2 ^ (gbits + pageBits)} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (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(user_data_C); typ_uinfo_t TYPE(?'b) \<noteq> typ_uinfo_t TYPE(8 word)\<rbrakk> \<Longrightarrow> clift (hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) ?arr) (t_hrs_' (globals x))) = cslift x

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> range_cover ptr sz (gbits + pageBits) n \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> valid_machine_state' \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+n * 2 ^ (gbits + pageBits)}) \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ (gbits + pageBits)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ (gbits + pageBits)) ptr = replicate (n * 2 ^ (gbits + pageBits)) 0) \<and> {ptr..+n * 2 ^ (gbits + pageBits)} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (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(user_data_C); typ_uinfo_t TYPE(?'b) \<noteq> typ_uinfo_t TYPE(8 word)\<rbrakk> \<Longrightarrow> clift (hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) ?arr) (t_hrs_' (globals x))) = cslift x

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> range_cover ptr sz (gbits + pageBits) n \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> valid_machine_state' \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+n * 2 ^ (gbits + pageBits)}) \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ (gbits + pageBits)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ (gbits + pageBits)) ptr = replicate (n * 2 ^ (gbits + pageBits)) 0) \<and> {ptr..+n * 2 ^ (gbits + pageBits)} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (state)
this:
\<lbrakk>KOUserData \<equiv> ?x; \<forall>v. projectKO_opt ?x \<noteq> Some v\<rbrakk> \<Longrightarrow> projectKO_opt \<circ>\<^sub>m (\<lambda>x. if x \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) then Some KOUserData else ksPSpace \<sigma> x) = projectKO_opt \<circ>\<^sub>m ksPSpace \<sigma>

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> range_cover ptr sz (gbits + pageBits) n \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> valid_machine_state' \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+n * 2 ^ (gbits + pageBits)}) \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ (gbits + pageBits)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ (gbits + pageBits)) ptr = replicate (n * 2 ^ (gbits + pageBits)) 0) \<and> {ptr..+n * 2 ^ (gbits + pageBits)} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (state)
this:
map_to_ctes (\<lambda>xa. if xa \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr ko) then Some ko else ksPSpace \<sigma> xa) = (\<lambda>x. if Inr object_type.SmallPageObject = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> x \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr ko) \<or> Inr object_type.SmallPageObject = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> x && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr ko) \<and> x && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then Some (CTE capability.NullCap nullMDBNode) else ctes_of \<sigma> x)

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> range_cover ptr sz (gbits + pageBits) n \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> valid_machine_state' \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+n * 2 ^ (gbits + pageBits)}) \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ (gbits + pageBits)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ (gbits + pageBits)) ptr = replicate (n * 2 ^ (gbits + pageBits)) 0) \<and> {ptr..+n * 2 ^ (gbits + pageBits)} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (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> ''user_data_C'' \<and> typ_name (typ_info_t TYPE(?'b1)) \<noteq> ''word0000010'' \<and> typ_name (typ_info_t TYPE(?'b1)) \<noteq> ''word0000010_array_000000000010''; ''user_data_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 (n * 2 ^ gbits) (PTR(user_data_C) ptr) ?arr1) (t_hrs_' (globals x)))) c_guard = c_h_t_valid x

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> range_cover ptr sz (gbits + pageBits) n \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> valid_machine_state' \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+n * 2 ^ (gbits + pageBits)}) \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ (gbits + pageBits)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ (gbits + pageBits)) ptr = replicate (n * 2 ^ (gbits + pageBits)) 0) \<and> {ptr..+n * 2 ^ (gbits + pageBits)} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<forall>t<n * 2 ^ gbits. c_guard (PTR(user_data_C) ptr +\<^sub>p int t) proof (prove)
goal (2 subgoals):
 1. 2 \<le> objBitsKO ko
 2. align_of TYPE(user_data_C) = 2\<^sup>2 proof (prove)
goal:
No subgoals! proof (state)
this:
\<forall>t<n * 2 ^ gbits. c_guard (PTR(user_data_C) ptr +\<^sub>p int t)

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> range_cover ptr sz (gbits + pageBits) n \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> valid_machine_state' \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+n * 2 ^ (gbits + pageBits)}) \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ (gbits + pageBits)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ (gbits + pageBits)) ptr = replicate (n * 2 ^ (gbits + pageBits)) 0) \<and> {ptr..+n * 2 ^ (gbits + pageBits)} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (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> range_cover ptr sz (gbits + pageBits) n \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> valid_machine_state' \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+n * 2 ^ (gbits + pageBits)}) \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ (gbits + pageBits)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ (gbits + pageBits)) ptr = replicate (n * 2 ^ (gbits + pageBits)) 0) \<and> {ptr..+n * 2 ^ (gbits + pageBits)} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (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 KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>)) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (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 KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x)))) cte_Ptr ccte_relation \<and> cpspace_tcb_relation (foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>)) (hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x))) \<and> cmap_relation (map_to_eps (foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x)))) ep_Ptr (cendpoint_relation (clift (hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x))))) \<and> cmap_relation (map_to_ntfns (foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x)))) ntfn_Ptr (cnotification_relation (clift (hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x))))) \<and> cmap_relation (map_to_pdes (foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x)))) pde_Ptr cpde_relation \<and> cmap_relation (map_to_ptes (foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x)))) pte_Ptr cpte_relation \<and> cmap_relation (map_to_asidpools (foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x)))) ap_Ptr casid_pool_relation \<and> cpspace_user_data_relation (foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>)) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x))) \<and> cpspace_device_data_relation (foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>)) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x))) \<and> cpspace_pde_array_relation (foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>)) (hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x))) \<and> cpspace_pte_array_relation (foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>)) (hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (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
region_is_bytes ptr (n * 2 ^ (gbits + pageBits)) x
range_cover ptr sz (objBitsKO ko) (n * 2 ^ gbits)
size_of TYPE(user_data_C) = 2 ^ objBitsKO ko

goal (1 subgoal):
 1. cmap_relation (map_to_ctes (foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x)))) cte_Ptr ccte_relation \<and> cpspace_tcb_relation (foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>)) (hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x))) \<and> cmap_relation (map_to_eps (foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x)))) ep_Ptr (cendpoint_relation (clift (hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x))))) \<and> cmap_relation (map_to_ntfns (foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x)))) ntfn_Ptr (cnotification_relation (clift (hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x))))) \<and> cmap_relation (map_to_pdes (foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x)))) pde_Ptr cpde_relation \<and> cmap_relation (map_to_ptes (foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x)))) pte_Ptr cpte_relation \<and> cmap_relation (map_to_asidpools (foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x)))) ap_Ptr casid_pool_relation \<and> cpspace_user_data_relation (foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>)) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x))) \<and> cpspace_device_data_relation (foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>)) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x))) \<and> cpspace_pde_array_relation (foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>)) (hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x))) \<and> cpspace_pte_array_relation (foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>)) (hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>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; region_is_bytes ptr (n * 2 ^ (gbits + pageBits)) x; range_cover ptr sz (objBitsKO ko) (n * 2 ^ gbits); size_of TYPE(user_data_C) = 2 ^ objBitsKO ko\<rbrakk> \<Longrightarrow> cmap_relation (map_to_ctes (foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x)))) cte_Ptr ccte_relation \<and> cpspace_tcb_relation (foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>)) (hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x))) \<and> cmap_relation (map_to_eps (foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x)))) ep_Ptr (cendpoint_relation (clift (hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x))))) \<and> cmap_relation (map_to_ntfns (foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x)))) ntfn_Ptr (cnotification_relation (clift (hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x))))) \<and> cmap_relation (map_to_pdes (foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x)))) pde_Ptr cpde_relation \<and> cmap_relation (map_to_ptes (foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x)))) pte_Ptr cpte_relation \<and> cmap_relation (map_to_asidpools (foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x)))) ap_Ptr casid_pool_relation \<and> cpspace_user_data_relation (foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>)) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x))) \<and> cpspace_device_data_relation (foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>)) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x))) \<and> cpspace_pde_array_relation (foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>)) (hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x))) \<and> cpspace_pte_array_relation (foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>)) (hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>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; region_is_bytes ptr (n * 2 ^ (gbits + pageBits)) x; range_cover ptr sz (objBitsKO ko) (n * 2 ^ gbits); size_of TYPE(user_data_C) = 2 ^ objBitsKO ko\<rbrakk> \<Longrightarrow> cmap_relation (map_to_ctes (foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x)))) cte_Ptr ccte_relation \<and> cpspace_tcb_relation (foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>)) (hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x))) \<and> cmap_relation (map_to_eps (foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x)))) ep_Ptr (cendpoint_relation (clift (hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x))))) \<and> cmap_relation (map_to_ntfns (foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x)))) ntfn_Ptr (cnotification_relation (clift (hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x))))) \<and> cmap_relation (map_to_pdes (foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x)))) pde_Ptr cpde_relation \<and> cmap_relation (map_to_ptes (foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x)))) pte_Ptr cpte_relation \<and> cmap_relation (map_to_asidpools (foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x)))) ap_Ptr casid_pool_relation \<and> cpspace_user_data_relation (foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>)) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x))) \<and> cpspace_device_data_relation (foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>)) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x))) \<and> cpspace_pde_array_relation (foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>)) (hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x))) \<and> cpspace_pte_array_relation (foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>)) (hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>region_is_bytes ptr (n * 2 ^ (gbits + pageBits)) x; range_cover ptr sz (objBitsKO ko) (n * 2 ^ gbits); size_of TYPE(user_data_C) = 2 ^ objBitsKO ko; 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_ctes (\<lambda>x. if x \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) then Some KOUserData else ksPSpace \<sigma> x)) (cslift x) cte_Ptr ccte_relation \<and> cmap_relation (map_to_tcbs (\<lambda>x. if x \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) then Some KOUserData 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 (n * 2 ^ gbits) ptr KOUserData) then Some KOUserData 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 (n * 2 ^ gbits) ptr KOUserData) then Some KOUserData 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 (n * 2 ^ gbits) ptr KOUserData) then Some KOUserData 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 (n * 2 ^ gbits) ptr KOUserData) then Some KOUserData 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 (n * 2 ^ gbits) ptr KOUserData) then Some KOUserData else ksPSpace \<sigma> x)) (cslift x) ap_Ptr casid_pool_relation \<and> cpspace_user_data_relation (\<lambda>x. if x \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) then Some KOUserData else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x))) \<and> cmap_relation (heap_to_device_data (\<lambda>x. if x \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) then Some KOUserData 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 (n * 2 ^ gbits) ptr KOUserData) then Some KOUserData 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 (n * 2 ^ gbits) ptr KOUserData) then Some KOUserData else ksPSpace \<sigma> x)) (c_h_t_valid x) pt_Ptr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>region_is_bytes ptr (n * 2 ^ gbits * 2 ^ pageBits) x; range_cover ptr sz (objBitsKO KOUserData) (n * 2 ^ gbits); size_of TYPE(user_data_C) = 2 ^ objBitsKO KOUserData; 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> cpspace_user_data_relation (\<lambda>x. if x \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) then Some KOUserData else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x))) proof (prove)
goal (6 subgoals):
 1. \<lbrakk>region_is_bytes ptr (n * 2 ^ gbits * 2 ^ pageBits) x; range_cover ptr sz (objBitsKO KOUserData) (n * 2 ^ gbits); size_of TYPE(user_data_C) = 2 ^ objBitsKO KOUserData; 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> region_is_bytes ptr (n * 2 ^ gbits * size_of TYPE(user_data_C)) x
 2. \<lbrakk>region_is_bytes ptr (n * 2 ^ gbits * 2 ^ pageBits) x; range_cover ptr sz (objBitsKO KOUserData) (n * 2 ^ gbits); size_of TYPE(user_data_C) = 2 ^ objBitsKO KOUserData; 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> typ_uinfo_t TYPE(user_data_C) \<noteq> typ_uinfo_t TYPE(8 word)
 3. \<lbrakk>region_is_bytes ptr (n * 2 ^ gbits * 2 ^ pageBits) x; range_cover ptr sz (objBitsKO KOUserData) (n * 2 ^ gbits); size_of TYPE(user_data_C) = 2 ^ objBitsKO KOUserData; 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> ?nb15 = n * 2 ^ gbits * size_of TYPE(user_data_C)
 4. \<lbrakk>region_is_bytes ptr (n * 2 ^ gbits * 2 ^ pageBits) x; range_cover ptr sz (objBitsKO KOUserData) (n * 2 ^ gbits); size_of TYPE(user_data_C) = 2 ^ objBitsKO KOUserData; 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> n * 2 ^ gbits * size_of TYPE(user_data_C) < 2 ^ word_bits
 5. \<lbrakk>region_is_bytes ptr (n * 2 ^ gbits * 2 ^ pageBits) x; range_cover ptr sz (objBitsKO KOUserData) (n * 2 ^ gbits); size_of TYPE(user_data_C) = 2 ^ objBitsKO KOUserData; 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> heap_list (hrs_mem (t_hrs_' (globals x))) ?nb15 ptr = replicate ?nb15 0
 6. \<lbrakk>region_is_bytes ptr (n * 2 ^ gbits * 2 ^ pageBits) x; range_cover ptr sz (objBitsKO KOUserData) (n * 2 ^ gbits); size_of TYPE(user_data_C) = 2 ^ objBitsKO KOUserData; 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 (heap_to_user_data (\<lambda>x. if x \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) then Some KOUserData else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>))) (\<lambda>y. if y \<in> ((+\<^sub>p) (PTR(user_data_C) ptr) \<circ> int) ` {k. k < n * 2 ^ gbits} then Some (from_bytes (replicate (size_of TYPE(user_data_C)) 0)) else cslift x y) PTR(user_data_C) cuser_user_data_relation proof (prove)
goal (5 subgoals):
 1. \<lbrakk>region_is_bytes ptr (n * 2 ^ gbits * 2 ^ pageBits) x; range_cover ptr sz (objBitsKO KOUserData) (n * 2 ^ gbits); size_of TYPE(user_data_C) = 2 ^ objBitsKO KOUserData; 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> typ_uinfo_t TYPE(user_data_C) \<noteq> typ_uinfo_t TYPE(8 word)
 2. \<lbrakk>region_is_bytes ptr (n * 2 ^ gbits * 2 ^ pageBits) x; range_cover ptr sz (objBitsKO KOUserData) (n * 2 ^ gbits); size_of TYPE(user_data_C) = 2 ^ objBitsKO KOUserData; 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> ?nb15 = n * 2 ^ gbits * size_of TYPE(user_data_C)
 3. \<lbrakk>region_is_bytes ptr (n * 2 ^ gbits * 2 ^ pageBits) x; range_cover ptr sz (objBitsKO KOUserData) (n * 2 ^ gbits); size_of TYPE(user_data_C) = 2 ^ objBitsKO KOUserData; 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> n * 2 ^ gbits * size_of TYPE(user_data_C) < 2 ^ word_bits
 4. \<lbrakk>region_is_bytes ptr (n * 2 ^ gbits * 2 ^ pageBits) x; range_cover ptr sz (objBitsKO KOUserData) (n * 2 ^ gbits); size_of TYPE(user_data_C) = 2 ^ objBitsKO KOUserData; 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> heap_list (hrs_mem (t_hrs_' (globals x))) ?nb15 ptr = replicate ?nb15 0
 5. \<lbrakk>region_is_bytes ptr (n * 2 ^ gbits * 2 ^ pageBits) x; range_cover ptr sz (objBitsKO KOUserData) (n * 2 ^ gbits); size_of TYPE(user_data_C) = 2 ^ objBitsKO KOUserData; 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 (heap_to_user_data (\<lambda>x. if x \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) then Some KOUserData else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>))) (\<lambda>y. if y \<in> ((+\<^sub>p) (PTR(user_data_C) ptr) \<circ> int) ` {k. k < n * 2 ^ gbits} then Some (from_bytes (replicate (size_of TYPE(user_data_C)) 0)) else cslift x y) PTR(user_data_C) cuser_user_data_relation proof (prove)
goal (4 subgoals):
 1. \<lbrakk>region_is_bytes ptr (n * 2 ^ gbits * 2 ^ pageBits) x; range_cover ptr sz (objBitsKO KOUserData) (n * 2 ^ gbits); size_of TYPE(user_data_C) = 2 ^ objBitsKO KOUserData; 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> ?nb15 = n * 2 ^ gbits * size_of TYPE(user_data_C)
 2. \<lbrakk>region_is_bytes ptr (n * 2 ^ gbits * 2 ^ pageBits) x; range_cover ptr sz (objBitsKO KOUserData) (n * 2 ^ gbits); size_of TYPE(user_data_C) = 2 ^ objBitsKO KOUserData; 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> n * 2 ^ gbits * size_of TYPE(user_data_C) < 2 ^ word_bits
 3. \<lbrakk>region_is_bytes ptr (n * 2 ^ gbits * 2 ^ pageBits) x; range_cover ptr sz (objBitsKO KOUserData) (n * 2 ^ gbits); size_of TYPE(user_data_C) = 2 ^ objBitsKO KOUserData; 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> heap_list (hrs_mem (t_hrs_' (globals x))) ?nb15 ptr = replicate ?nb15 0
 4. \<lbrakk>region_is_bytes ptr (n * 2 ^ gbits * 2 ^ pageBits) x; range_cover ptr sz (objBitsKO KOUserData) (n * 2 ^ gbits); size_of TYPE(user_data_C) = 2 ^ objBitsKO KOUserData; 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 (heap_to_user_data (\<lambda>x. if x \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) then Some KOUserData else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>))) (\<lambda>y. if y \<in> ((+\<^sub>p) (PTR(user_data_C) ptr) \<circ> int) ` {k. k < n * 2 ^ gbits} then Some (from_bytes (replicate (size_of TYPE(user_data_C)) 0)) else cslift x y) PTR(user_data_C) cuser_user_data_relation proof (prove)
goal (3 subgoals):
 1. \<lbrakk>region_is_bytes ptr (n * 2 ^ gbits * 2 ^ pageBits) x; range_cover ptr sz (objBitsKO KOUserData) (n * 2 ^ gbits); size_of TYPE(user_data_C) = 2 ^ objBitsKO KOUserData; 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> n * 2 ^ gbits * size_of TYPE(user_data_C) < 2 ^ word_bits
 2. \<lbrakk>region_is_bytes ptr (n * 2 ^ gbits * 2 ^ pageBits) x; range_cover ptr sz (objBitsKO KOUserData) (n * 2 ^ gbits); size_of TYPE(user_data_C) = 2 ^ objBitsKO KOUserData; 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> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ gbits * 4096) ptr = replicate (n * 2 ^ gbits * 4096) 0
 3. \<lbrakk>region_is_bytes ptr (n * 2 ^ gbits * 2 ^ pageBits) x; range_cover ptr sz (objBitsKO KOUserData) (n * 2 ^ gbits); size_of TYPE(user_data_C) = 2 ^ objBitsKO KOUserData; 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 (heap_to_user_data (\<lambda>x. if x \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) then Some KOUserData else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>))) (\<lambda>y. if y \<in> ((+\<^sub>p) (PTR(user_data_C) ptr) \<circ> int) ` {k. k < n * 2 ^ gbits} then Some (from_bytes (replicate (size_of TYPE(user_data_C)) 0)) else cslift x y) PTR(user_data_C) cuser_user_data_relation proof (prove)
goal (3 subgoals):
 1. \<lbrakk>region_is_bytes ptr (n * 2 ^ gbits * 2 ^ pageBits) x; range_cover ptr sz (objBitsKO KOUserData) (n * 2 ^ gbits); size_of TYPE(user_data_C) = 2 ^ objBitsKO KOUserData; 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; n * 2 ^ (gbits + pageBits) < 2 ^ word_bits\<rbrakk> \<Longrightarrow> n * 2 ^ gbits * 2 ^ objBitsKO KOUserData < 2 ^ word_bits
 2. \<lbrakk>region_is_bytes ptr (n * 2 ^ gbits * 2 ^ pageBits) x; range_cover ptr sz (objBitsKO KOUserData) (n * 2 ^ gbits); size_of TYPE(user_data_C) = 2 ^ objBitsKO KOUserData; 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> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ gbits * 4096) ptr = replicate (n * 2 ^ gbits * 4096) 0
 3. \<lbrakk>region_is_bytes ptr (n * 2 ^ gbits * 2 ^ pageBits) x; range_cover ptr sz (objBitsKO KOUserData) (n * 2 ^ gbits); size_of TYPE(user_data_C) = 2 ^ objBitsKO KOUserData; 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 (heap_to_user_data (\<lambda>x. if x \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) then Some KOUserData else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>))) (\<lambda>y. if y \<in> ((+\<^sub>p) (PTR(user_data_C) ptr) \<circ> int) ` {k. k < n * 2 ^ gbits} then Some (from_bytes (replicate (size_of TYPE(user_data_C)) 0)) else cslift x y) PTR(user_data_C) cuser_user_data_relation proof (prove)
goal (2 subgoals):
 1. \<lbrakk>region_is_bytes ptr (n * 2 ^ gbits * 2 ^ pageBits) x; range_cover ptr sz (objBitsKO KOUserData) (n * 2 ^ gbits); size_of TYPE(user_data_C) = 2 ^ objBitsKO KOUserData; 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> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ gbits * 4096) ptr = replicate (n * 2 ^ gbits * 4096) 0
 2. \<lbrakk>region_is_bytes ptr (n * 2 ^ gbits * 2 ^ pageBits) x; range_cover ptr sz (objBitsKO KOUserData) (n * 2 ^ gbits); size_of TYPE(user_data_C) = 2 ^ objBitsKO KOUserData; 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 (heap_to_user_data (\<lambda>x. if x \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) then Some KOUserData else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>))) (\<lambda>y. if y \<in> ((+\<^sub>p) (PTR(user_data_C) ptr) \<circ> int) ` {k. k < n * 2 ^ gbits} then Some (from_bytes (replicate (size_of TYPE(user_data_C)) 0)) else cslift x y) PTR(user_data_C) cuser_user_data_relation proof (prove)
goal (2 subgoals):
 1. \<lbrakk>region_is_bytes ptr (n * 2 ^ gbits * 2 ^ pageBits) x; range_cover ptr sz (objBitsKO KOUserData) (n * 2 ^ gbits); size_of TYPE(user_data_C) = 2 ^ objBitsKO KOUserData; 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; heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ (gbits + pageBits)) ptr = replicate (n * 2 ^ (gbits + pageBits)) 0\<rbrakk> \<Longrightarrow> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ gbits * 4096) ptr = replicate (n * 2 ^ gbits * 4096) 0
 2. \<lbrakk>region_is_bytes ptr (n * 2 ^ gbits * 2 ^ pageBits) x; range_cover ptr sz (objBitsKO KOUserData) (n * 2 ^ gbits); size_of TYPE(user_data_C) = 2 ^ objBitsKO KOUserData; 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 (heap_to_user_data (\<lambda>x. if x \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) then Some KOUserData else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>))) (\<lambda>y. if y \<in> ((+\<^sub>p) (PTR(user_data_C) ptr) \<circ> int) ` {k. k < n * 2 ^ gbits} then Some (from_bytes (replicate (size_of TYPE(user_data_C)) 0)) else cslift x y) PTR(user_data_C) cuser_user_data_relation proof (prove)
goal (1 subgoal):
 1. \<lbrakk>region_is_bytes ptr (n * 2 ^ gbits * 2 ^ pageBits) x; range_cover ptr sz (objBitsKO KOUserData) (n * 2 ^ gbits); size_of TYPE(user_data_C) = 2 ^ objBitsKO KOUserData; 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 (heap_to_user_data (\<lambda>x. if x \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) then Some KOUserData else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>))) (\<lambda>y. if y \<in> ((+\<^sub>p) (PTR(user_data_C) ptr) \<circ> int) ` {k. k < n * 2 ^ gbits} then Some (from_bytes (replicate (size_of TYPE(user_data_C)) 0)) else cslift x y) PTR(user_data_C) cuser_user_data_relation proof (prove)
goal (1 subgoal):
 1. \<lbrakk>region_is_bytes ptr (n * 2 ^ gbits * 2 ^ pageBits) x; range_cover ptr sz pageBits (n * 2 ^ gbits); size_of TYPE(user_data_C) = 2 ^ pageBits; 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 (heap_to_user_data (\<lambda>x. if x \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) then Some KOUserData else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>))) (\<lambda>y. if y \<in> PTR(user_data_C) ` set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) then Some (from_bytes (replicate (2 ^ pageBits) 0)) else cslift x y) PTR(user_data_C) cuser_user_data_relation proof (prove)
goal (1 subgoal):
 1. \<lbrakk>region_is_bytes ptr (n * 2 ^ (gbits + pageBits)) x; range_cover ptr sz pageBits (n * 2 ^ gbits); size_of TYPE(user_data_C) = 2 ^ pageBits; 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 (heap_to_user_data (\<lambda>x. if x \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) then Some KOUserData else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>))) (\<lambda>y. if y \<in> PTR(user_data_C) ` set (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) then Some (from_bytes (replicate (2 ^ pageBits) 0)) else cslift x y) PTR(user_data_C) cuser_user_data_relation proof (prove)
goal:
No subgoals! proof (state)
this:
cpspace_relation (foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>)) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x)))

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> range_cover ptr sz (gbits + pageBits) n \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> valid_machine_state' \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+n * 2 ^ (gbits + pageBits)}) \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ (gbits + pageBits)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ (gbits + pageBits)) ptr = replicate (n * 2 ^ (gbits + pageBits)) 0) \<and> {ptr..+n * 2 ^ (gbits + pageBits)} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
using this:
cpspace_relation (foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>)) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x)))

goal (1 subgoal):
 1. (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
using this:
cpspace_relation (foldr (\<lambda>addr. data_map_insert addr KOUserData) (new_cap_addrs (n * 2 ^ gbits) ptr KOUserData) (ksPSpace \<sigma>)) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen (n * 2 ^ gbits) (PTR(user_data_C) ptr) arr) (t_hrs_' (globals x)))
(\<sigma>, x) \<in> rf_sr
region_is_bytes ptr (n * 2 ^ (gbits + pageBits)) x
{ptr..+n * 2 ^ (gbits + pageBits)} \<inter> kernel_data_refs = {}
(valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+n * 2 ^ (gbits + pageBits)}) \<sigma>

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

goal:
No subgoals!