theory Retype_C

lemma createObjects_ccorres_pde:
  defines "ko \<equiv> (KOArch (KOPDE (makeObject :: pde)))"
  shows "\<forall>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> ptr \<noteq> 0
  \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma>
  \<and> pspace_no_overlap' ptr sz \<sigma>
  \<and> ret_zero ptr (2 ^ pdBits) \<sigma>
  \<and> region_is_zero_bytes ptr (2 ^ pdBits) x
  \<and> range_cover ptr sz pdBits 1
  \<and> valid_global_refs' s
  \<and> kernel_data_refs \<inter> {ptr..+ 2 ^ pdBits} = {} \<longrightarrow>
  (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>)\<rparr>,
   x\<lparr>globals := globals x
                 \<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (Ptr ptr :: (pde_C[4096]) ptr) False)
                       (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 :: (pde_C[4096]) ptr" assume "?P \<sigma> x" hence rf: "(\<sigma>, x) \<in> rf_sr" and al: "is_aligned ptr pdBits" and ptr0: "ptr \<noteq> 0"
    and cover: "range_cover ptr sz pdBits 1"
    and sz: "pdBits \<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 rzo: "ret_zero ptr (2 ^ pdBits) \<sigma>"
    and empty: "region_is_bytes ptr (2 ^ pdBits) x"
    and zero: "heap_list_is_zero (hrs_mem (t_hrs_' (globals x))) ptr (2 ^ pdBits)"
    and kernel_data_refs_disj : "kernel_data_refs \<inter> {ptr..+ 2 ^ pdBits} = {}" by (clarsimp simp:range_cover_def[where 'a=32, folded word_bits_def])+ 

  (* obj specific *)
   have mko: "\<And>dev. makeObjectKO dev (Inr ARM_H.PageDirectoryObject) = Some ko" by (simp add: ko_def makeObjectKO_def) note blah[simp del] =  atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff
          Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex have relrl':
    "from_bytes (replicate (size_of TYPE(pde_C)) 0)
          = pde_C.words_C_update (\<lambda>_. Arrays.update (pde_C.words_C undefined) 0 0) undefined" apply (simp add: from_bytes_def) apply (simp add: typ_info_simps pde_C_tag_def pde_lift_def pde_get_tag_def
      size_td_lt_final_pad size_td_lt_ti_typ_pad_combine Let_def size_of_def) apply (simp add: final_pad_def Let_def size_td_lt_ti_typ_pad_combine Let_def
      size_of_def padup_def align_td_array' size_td_array update_ti_adjust_ti
      ti_typ_pad_combine_def Let_def ti_typ_combine_def empty_typ_info_def) apply (simp add: typ_info_array array_tag_def eval_nat_numeral) apply (simp add: array_tag_n.simps) apply (simp add: final_pad_def Let_def size_td_lt_ti_typ_pad_combine Let_def
      size_of_def padup_def align_td_array' size_td_array update_ti_adjust_ti
      ti_typ_pad_combine_def Let_def ti_typ_combine_def empty_typ_info_def) apply (simp add: update_ti_t_word32_0s pde_tag_defs) done have relrl:
    "cpde_relation makeObject (from_bytes (replicate (size_of TYPE(pde_C)) 0))" unfolding cpde_relation_def apply (simp only: relrl') apply (simp add: Let_def makeObject_pde pde_lift_def) apply (simp add: pde_lift_def pde_get_tag_def pde_pde_invalid_def) done have stored_asid: "pde_stored_asid (from_bytes (replicate (size_of TYPE(pde_C)) 0))
                            = None" apply (simp only: relrl') apply (simp add: pde_stored_asid_def pde_lift_def pde_pde_invalid_lift_def Let_def
                     pde_get_tag_def pde_pde_invalid_def) done 

  (* /obj specific *)

  (* s/obj/obj'/ *)
   have szo: "size_of TYPE(pde_C[4096]) = 2 ^ pdBits" by (simp add: size_of_def size_td_array pdBits_def pageBits_def pdeBits_def) have szo2: "4096 * size_of TYPE(pde_C) = 2 ^ pdBits" by (simp add: szo[symmetric]) have szo': "size_of TYPE(pde_C) = 2 ^ objBitsKO ko" by (simp add: objBits_simps ko_def archObjSize_def pdBits_def pageBits_def pdeBits_def) note rl' = cslift_ptr_retyp_other_inst[where n=1,
    simplified, OF empty cover[simplified] szo[symmetric] szo] have sz_weaken: "objBitsKO ko \<le> pdBits" by (simp add: objBits_simps ko_def archObjSize_def pdBits_def pageBits_def) have cover': "range_cover ptr sz (objBitsKO ko) 4096" apply (rule range_cover_rel[OF cover sz_weaken]) apply (simp add: pdBits_def objBits_simps ko_def archObjSize_def pageBits_def) done from sz sz_weaken have sz': "objBitsKO ko \<le> sz" by simp note al' = is_aligned_weaken[OF al sz_weaken] have koT: "koTypeOf ko = ArchT PDET" by (simp add: ko_def) 

  (* rest used to be generic, but PD arrays are complicating everything *)

   note rl = projectKO_opt_retyp_other [OF cover' pal pno ko_def] note cterl = retype_ctes_helper [OF pal pdst pno al' sz' szb mko cover'] have guard: "c_guard ?ptr" apply (rule is_aligned_c_guard[where n=pdBits and m=2]) apply (simp_all add: al ptr0 align_of_def align_td_array) apply (simp_all add: pdBits_def pageBits_def pdeBits_def) done have guard': "\<forall>n < 4096. c_guard (pde_Ptr ptr +\<^sub>p int n)" apply (rule retype_guard_helper [OF cover' ptr0 szo', where m=2]) apply (simp_all add: objBits_simps ko_def archObjSize_def align_of_def pdeBits_def) done note rl' = cslift_ptr_retyp_other_inst[OF _ cover refl szo,
    simplified szo, simplified, OF empty] from rf have pderl: "cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) Ptr cpde_relation" unfolding rf_sr_def cstate_relation_def by (simp add: Let_def cpspace_relation_def) note ht_rl = clift_eq_h_t_valid_eq[OF rl', OF tag_disj_via_td_name, simplified] have pde_arr: "cpspace_pde_array_relation (ksPSpace \<sigma>) (t_hrs_' (globals x))
    \<Longrightarrow> cpspace_pde_array_relation ?ks ?ks'" apply (erule cmap_relation_array_add_array[OF _ al]) apply (simp add: foldr_upd_app_if[folded data_map_insert_def]) apply (rule projectKO_opt_retyp_same, simp add: ko_def projectKOs) apply (simp add: h_t_valid_clift_Some_iff dom_def split: if_split) apply (subst clift_ptr_retyps_gen_prev_memset_same[where n=1, simplified, OF guard],
         simp_all only: szo empty, simp_all add: zero)[1] apply (simp add: pdBits_def pageBits_def word_bits_def pdeBits_def) apply (auto split: if_split)[1] apply (simp_all add: objBits_simps archObjSize_def pdBits_def
                           pageBits_def ko_def word_bits_def pdeBits_def) done from rf have cpsp: "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 pde_arr supply image_cong_simp [cong del] apply (clarsimp simp: rl' cterl cte_C_size tag_disj_via_td_name
                          foldr_upd_app_if [folded data_map_insert_def]) apply (simp add: ht_rl) apply (simp add: ptr_retyp_to_array[simplified]) apply (subst clift_ptr_retyps_gen_prev_memset_same[OF guard'], simp_all only: szo2 empty) apply simp apply (simp(no_asm) add: pdBits_def pageBits_def word_bits_def pdeBits_def) apply (simp add: zero) apply (simp add: rl projectKOs) apply (simp add: rl projectKO_opt_retyp_same ko_def projectKOs Let_def
                     ptr_add_to_new_cap_addrs [OF szo']
               cong: if_cong) apply (erule cmap_relation_retype) apply (insert relrl, auto) done moreover from rf szb al have "ptr_span (pd_Ptr (symbol_table ''armKSGlobalPD'')) \<inter> {ptr ..+ 2 ^ pdBits} = {}" apply (clarsimp simp: valid_global_refs'_def  Let_def
                          valid_refs'_def ran_def rf_sr_def cstate_relation_def) apply (erule disjoint_subset) apply (simp add:kernel_data_refs_disj) done moreover from rf have stored_asids: "(pde_stored_asid \<circ>\<^sub>m clift ?ks')
                         = (pde_stored_asid \<circ>\<^sub>m cslift x)" unfolding rf_sr_def using cpsp empty supply image_cong_simp [cong del] apply (clarsimp simp: rl' cterl cte_C_size tag_disj_via_td_name foldr_upd_app_if [folded data_map_insert_def]) apply (simp add: ptr_retyp_to_array[simplified]) apply (subst clift_ptr_retyps_gen_prev_memset_same[OF guard'], simp_all only: szo2 empty) apply simp apply (simp add: pdBits_def word_bits_def pageBits_def pdeBits_def) apply (simp add: zero) apply (rule ext) apply (simp add: map_comp_def stored_asid[simplified] split: option.split if_split) apply (simp only: o_def CTypesDefs.ptr_add_def' Abs_fnat_hom_mult) apply (clarsimp simp only:) apply (drule h_t_valid_intvl_htd_contains_uinfo_t [OF h_t_valid_clift]) apply (rule intvl_self, simp) apply clarsimp apply (subst (asm) empty[unfolded region_is_bytes'_def]) apply (simp add: objBits_simps archObjSize_def ko_def pdBits_def pageBits_def
                       offs_in_intvl_iff unat_word_ariths unat_of_nat pdeBits_def) apply clarsimp apply clarsimp done ultimately show ?thesis using rf empty kernel_data_refs_disj 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 (clarsimp simp add: rl' cte_C_size cterl tag_disj_via_td_name
                              hrs_htd_update ht_rl foldr_upd_app_if [folded data_map_insert_def]
                              projectKOs rl cvariable_array_ptr_retyps[OF szo]
                              zero_ranges_ptr_retyps[where p="pd_Ptr ptr", simplified szo]) apply (subst h_t_valid_ptr_retyps_gen_disjoint) apply assumption apply (simp add:szo cte_C_size cte_level_bits_def) apply (erule disjoint_subset) apply (simp add: ko_def projectKOs objBits_simps archObjSize_def
                      pdeBits_def
                      pdBits_def pageBits_def del: replicate_numeral) apply (subst h_t_valid_ptr_retyps_gen_disjoint) apply assumption apply (simp add:szo cte_C_size cte_level_bits_def) apply (erule disjoint_subset) apply (simp add: ko_def projectKOs objBits_simps archObjSize_def
                      pdeBits_def
                      pdBits_def pageBits_def del: replicate_numeral) apply (simp add:szo ptr_retyps_htd_safe_neg hrs_htd_def
      kernel_data_refs_domain_eq_rotate pdeBits_def
      ko_def projectKOs objBits_simps archObjSize_def Int_ac
      pdBits_def pageBits_def
      del: replicate_numeral) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+2 ^ pdBits}) \<sigma> \<and> (region_is_bytes ptr (2 ^ pdBits) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ pdBits) ptr = replicate (2 ^ pdBits) 0) \<and> range_cover ptr sz pdBits 1 \<and> valid_global_refs' s \<and> kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {} \<longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (state)
goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+2 ^ pdBits}) \<sigma> \<and> (region_is_bytes ptr (2 ^ pdBits) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ pdBits) ptr = replicate (2 ^ pdBits) 0) \<and> range_cover ptr sz pdBits 1 \<and> valid_global_refs' s \<and> kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (state)
goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+2 ^ pdBits}) \<sigma> \<and> (region_is_bytes ptr (2 ^ pdBits) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ pdBits) ptr = replicate (2 ^ pdBits) 0) \<and> range_cover ptr sz pdBits 1 \<and> valid_global_refs' s \<and> kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (state)
goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+2 ^ pdBits}) \<sigma> \<and> (region_is_bytes ptr (2 ^ pdBits) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ pdBits) ptr = replicate (2 ^ pdBits) 0) \<and> range_cover ptr sz pdBits 1 \<and> valid_global_refs' s \<and> kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (state)
goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+2 ^ pdBits}) \<sigma> \<and> (region_is_bytes ptr (2 ^ pdBits) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ pdBits) ptr = replicate (2 ^ pdBits) 0) \<and> range_cover ptr sz pdBits 1 \<and> valid_global_refs' s \<and> kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (state)
goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+2 ^ pdBits}) \<sigma> \<and> (region_is_bytes ptr (2 ^ pdBits) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ pdBits) ptr = replicate (2 ^ pdBits) 0) \<and> range_cover ptr sz pdBits 1 \<and> valid_global_refs' s \<and> kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (state)
goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+2 ^ pdBits}) \<sigma> \<and> (region_is_bytes ptr (2 ^ pdBits) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ pdBits) ptr = replicate (2 ^ pdBits) 0) \<and> range_cover ptr sz pdBits 1 \<and> valid_global_refs' s \<and> kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (state)
this:
(\<sigma>, x) \<in> rf_sr \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+2 ^ pdBits}) \<sigma> \<and> (region_is_bytes ptr (2 ^ pdBits) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ pdBits) ptr = replicate (2 ^ pdBits) 0) \<and> range_cover ptr sz pdBits 1 \<and> valid_global_refs' s \<and> kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {}

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+2 ^ pdBits}) \<sigma> \<and> (region_is_bytes ptr (2 ^ pdBits) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ pdBits) ptr = replicate (2 ^ pdBits) 0) \<and> range_cover ptr sz pdBits 1 \<and> valid_global_refs' s \<and> kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
using this:
(\<sigma>, x) \<in> rf_sr \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+2 ^ pdBits}) \<sigma> \<and> (region_is_bytes ptr (2 ^ pdBits) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ pdBits) ptr = replicate (2 ^ pdBits) 0) \<and> range_cover ptr sz pdBits 1 \<and> valid_global_refs' s \<and> kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {}

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

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+2 ^ pdBits}) \<sigma> \<and> (region_is_bytes ptr (2 ^ pdBits) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ pdBits) ptr = replicate (2 ^ pdBits) 0) \<and> range_cover ptr sz pdBits 1 \<and> valid_global_refs' s \<and> kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (state)
this:
(\<sigma>, x) \<in> rf_sr
is_aligned ptr pdBits
ptr \<noteq> 0
range_cover ptr sz pdBits 1
pdBits \<le> sz
sz < word_bits
pspace_aligned' \<sigma>
pspace_distinct' \<sigma>
pspace_no_overlap' ptr sz \<sigma>
(valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+2 ^ pdBits}) \<sigma>
region_is_bytes ptr (2 ^ pdBits) x
heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ pdBits) ptr = replicate (2 ^ pdBits) 0
kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {}

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+2 ^ pdBits}) \<sigma> \<and> (region_is_bytes ptr (2 ^ pdBits) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ pdBits) ptr = replicate (2 ^ pdBits) 0) \<and> range_cover ptr sz pdBits 1 \<and> valid_global_refs' s \<and> kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>dev. makeObjectKO dev (Inr object_type.PageDirectoryObject) = Some ko proof (state)
this:
makeObjectKO ?dev2 (Inr object_type.PageDirectoryObject) = Some ko

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+2 ^ pdBits}) \<sigma> \<and> (region_is_bytes ptr (2 ^ pdBits) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ pdBits) ptr = replicate (2 ^ pdBits) 0) \<and> range_cover ptr sz pdBits 1 \<and> valid_global_refs' s \<and> kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (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> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+2 ^ pdBits}) \<sigma> \<and> (region_is_bytes ptr (2 ^ pdBits) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ pdBits) ptr = replicate (2 ^ pdBits) 0) \<and> range_cover ptr sz pdBits 1 \<and> valid_global_refs' s \<and> kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. from_bytes (replicate (size_of TYPE(pde_C)) 0) = pde_C.words_C_update (\<lambda>_. Arrays.update (pde_C.words_C undefined) 0 0) undefined proof (prove)
goal (1 subgoal):
 1. update_ti_t (typ_info_t TYPE(pde_C)) [0, 0, 0, 0] undefined = pde_C.words_C_update (\<lambda>_. Arrays.update (pde_C.words_C undefined) 0 0) undefined proof (prove)
goal (1 subgoal):
 1. update_ti_t (final_pad (ti_typ_pad_combine TYPE(32 word[1]) pde_C.words_C (pde_C.words_C_update \<circ> (\<lambda>x _. x)) ''words_C'' (empty_typ_info ''pde_C''))) [0, 0, 0, 0] undefined = pde_C.words_C_update (\<lambda>_. Arrays.update (pde_C.words_C undefined) 0 0) undefined proof (prove)
goal (1 subgoal):
 1. pde_C.words_C_update (\<lambda>_. update_ti_t (typ_info_t TYPE(32 word[1])) [0, 0, 0, 0] (pde_C.words_C undefined)) undefined = pde_C.words_C_update (\<lambda>_. Arrays.update (pde_C.words_C undefined) 0 0) undefined proof (prove)
goal (1 subgoal):
 1. pde_C.words_C_update (\<lambda>_. update_ti_t (array_tag_n (Suc 0)) [0, 0, 0, 0] (pde_C.words_C undefined)) undefined = pde_C.words_C_update (\<lambda>_. Arrays.update (pde_C.words_C undefined) 0 0) undefined proof (prove)
goal (1 subgoal):
 1. pde_C.words_C_update (\<lambda>_. update_ti_t (ti_typ_combine TYPE(32 word) (\<lambda>x. x.[0]) (\<lambda>x f. Arrays.update f 0 x) [] (empty_typ_info (CHR ''w'' # CHR ''o'' # CHR ''r'' # CHR ''d'' # CHR ''0'' # CHR ''0'' # CHR ''0'' # CHR ''0'' # CHR ''0'' # CHR ''1'' # CHR ''0'' # CHR ''_'' # CHR ''a'' # CHR ''r'' # CHR ''r'' # CHR ''a'' # CHR ''y'' # CHR ''_'' # nat_to_bin_string (Suc 0)))) [0, 0, 0, 0] (pde_C.words_C undefined)) undefined = pde_C.words_C_update (\<lambda>_. Arrays.update (pde_C.words_C undefined) 0 0) undefined proof (prove)
goal (1 subgoal):
 1. pde_C.words_C_update (\<lambda>_. Arrays.update (pde_C.words_C undefined) 0 (update_ti_t (typ_info_t TYPE(32 word)) [0, 0, 0, 0] (pde_C.words_C undefined.[0]))) undefined = pde_C.words_C_update (\<lambda>_. Arrays.update (pde_C.words_C undefined) 0 0) undefined proof (prove)
goal:
No subgoals! proof (state)
this:
from_bytes (replicate (size_of TYPE(pde_C)) 0) = pde_C.words_C_update (\<lambda>_. Arrays.update (pde_C.words_C undefined) 0 0) undefined

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+2 ^ pdBits}) \<sigma> \<and> (region_is_bytes ptr (2 ^ pdBits) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ pdBits) ptr = replicate (2 ^ pdBits) 0) \<and> range_cover ptr sz pdBits 1 \<and> valid_global_refs' s \<and> kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. cpde_relation makeObject (from_bytes (replicate (size_of TYPE(pde_C)) 0)) proof (prove)
goal (1 subgoal):
 1. let cpde' = pde_lift (from_bytes (replicate (size_of TYPE(pde_C)) 0)) in case makeObject of ARM_H.InvalidPDE \<Rightarrow> \<exists>inv. cpde' = Some (Pde_pde_invalid inv) | ARM_H.PageTablePDE frame parity domain \<Rightarrow> cpde' = Some (Pde_pde_coarse \<lparr>pde_pde_coarse_CL.address_CL = frame, P_CL = of_bool parity, Domain_CL = domain\<rparr>) | ARM_H.SectionPDE frame parity domain cacheable global xn rights \<Rightarrow> cpde' = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = frame, size_CL = 0, nG_CL = of_bool (\<not> global), S_CL = s_from_cacheable cacheable, APX_CL = 0, TEX_CL = tex_from_cacheable cacheable, AP_CL = ap_from_vm_rights rights, P_CL = of_bool parity, Domain_CL = domain, XN_CL = of_bool xn, C_CL = 0, B_CL = b_from_cacheable cacheable\<rparr>) | ARM_H.SuperSectionPDE frame parity cacheable global xn rights \<Rightarrow> cpde' = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = frame, size_CL = 1, nG_CL = of_bool (\<not> global), S_CL = s_from_cacheable cacheable, APX_CL = 0, TEX_CL = tex_from_cacheable cacheable, AP_CL = ap_from_vm_rights rights, P_CL = of_bool parity, Domain_CL = 0, XN_CL = of_bool xn, C_CL = 0, B_CL = b_from_cacheable cacheable\<rparr>) proof (prove)
goal (1 subgoal):
 1. let cpde' = pde_lift (pde_C.words_C_update (\<lambda>_. Arrays.update (pde_C.words_C undefined) 0 0) undefined) in case makeObject of ARM_H.InvalidPDE \<Rightarrow> \<exists>inv. cpde' = Some (Pde_pde_invalid inv) | ARM_H.PageTablePDE frame parity domain \<Rightarrow> cpde' = Some (Pde_pde_coarse \<lparr>pde_pde_coarse_CL.address_CL = frame, P_CL = of_bool parity, Domain_CL = domain\<rparr>) | ARM_H.SectionPDE frame parity domain cacheable global xn rights \<Rightarrow> cpde' = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = frame, size_CL = 0, nG_CL = of_bool (\<not> global), S_CL = s_from_cacheable cacheable, APX_CL = 0, TEX_CL = tex_from_cacheable cacheable, AP_CL = ap_from_vm_rights rights, P_CL = of_bool parity, Domain_CL = domain, XN_CL = of_bool xn, C_CL = 0, B_CL = b_from_cacheable cacheable\<rparr>) | ARM_H.SuperSectionPDE frame parity cacheable global xn rights \<Rightarrow> cpde' = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = frame, size_CL = 1, nG_CL = of_bool (\<not> global), S_CL = s_from_cacheable cacheable, APX_CL = 0, TEX_CL = tex_from_cacheable cacheable, AP_CL = ap_from_vm_rights rights, P_CL = of_bool parity, Domain_CL = 0, XN_CL = of_bool xn, C_CL = 0, B_CL = b_from_cacheable cacheable\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<exists>inv. (if pde_get_tag (pde_C.words_C_update (\<lambda>_. Arrays.update (pde_C.words_C undefined) 0 0) undefined) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid then Some (Pde_pde_invalid \<lparr>stored_hw_asid_CL = (pde_C.words_C (pde_C.words_C_update (\<lambda>_. Arrays.update (pde_C.words_C undefined) 0 0) undefined).[0] >> 24) && mask 8, stored_asid_valid_CL = (pde_C.words_C (pde_C.words_C_update (\<lambda>_. Arrays.update (pde_C.words_C undefined) 0 0) undefined).[0] >> 23) && mask 1\<rparr>) else if pde_get_tag (pde_C.words_C_update (\<lambda>_. Arrays.update (pde_C.words_C undefined) 0 0) undefined) = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse then Some (Pde_pde_coarse \<lparr>pde_pde_coarse_CL.address_CL = (pde_C.words_C (pde_C.words_C_update (\<lambda>_. Arrays.update (pde_C.words_C undefined) 0 0) undefined).[0] << 0) && ~~ mask 10, P_CL = (pde_C.words_C (pde_C.words_C_update (\<lambda>_. Arrays.update (pde_C.words_C undefined) 0 0) undefined).[0] >> 9) && mask 1, Domain_CL = (pde_C.words_C (pde_C.words_C_update (\<lambda>_. Arrays.update (pde_C.words_C undefined) 0 0) undefined).[0] >> 5) && mask 4\<rparr>) else if pde_get_tag (pde_C.words_C_update (\<lambda>_. Arrays.update (pde_C.words_C undefined) 0 0) undefined) = SCAST(32 signed \<rightarrow> 32) pde_pde_section then Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = (pde_C.words_C (pde_C.words_C_update (\<lambda>_. Arrays.update (pde_C.words_C undefined) 0 0) undefined).[0] << 0) && ~~ mask 20, size_CL = (pde_C.words_C (pde_C.words_C_update (\<lambda>_. Arrays.update (pde_C.words_C undefined) 0 0) undefined).[0] >> 18) && mask 1, nG_CL = (pde_C.words_C (pde_C.words_C_update (\<lambda>_. Arrays.update (pde_C.words_C undefined) 0 0) undefined).[0] >> 17) && mask 1, S_CL = (pde_C.words_C (pde_C.words_C_update (\<lambda>_. Arrays.update (pde_C.words_C undefined) 0 0) undefined).[0] >> 16) && mask 1, APX_CL = (pde_C.words_C (pde_C.words_C_update (\<lambda>_. Arrays.update (pde_C.words_C undefined) 0 0) undefined).[0] >> 15) && mask 1, TEX_CL = (pde_C.words_C (pde_C.words_C_update (\<lambda>_. Arrays.update (pde_C.words_C undefined) 0 0) undefined).[0] >> 12) && mask 3, AP_CL = (pde_C.words_C (pde_C.words_C_update (\<lambda>_. Arrays.update (pde_C.words_C undefined) 0 0) undefined).[0] >> 10) && mask 2, P_CL = (pde_C.words_C (pde_C.words_C_update (\<lambda>_. Arrays.update (pde_C.words_C undefined) 0 0) undefined).[0] >> 9) && mask 1, Domain_CL = (pde_C.words_C (pde_C.words_C_update (\<lambda>_. Arrays.update (pde_C.words_C undefined) 0 0) undefined).[0] >> 5) && mask 4, XN_CL = (pde_C.words_C (pde_C.words_C_update (\<lambda>_. Arrays.update (pde_C.words_C undefined) 0 0) undefined).[0] >> 4) && mask 1, C_CL = (pde_C.words_C (pde_C.words_C_update (\<lambda>_. Arrays.update (pde_C.words_C undefined) 0 0) undefined).[0] >> 3) && mask 1, B_CL = (pde_C.words_C (pde_C.words_C_update (\<lambda>_. Arrays.update (pde_C.words_C undefined) 0 0) undefined).[0] >> 2) && mask 1\<rparr>) else if pde_get_tag (pde_C.words_C_update (\<lambda>_. Arrays.update (pde_C.words_C undefined) 0 0) undefined) = SCAST(32 signed \<rightarrow> 32) pde_pde_reserved then Some Pde_pde_reserved else None) = Some (Pde_pde_invalid inv) proof (prove)
goal:
No subgoals! proof (state)
this:
cpde_relation makeObject (from_bytes (replicate (size_of TYPE(pde_C)) 0))

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+2 ^ pdBits}) \<sigma> \<and> (region_is_bytes ptr (2 ^ pdBits) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ pdBits) ptr = replicate (2 ^ pdBits) 0) \<and> range_cover ptr sz pdBits 1 \<and> valid_global_refs' s \<and> kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. pde_stored_asid (from_bytes (replicate (size_of TYPE(pde_C)) 0)) = None proof (prove)
goal (1 subgoal):
 1. pde_stored_asid (pde_C.words_C_update (\<lambda>_. Arrays.update (pde_C.words_C undefined) 0 0) undefined) = None proof (prove)
goal:
No subgoals! proof (state)
this:
pde_stored_asid (from_bytes (replicate (size_of TYPE(pde_C)) 0)) = None

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+2 ^ pdBits}) \<sigma> \<and> (region_is_bytes ptr (2 ^ pdBits) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ pdBits) ptr = replicate (2 ^ pdBits) 0) \<and> range_cover ptr sz pdBits 1 \<and> valid_global_refs' s \<and> kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (state)
this:
pde_stored_asid (from_bytes (replicate (size_of TYPE(pde_C)) 0)) = None

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+2 ^ pdBits}) \<sigma> \<and> (region_is_bytes ptr (2 ^ pdBits) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ pdBits) ptr = replicate (2 ^ pdBits) 0) \<and> range_cover ptr sz pdBits 1 \<and> valid_global_refs' s \<and> kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. size_of TYPE(pde_C[4096]) = 2 ^ pdBits proof (state)
this:
size_of TYPE(pde_C[4096]) = 2 ^ pdBits

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+2 ^ pdBits}) \<sigma> \<and> (region_is_bytes ptr (2 ^ pdBits) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ pdBits) ptr = replicate (2 ^ pdBits) 0) \<and> range_cover ptr sz pdBits 1 \<and> valid_global_refs' s \<and> kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. 4096 * size_of TYPE(pde_C) = 2 ^ pdBits proof (state)
this:
4096 * size_of TYPE(pde_C) = 2 ^ pdBits

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+2 ^ pdBits}) \<sigma> \<and> (region_is_bytes ptr (2 ^ pdBits) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ pdBits) ptr = replicate (2 ^ pdBits) 0) \<and> range_cover ptr sz pdBits 1 \<and> valid_global_refs' s \<and> kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. size_of TYPE(pde_C) = 2 ^ objBitsKO ko proof (state)
this:
size_of TYPE(pde_C) = 2 ^ objBitsKO ko

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+2 ^ pdBits}) \<sigma> \<and> (region_is_bytes ptr (2 ^ pdBits) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ pdBits) ptr = replicate (2 ^ pdBits) 0) \<and> range_cover ptr sz pdBits 1 \<and> valid_global_refs' s \<and> kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (state)
this:
\<lbrakk>typ_uinfo_t TYPE(pde_C[4096]) \<bottom>\<^sub>t typ_uinfo_t TYPE(?'b); typ_uinfo_t TYPE(?'b) \<noteq> typ_uinfo_t TYPE(8 word)\<rbrakk> \<Longrightarrow> clift (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) ?arr) (t_hrs_' (globals x))) = cslift x

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+2 ^ pdBits}) \<sigma> \<and> (region_is_bytes ptr (2 ^ pdBits) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ pdBits) ptr = replicate (2 ^ pdBits) 0) \<and> range_cover ptr sz pdBits 1 \<and> valid_global_refs' s \<and> kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. objBitsKO ko \<le> pdBits proof (state)
this:
objBitsKO ko \<le> pdBits

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+2 ^ pdBits}) \<sigma> \<and> (region_is_bytes ptr (2 ^ pdBits) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ pdBits) ptr = replicate (2 ^ pdBits) 0) \<and> range_cover ptr sz pdBits 1 \<and> valid_global_refs' s \<and> kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. range_cover ptr sz (objBitsKO ko) 4096 proof (prove)
goal (1 subgoal):
 1. 4096 = 2 ^ (pdBits - objBitsKO ko) * 1 proof (prove)
goal:
No subgoals! proof (state)
this:
range_cover ptr sz (objBitsKO ko) 4096

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+2 ^ pdBits}) \<sigma> \<and> (region_is_bytes ptr (2 ^ pdBits) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ pdBits) ptr = replicate (2 ^ pdBits) 0) \<and> range_cover ptr sz pdBits 1 \<and> valid_global_refs' s \<and> kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (chain)
picking this:
pdBits \<le> sz
objBitsKO ko \<le> pdBits proof (prove)
using this:
pdBits \<le> sz
objBitsKO ko \<le> pdBits

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

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+2 ^ pdBits}) \<sigma> \<and> (region_is_bytes ptr (2 ^ pdBits) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ pdBits) ptr = replicate (2 ^ pdBits) 0) \<and> range_cover ptr sz pdBits 1 \<and> valid_global_refs' s \<and> kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (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> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+2 ^ pdBits}) \<sigma> \<and> (region_is_bytes ptr (2 ^ pdBits) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ pdBits) ptr = replicate (2 ^ pdBits) 0) \<and> range_cover ptr sz pdBits 1 \<and> valid_global_refs' s \<and> kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. koTypeOf ko = ArchT PDET proof (state)
this:
koTypeOf ko = ArchT PDET

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+2 ^ pdBits}) \<sigma> \<and> (region_is_bytes ptr (2 ^ pdBits) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ pdBits) ptr = replicate (2 ^ pdBits) 0) \<and> range_cover ptr sz pdBits 1 \<and> valid_global_refs' s \<and> kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (state)
this:
koTypeOf ko = ArchT PDET

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+2 ^ pdBits}) \<sigma> \<and> (region_is_bytes ptr (2 ^ pdBits) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ pdBits) ptr = replicate (2 ^ pdBits) 0) \<and> range_cover ptr sz pdBits 1 \<and> valid_global_refs' s \<and> kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (state)
this:
\<forall>v. projectKO_opt (KOArch (KOPDE makeObject)) \<noteq> Some v \<Longrightarrow> projectKO_opt \<circ>\<^sub>m (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko else ksPSpace \<sigma> x) = projectKO_opt \<circ>\<^sub>m ksPSpace \<sigma>

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+2 ^ pdBits}) \<sigma> \<and> (region_is_bytes ptr (2 ^ pdBits) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ pdBits) ptr = replicate (2 ^ pdBits) 0) \<and> range_cover ptr sz pdBits 1 \<and> valid_global_refs' s \<and> kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (state)
this:
map_to_ctes (\<lambda>xa. if xa \<in> set (new_cap_addrs 4096 ptr ko) then Some ko else ksPSpace \<sigma> xa) = (\<lambda>x. if Inr object_type.PageDirectoryObject = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> x \<in> set (new_cap_addrs 4096 ptr ko) \<or> Inr object_type.PageDirectoryObject = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> x && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs 4096 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> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+2 ^ pdBits}) \<sigma> \<and> (region_is_bytes ptr (2 ^ pdBits) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ pdBits) ptr = replicate (2 ^ pdBits) 0) \<and> range_cover ptr sz pdBits 1 \<and> valid_global_refs' s \<and> kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. c_guard (pd_Ptr ptr) proof (prove)
goal (5 subgoals):
 1. is_aligned (ptr_val (pd_Ptr ptr)) pdBits
 2. ptr_val (pd_Ptr ptr) \<noteq> 0
 3. align_of TYPE(pde_C[4096]) = 2\<^sup>2
 4. size_of TYPE(pde_C[4096]) \<le> 2 ^ pdBits
 5. 2 \<le> pdBits proof (prove)
goal (2 subgoals):
 1. 16384 \<le> 2 ^ pdBits
 2. 2 \<le> pdBits proof (prove)
goal:
No subgoals! proof (state)
this:
c_guard (pd_Ptr ptr)

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

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+2 ^ pdBits}) \<sigma> \<and> (region_is_bytes ptr (2 ^ pdBits) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ pdBits) ptr = replicate (2 ^ pdBits) 0) \<and> range_cover ptr sz pdBits 1 \<and> valid_global_refs' s \<and> kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (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(pde_C[4096]); typ_uinfo_t TYPE(?'b) \<noteq> typ_uinfo_t TYPE(8 word)\<rbrakk> \<Longrightarrow> clift (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) ?arr) (t_hrs_' (globals x))) = cslift x

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+2 ^ pdBits}) \<sigma> \<and> (region_is_bytes ptr (2 ^ pdBits) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ pdBits) ptr = replicate (2 ^ pdBits) 0) \<and> range_cover ptr sz pdBits 1 \<and> valid_global_refs' s \<and> kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (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. cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation 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. cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation proof (state)
this:
cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+2 ^ pdBits}) \<sigma> \<and> (region_is_bytes ptr (2 ^ pdBits) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ pdBits) ptr = replicate (2 ^ pdBits) 0) \<and> range_cover ptr sz pdBits 1 \<and> valid_global_refs' s \<and> kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (state)
this:
\<lbrakk>typ_name (typ_info_t TYPE(?'b1)) \<noteq> ''!pad_typ''; typ_name (typ_info_t TYPE(?'b1)) \<noteq> ''pde_C'' \<and> typ_name (typ_info_t TYPE(?'b1)) \<noteq> ''word0000010'' \<and> typ_name (typ_info_t TYPE(?'b1)) \<noteq> ''word0000010_array_10'' \<and> typ_name (typ_info_t TYPE(?'b1)) \<noteq> CHR ''p'' # CHR ''d'' # CHR ''e'' # CHR ''_'' # CHR ''C'' # CHR ''_'' # CHR ''a'' # CHR ''r'' # CHR ''r'' # CHR ''a'' # CHR ''y'' # CHR ''_'' # nat_to_bin_string 4096; CHR ''p'' # CHR ''d'' # CHR ''e'' # CHR ''_'' # CHR ''C'' # CHR ''_'' # CHR ''a'' # CHR ''r'' # CHR ''r'' # CHR ''a'' # CHR ''y'' # CHR ''_'' # nat_to_bin_string 4096 \<notin> td_names (typ_info_t TYPE(?'b1)); typ_uinfo_t TYPE(?'b1) \<noteq> typ_uinfo_t TYPE(8 word)\<rbrakk> \<Longrightarrow> h_t_valid (hrs_htd (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr 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> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+2 ^ pdBits}) \<sigma> \<and> (region_is_bytes ptr (2 ^ pdBits) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ pdBits) ptr = replicate (2 ^ pdBits) 0) \<and> range_cover ptr sz pdBits 1 \<and> valid_global_refs' s \<and> kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr \<Longrightarrow> cpspace_pde_array_relation (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>)) (hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x))) proof (prove)
goal (6 subgoals):
 1. map_to_pdes (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>)) = (\<lambda>x. if x \<in> set (new_cap_addrs ?sz ptr ?ko) then Some ?v else map_to_pdes (ksPSpace \<sigma>) x)
 2. \<forall>xa. x \<Turnstile>\<^sub>c xa \<longrightarrow> is_aligned (ptr_val xa) pdBits \<Longrightarrow> \<forall>y. hrs_htd (hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x))) \<Turnstile>\<^sub>t y = (y = pd_Ptr ptr \<or> x \<Turnstile>\<^sub>c y)
 3. ?sz = 2 ^ (pdBits - objBits ?v)
 4. objBitsKO ?ko = objBitsKO (injectKOS ?v)
 5. objBits ?v \<le> pdBits
 6. pdBits < word_bits proof (prove)
goal (6 subgoals):
 1. map_to_pdes (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko else ksPSpace \<sigma> x) = (\<lambda>x. if x \<in> set (new_cap_addrs ?sz ptr ?ko) then Some ?v else map_to_pdes (ksPSpace \<sigma>) x)
 2. \<forall>xa. x \<Turnstile>\<^sub>c xa \<longrightarrow> is_aligned (ptr_val xa) pdBits \<Longrightarrow> \<forall>y. hrs_htd (hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x))) \<Turnstile>\<^sub>t y = (y = pd_Ptr ptr \<or> x \<Turnstile>\<^sub>c y)
 3. ?sz = 2 ^ (pdBits - objBits ?v)
 4. objBitsKO ?ko = objBitsKO (injectKOS ?v)
 5. objBits ?v \<le> pdBits
 6. pdBits < word_bits proof (prove)
goal (5 subgoals):
 1. \<forall>xa. x \<Turnstile>\<^sub>c xa \<longrightarrow> is_aligned (ptr_val xa) pdBits \<Longrightarrow> \<forall>y. hrs_htd (hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x))) \<Turnstile>\<^sub>t y = (y = pd_Ptr ptr \<or> x \<Turnstile>\<^sub>c y)
 2. 4096 = 2 ^ (pdBits - objBits makeObject)
 3. objBitsKO ko = objBitsKO (injectKOS makeObject)
 4. objBits makeObject \<le> pdBits
 5. pdBits < word_bits proof (prove)
goal (5 subgoals):
 1. \<forall>xa. (\<exists>v. cslift x xa = Some v) \<longrightarrow> is_aligned (ptr_val xa) pdBits \<Longrightarrow> \<forall>y. (\<exists>v. clift (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x))) y = Some v) = (y = pd_Ptr ptr \<or> (\<exists>v. cslift x y = Some v))
 2. 4096 = 2 ^ (pdBits - objBits makeObject)
 3. objBitsKO ko = objBitsKO (injectKOS makeObject)
 4. objBits makeObject \<le> pdBits
 5. pdBits < word_bits proof (prove)
goal (6 subgoals):
 1. \<forall>xa. (\<exists>v. cslift x xa = Some v) \<longrightarrow> is_aligned (ptr_val xa) pdBits \<Longrightarrow> pdBits < word_bits
 2. \<forall>xa. (\<exists>v. cslift x xa = Some v) \<longrightarrow> is_aligned (ptr_val xa) pdBits \<Longrightarrow> \<forall>y. (\<exists>v. (if y = pd_Ptr ptr then Some (from_bytes (replicate (2 ^ pdBits) 0)) else cslift x y) = Some v) = (y = pd_Ptr ptr \<or> (\<exists>v. cslift x y = Some v))
 3. 4096 = 2 ^ (pdBits - objBits makeObject)
 4. objBitsKO ko = objBitsKO (injectKOS makeObject)
 5. objBits makeObject \<le> pdBits
 6. pdBits < word_bits proof (prove)
goal (5 subgoals):
 1. \<forall>xa. (\<exists>v. cslift x xa = Some v) \<longrightarrow> is_aligned (ptr_val xa) pdBits \<Longrightarrow> \<forall>y. (\<exists>v. (if y = pd_Ptr ptr then Some (from_bytes (replicate (2 ^ pdBits) 0)) else cslift x y) = Some v) = (y = pd_Ptr ptr \<or> (\<exists>v. cslift x y = Some v))
 2. 4096 = 2 ^ (pdBits - objBits makeObject)
 3. objBitsKO ko = objBitsKO (injectKOS makeObject)
 4. objBits makeObject \<le> pdBits
 5. pdBits < word_bits proof (prove)
goal (4 subgoals):
 1. 4096 = 2 ^ (pdBits - objBits makeObject)
 2. objBitsKO ko = objBitsKO (injectKOS makeObject)
 3. objBits makeObject \<le> pdBits
 4. pdBits < word_bits proof (prove)
goal:
No subgoals! proof (state)
this:
carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr \<Longrightarrow> cpspace_pde_array_relation (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>)) (hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x)))

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

goal (1 subgoal):
 1. cmap_relation (map_to_ctes (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x)))) cte_Ptr ccte_relation \<and> cpspace_tcb_relation (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>)) (hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x))) \<and> cmap_relation (map_to_eps (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x)))) ep_Ptr (cendpoint_relation (clift (hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x))))) \<and> cmap_relation (map_to_ntfns (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x)))) ntfn_Ptr (cnotification_relation (clift (hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x))))) \<and> cmap_relation (map_to_pdes (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x)))) pde_Ptr cpde_relation \<and> cmap_relation (map_to_ptes (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x)))) pte_Ptr cpte_relation \<and> cmap_relation (map_to_asidpools (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x)))) ap_Ptr casid_pool_relation \<and> cpspace_user_data_relation (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>)) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x))) \<and> cpspace_device_data_relation (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>)) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x))) \<and> cpspace_pde_array_relation (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>)) (hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x))) \<and> cpspace_pte_array_relation (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>)) (hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (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
carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr \<Longrightarrow> cpspace_pde_array_relation (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>)) (hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x)))

goal (1 subgoal):
 1. cmap_relation (map_to_ctes (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x)))) cte_Ptr ccte_relation \<and> cpspace_tcb_relation (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>)) (hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x))) \<and> cmap_relation (map_to_eps (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x)))) ep_Ptr (cendpoint_relation (clift (hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x))))) \<and> cmap_relation (map_to_ntfns (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x)))) ntfn_Ptr (cnotification_relation (clift (hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x))))) \<and> cmap_relation (map_to_pdes (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x)))) pde_Ptr cpde_relation \<and> cmap_relation (map_to_ptes (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x)))) pte_Ptr cpte_relation \<and> cmap_relation (map_to_asidpools (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x)))) ap_Ptr casid_pool_relation \<and> cpspace_user_data_relation (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>)) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x))) \<and> cpspace_device_data_relation (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>)) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x))) \<and> cpspace_pde_array_relation (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>)) (hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x))) \<and> cpspace_pte_array_relation (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>)) (hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cpspace_pde_array_relation (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko else ksPSpace \<sigma> x) (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x))); cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr\<rbrakk> \<Longrightarrow> cmap_relation (map_to_tcbs (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko 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 4096 ptr ko) then Some ko 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 4096 ptr ko) then Some ko 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 4096 ptr ko) then Some ko else ksPSpace \<sigma> x)) (clift (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x)))) pde_Ptr cpde_relation \<and> cmap_relation (map_to_ptes (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko 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 4096 ptr ko) then Some ko else ksPSpace \<sigma> x)) (cslift x) ap_Ptr casid_pool_relation \<and> cmap_relation (heap_to_user_data (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation \<and> cmap_relation (heap_to_device_data (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation \<and> cpspace_pte_array_relation (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko else ksPSpace \<sigma> x) (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cpspace_pde_array_relation (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko else ksPSpace \<sigma> x) (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x))); cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr\<rbrakk> \<Longrightarrow> cmap_relation (map_to_tcbs (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko 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 4096 ptr ko) then Some ko 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 4096 ptr ko) then Some ko 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 4096 ptr ko) then Some ko else ksPSpace \<sigma> x)) (clift (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x)))) pde_Ptr cpde_relation \<and> cmap_relation (map_to_ptes (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko 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 4096 ptr ko) then Some ko else ksPSpace \<sigma> x)) (cslift x) ap_Ptr casid_pool_relation \<and> cmap_relation (heap_to_user_data (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation \<and> cmap_relation (heap_to_device_data (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation \<and> carray_map_relation ptBits (map_to_ptes (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko else ksPSpace \<sigma> x)) (c_h_t_valid x) pt_Ptr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cpspace_pde_array_relation (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko else ksPSpace \<sigma> x) (hrs_htd_update (ptr_retyps_gen 4096 (pde_Ptr ptr) True) (t_hrs_' (globals x))); cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr\<rbrakk> \<Longrightarrow> cmap_relation (map_to_tcbs (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko 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 4096 ptr ko) then Some ko 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 4096 ptr ko) then Some ko 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 4096 ptr ko) then Some ko else ksPSpace \<sigma> x)) (clift (hrs_htd_update (ptr_retyps_gen 4096 (pde_Ptr ptr) True) (t_hrs_' (globals x)))) pde_Ptr cpde_relation \<and> cmap_relation (map_to_ptes (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko 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 4096 ptr ko) then Some ko else ksPSpace \<sigma> x)) (cslift x) ap_Ptr casid_pool_relation \<and> cmap_relation (heap_to_user_data (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation \<and> cmap_relation (heap_to_device_data (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation \<and> carray_map_relation ptBits (map_to_ptes (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko else ksPSpace \<sigma> x)) (c_h_t_valid x) pt_Ptr proof (prove)
goal (4 subgoals):
 1. \<lbrakk>cpspace_pde_array_relation (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko else ksPSpace \<sigma> x) (hrs_htd_update (ptr_retyps_gen 4096 (pde_Ptr ptr) True) (t_hrs_' (globals x))); 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(pde_C) \<noteq> typ_uinfo_t TYPE(8 word)
 2. \<lbrakk>cpspace_pde_array_relation (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko else ksPSpace \<sigma> x) (hrs_htd_update (ptr_retyps_gen 4096 (pde_Ptr ptr) True) (t_hrs_' (globals x))); 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> 2 ^ pdBits < 2 ^ word_bits
 3. \<lbrakk>cpspace_pde_array_relation (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko else ksPSpace \<sigma> x) (hrs_htd_update (ptr_retyps_gen 4096 (pde_Ptr ptr) True) (t_hrs_' (globals x))); 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))) (2 ^ pdBits) ptr = replicate (2 ^ pdBits) 0
 4. \<lbrakk>cpspace_pde_array_relation (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko else ksPSpace \<sigma> x) (hrs_htd_update (ptr_retyps_gen 4096 (pde_Ptr ptr) True) (t_hrs_' (globals x))); cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr\<rbrakk> \<Longrightarrow> cmap_relation (map_to_tcbs (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko 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 4096 ptr ko) then Some ko 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 4096 ptr ko) then Some ko 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 4096 ptr ko) then Some ko else ksPSpace \<sigma> x)) (\<lambda>y. if y \<in> ((+\<^sub>p) (pde_Ptr ptr) \<circ> int) ` {k. k < 4096} then Some (from_bytes (replicate (size_of TYPE(pde_C)) 0)) else cslift x y) pde_Ptr cpde_relation \<and> cmap_relation (map_to_ptes (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko 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 4096 ptr ko) then Some ko else ksPSpace \<sigma> x)) (cslift x) ap_Ptr casid_pool_relation \<and> cmap_relation (heap_to_user_data (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation \<and> cmap_relation (heap_to_device_data (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation \<and> carray_map_relation ptBits (map_to_ptes (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko else ksPSpace \<sigma> x)) (c_h_t_valid x) pt_Ptr proof (prove)
goal (3 subgoals):
 1. \<lbrakk>cpspace_pde_array_relation (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko else ksPSpace \<sigma> x) (hrs_htd_update (ptr_retyps_gen 4096 (pde_Ptr ptr) True) (t_hrs_' (globals x))); 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> 2 ^ pdBits < 2 ^ word_bits
 2. \<lbrakk>cpspace_pde_array_relation (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko else ksPSpace \<sigma> x) (hrs_htd_update (ptr_retyps_gen 4096 (pde_Ptr ptr) True) (t_hrs_' (globals x))); 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))) (2 ^ pdBits) ptr = replicate (2 ^ pdBits) 0
 3. \<lbrakk>cpspace_pde_array_relation (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko else ksPSpace \<sigma> x) (hrs_htd_update (ptr_retyps_gen 4096 (pde_Ptr ptr) True) (t_hrs_' (globals x))); cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr\<rbrakk> \<Longrightarrow> cmap_relation (map_to_tcbs (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko 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 4096 ptr ko) then Some ko 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 4096 ptr ko) then Some ko 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 4096 ptr ko) then Some ko else ksPSpace \<sigma> x)) (\<lambda>y. if y \<in> ((+\<^sub>p) (pde_Ptr ptr) \<circ> int) ` {k. k < 4096} then Some (from_bytes (replicate (size_of TYPE(pde_C)) 0)) else cslift x y) pde_Ptr cpde_relation \<and> cmap_relation (map_to_ptes (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko 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 4096 ptr ko) then Some ko else ksPSpace \<sigma> x)) (cslift x) ap_Ptr casid_pool_relation \<and> cmap_relation (heap_to_user_data (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation \<and> cmap_relation (heap_to_device_data (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation \<and> carray_map_relation ptBits (map_to_ptes (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko else ksPSpace \<sigma> x)) (c_h_t_valid x) pt_Ptr proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cpspace_pde_array_relation (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko else ksPSpace \<sigma> x) (hrs_htd_update (ptr_retyps_gen 4096 (pde_Ptr ptr) True) (t_hrs_' (globals x))); 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))) (2 ^ pdBits) ptr = replicate (2 ^ pdBits) 0
 2. \<lbrakk>cpspace_pde_array_relation (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko else ksPSpace \<sigma> x) (hrs_htd_update (ptr_retyps_gen 4096 (pde_Ptr ptr) True) (t_hrs_' (globals x))); cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr\<rbrakk> \<Longrightarrow> cmap_relation (map_to_tcbs (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko 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 4096 ptr ko) then Some ko 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 4096 ptr ko) then Some ko 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 4096 ptr ko) then Some ko else ksPSpace \<sigma> x)) (\<lambda>y. if y \<in> ((+\<^sub>p) (pde_Ptr ptr) \<circ> int) ` {k. k < 4096} then Some (from_bytes (replicate (size_of TYPE(pde_C)) 0)) else cslift x y) pde_Ptr cpde_relation \<and> cmap_relation (map_to_ptes (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko 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 4096 ptr ko) then Some ko else ksPSpace \<sigma> x)) (cslift x) ap_Ptr casid_pool_relation \<and> cmap_relation (heap_to_user_data (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation \<and> cmap_relation (heap_to_device_data (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation \<and> carray_map_relation ptBits (map_to_ptes (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko else ksPSpace \<sigma> x)) (c_h_t_valid x) pt_Ptr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cpspace_pde_array_relation (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko else ksPSpace \<sigma> x) (hrs_htd_update (ptr_retyps_gen 4096 (pde_Ptr ptr) True) (t_hrs_' (globals x))); cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr\<rbrakk> \<Longrightarrow> cmap_relation (map_to_tcbs (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko 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 4096 ptr ko) then Some ko 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 4096 ptr ko) then Some ko 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 4096 ptr ko) then Some ko else ksPSpace \<sigma> x)) (\<lambda>y. if y \<in> ((+\<^sub>p) (pde_Ptr ptr) \<circ> int) ` {k. k < 4096} then Some (from_bytes (replicate (size_of TYPE(pde_C)) 0)) else cslift x y) pde_Ptr cpde_relation \<and> cmap_relation (map_to_ptes (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko 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 4096 ptr ko) then Some ko else ksPSpace \<sigma> x)) (cslift x) ap_Ptr casid_pool_relation \<and> cmap_relation (heap_to_user_data (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation \<and> cmap_relation (heap_to_device_data (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation \<and> carray_map_relation ptBits (map_to_ptes (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko else ksPSpace \<sigma> x)) (c_h_t_valid x) pt_Ptr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cpspace_pde_array_relation (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko else ksPSpace \<sigma> x) (hrs_htd_update (ptr_retyps_gen 4096 (pde_Ptr ptr) True) (t_hrs_' (globals x))); 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_pdes (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko else ksPSpace \<sigma> x)) (\<lambda>y. if y \<in> ((+\<^sub>p) (pde_Ptr ptr) \<circ> int) ` {k. k < 4096} then Some (from_bytes (replicate (size_of TYPE(pde_C)) 0)) else cslift x y) pde_Ptr cpde_relation proof (prove)
goal (1 subgoal):
 1. \<lbrakk>carray_map_relation pdBits (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr (KOArch (KOPDE makeObject))) then Some makeObject else map_to_pdes (ksPSpace \<sigma>) x) (h_t_valid (hrs_htd (hrs_htd_update (ptr_retyps_gen 4096 (pde_Ptr ptr) True) (t_hrs_' (globals x)))) c_guard) pd_Ptr; cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr\<rbrakk> \<Longrightarrow> cmap_relation (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr (KOArch (KOPDE makeObject))) then Some makeObject else map_to_pdes (ksPSpace \<sigma>) x) (\<lambda>y. if y \<in> pde_Ptr ` set (new_cap_addrs 4096 ptr (KOArch (KOPDE makeObject))) then Some (from_bytes [0, 0, 0, 0]) else cslift x y) pde_Ptr cpde_relation proof (prove)
goal (1 subgoal):
 1. \<lbrakk>carray_map_relation pdBits (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr (KOArch (KOPDE makeObject))) then Some makeObject else map_to_pdes (ksPSpace \<sigma>) x) (h_t_valid (hrs_htd (hrs_htd_update (ptr_retyps_gen 4096 (pde_Ptr ptr) True) (t_hrs_' (globals x)))) c_guard) pd_Ptr; 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_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> cpde_relation makeObject (from_bytes [0, 0, 0, 0]) proof (prove)
goal:
No subgoals! proof (state)
this:
cpspace_relation (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>)) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x)))

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+2 ^ pdBits}) \<sigma> \<and> (region_is_bytes ptr (2 ^ pdBits) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ pdBits) ptr = replicate (2 ^ pdBits) 0) \<and> range_cover ptr sz pdBits 1 \<and> valid_global_refs' s \<and> kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (state)
this:
cpspace_relation (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>)) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x)))

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+2 ^ pdBits}) \<sigma> \<and> (region_is_bytes ptr (2 ^ pdBits) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ pdBits) ptr = replicate (2 ^ pdBits) 0) \<and> range_cover ptr sz pdBits 1 \<and> valid_global_refs' s \<and> kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (chain)
picking this:
(\<sigma>, x) \<in> rf_sr
sz < word_bits
is_aligned ptr pdBits proof (prove)
using this:
(\<sigma>, x) \<in> rf_sr
sz < word_bits
is_aligned ptr pdBits

goal (1 subgoal):
 1. ptr_span armKSGlobalPD_Ptr \<inter> {ptr..+2 ^ pdBits} = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sz < word_bits; is_aligned ptr pdBits; cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)); cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); carch_state_relation (ksArchState \<sigma>) (globals x); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {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> {symbol_table ''armKSGlobalPD''..+16384} \<inter> {ptr..+2 ^ pdBits} = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sz < word_bits; is_aligned ptr pdBits; cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)); cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); carch_state_relation (ksArchState \<sigma>) (globals x); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; 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> kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {} proof (prove)
goal:
No subgoals! proof (state)
this:
ptr_span armKSGlobalPD_Ptr \<inter> {ptr..+2 ^ pdBits} = {}

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+2 ^ pdBits}) \<sigma> \<and> (region_is_bytes ptr (2 ^ pdBits) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ pdBits) ptr = replicate (2 ^ pdBits) 0) \<and> range_cover ptr sz pdBits 1 \<and> valid_global_refs' s \<and> kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (state)
this:
ptr_span armKSGlobalPD_Ptr \<inter> {ptr..+2 ^ pdBits} = {}

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+2 ^ pdBits}) \<sigma> \<and> (region_is_bytes ptr (2 ^ pdBits) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ pdBits) ptr = replicate (2 ^ pdBits) 0) \<and> range_cover ptr sz pdBits 1 \<and> valid_global_refs' s \<and> kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (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. pde_stored_asid \<circ>\<^sub>m clift (hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x))) = pde_stored_asid \<circ>\<^sub>m cslift x proof (prove)
using this:
(\<sigma>, x) \<in> {(s, s'). cstate_relation s (globals s')}

goal (1 subgoal):
 1. pde_stored_asid \<circ>\<^sub>m clift (hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x))) = pde_stored_asid \<circ>\<^sub>m cslift x proof (prove)
using this:
(\<sigma>, x) \<in> {(s, s'). cstate_relation s (globals s')}
cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x))
region_is_bytes ptr (2 ^ pdBits) x

goal (1 subgoal):
 1. pde_stored_asid \<circ>\<^sub>m clift (hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x))) = pde_stored_asid \<circ>\<^sub>m cslift x proof (prove)
using this:
(\<sigma>, x) \<in> {(s, s'). cstate_relation s (globals s')}
cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x))
region_is_bytes ptr (2 ^ pdBits) x

goal (1 subgoal):
 1. pde_stored_asid \<circ>\<^sub>m clift (hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x))) = pde_stored_asid \<circ>\<^sub>m cslift x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cstate_relation \<sigma> (globals x); cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)); region_is_bytes ptr (2 ^ pdBits) x\<rbrakk> \<Longrightarrow> pde_stored_asid \<circ>\<^sub>m clift (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x))) = pde_stored_asid \<circ>\<^sub>m cslift x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cstate_relation \<sigma> (globals x); cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)); region_is_bytes ptr (2 ^ pdBits) x\<rbrakk> \<Longrightarrow> pde_stored_asid \<circ>\<^sub>m clift (hrs_htd_update (ptr_retyps_gen 4096 (pde_Ptr ptr) True) (t_hrs_' (globals x))) = pde_stored_asid \<circ>\<^sub>m cslift x proof (prove)
goal (4 subgoals):
 1. \<lbrakk>cstate_relation \<sigma> (globals x); cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)); True\<rbrakk> \<Longrightarrow> typ_uinfo_t TYPE(pde_C) \<noteq> typ_uinfo_t TYPE(8 word)
 2. \<lbrakk>cstate_relation \<sigma> (globals x); cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)); True\<rbrakk> \<Longrightarrow> 2 ^ pdBits < 2 ^ word_bits
 3. \<lbrakk>cstate_relation \<sigma> (globals x); cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)); True\<rbrakk> \<Longrightarrow> heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ pdBits) ptr = replicate (2 ^ pdBits) 0
 4. \<lbrakk>cstate_relation \<sigma> (globals x); cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)); True\<rbrakk> \<Longrightarrow> pde_stored_asid \<circ>\<^sub>m (\<lambda>y. if y \<in> ((+\<^sub>p) (pde_Ptr ptr) \<circ> int) ` {k. k < 4096} then Some (from_bytes (replicate (size_of TYPE(pde_C)) 0)) else cslift x y) = pde_stored_asid \<circ>\<^sub>m cslift x proof (prove)
goal (3 subgoals):
 1. \<lbrakk>cstate_relation \<sigma> (globals x); cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)); True\<rbrakk> \<Longrightarrow> 2 ^ pdBits < 2 ^ word_bits
 2. \<lbrakk>cstate_relation \<sigma> (globals x); cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)); True\<rbrakk> \<Longrightarrow> heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ pdBits) ptr = replicate (2 ^ pdBits) 0
 3. \<lbrakk>cstate_relation \<sigma> (globals x); cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)); True\<rbrakk> \<Longrightarrow> pde_stored_asid \<circ>\<^sub>m (\<lambda>y. if y \<in> ((+\<^sub>p) (pde_Ptr ptr) \<circ> int) ` {k. k < 4096} then Some (from_bytes (replicate (size_of TYPE(pde_C)) 0)) else cslift x y) = pde_stored_asid \<circ>\<^sub>m cslift x proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cstate_relation \<sigma> (globals x); cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)); True\<rbrakk> \<Longrightarrow> heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ pdBits) ptr = replicate (2 ^ pdBits) 0
 2. \<lbrakk>cstate_relation \<sigma> (globals x); cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)); True\<rbrakk> \<Longrightarrow> pde_stored_asid \<circ>\<^sub>m (\<lambda>y. if y \<in> ((+\<^sub>p) (pde_Ptr ptr) \<circ> int) ` {k. k < 4096} then Some (from_bytes (replicate (size_of TYPE(pde_C)) 0)) else cslift x y) = pde_stored_asid \<circ>\<^sub>m cslift x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cstate_relation \<sigma> (globals x); cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)); True\<rbrakk> \<Longrightarrow> pde_stored_asid \<circ>\<^sub>m (\<lambda>y. if y \<in> ((+\<^sub>p) (pde_Ptr ptr) \<circ> int) ` {k. k < 4096} then Some (from_bytes (replicate (size_of TYPE(pde_C)) 0)) else cslift x y) = pde_stored_asid \<circ>\<^sub>m cslift x proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>cstate_relation \<sigma> (globals x); cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)); True\<rbrakk> \<Longrightarrow> (pde_stored_asid \<circ>\<^sub>m (\<lambda>y. if y \<in> ((+\<^sub>p) (pde_Ptr ptr) \<circ> int) ` {k. k < 4096} then Some (from_bytes (replicate (size_of TYPE(pde_C)) 0)) else cslift x y)) xa = (pde_stored_asid \<circ>\<^sub>m cslift x) xa proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>cstate_relation \<sigma> (globals x); cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> xa \<in> ((+\<^sub>p) (pde_Ptr ptr) \<circ> int) ` {k. k < 4096} \<longrightarrow> (\<forall>x2. cslift x xa = Some x2 \<longrightarrow> None = pde_stored_asid x2) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>cstate_relation \<sigma> (globals x); cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> xa \<in> (\<lambda>x. pde_Ptr (ptr + word_of_int (int x) * word_of_nat (size_of TYPE(pde_C)))) ` {k. k < 4096} \<longrightarrow> (\<forall>x2. cslift x xa = Some x2 \<longrightarrow> None = pde_stored_asid x2) proof (prove)
goal (1 subgoal):
 1. \<And>xa xaa x2. \<lbrakk>cstate_relation \<sigma> (globals x); cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)); xaa < 4096; cslift x (pde_Ptr (ptr + word_of_int (int xaa) * word_of_nat (size_of TYPE(pde_C)))) = Some x2\<rbrakk> \<Longrightarrow> None = pde_stored_asid x2 proof (prove)
goal (2 subgoals):
 1. \<And>xa xaa x2. \<lbrakk>cstate_relation \<sigma> (globals x); cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)); xaa < 4096\<rbrakk> \<Longrightarrow> ?x25 xa xaa x2 \<in> ptr_span (pde_Ptr (ptr + word_of_int (int xaa) * word_of_nat (size_of TYPE(pde_C))))
 2. \<And>xa xaa x2. \<lbrakk>cstate_relation \<sigma> (globals x); cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)); xaa < 4096; \<exists>n. snd (hrs_htd (t_hrs_' (globals x)) (?x25 xa xaa x2)) n \<noteq> None \<and> fst (the (snd (hrs_htd (t_hrs_' (globals x)) (?x25 xa xaa x2)) n)) = typ_uinfo_t TYPE(pde_C)\<rbrakk> \<Longrightarrow> None = pde_stored_asid x2 proof (prove)
goal (1 subgoal):
 1. \<And>xa xaa x2. \<lbrakk>cstate_relation \<sigma> (globals x); cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)); xaa < 4096; \<exists>n. snd (hrs_htd (t_hrs_' (globals x)) (ptr_val (pde_Ptr (ptr + word_of_int (int xaa) * word_of_nat (size_of TYPE(pde_C)))))) n \<noteq> None \<and> fst (the (snd (hrs_htd (t_hrs_' (globals x)) (ptr_val (pde_Ptr (ptr + word_of_int (int xaa) * word_of_nat (size_of TYPE(pde_C)))))) n)) = typ_uinfo_t TYPE(pde_C)\<rbrakk> \<Longrightarrow> None = pde_stored_asid x2 proof (prove)
goal (1 subgoal):
 1. \<And>xa x2 n b. \<lbrakk>cstate_relation \<sigma> (globals x); cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)); xa < 4096; snd (hrs_htd (t_hrs_' (globals x)) (ptr + word_of_nat xa * 4)) n = Some (typ_uinfo_t TYPE(pde_C), b)\<rbrakk> \<Longrightarrow> None = pde_stored_asid x2 proof (prove)
goal (3 subgoals):
 1. \<And>xa x2 n b. \<lbrakk>cstate_relation \<sigma> (globals x); cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)); xa < 4096\<rbrakk> \<Longrightarrow> ptr + word_of_nat xa * 4 \<in> {ptr..+2 ^ pdBits}
 2. \<And>xa x2 n b. \<lbrakk>cstate_relation \<sigma> (globals x); cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)); xa < 4096\<rbrakk> \<Longrightarrow> typ_uinfo_t TYPE(pde_C) \<noteq> typ_uinfo_t TYPE(8 word)
 3. \<And>xa x2 n b. \<lbrakk>cstate_relation \<sigma> (globals x); cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)); xa < 4096; False\<rbrakk> \<Longrightarrow> None = pde_stored_asid x2 proof (prove)
goal (2 subgoals):
 1. \<And>xa x2 n b. \<lbrakk>cstate_relation \<sigma> (globals x); cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)); xa < 4096\<rbrakk> \<Longrightarrow> typ_uinfo_t TYPE(pde_C) \<noteq> typ_uinfo_t TYPE(8 word)
 2. \<And>xa x2 n b. \<lbrakk>cstate_relation \<sigma> (globals x); cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)); xa < 4096; False\<rbrakk> \<Longrightarrow> None = pde_stored_asid x2 proof (prove)
goal (1 subgoal):
 1. \<And>xa x2 n b. \<lbrakk>cstate_relation \<sigma> (globals x); cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)); xa < 4096; False\<rbrakk> \<Longrightarrow> None = pde_stored_asid x2 proof (prove)
goal:
No subgoals! proof (state)
this:
pde_stored_asid \<circ>\<^sub>m clift (hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x))) = pde_stored_asid \<circ>\<^sub>m cslift x

goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> ptr \<noteq> 0 \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pspace_no_overlap' ptr sz \<sigma> \<and> (valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+2 ^ pdBits}) \<sigma> \<and> (region_is_bytes ptr (2 ^ pdBits) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ pdBits) ptr = replicate (2 ^ pdBits) 0) \<and> range_cover ptr sz pdBits 1 \<and> valid_global_refs' s \<and> kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (chain)
picking this:
cpspace_relation (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>)) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x)))
ptr_span armKSGlobalPD_Ptr \<inter> {ptr..+2 ^ pdBits} = {}
pde_stored_asid \<circ>\<^sub>m clift (hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x))) = pde_stored_asid \<circ>\<^sub>m cslift x proof (prove)
using this:
cpspace_relation (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>)) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x)))
ptr_span armKSGlobalPD_Ptr \<inter> {ptr..+2 ^ pdBits} = {}
pde_stored_asid \<circ>\<^sub>m clift (hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x))) = pde_stored_asid \<circ>\<^sub>m cslift x

goal (1 subgoal):
 1. (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
using this:
cpspace_relation (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>)) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x)))
ptr_span armKSGlobalPD_Ptr \<inter> {ptr..+2 ^ pdBits} = {}
pde_stored_asid \<circ>\<^sub>m clift (hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x))) = pde_stored_asid \<circ>\<^sub>m cslift x
(\<sigma>, x) \<in> rf_sr
region_is_bytes ptr (2 ^ pdBits) x
kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {}
(valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+2 ^ pdBits}) \<sigma>

goal (1 subgoal):
 1. (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cpspace_relation (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>)) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x))); {symbol_table ''armKSGlobalPD''..+16384} \<inter> {ptr..+2 ^ pdBits} = {}; pde_stored_asid \<circ>\<^sub>m clift (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x))) = pde_stored_asid \<circ>\<^sub>m cslift 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 (2 ^ pdBits) x; kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {}; valid_objs' \<sigma> \<and> untyped_ranges_zero' \<sigma> \<and> caps_overlap_reserved' {ptr..+2 ^ pdBits} \<sigma>\<rbrakk> \<Longrightarrow> zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x))) \<and> carch_state_relation (ksArchState \<sigma>) (globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x))\<rparr>) \<and> cmachine_state_relation (ksMachineState \<sigma>) (globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x))\<rparr>) \<and> cvariable_array_map_relation (gsCNodes \<sigma>) ((^) 2) cte_Ptr (hrs_htd (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x)))) \<and> cvariable_array_map_relation (map_to_tcbs (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>))) (\<lambda>x. 5) cte_Ptr (hrs_htd (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x)))) \<and> hrs_htd (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x))) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr \<and> hrs_htd (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x))) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr \<and> htd_safe domain (hrs_htd (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x)))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cpspace_relation (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>)) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x))); {symbol_table ''armKSGlobalPD''..+16384} \<inter> {ptr..+2 ^ pdBits} = {}; pde_stored_asid \<circ>\<^sub>m clift (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x))) = pde_stored_asid \<circ>\<^sub>m cslift 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 (2 ^ pdBits) x; kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {}; valid_objs' \<sigma> \<and> untyped_ranges_zero' \<sigma> \<and> caps_overlap_reserved' {ptr..+2 ^ pdBits} \<sigma>\<rbrakk> \<Longrightarrow> zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x))) \<and> cvariable_array_map_relation (gsCNodes \<sigma>) ((^) 2) cte_Ptr (hrs_htd (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x)))) \<and> cvariable_array_map_relation (map_to_tcbs (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>))) (\<lambda>x. 5) cte_Ptr (hrs_htd (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x)))) \<and> hrs_htd (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x))) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr \<and> hrs_htd (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x))) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr \<and> htd_safe domain (hrs_htd (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x)))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cpspace_relation (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x))); {symbol_table ''armKSGlobalPD''..+16384} \<inter> {ptr..+2 ^ pdBits} = {}; pde_stored_asid \<circ>\<^sub>m clift (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x))) = pde_stored_asid \<circ>\<^sub>m cslift x; region_is_bytes ptr (2 ^ pdBits) x; kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {}; 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..+2 ^ pdBits} \<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>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {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> ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False (hrs_htd (t_hrs_' (globals x))) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr \<and> ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False (hrs_htd (t_hrs_' (globals x))) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr \<and> htd_safe domain (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False (hrs_htd (t_hrs_' (globals x)))) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>cpspace_relation (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x))); {symbol_table ''armKSGlobalPD''..+16384} \<inter> {ptr..+2 ^ pdBits} = {}; pde_stored_asid \<circ>\<^sub>m clift (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x))) = pde_stored_asid \<circ>\<^sub>m cslift x; region_is_bytes ptr (2 ^ pdBits) x; kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {}; 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..+2 ^ pdBits} \<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>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {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> x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr
 2. \<lbrakk>cpspace_relation (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x))); {symbol_table ''armKSGlobalPD''..+16384} \<inter> {ptr..+2 ^ pdBits} = {}; pde_stored_asid \<circ>\<^sub>m clift (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x))) = pde_stored_asid \<circ>\<^sub>m cslift x; region_is_bytes ptr (2 ^ pdBits) x; kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {}; 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..+2 ^ pdBits} \<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>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {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> ptr_span intStateIRQNode_array_Ptr \<inter> {ptr_val (pd_Ptr ptr)..+Suc 0 * size_of TYPE(pde_C[4096])} = {}
 3. \<lbrakk>cpspace_relation (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x))); {symbol_table ''armKSGlobalPD''..+16384} \<inter> {ptr..+2 ^ pdBits} = {}; pde_stored_asid \<circ>\<^sub>m clift (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x))) = pde_stored_asid \<circ>\<^sub>m cslift x; region_is_bytes ptr (2 ^ pdBits) x; kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {}; 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..+2 ^ pdBits} \<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>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {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> True \<and> ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False (hrs_htd (t_hrs_' (globals x))) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr \<and> htd_safe domain (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False (hrs_htd (t_hrs_' (globals x)))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cpspace_relation (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x))); {symbol_table ''armKSGlobalPD''..+16384} \<inter> {ptr..+2 ^ pdBits} = {}; pde_stored_asid \<circ>\<^sub>m clift (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x))) = pde_stored_asid \<circ>\<^sub>m cslift x; region_is_bytes ptr (2 ^ pdBits) x; kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {}; 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..+2 ^ pdBits} \<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>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {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> ptr_span intStateIRQNode_array_Ptr \<inter> {ptr_val (pd_Ptr ptr)..+Suc 0 * size_of TYPE(pde_C[4096])} = {}
 2. \<lbrakk>cpspace_relation (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x))); {symbol_table ''armKSGlobalPD''..+16384} \<inter> {ptr..+2 ^ pdBits} = {}; pde_stored_asid \<circ>\<^sub>m clift (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x))) = pde_stored_asid \<circ>\<^sub>m cslift x; region_is_bytes ptr (2 ^ pdBits) x; kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {}; 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..+2 ^ pdBits} \<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>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {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> True \<and> ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False (hrs_htd (t_hrs_' (globals x))) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr \<and> htd_safe domain (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False (hrs_htd (t_hrs_' (globals x)))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cpspace_relation (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x))); {symbol_table ''armKSGlobalPD''..+16384} \<inter> {ptr..+2 ^ pdBits} = {}; pde_stored_asid \<circ>\<^sub>m clift (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x))) = pde_stored_asid \<circ>\<^sub>m cslift x; region_is_bytes ptr (2 ^ pdBits) x; kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {}; 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..+2 ^ pdBits} \<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>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {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> {symbol_table ''intStateIRQNode''..+4096} \<inter> {ptr..+16384} = {}
 2. \<lbrakk>cpspace_relation (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x))); {symbol_table ''armKSGlobalPD''..+16384} \<inter> {ptr..+2 ^ pdBits} = {}; pde_stored_asid \<circ>\<^sub>m clift (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x))) = pde_stored_asid \<circ>\<^sub>m cslift x; region_is_bytes ptr (2 ^ pdBits) x; kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {}; 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..+2 ^ pdBits} \<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>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {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> True \<and> ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False (hrs_htd (t_hrs_' (globals x))) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr \<and> htd_safe domain (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False (hrs_htd (t_hrs_' (globals x)))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cpspace_relation (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x))); {symbol_table ''armKSGlobalPD''..+16384} \<inter> {ptr..+2 ^ pdBits} = {}; pde_stored_asid \<circ>\<^sub>m clift (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x))) = pde_stored_asid \<circ>\<^sub>m cslift x; region_is_bytes ptr (2 ^ pdBits) x; kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {}; 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..+2 ^ pdBits} \<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>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {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> kernel_data_refs \<inter> {ptr..+16384} = {}
 2. \<lbrakk>cpspace_relation (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x))); {symbol_table ''armKSGlobalPD''..+16384} \<inter> {ptr..+2 ^ pdBits} = {}; pde_stored_asid \<circ>\<^sub>m clift (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x))) = pde_stored_asid \<circ>\<^sub>m cslift x; region_is_bytes ptr (2 ^ pdBits) x; kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {}; 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..+2 ^ pdBits} \<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>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {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> True \<and> ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False (hrs_htd (t_hrs_' (globals x))) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr \<and> htd_safe domain (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False (hrs_htd (t_hrs_' (globals x)))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cpspace_relation (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x))); {symbol_table ''armKSGlobalPD''..+16384} \<inter> {ptr..+2 ^ pdBits} = {}; pde_stored_asid \<circ>\<^sub>m clift (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x))) = pde_stored_asid \<circ>\<^sub>m cslift x; region_is_bytes ptr (2 ^ pdBits) x; kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {}; 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..+2 ^ pdBits} \<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>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {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> True \<and> ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False (hrs_htd (t_hrs_' (globals x))) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr \<and> htd_safe domain (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False (hrs_htd (t_hrs_' (globals x)))) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>cpspace_relation (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x))); {symbol_table ''armKSGlobalPD''..+16384} \<inter> {ptr..+2 ^ pdBits} = {}; pde_stored_asid \<circ>\<^sub>m clift (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x))) = pde_stored_asid \<circ>\<^sub>m cslift x; region_is_bytes ptr (2 ^ pdBits) x; kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {}; 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..+2 ^ pdBits} \<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>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {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> x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr
 2. \<lbrakk>cpspace_relation (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x))); {symbol_table ''armKSGlobalPD''..+16384} \<inter> {ptr..+2 ^ pdBits} = {}; pde_stored_asid \<circ>\<^sub>m clift (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x))) = pde_stored_asid \<circ>\<^sub>m cslift x; region_is_bytes ptr (2 ^ pdBits) x; kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {}; 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..+2 ^ pdBits} \<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>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {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> ptr_span armKSGlobalPD_Ptr \<inter> {ptr_val (pd_Ptr ptr)..+Suc 0 * size_of TYPE(pde_C[4096])} = {}
 3. \<lbrakk>cpspace_relation (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x))); {symbol_table ''armKSGlobalPD''..+16384} \<inter> {ptr..+2 ^ pdBits} = {}; pde_stored_asid \<circ>\<^sub>m clift (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x))) = pde_stored_asid \<circ>\<^sub>m cslift x; region_is_bytes ptr (2 ^ pdBits) x; kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {}; 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..+2 ^ pdBits} \<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>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {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> True \<and> True \<and> htd_safe domain (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False (hrs_htd (t_hrs_' (globals x)))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cpspace_relation (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x))); {symbol_table ''armKSGlobalPD''..+16384} \<inter> {ptr..+2 ^ pdBits} = {}; pde_stored_asid \<circ>\<^sub>m clift (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x))) = pde_stored_asid \<circ>\<^sub>m cslift x; region_is_bytes ptr (2 ^ pdBits) x; kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {}; 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..+2 ^ pdBits} \<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>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {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> ptr_span armKSGlobalPD_Ptr \<inter> {ptr_val (pd_Ptr ptr)..+Suc 0 * size_of TYPE(pde_C[4096])} = {}
 2. \<lbrakk>cpspace_relation (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x))); {symbol_table ''armKSGlobalPD''..+16384} \<inter> {ptr..+2 ^ pdBits} = {}; pde_stored_asid \<circ>\<^sub>m clift (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x))) = pde_stored_asid \<circ>\<^sub>m cslift x; region_is_bytes ptr (2 ^ pdBits) x; kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {}; 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..+2 ^ pdBits} \<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>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {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> True \<and> True \<and> htd_safe domain (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False (hrs_htd (t_hrs_' (globals x)))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cpspace_relation (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x))); {symbol_table ''armKSGlobalPD''..+16384} \<inter> {ptr..+2 ^ pdBits} = {}; pde_stored_asid \<circ>\<^sub>m clift (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x))) = pde_stored_asid \<circ>\<^sub>m cslift x; region_is_bytes ptr (2 ^ pdBits) x; kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {}; 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..+2 ^ pdBits} \<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>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {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> {symbol_table ''armKSGlobalPD''..+16384} \<inter> {ptr..+16384} = {}
 2. \<lbrakk>cpspace_relation (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x))); {symbol_table ''armKSGlobalPD''..+16384} \<inter> {ptr..+2 ^ pdBits} = {}; pde_stored_asid \<circ>\<^sub>m clift (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x))) = pde_stored_asid \<circ>\<^sub>m cslift x; region_is_bytes ptr (2 ^ pdBits) x; kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {}; 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..+2 ^ pdBits} \<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>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {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> True \<and> True \<and> htd_safe domain (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False (hrs_htd (t_hrs_' (globals x)))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cpspace_relation (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x))); {symbol_table ''armKSGlobalPD''..+16384} \<inter> {ptr..+2 ^ pdBits} = {}; pde_stored_asid \<circ>\<^sub>m clift (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x))) = pde_stored_asid \<circ>\<^sub>m cslift x; region_is_bytes ptr (2 ^ pdBits) x; kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {}; 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..+2 ^ pdBits} \<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>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; 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> kernel_data_refs \<inter> {ptr..+16384} = {}
 2. \<lbrakk>cpspace_relation (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x))); {symbol_table ''armKSGlobalPD''..+16384} \<inter> {ptr..+2 ^ pdBits} = {}; pde_stored_asid \<circ>\<^sub>m clift (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x))) = pde_stored_asid \<circ>\<^sub>m cslift x; region_is_bytes ptr (2 ^ pdBits) x; kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {}; 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..+2 ^ pdBits} \<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>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {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> True \<and> True \<and> htd_safe domain (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False (hrs_htd (t_hrs_' (globals x)))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cpspace_relation (\<lambda>x. if x \<in> set (new_cap_addrs 4096 ptr ko) then Some ko else ksPSpace \<sigma> x) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x))); {symbol_table ''armKSGlobalPD''..+16384} \<inter> {ptr..+2 ^ pdBits} = {}; pde_stored_asid \<circ>\<^sub>m clift (hrs_htd_update (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False) (t_hrs_' (globals x))) = pde_stored_asid \<circ>\<^sub>m cslift x; region_is_bytes ptr (2 ^ pdBits) x; kernel_data_refs \<inter> {ptr..+2 ^ pdBits} = {}; 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..+2 ^ pdBits} \<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>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {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> True \<and> True \<and> htd_safe domain (ptr_retyps_gen (Suc 0) (pd_Ptr ptr) False (hrs_htd (t_hrs_' (globals x)))) proof (prove)
goal:
No subgoals! proof (state)
this:
(\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs 4096 ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen 1 (pd_Ptr ptr) False) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr

goal:
No subgoals!