theory Retype_C

lemma createObjects_ccorres_cte:
  defines "ko \<equiv> (KOCTE (makeObject :: cte))"
  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 (n * 2 ^ objBitsKO ko) \<sigma>
  \<and> region_is_zero_bytes ptr (n * 2 ^ objBitsKO ko) x
  \<and> range_cover ptr sz (objBitsKO ko) n
  \<and> {ptr ..+ n * (2 ^ objBitsKO ko)} \<inter> kernel_data_refs = {}
   \<longrightarrow>
  (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace \<sigma>)\<rparr>,
   x\<lparr>globals := globals x
                 \<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen n (Ptr ptr :: cte_C ptr) True)
                       (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 :: cte_C ptr" assume "?P \<sigma> x" hence rf: "(\<sigma>, x) \<in> rf_sr"
    and cover: "range_cover ptr sz (objBitsKO ko) n"
    and al: "is_aligned ptr (objBitsKO ko)" and ptr0: "ptr \<noteq> 0"
    and sz: "objBitsKO ko \<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 (n * 2 ^ objBitsKO ko) \<sigma>"
    and empty: "region_is_bytes ptr (n * (2 ^ objBitsKO ko)) x"
    and zero: "heap_list_is_zero (hrs_mem (t_hrs_' (globals x))) ptr (n * (2 ^ objBitsKO ko))"
    and rc: "range_cover ptr sz (objBitsKO ko) n"
    and kdr: "{ptr..+n * 2 ^ objBitsKO ko} \<inter> kernel_data_refs = {}" by (clarsimp simp:range_cover_def[where 'a=32, folded word_bits_def])+ 

  (* obj specific *)
   have mko: "\<And>dev. makeObjectKO dev (Inr (APIObjectType  ArchTypes_H.apiobject_type.CapTableObject)) = Some ko" by (simp add: ko_def makeObjectKO_def) note relrl = ccte_relation_makeObject 

  (* /obj specific *)

  (* s/obj/obj'/ *)
   have szo: "size_of TYPE(cte_C) = 2 ^ objBitsKO ko" by (simp add: size_of_def objBits_simps' ko_def) have szo': "n * 2 ^ objBitsKO ko = n * size_of TYPE(cte_C)" using sz apply (subst szo) apply (simp add: power_add [symmetric]) done note rl' = cslift_ptr_retyp_other_inst[OF empty cover szo' szo] 

  (* rest is generic *)
   note rl = projectKO_opt_retyp_other [OF rc pal pno ko_def] note cterl = retype_ctes_helper [OF pal pdst pno al sz szb mko rc, simplified] note ht_rl = clift_eq_h_t_valid_eq[OF rl', OF tag_disj_via_td_name, simplified] have guard:
    "\<forall>b< n. c_guard (CTypesDefs.ptr_add ?ptr (of_nat b))" apply (rule retype_guard_helper[where m=2, OF cover ptr0 szo]) apply (simp add: ko_def objBits_simps' align_of_def)+ done note irq = h_t_valid_eq_array_valid[where 'a=cte_C]
    h_t_array_valid_ptr_retyps_gen[where p="Ptr ptr", simplified, OF szo empty] with rf have irq: "h_t_valid (hrs_htd ?ks') c_guard intStateIRQNode_array_Ptr" apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def) apply (simp add: hrs_htd_update h_t_valid_eq_array_valid) apply (simp add: h_t_array_valid_ptr_retyps_gen[OF szo] empty) done note if_cong[cong]  (* needed by some of the [simplified]'s below. *)
   from rf have "cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x))" unfolding rf_sr_def cstate_relation_def by (simp add: Let_def) hence "cpspace_relation ?ks (underlying_memory (ksMachineState \<sigma>)) ?ks'" unfolding cpspace_relation_def apply - supply image_cong_simp [cong del] apply (clarsimp simp: rl' cterl tag_disj_via_td_name foldr_upd_app_if [folded data_map_insert_def]) apply (subst clift_ptr_retyps_gen_prev_memset_same[OF guard _ _ szo' _ zero],
      simp_all only: szo empty, simp_all) apply (rule range_cover.strong_times_32[OF cover refl]) apply (simp add: ptr_add_to_new_cap_addrs [OF szo] ht_rl) apply (simp add: rl projectKO_opt_retyp_same projectKOs) apply (simp add: ko_def projectKO_opt_retyp_same projectKOs cong: if_cong) apply (subst makeObject_cte[symmetric]) apply (erule cmap_relation_retype) apply (rule relrl[simplified szo ko_def]) done thus ?thesis using rf empty kdr irq rzo apply (simp add: rf_sr_def cstate_relation_def Let_def rl' tag_disj_via_td_name) apply (simp add: carch_state_relation_def cmachine_state_relation_def) apply (simp add: rl' cterl tag_disj_via_td_name h_t_valid_clift_Some_iff) apply (clarsimp simp: hrs_htd_update ptr_retyps_htd_safe_neg szo
                          kernel_data_refs_domain_eq_rotate
                          rl foldr_upd_app_if [folded data_map_insert_def] projectKOs
                          zero_ranges_ptr_retyps
                          ht_rl cvariable_array_ptr_retyps[OF szo]) 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..+n * 2 ^ objBitsKO ko}) \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ objBitsKO ko) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ objBitsKO ko) ptr = replicate (n * 2 ^ objBitsKO ko) 0) \<and> range_cover ptr sz (objBitsKO ko) n \<and> {ptr..+n * 2 ^ objBitsKO ko} \<inter> kernel_data_refs = {} \<longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (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..+n * 2 ^ objBitsKO ko}) \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ objBitsKO ko) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ objBitsKO ko) ptr = replicate (n * 2 ^ objBitsKO ko) 0) \<and> range_cover ptr sz (objBitsKO ko) n \<and> {ptr..+n * 2 ^ objBitsKO ko} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (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..+n * 2 ^ objBitsKO ko}) \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ objBitsKO ko) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ objBitsKO ko) ptr = replicate (n * 2 ^ objBitsKO ko) 0) \<and> range_cover ptr sz (objBitsKO ko) n \<and> {ptr..+n * 2 ^ objBitsKO ko} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (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..+n * 2 ^ objBitsKO ko}) \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ objBitsKO ko) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ objBitsKO ko) ptr = replicate (n * 2 ^ objBitsKO ko) 0) \<and> range_cover ptr sz (objBitsKO ko) n \<and> {ptr..+n * 2 ^ objBitsKO ko} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (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..+n * 2 ^ objBitsKO ko}) \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ objBitsKO ko) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ objBitsKO ko) ptr = replicate (n * 2 ^ objBitsKO ko) 0) \<and> range_cover ptr sz (objBitsKO ko) n \<and> {ptr..+n * 2 ^ objBitsKO ko} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (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..+n * 2 ^ objBitsKO ko}) \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ objBitsKO ko) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ objBitsKO ko) ptr = replicate (n * 2 ^ objBitsKO ko) 0) \<and> range_cover ptr sz (objBitsKO ko) n \<and> {ptr..+n * 2 ^ objBitsKO ko} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (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..+n * 2 ^ objBitsKO ko}) \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ objBitsKO ko) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ objBitsKO ko) ptr = replicate (n * 2 ^ objBitsKO ko) 0) \<and> range_cover ptr sz (objBitsKO ko) n \<and> {ptr..+n * 2 ^ objBitsKO ko} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (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..+n * 2 ^ objBitsKO ko}) \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ objBitsKO ko) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ objBitsKO ko) ptr = replicate (n * 2 ^ objBitsKO ko) 0) \<and> range_cover ptr sz (objBitsKO ko) n \<and> {ptr..+n * 2 ^ objBitsKO ko} \<inter> kernel_data_refs = {}

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..+n * 2 ^ objBitsKO ko}) \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ objBitsKO ko) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ objBitsKO ko) ptr = replicate (n * 2 ^ objBitsKO ko) 0) \<and> range_cover ptr sz (objBitsKO ko) n \<and> {ptr..+n * 2 ^ objBitsKO ko} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (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..+n * 2 ^ objBitsKO ko}) \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ objBitsKO ko) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ objBitsKO ko) ptr = replicate (n * 2 ^ objBitsKO ko) 0) \<and> range_cover ptr sz (objBitsKO ko) n \<and> {ptr..+n * 2 ^ objBitsKO ko} \<inter> kernel_data_refs = {}

goal (1 subgoal):
 1. (((\<sigma>, x) \<in> rf_sr &&& range_cover ptr sz (objBitsKO ko) n &&& is_aligned ptr (objBitsKO ko)) &&& (ptr \<noteq> 0 &&& objBitsKO ko \<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..+n * 2 ^ objBitsKO ko}) \<sigma>) &&& (region_is_bytes ptr (n * 2 ^ objBitsKO ko) x &&& heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ objBitsKO ko) ptr = replicate (n * 2 ^ objBitsKO ko) 0) &&& range_cover ptr sz (objBitsKO ko) n &&& {ptr..+n * 2 ^ objBitsKO ko} \<inter> kernel_data_refs = {} proof (state)
this:
(\<sigma>, x) \<in> rf_sr
range_cover ptr sz (objBitsKO ko) n
is_aligned ptr (objBitsKO ko)
ptr \<noteq> 0
objBitsKO ko \<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..+n * 2 ^ objBitsKO ko}) \<sigma>
region_is_bytes ptr (n * 2 ^ objBitsKO ko) x
heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ objBitsKO ko) ptr = replicate (n * 2 ^ objBitsKO ko) 0
range_cover ptr sz (objBitsKO ko) n
{ptr..+n * 2 ^ objBitsKO ko} \<inter> kernel_data_refs = {}

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..+n * 2 ^ objBitsKO ko}) \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ objBitsKO ko) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ objBitsKO ko) ptr = replicate (n * 2 ^ objBitsKO ko) 0) \<and> range_cover ptr sz (objBitsKO ko) n \<and> {ptr..+n * 2 ^ objBitsKO ko} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (state)
this:
(\<sigma>, x) \<in> rf_sr
range_cover ptr sz (objBitsKO ko) n
is_aligned ptr (objBitsKO ko)
ptr \<noteq> 0
objBitsKO ko \<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..+n * 2 ^ objBitsKO ko}) \<sigma>
region_is_bytes ptr (n * 2 ^ objBitsKO ko) x
heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ objBitsKO ko) ptr = replicate (n * 2 ^ objBitsKO ko) 0
range_cover ptr sz (objBitsKO ko) n
{ptr..+n * 2 ^ objBitsKO ko} \<inter> kernel_data_refs = {}

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..+n * 2 ^ objBitsKO ko}) \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ objBitsKO ko) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ objBitsKO ko) ptr = replicate (n * 2 ^ objBitsKO ko) 0) \<and> range_cover ptr sz (objBitsKO ko) n \<and> {ptr..+n * 2 ^ objBitsKO ko} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>dev. makeObjectKO dev (Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject)) = Some ko proof (state)
this:
makeObjectKO ?dev2 (Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject)) = 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..+n * 2 ^ objBitsKO ko}) \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ objBitsKO ko) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ objBitsKO ko) ptr = replicate (n * 2 ^ objBitsKO ko) 0) \<and> range_cover ptr sz (objBitsKO ko) n \<and> {ptr..+n * 2 ^ objBitsKO ko} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (state)
this:
ccte_relation makeObject (from_bytes (replicate (size_of TYPE(cte_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..+n * 2 ^ objBitsKO ko}) \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ objBitsKO ko) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ objBitsKO ko) ptr = replicate (n * 2 ^ objBitsKO ko) 0) \<and> range_cover ptr sz (objBitsKO ko) n \<and> {ptr..+n * 2 ^ objBitsKO ko} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (state)
this:
ccte_relation makeObject (from_bytes (replicate (size_of TYPE(cte_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..+n * 2 ^ objBitsKO ko}) \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ objBitsKO ko) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ objBitsKO ko) ptr = replicate (n * 2 ^ objBitsKO ko) 0) \<and> range_cover ptr sz (objBitsKO ko) n \<and> {ptr..+n * 2 ^ objBitsKO ko} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. size_of TYPE(cte_C) = 2 ^ objBitsKO ko proof (state)
this:
size_of TYPE(cte_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..+n * 2 ^ objBitsKO ko}) \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ objBitsKO ko) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ objBitsKO ko) ptr = replicate (n * 2 ^ objBitsKO ko) 0) \<and> range_cover ptr sz (objBitsKO ko) n \<and> {ptr..+n * 2 ^ objBitsKO ko} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. n * 2 ^ objBitsKO ko = n * size_of TYPE(cte_C) proof (prove)
using this:
objBitsKO ko \<le> sz

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

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..+n * 2 ^ objBitsKO ko}) \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ objBitsKO ko) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ objBitsKO ko) ptr = replicate (n * 2 ^ objBitsKO ko) 0) \<and> range_cover ptr sz (objBitsKO ko) n \<and> {ptr..+n * 2 ^ objBitsKO ko} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (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(cte_C); typ_uinfo_t TYPE(?'b) \<noteq> typ_uinfo_t TYPE(8 word)\<rbrakk> \<Longrightarrow> clift (hrs_htd_update (ptr_retyps_gen n (cte_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..+n * 2 ^ objBitsKO ko}) \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ objBitsKO ko) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ objBitsKO ko) ptr = replicate (n * 2 ^ objBitsKO ko) 0) \<and> range_cover ptr sz (objBitsKO ko) n \<and> {ptr..+n * 2 ^ objBitsKO ko} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (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(cte_C); typ_uinfo_t TYPE(?'b) \<noteq> typ_uinfo_t TYPE(8 word)\<rbrakk> \<Longrightarrow> clift (hrs_htd_update (ptr_retyps_gen n (cte_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..+n * 2 ^ objBitsKO ko}) \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ objBitsKO ko) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ objBitsKO ko) ptr = replicate (n * 2 ^ objBitsKO ko) 0) \<and> range_cover ptr sz (objBitsKO ko) n \<and> {ptr..+n * 2 ^ objBitsKO ko} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (state)
this:
\<forall>v. projectKO_opt (KOCTE makeObject) \<noteq> Some v \<Longrightarrow> projectKO_opt \<circ>\<^sub>m (\<lambda>x. if x \<in> set (new_cap_addrs n 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..+n * 2 ^ objBitsKO ko}) \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ objBitsKO ko) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ objBitsKO ko) ptr = replicate (n * 2 ^ objBitsKO ko) 0) \<and> range_cover ptr sz (objBitsKO ko) n \<and> {ptr..+n * 2 ^ objBitsKO ko} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (state)
this:
map_to_ctes (\<lambda>xa. if xa \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace \<sigma> xa) = (\<lambda>x. if x \<in> set (new_cap_addrs n ptr ko) 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..+n * 2 ^ objBitsKO ko}) \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ objBitsKO ko) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ objBitsKO ko) ptr = replicate (n * 2 ^ objBitsKO ko) 0) \<and> range_cover ptr sz (objBitsKO ko) n \<and> {ptr..+n * 2 ^ objBitsKO ko} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (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> ''cte_C'' \<and> typ_name (typ_info_t TYPE(?'b1)) \<noteq> ''cap_C'' \<and> typ_name (typ_info_t TYPE(?'b1)) \<noteq> ''mdb_node_C'' \<and> typ_name (typ_info_t TYPE(?'b1)) \<noteq> ''word0000010'' \<and> typ_name (typ_info_t TYPE(?'b1)) \<noteq> ''word0000010_array_010''; ''cte_C'' \<notin> td_names (typ_info_t TYPE(?'b1)); typ_uinfo_t TYPE(?'b1) \<noteq> typ_uinfo_t TYPE(8 word)\<rbrakk> \<Longrightarrow> h_t_valid (hrs_htd (hrs_htd_update (ptr_retyps_gen n (cte_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..+n * 2 ^ objBitsKO ko}) \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ objBitsKO ko) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ objBitsKO ko) ptr = replicate (n * 2 ^ objBitsKO ko) 0) \<and> range_cover ptr sz (objBitsKO ko) n \<and> {ptr..+n * 2 ^ objBitsKO ko} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<forall>b<n. c_guard (cte_Ptr ptr +\<^sub>p int b) proof (prove)
goal (2 subgoals):
 1. 2 \<le> objBitsKO ko
 2. align_of TYPE(cte_C) = 2\<^sup>2 proof (prove)
goal:
No subgoals! proof (state)
this:
\<forall>b<n. c_guard (cte_Ptr ptr +\<^sub>p int 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..+n * 2 ^ objBitsKO ko}) \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ objBitsKO ko) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ objBitsKO ko) ptr = replicate (n * 2 ^ objBitsKO ko) 0) \<and> range_cover ptr sz (objBitsKO ko) n \<and> {ptr..+n * 2 ^ objBitsKO ko} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (state)
this:
?htd,?gd \<Turnstile>\<^sub>t ?p = (?gd ?p \<and> h_t_array_valid ?htd (PTR_COERCE(cte_C[?'b] \<rightarrow> cte_C) ?p) CARD(?'b))
h_t_array_valid (hrs_htd (t_hrs_' (globals x))) ?p' ?n' \<Longrightarrow> h_t_array_valid (ptr_retyps_gen n (cte_Ptr ptr) ?arr (hrs_htd (t_hrs_' (globals x)))) ?p' ?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..+n * 2 ^ objBitsKO ko}) \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ objBitsKO ko) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ objBitsKO ko) ptr = replicate (n * 2 ^ objBitsKO ko) 0) \<and> range_cover ptr sz (objBitsKO ko) n \<and> {ptr..+n * 2 ^ objBitsKO ko} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (chain)
picking this:
(\<sigma>, x) \<in> rf_sr
?htd,?gd \<Turnstile>\<^sub>t ?p = (?gd ?p \<and> h_t_array_valid ?htd (PTR_COERCE(cte_C[?'b] \<rightarrow> cte_C) ?p) CARD(?'b))
h_t_array_valid (hrs_htd (t_hrs_' (globals x))) ?p' ?n' \<Longrightarrow> h_t_array_valid (ptr_retyps_gen n (cte_Ptr ptr) ?arr (hrs_htd (t_hrs_' (globals x)))) ?p' ?n' proof (prove)
using this:
(\<sigma>, x) \<in> rf_sr
?htd,?gd \<Turnstile>\<^sub>t ?p = (?gd ?p \<and> h_t_array_valid ?htd (PTR_COERCE(cte_C[?'b] \<rightarrow> cte_C) ?p) CARD(?'b))
h_t_array_valid (hrs_htd (t_hrs_' (globals x))) ?p' ?n' \<Longrightarrow> h_t_array_valid (ptr_retyps_gen n (cte_Ptr ptr) ?arr (hrs_htd (t_hrs_' (globals x)))) ?p' ?n'

goal (1 subgoal):
 1. hrs_htd (hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (t_hrs_' (globals x))) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>htd gd p. htd,gd \<Turnstile>\<^sub>t p = (gd p \<and> h_t_array_valid htd (PTR_COERCE(cte_C[?'b1] \<rightarrow> cte_C) p) CARD(?'b1)); \<And>p' n' arr. h_t_array_valid (hrs_htd (t_hrs_' (globals x))) p' n' \<Longrightarrow> h_t_array_valid (ptr_retyps_gen n (cte_Ptr ptr) arr (hrs_htd (t_hrs_' (globals x)))) p' n'; 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> hrs_htd (hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (t_hrs_' (globals x))) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>p' n' arr. h_t_array_valid (hrs_htd (t_hrs_' (globals x))) p' n' \<Longrightarrow> h_t_array_valid (ptr_retyps_gen n (cte_Ptr ptr) arr (hrs_htd (t_hrs_' (globals x)))) p' n'; 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>; c_guard intStateIRQNode_array_Ptr \<and> h_t_array_valid (hrs_htd (t_hrs_' (globals x))) intStateIRQNode_Ptr 256; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; c_guard armKSGlobalPD_Ptr \<and> h_t_array_valid (hrs_htd (t_hrs_' (globals x))) (pde_Ptr (symbol_table ''armKSGlobalPD'')) 4096; {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> h_t_array_valid (ptr_retyps_gen n (cte_Ptr ptr) True (hrs_htd (t_hrs_' (globals x)))) intStateIRQNode_Ptr 256 proof (prove)
goal:
No subgoals! proof (state)
this:
hrs_htd (hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (t_hrs_' (globals x))) \<Turnstile>\<^sub>t intStateIRQNode_array_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..+n * 2 ^ objBitsKO ko}) \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ objBitsKO ko) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ objBitsKO ko) ptr = replicate (n * 2 ^ objBitsKO ko) 0) \<and> range_cover ptr sz (objBitsKO ko) n \<and> {ptr..+n * 2 ^ objBitsKO ko} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (state)
this:
\<lbrakk>?b = ?c; ?c \<Longrightarrow> ?x = ?u; \<not> ?c \<Longrightarrow> ?y = ?v\<rbrakk> \<Longrightarrow> (if ?b then ?x else ?y) = (if ?c then ?u else ?v)

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..+n * 2 ^ objBitsKO ko}) \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ objBitsKO ko) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ objBitsKO ko) ptr = replicate (n * 2 ^ objBitsKO ko) 0) \<and> range_cover ptr sz (objBitsKO ko) n \<and> {ptr..+n * 2 ^ objBitsKO ko} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr proof (state)
this:
\<lbrakk>?b = ?c; ?c \<Longrightarrow> ?x = ?u; \<not> ?c \<Longrightarrow> ?y = ?v\<rbrakk> \<Longrightarrow> (if ?b then ?x else ?y) = (if ?c then ?u else ?v)

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..+n * 2 ^ objBitsKO ko}) \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ objBitsKO ko) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ objBitsKO ko) ptr = replicate (n * 2 ^ objBitsKO ko) 0) \<and> range_cover ptr sz (objBitsKO ko) n \<and> {ptr..+n * 2 ^ objBitsKO ko} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (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..+n * 2 ^ objBitsKO ko}) \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ objBitsKO ko) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ objBitsKO ko) ptr = replicate (n * 2 ^ objBitsKO ko) 0) \<and> range_cover ptr sz (objBitsKO ko) n \<and> {ptr..+n * 2 ^ objBitsKO ko} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (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 n ptr ko) (ksPSpace \<sigma>)) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (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 n ptr ko) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (t_hrs_' (globals x)))) cte_Ptr ccte_relation \<and> cpspace_tcb_relation (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace \<sigma>)) (hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (t_hrs_' (globals x))) \<and> cmap_relation (map_to_eps (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (t_hrs_' (globals x)))) ep_Ptr (cendpoint_relation (clift (hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (t_hrs_' (globals x))))) \<and> cmap_relation (map_to_ntfns (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (t_hrs_' (globals x)))) ntfn_Ptr (cnotification_relation (clift (hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (t_hrs_' (globals x))))) \<and> cmap_relation (map_to_pdes (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (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 n ptr ko) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (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 n ptr ko) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (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 n ptr ko) (ksPSpace \<sigma>)) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (t_hrs_' (globals x))) \<and> cpspace_device_data_relation (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace \<sigma>)) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (t_hrs_' (globals x))) \<and> cpspace_pde_array_relation (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace \<sigma>)) (hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (t_hrs_' (globals x))) \<and> cpspace_pte_array_relation (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace \<sigma>)) (hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (t_hrs_' (globals x))) proof (prove)
goal (1 subgoal):
 1. cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation \<and> cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation \<and> cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)) \<and> cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)) \<and> cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation \<and> cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation \<and> cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation \<and> cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation \<and> cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation \<and> carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr \<and> carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr \<Longrightarrow> cmap_relation (map_to_ctes (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (t_hrs_' (globals x)))) cte_Ptr ccte_relation \<and> cpspace_tcb_relation (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace \<sigma>)) (hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (t_hrs_' (globals x))) \<and> cmap_relation (map_to_eps (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (t_hrs_' (globals x)))) ep_Ptr (cendpoint_relation (clift (hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (t_hrs_' (globals x))))) \<and> cmap_relation (map_to_ntfns (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (t_hrs_' (globals x)))) ntfn_Ptr (cnotification_relation (clift (hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (t_hrs_' (globals x))))) \<and> cmap_relation (map_to_pdes (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (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 n ptr ko) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (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 n ptr ko) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (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 n ptr ko) (ksPSpace \<sigma>)) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (t_hrs_' (globals x))) \<and> cpspace_device_data_relation (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace \<sigma>)) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (t_hrs_' (globals x))) \<and> cpspace_pde_array_relation (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace \<sigma>)) (hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (t_hrs_' (globals x))) \<and> cpspace_pte_array_relation (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace \<sigma>)) (hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (t_hrs_' (globals x))) proof (prove)
goal (1 subgoal):
 1. cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation \<and> cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation \<and> cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)) \<and> cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)) \<and> cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation \<and> cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation \<and> cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation \<and> cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation \<and> cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation \<and> carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr \<and> carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr \<Longrightarrow> cmap_relation (map_to_ctes (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (t_hrs_' (globals x)))) cte_Ptr ccte_relation \<and> cpspace_tcb_relation (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace \<sigma>)) (hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (t_hrs_' (globals x))) \<and> cmap_relation (map_to_eps (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (t_hrs_' (globals x)))) ep_Ptr (cendpoint_relation (clift (hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (t_hrs_' (globals x))))) \<and> cmap_relation (map_to_ntfns (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (t_hrs_' (globals x)))) ntfn_Ptr (cnotification_relation (clift (hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (t_hrs_' (globals x))))) \<and> cmap_relation (map_to_pdes (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (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 n ptr ko) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (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 n ptr ko) (ksPSpace \<sigma>))) (clift (hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (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 n ptr ko) (ksPSpace \<sigma>)) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (t_hrs_' (globals x))) \<and> cpspace_device_data_relation (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace \<sigma>)) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (t_hrs_' (globals x))) \<and> cpspace_pde_array_relation (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace \<sigma>)) (hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (t_hrs_' (globals x))) \<and> cpspace_pte_array_relation (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace \<sigma>)) (hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (t_hrs_' (globals x))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr\<rbrakk> \<Longrightarrow> cmap_relation (\<lambda>x. if x \<in> set (new_cap_addrs n ptr ko) then Some (CTE capability.NullCap nullMDBNode) else ctes_of \<sigma> x) (clift (hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (t_hrs_' (globals x)))) cte_Ptr ccte_relation \<and> cmap_relation (map_to_tcbs (\<lambda>x. if x \<in> set (new_cap_addrs n 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 n 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 n 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 n ptr ko) then Some ko else ksPSpace \<sigma> x)) (cslift x) pde_Ptr cpde_relation \<and> cmap_relation (map_to_ptes (\<lambda>x. if x \<in> set (new_cap_addrs n 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 n 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 n 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 n 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_pde_array_relation (\<lambda>x. if x \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace \<sigma> x) (hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (t_hrs_' (globals x))) \<and> cpspace_pte_array_relation (\<lambda>x. if x \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace \<sigma> x) (hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (t_hrs_' (globals x))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr\<rbrakk> \<Longrightarrow> n * 2 ^ objBitsKO ko < 2 ^ word_bits
 2. \<lbrakk>cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr\<rbrakk> \<Longrightarrow> cmap_relation (\<lambda>x. if x \<in> set (new_cap_addrs n ptr ko) then Some (CTE capability.NullCap nullMDBNode) else ctes_of \<sigma> x) (\<lambda>y. if y \<in> ((+\<^sub>p) (cte_Ptr ptr) \<circ> int) ` {k. k < n} then Some (from_bytes (replicate (2 ^ objBitsKO ko) 0)) else cslift x y) cte_Ptr ccte_relation \<and> cmap_relation (map_to_tcbs (\<lambda>x. if x \<in> set (new_cap_addrs n 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 n 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 n 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 n ptr ko) then Some ko else ksPSpace \<sigma> x)) (cslift x) pde_Ptr cpde_relation \<and> cmap_relation (map_to_ptes (\<lambda>x. if x \<in> set (new_cap_addrs n 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 n 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 n 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 n 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_pde_array_relation (\<lambda>x. if x \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace \<sigma> x) (hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (t_hrs_' (globals x))) \<and> cpspace_pte_array_relation (\<lambda>x. if x \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace \<sigma> x) (hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (t_hrs_' (globals x))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr\<rbrakk> \<Longrightarrow> cmap_relation (\<lambda>x. if x \<in> set (new_cap_addrs n ptr ko) then Some (CTE capability.NullCap nullMDBNode) else ctes_of \<sigma> x) (\<lambda>y. if y \<in> ((+\<^sub>p) (cte_Ptr ptr) \<circ> int) ` {k. k < n} then Some (from_bytes (replicate (2 ^ objBitsKO ko) 0)) else cslift x y) cte_Ptr ccte_relation \<and> cmap_relation (map_to_tcbs (\<lambda>x. if x \<in> set (new_cap_addrs n 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 n 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 n 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 n ptr ko) then Some ko else ksPSpace \<sigma> x)) (cslift x) pde_Ptr cpde_relation \<and> cmap_relation (map_to_ptes (\<lambda>x. if x \<in> set (new_cap_addrs n 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 n 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 n 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 n 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_pde_array_relation (\<lambda>x. if x \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace \<sigma> x) (hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (t_hrs_' (globals x))) \<and> cpspace_pte_array_relation (\<lambda>x. if x \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace \<sigma> x) (hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (t_hrs_' (globals x))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr\<rbrakk> \<Longrightarrow> cmap_relation (\<lambda>x. if x \<in> set (new_cap_addrs n ptr ko) then Some (CTE capability.NullCap nullMDBNode) else ctes_of \<sigma> x) (\<lambda>y. if y \<in> cte_Ptr ` set (new_cap_addrs n ptr ko) then Some (from_bytes (replicate (2 ^ objBitsKO ko) 0)) else cslift x y) cte_Ptr ccte_relation \<and> cmap_relation (map_to_tcbs (\<lambda>x. if x \<in> set (new_cap_addrs n 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 n 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 n 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 n ptr ko) then Some ko else ksPSpace \<sigma> x)) (cslift x) pde_Ptr cpde_relation \<and> cmap_relation (map_to_ptes (\<lambda>x. if x \<in> set (new_cap_addrs n 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 n 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 n 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 n 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 pdBits (map_to_pdes (\<lambda>x. if x \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace \<sigma> x)) (c_h_t_valid x) pd_Ptr \<and> carray_map_relation ptBits (map_to_ptes (\<lambda>x. if x \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace \<sigma> x)) (c_h_t_valid x) pt_Ptr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr\<rbrakk> \<Longrightarrow> cmap_relation (\<lambda>x. if x \<in> set (new_cap_addrs n ptr ko) then Some (CTE capability.NullCap nullMDBNode) else ctes_of \<sigma> x) (\<lambda>y. if y \<in> cte_Ptr ` set (new_cap_addrs n ptr ko) then Some (from_bytes (replicate (2 ^ objBitsKO ko) 0)) else cslift x y) cte_Ptr ccte_relation proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr\<rbrakk> \<Longrightarrow> cmap_relation (\<lambda>x. if x \<in> set (new_cap_addrs n ptr (KOCTE makeObject)) then Some (CTE capability.NullCap nullMDBNode) else ctes_of \<sigma> x) (\<lambda>y. if y \<in> cte_Ptr ` set (new_cap_addrs n ptr (KOCTE makeObject)) then Some (from_bytes (replicate (2 ^ objBitsKO (KOCTE makeObject)) 0)) else cslift x y) cte_Ptr ccte_relation proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr\<rbrakk> \<Longrightarrow> cmap_relation (\<lambda>x. if x \<in> set (new_cap_addrs n ptr (KOCTE makeObject)) then Some makeObject else ctes_of \<sigma> x) (\<lambda>y. if y \<in> cte_Ptr ` set (new_cap_addrs n ptr (KOCTE makeObject)) then Some (from_bytes (replicate (2 ^ objBitsKO (KOCTE makeObject)) 0)) else cslift x y) cte_Ptr ccte_relation proof (prove)
goal (1 subgoal):
 1. \<lbrakk>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> ccte_relation makeObject (from_bytes (replicate (2 ^ objBitsKO (KOCTE makeObject)) 0)) proof (prove)
goal:
No subgoals! proof (state)
this:
cpspace_relation (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace \<sigma>)) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (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..+n * 2 ^ objBitsKO ko}) \<sigma> \<and> (region_is_bytes ptr (n * 2 ^ objBitsKO ko) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (n * 2 ^ objBitsKO ko) ptr = replicate (n * 2 ^ objBitsKO ko) 0) \<and> range_cover ptr sz (objBitsKO ko) n \<and> {ptr..+n * 2 ^ objBitsKO ko} \<inter> kernel_data_refs = {} \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (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 n ptr ko) (ksPSpace \<sigma>)) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (t_hrs_' (globals x)))

goal (1 subgoal):
 1. (\<sigma>\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (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 n ptr ko) (ksPSpace \<sigma>)) (underlying_memory (ksMachineState \<sigma>)) (hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (t_hrs_' (globals x)))
(\<sigma>, x) \<in> rf_sr
region_is_bytes ptr (n * 2 ^ objBitsKO ko) x
{ptr..+n * 2 ^ objBitsKO ko} \<inter> kernel_data_refs = {}
hrs_htd (hrs_htd_update (ptr_retyps_gen n (cte_Ptr ptr) True) (t_hrs_' (globals x))) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr
(valid_objs' and untyped_ranges_zero' and caps_overlap_reserved' {ptr..+n * 2 ^ objBitsKO ko}) \<sigma>

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

goal:
No subgoals!