theory StoreWord_C

lemma storeWordUser_rf_sr_upd':
  shows "\<forall>\<sigma> s.
   (\<sigma>, s) \<in> rf_sr \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma>
                   \<and> pointerInUserData ptr \<sigma> \<and> is_aligned ptr 2 \<longrightarrow>
   (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m.
           m(ptr := word_rsplit (w::word32) ! 3, ptr + 1 := word_rsplit w ! 2,
             ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0))
                   (ksMachineState \<sigma>)\<rparr>,
    s\<lparr>globals := globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (Ptr ptr) w) (t_hrs_' (globals s))\<rparr>\<rparr>) \<in> rf_sr"
  (is "\<forall>\<sigma> s. ?P \<sigma> s \<longrightarrow>
    (\<sigma>\<lparr>ksMachineState := ?ms \<sigma>\<rparr>,
     s\<lparr>globals := globals s\<lparr>t_hrs_' := ?ks' s\<rparr>\<rparr>) \<in> rf_sr") proof (intro allI impI) fix \<sigma> s let ?thesis = "(\<sigma>\<lparr>ksMachineState := ?ms \<sigma>\<rparr>, s\<lparr>globals := globals s\<lparr>t_hrs_' := ?ks' s\<rparr>\<rparr>) \<in> rf_sr" let ?ms = "?ms \<sigma>" let ?ks' = "?ks' s" let ?ptr = "Ptr ptr :: word32 ptr" let ?hp = "t_hrs_' (globals s)" assume "?P \<sigma> s" hence rf: "(\<sigma>, s) \<in> rf_sr" and al: "is_aligned ptr 2"
    and pal: "pspace_aligned' \<sigma>" and pdst: "pspace_distinct' \<sigma>"
    and piud: "pointerInUserData ptr \<sigma>" by simp_all define offset where "offset \<equiv> ucast ((ptr && mask pageBits) >> 2) :: 10 word" define base where "base \<equiv> Ptr (ptr && ~~ mask  pageBits) :: user_data_C ptr" from piud obtain old_w where
    old_w: "heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (ptr_val base) = Some old_w" apply (clarsimp simp: heap_to_user_data_def pointerInUserData_def Let_def) apply (drule user_data_at_ko) apply (drule ko_at_projectKO_opt) apply (simp add: base_def) done from rf obtain page :: user_data_C
    where page: "cslift s base = Some page" apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def cpspace_relation_def) apply (erule cmap_relationE1, rule old_w) apply simp done from page have page_def: "page = the (cslift s base)" by simp have size_td_list_map[rule_format, OF order_refl]:
    "\<And>f xs v S. set xs \<subseteq> S \<longrightarrow> (\<forall>x. x \<in> S \<longrightarrow> size_td_pair (f x) = v)
        \<longrightarrow> size_td_list (map f xs) = v * length xs" apply (induct_tac xs) apply simp_all done have user_data_upd:
    "\<And>A f v. heap_update base (user_data_C.words_C_update f v) =
            heap_update (ptr_coerce base) (f (user_data_C.words_C v))" apply (rule ext) apply (simp add: heap_update_def to_bytes_def) apply (simp add: user_data_C_typ_tag user_data_C_tag_def) apply (simp add: final_pad_def Let_def) apply (simp add: align_td_array' cong: if_cong) apply (simp add: ti_typ_pad_combine_def Let_def ti_typ_combine_def adjust_ti_def empty_typ_info_def size_td_array cong: if_cong) apply (simp add: padup_def) apply (simp add: typ_info_array') apply (simp add: size_of_def size_td_list_map) done have ud_split: "\<And>x z. user_data_C.words_C_update (\<lambda>_. x) z = user_data_C x" by (case_tac z, simp) have map_td_list_map:
    "\<And>f xs. map_td_list f xs = map (map_td_pair f) xs" by (induct_tac xs, simp_all) have update_ti_t_Cons_foo:
  "\<And>Cons upd adjs f v v'. \<lbrakk> v = Cons v'; \<And>a ys v. length ys = size_td_pair a
            \<Longrightarrow> update_ti_pair (map_td_pair f a) ys (Cons v) = Cons (update_ti_pair a ys v) \<rbrakk>
      \<Longrightarrow> \<forall>xs. update_ti_list_t (map_td_list f adjs) xs v
     = Cons (update_ti_list_t adjs xs v')" apply (simp add: update_ti_list_t_def split: if_split) apply (induct_tac adjs) apply simp apply clarsimp done note if_cong[cong] have hval:
    "\<And>hp. h_val hp base = user_data_C (h_val hp (ptr_coerce base))" apply (simp add: h_val_def base_def from_bytes_def) apply (simp add: user_data_C_typ_tag user_data_C_tag_def) apply (simp add: final_pad_def Let_def) apply (simp add: align_td_array' cong: if_cong) apply (simp add: ti_typ_pad_combine_def Let_def ti_typ_combine_def adjust_ti_def empty_typ_info_def size_td_array) apply (simp add: padup_def size_of_def typ_info_array' size_td_list_map) apply (simp add: map_td_list_map) apply (rule injD[where f=user_data_C.words_C]) apply (rule injI) apply (case_tac x, case_tac y, simp) apply (simp add: map_td_list_map del: map_map) apply (rule trans, rule_tac acc=user_data_C.words_C
                          and f="map_td_pair (K (K (update_desc user_data_C (\<lambda>a b. user_data_C.words_C a))))"
                          in update_ti_t_acc_foo[rule_format]) apply (clarsimp simp: map_td_list_map typ_info_word
                            adjust_ti_def update_desc_def) apply simp apply simp apply (simp add: update_ti_list_array'[where g="\<lambda>n. typ_info_t TYPE(word32)", OF refl]
                     typ_info_word adjust_ti_def update_desc_def) apply (rule Arrays.cart_eq[THEN iffD2], clarsimp) apply (subst index_fold_update | clarsimp)+ apply (subst if_P, arith)+ apply simp done from and_mask_less_size [of pageBits ptr] have ptr_mask_less: "ptr && mask pageBits >> 2 < 2^10" apply - apply (rule shiftr_less_t2n) apply (simp add: pageBits_def word_size) done hence uoffset:
    "unat offset = unat (ptr && mask pageBits >> 2)" apply (simp add: offset_def) apply (simp add: unat_ucast) apply (simp add: word_less_nat_alt) done have heap_upd:
    "heap_update ?ptr w =
    (\<lambda>hp. heap_update base (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat offset) w) (h_val hp base)) hp)" apply (rule ext) apply (subst user_data_upd) apply (subst hval) apply (unfold base_def uoffset) apply simp apply (subst heap_update_Array_element) apply (insert ptr_mask_less)[1] apply (simp add: word_less_nat_alt) apply (simp add: ptr_add_def word_shift_by_2 shiftr_shiftl1) apply (simp add: al is_aligned_andI1) apply (simp add: word_plus_and_or_coroll2 add.commute) done have x': "\<And>x::10 word. (ucast x * 4::word32) && ~~ mask pageBits = 0" proof - fix x::"10 word" have "ucast x * 4 = (ucast x << 2 :: word32)" by (simp add: shiftl_t2n) thus "?thesis x" apply simp apply (rule word_eqI) apply (clarsimp simp: word_size nth_shiftl word_ops_nth_size nth_ucast) apply (drule test_bit_size) apply (clarsimp simp: word_size pageBits_def) apply arith done qed have x: "\<And>(x::word32) (y::10 word).
    is_aligned x pageBits \<Longrightarrow> x + ucast y * 4 && ~~ mask pageBits = x" apply (subst mask_out_add_aligned [symmetric], assumption) apply (clarsimp simp: x') done from piud al have relrl: "cmap_relation (heap_to_user_data (ksPSpace \<sigma>)
                                 (underlying_memory (ksMachineState \<sigma>)))
                             (cslift s) Ptr cuser_user_data_relation
    \<Longrightarrow> cmap_relation
        (heap_to_user_data (ksPSpace \<sigma>)
          ((underlying_memory (ksMachineState \<sigma>))(
                   ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2,
                   ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0)))
        (\<lambda>y. if ptr_val y = (ptr_val ?ptr) && ~~ mask pageBits
             then Some (user_data_C.words_C_update
                         (\<lambda>ws. Arrays.update ws (unat (ucast ((ptr && mask pageBits) >> 2) :: 10 word)) w)
                         (the (cslift s y)))
             else cslift s y)
        Ptr cuser_user_data_relation" apply - apply (rule cmap_relationI) apply (clarsimp simp: dom_heap_to_user_data cmap_relation_def dom_if_Some
                   intro!: Un_absorb1 [symmetric]) apply (clarsimp simp: pointerInUserData_def) apply (drule user_data_at_ko) apply (drule ko_at_projectKO_opt) apply (case_tac x) apply clarsimp apply fastforce apply clarsimp apply (case_tac "x = ptr && ~~ mask pageBits") apply (fastforce simp: heap_to_user_data_def Let_def user_data_relation_upd cmap_relation_def
                     dest: bspec) apply clarsimp apply (subgoal_tac "Some v = heap_to_user_data (ksPSpace \<sigma>)
                             (underlying_memory (ksMachineState \<sigma>)) x") apply (clarsimp simp: heap_to_user_data_def Let_def map_option_case
                    split: option.split_asm) apply (fastforce simp: cmap_relation_def dest: bspec) apply (clarsimp simp: heap_to_user_data_def Let_def) apply (frule (1) cmap_relation_cs_atD) apply simp apply clarsimp apply (drule map_to_ko_atI) apply (rule pal) apply (rule pdst) apply (subgoal_tac "is_aligned x pageBits") prefer 2 apply (clarsimp simp: obj_at'_def objBits_simps simp: projectKOs) apply (subgoal_tac "is_aligned x 2") prefer 2 apply (erule is_aligned_weaken) apply (simp add: pageBits_def) apply (rule ext) apply (subst byte_to_word_heap_upd_neq, assumption+, clarsimp simp: x, simp)+ apply (subst byte_to_word_heap_upd_neq [where n=0, simplified], assumption+) apply (clarsimp simp: x) apply simp done have hrs_mem:
    "\<And>f hp'.
    hrs_mem_update (\<lambda>hp. heap_update base (f (h_val hp base)) hp) hp'
    = hrs_mem_update (heap_update base (f (h_val (hrs_mem hp') base))) hp'" by (simp add: hrs_mem_update_def split_def hrs_mem_def) from page have rl': "typ_uinfo_t TYPE(user_data_C) \<bottom>\<^sub>t typ_uinfo_t TYPE('t :: mem_type) \<Longrightarrow>
    (clift (hrs_mem_update (heap_update ?ptr w) (t_hrs_' (globals s))) :: ('t :: mem_type) typ_heap)
    = cslift s" apply (subst heap_upd) apply (subst hrs_mem) apply (simp add: typ_heap_simps clift_heap_update_same) done have subset: "{ptr..+ 2 ^ 2} \<subseteq> {ptr && ~~ mask pageBits ..+ 2 ^ pageBits}" apply (simp only: upto_intvl_eq al is_aligned_neg_mask2) apply (cut_tac ptr="ptr && ~~ mask pageBits" and x="ptr && mask pageBits"
      in aligned_range_offset_subset, rule is_aligned_neg_mask2) apply (rule is_aligned_andI1[OF al]) apply (simp add: pageBits_def) apply (rule and_mask_less', simp add: pageBits_def) apply (erule order_trans[rotated]) apply (simp add: mask_out_sub_mask) done hence zr: "\<And>rs. zero_ranges_are_zero rs (hrs_mem_update (heap_update ?ptr w) (t_hrs_' (globals s)))
        = zero_ranges_are_zero rs (t_hrs_' (globals s))" using page apply (clarsimp simp: zero_ranges_are_zero_def hrs_mem_update base_def
                          heap_update_def
          intro!: ball_cong[OF refl] conj_cong[OF refl]) apply (drule region_actually_is_bytes) apply (frule(1) region_is_bytes_disjoint[rotated 2, OF h_t_valid_clift]) apply simp apply (subst heap_list_update_disjoint_same, simp_all) apply ((subst Int_commute)?, erule disjoint_subset2[rotated]) apply (simp add: pageBits_def) done have cmap_relation_heap_cong:
    "\<And>as cs cs' f rel. \<lbrakk> cmap_relation as cs f rel; cs = cs' \<rbrakk> \<Longrightarrow> cmap_relation as cs' f rel" by simp from rf have "cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals s))" unfolding rf_sr_def cstate_relation_def by (simp add: Let_def) hence "cpspace_relation (ksPSpace \<sigma>) (underlying_memory ?ms) ?ks'" unfolding cpspace_relation_def using page apply - apply (clarsimp simp: rl' tag_disj_via_td_name) apply (drule relrl) apply (simp add: heap_upd) apply (subst hrs_mem) apply (simp add: base_def offset_def) apply (rule conjI) apply (erule cmap_relation_heap_cong) apply (simp add: typ_heap_simps') apply (rule ext) apply clarsimp apply (case_tac y) apply (clarsimp split: if_split) apply (rule cmap_relationI) apply (clarsimp simp: dom_heap_to_device_data cmap_relation_def dom_if_Some
                  intro!: Un_absorb1 [symmetric]) using pal apply (subst(asm) heap_to_device_data_seperate) apply (simp add:piud al du_ptr_disjoint pal pdst)+ apply (subst(asm) heap_to_device_data_seperate) apply (simp add:piud al du_ptr_disjoint pal pdst)+ apply (subst(asm) heap_to_device_data_seperate) apply (simp add:piud al du_ptr_disjoint pal pdst)+ apply (subst(asm) heap_to_device_data_seperate) apply (simp add:piud al du_ptr_disjoint pal pdst)+ apply (erule cmap_relation_relI[where rel = cuser_user_data_device_relation]) apply simp+ done thus ?thesis using rf 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 carch_globals_def) apply (simp add: rl' tag_disj_via_td_name zr) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma> s. (\<sigma>, s) \<in> rf_sr \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pointerInUserData ptr \<sigma> \<and> is_aligned ptr 2 \<longrightarrow> (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>)\<rparr>, s\<lparr>globals := globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))\<rparr>\<rparr>) \<in> rf_sr proof (state)
goal (1 subgoal):
 1. \<And>\<sigma> s. (\<sigma>, s) \<in> rf_sr \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pointerInUserData ptr \<sigma> \<and> is_aligned ptr 2 \<Longrightarrow> (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>)\<rparr>, s\<lparr>globals := globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))\<rparr>\<rparr>) \<in> rf_sr proof (state)
goal (1 subgoal):
 1. \<And>\<sigma> s. (\<sigma>, s) \<in> rf_sr \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pointerInUserData ptr \<sigma> \<and> is_aligned ptr 2 \<Longrightarrow> (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>)\<rparr>, s\<lparr>globals := globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))\<rparr>\<rparr>) \<in> rf_sr proof (state)
goal (1 subgoal):
 1. \<And>\<sigma> s. (\<sigma>, s) \<in> rf_sr \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pointerInUserData ptr \<sigma> \<and> is_aligned ptr 2 \<Longrightarrow> (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>)\<rparr>, s\<lparr>globals := globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))\<rparr>\<rparr>) \<in> rf_sr proof (state)
goal (1 subgoal):
 1. \<And>\<sigma> s. (\<sigma>, s) \<in> rf_sr \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pointerInUserData ptr \<sigma> \<and> is_aligned ptr 2 \<Longrightarrow> (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>)\<rparr>, s\<lparr>globals := globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))\<rparr>\<rparr>) \<in> rf_sr proof (state)
goal (1 subgoal):
 1. \<And>\<sigma> s. (\<sigma>, s) \<in> rf_sr \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pointerInUserData ptr \<sigma> \<and> is_aligned ptr 2 \<Longrightarrow> (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>)\<rparr>, s\<lparr>globals := globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))\<rparr>\<rparr>) \<in> rf_sr proof (state)
goal (1 subgoal):
 1. \<And>\<sigma> s. (\<sigma>, s) \<in> rf_sr \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pointerInUserData ptr \<sigma> \<and> is_aligned ptr 2 \<Longrightarrow> (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>)\<rparr>, s\<lparr>globals := globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))\<rparr>\<rparr>) \<in> rf_sr proof (state)
goal (1 subgoal):
 1. \<And>\<sigma> s. (\<sigma>, s) \<in> rf_sr \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pointerInUserData ptr \<sigma> \<and> is_aligned ptr 2 \<Longrightarrow> (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>)\<rparr>, s\<lparr>globals := globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))\<rparr>\<rparr>) \<in> rf_sr proof (state)
this:
(\<sigma>, s) \<in> rf_sr \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pointerInUserData ptr \<sigma> \<and> is_aligned ptr 2

goal (1 subgoal):
 1. \<And>\<sigma> s. (\<sigma>, s) \<in> rf_sr \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pointerInUserData ptr \<sigma> \<and> is_aligned ptr 2 \<Longrightarrow> (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>)\<rparr>, s\<lparr>globals := globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
using this:
(\<sigma>, s) \<in> rf_sr \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pointerInUserData ptr \<sigma> \<and> is_aligned ptr 2

goal (1 subgoal):
 1. ((\<sigma>, s) \<in> rf_sr &&& is_aligned ptr 2) &&& pspace_aligned' \<sigma> &&& pspace_distinct' \<sigma> &&& pointerInUserData ptr \<sigma> proof (state)
this:
(\<sigma>, s) \<in> rf_sr
is_aligned ptr 2
pspace_aligned' \<sigma>
pspace_distinct' \<sigma>
pointerInUserData ptr \<sigma>

goal (1 subgoal):
 1. \<And>\<sigma> s. (\<sigma>, s) \<in> rf_sr \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pointerInUserData ptr \<sigma> \<and> is_aligned ptr 2 \<Longrightarrow> (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>)\<rparr>, s\<lparr>globals := globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))\<rparr>\<rparr>) \<in> rf_sr proof (state)
this:
offset \<equiv> UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2)

goal (1 subgoal):
 1. \<And>\<sigma> s. (\<sigma>, s) \<in> rf_sr \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pointerInUserData ptr \<sigma> \<and> is_aligned ptr 2 \<Longrightarrow> (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>)\<rparr>, s\<lparr>globals := globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))\<rparr>\<rparr>) \<in> rf_sr proof (state)
this:
base \<equiv> PTR(user_data_C) (ptr && ~~ mask pageBits)

goal (1 subgoal):
 1. \<And>\<sigma> s. (\<sigma>, s) \<in> rf_sr \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pointerInUserData ptr \<sigma> \<and> is_aligned ptr 2 \<Longrightarrow> (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>)\<rparr>, s\<lparr>globals := globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))\<rparr>\<rparr>) \<in> rf_sr proof (chain)
picking this:
pointerInUserData ptr \<sigma> proof (prove)
using this:
pointerInUserData ptr \<sigma>

goal (1 subgoal):
 1. (\<And>old_w. heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (ptr_val base) = Some old_w \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>z. map_to_user_data (ksPSpace \<sigma>) (ptr_val base) = Some z \<Longrightarrow> thesis; typ_at' UserDataT (ptr && ~~ mask pageBits) \<sigma>\<rbrakk> \<Longrightarrow> thesis proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>z. map_to_user_data (ksPSpace \<sigma>) (ptr_val base) = Some z \<Longrightarrow> thesis; ko_at' UserData (ptr && ~~ mask pageBits) \<sigma>\<rbrakk> \<Longrightarrow> thesis proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>z. map_to_user_data (ksPSpace \<sigma>) (ptr_val base) = Some z \<Longrightarrow> thesis; map_to_user_data (ksPSpace \<sigma>) (ptr && ~~ mask pageBits) = Some UserData\<rbrakk> \<Longrightarrow> thesis proof (prove)
goal:
No subgoals! proof (state)
this:
heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (ptr_val base) = Some old_w

goal (1 subgoal):
 1. \<And>\<sigma> s. (\<sigma>, s) \<in> rf_sr \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pointerInUserData ptr \<sigma> \<and> is_aligned ptr 2 \<Longrightarrow> (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>)\<rparr>, s\<lparr>globals := globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))\<rparr>\<rparr>) \<in> rf_sr proof (chain)
picking this:
(\<sigma>, s) \<in> rf_sr proof (prove)
using this:
(\<sigma>, s) \<in> rf_sr

goal (1 subgoal):
 1. (\<And>page. cslift s base = Some page \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>page. cslift s base = Some page \<Longrightarrow> thesis; cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift s) ep_Ptr (cendpoint_relation (cslift s)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift s) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift s) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift s) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid s) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid s) pt_Ptr; cready_queues_relation (cslift s) (ksReadyQueues_' (globals s)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals s)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals s) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals s)); carch_state_relation (ksArchState \<sigma>) (globals s); cmachine_state_relation (ksMachineState \<sigma>) (globals s); cte_array_relation \<sigma> (globals s); tcb_cte_array_relation \<sigma> (globals s); apsnd fst (ghost'state_' (globals s)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals s)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals s) = ksWorkUnitsCompleted \<sigma>; s \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; s \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s))); - 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 s) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals s) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals s) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> thesis proof (prove)
goal (1 subgoal):
 1. \<And>y'. \<lbrakk>\<And>page. cslift s base = Some page \<Longrightarrow> thesis; cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift s) ep_Ptr (cendpoint_relation (cslift s)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift s) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift s) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift s) ap_Ptr casid_pool_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid s) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid s) pt_Ptr; cready_queues_relation (cslift s) (ksReadyQueues_' (globals s)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals s)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals s) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals s)); carch_state_relation (ksArchState \<sigma>) (globals s); cmachine_state_relation (ksMachineState \<sigma>) (globals s); cte_array_relation \<sigma> (globals s); tcb_cte_array_relation \<sigma> (globals s); apsnd fst (ghost'state_' (globals s)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals s)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals s) = ksWorkUnitsCompleted \<sigma>; s \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; s \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s))); - 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 s) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals s) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals s) = ksDomainTime \<sigma>; heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (ptr_val base) = Some old_w; cuser_user_data_relation old_w y'; cslift s (PTR(user_data_C) (ptr_val base)) = Some y'\<rbrakk> \<Longrightarrow> thesis proof (prove)
goal:
No subgoals! proof (state)
this:
cslift s base = Some page

goal (1 subgoal):
 1. \<And>\<sigma> s. (\<sigma>, s) \<in> rf_sr \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pointerInUserData ptr \<sigma> \<and> is_aligned ptr 2 \<Longrightarrow> (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>)\<rparr>, s\<lparr>globals := globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))\<rparr>\<rparr>) \<in> rf_sr proof (chain)
picking this:
cslift s base = Some page proof (prove)
using this:
cslift s base = Some page

goal (1 subgoal):
 1. page = the (cslift s base) proof (state)
this:
page = the (cslift s base)

goal (1 subgoal):
 1. \<And>\<sigma> s. (\<sigma>, s) \<in> rf_sr \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pointerInUserData ptr \<sigma> \<and> is_aligned ptr 2 \<Longrightarrow> (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>)\<rparr>, s\<lparr>globals := globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>f xs v S. set xs \<subseteq> S \<longrightarrow> (\<forall>x. x \<in> S \<longrightarrow> size_td_pair (f x) = v) \<longrightarrow> size_td_list (map f xs) = v * length xs proof (prove)
goal (2 subgoals):
 1. \<And>f xs v S. set [] \<subseteq> S \<longrightarrow> (\<forall>x. x \<in> S \<longrightarrow> size_td_pair (f x) = v) \<longrightarrow> size_td_list (map f []) = v * length []
 2. \<And>f xs v S x1 x2. set x2 \<subseteq> S \<longrightarrow> (\<forall>x. x \<in> S \<longrightarrow> size_td_pair (f x) = v) \<longrightarrow> size_td_list (map f x2) = v * length x2 \<Longrightarrow> set (x1 # x2) \<subseteq> S \<longrightarrow> (\<forall>x. x \<in> S \<longrightarrow> size_td_pair (f x) = v) \<longrightarrow> size_td_list (map f (x1 # x2)) = v * length (x1 # x2) proof (prove)
goal:
No subgoals! proof (state)
this:
(\<And>x. x \<in> set ?xs \<Longrightarrow> size_td_pair (?f x) = ?v) \<Longrightarrow> size_td_list (map ?f ?xs) = ?v * length ?xs

goal (1 subgoal):
 1. \<And>\<sigma> s. (\<sigma>, s) \<in> rf_sr \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pointerInUserData ptr \<sigma> \<and> is_aligned ptr 2 \<Longrightarrow> (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>)\<rparr>, s\<lparr>globals := globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>A f v. heap_update base (user_data_C.words_C_update f v) = heap_update (PTR_COERCE(user_data_C \<rightarrow> 32 word[1024]) base) (f (user_data_C.words_C v)) proof (prove)
goal (1 subgoal):
 1. \<And>A f v x. heap_update base (user_data_C.words_C_update f v) x = heap_update (PTR_COERCE(user_data_C \<rightarrow> 32 word[1024]) base) (f (user_data_C.words_C v)) x proof (prove)
goal (1 subgoal):
 1. \<And>f v x. heap_update_list (ptr_val base) (access_ti (typ_info_t TYPE(user_data_C)) (user_data_C.words_C_update f v) (heap_list x 4096 (ptr_val base))) x = heap_update_list (ptr_val base) (access_ti (typ_info_t TYPE(32 word[1024])) (f (user_data_C.words_C v)) (heap_list x 4096 (ptr_val base))) x proof (prove)
goal (1 subgoal):
 1. \<And>f v x. heap_update_list (ptr_val base) (access_ti (final_pad (ti_typ_pad_combine TYPE(32 word[1024]) user_data_C.words_C (user_data_C.words_C_update \<circ> (\<lambda>x _. x)) ''words_C'' (empty_typ_info ''user_data_C''))) (user_data_C.words_C_update f v) (heap_list x 4096 (ptr_val base))) x = heap_update_list (ptr_val base) (access_ti (typ_info_t TYPE(32 word[1024])) (f (user_data_C.words_C v)) (heap_list x 4096 (ptr_val base))) x proof (prove)
goal (1 subgoal):
 1. \<And>f v x. heap_update_list (ptr_val base) (access_ti (if 0 < padup (2 ^ align_td (typ_info_t TYPE(32 word[1024]))) (size_td (ti_typ_pad_combine TYPE(32 word[1024]) user_data_C.words_C (user_data_C.words_C_update \<circ> (\<lambda>x _. x)) ''words_C'' (empty_typ_info ''user_data_C''))) then ti_pad_combine (padup (2 ^ align_td (typ_info_t TYPE(32 word[1024]))) (size_td (ti_typ_pad_combine TYPE(32 word[1024]) user_data_C.words_C (user_data_C.words_C_update \<circ> (\<lambda>x _. x)) ''words_C'' (empty_typ_info ''user_data_C'')))) (ti_typ_pad_combine TYPE(32 word[1024]) user_data_C.words_C (user_data_C.words_C_update \<circ> (\<lambda>x _. x)) ''words_C'' (empty_typ_info ''user_data_C'')) else ti_typ_pad_combine TYPE(32 word[1024]) user_data_C.words_C (user_data_C.words_C_update \<circ> (\<lambda>x _. x)) ''words_C'' (empty_typ_info ''user_data_C'')) (user_data_C.words_C_update f v) (heap_list x 4096 (ptr_val base))) x = heap_update_list (ptr_val base) (access_ti (typ_info_t TYPE(32 word[1024])) (f (user_data_C.words_C v)) (heap_list x 4096 (ptr_val base))) x proof (prove)
goal (1 subgoal):
 1. \<And>f v x. heap_update_list (ptr_val base) (access_ti (if 0 < padup 4 (size_td (ti_typ_pad_combine TYPE(32 word[1024]) user_data_C.words_C (user_data_C.words_C_update \<circ> (\<lambda>x _. x)) ''words_C'' (empty_typ_info ''user_data_C''))) then ti_pad_combine (padup 4 (size_td (ti_typ_pad_combine TYPE(32 word[1024]) user_data_C.words_C (user_data_C.words_C_update \<circ> (\<lambda>x _. x)) ''words_C'' (empty_typ_info ''user_data_C'')))) (ti_typ_pad_combine TYPE(32 word[1024]) user_data_C.words_C (user_data_C.words_C_update \<circ> (\<lambda>x _. x)) ''words_C'' (empty_typ_info ''user_data_C'')) else ti_typ_pad_combine TYPE(32 word[1024]) user_data_C.words_C (user_data_C.words_C_update \<circ> (\<lambda>x _. x)) ''words_C'' (empty_typ_info ''user_data_C'')) (user_data_C.words_C_update f v) (heap_list x 4096 (ptr_val base))) x = heap_update_list (ptr_val base) (access_ti (typ_info_t TYPE(32 word[1024])) (f (user_data_C.words_C v)) (heap_list x 4096 (ptr_val base))) x proof (prove)
goal (1 subgoal):
 1. \<And>f v x. heap_update_list (ptr_val base) (access_ti (if 0 < padup 4 4096 then ti_pad_combine (padup 4 4096) (TypDesc (TypAggregate [DTPair (map_td (\<lambda>n algn. update_desc user_data_C.words_C (user_data_C.words_C_update \<circ> (\<lambda>x _. x))) (typ_info_t TYPE(32 word[1024]))) ''words_C'']) ''user_data_C'') else TypDesc (TypAggregate [DTPair (map_td (\<lambda>n algn. update_desc user_data_C.words_C (user_data_C.words_C_update \<circ> (\<lambda>x _. x))) (typ_info_t TYPE(32 word[1024]))) ''words_C'']) ''user_data_C'') (user_data_C.words_C_update f v) (heap_list x 4096 (ptr_val base))) x = heap_update_list (ptr_val base) (access_ti (typ_info_t TYPE(32 word[1024])) (f (user_data_C.words_C v)) (heap_list x 4096 (ptr_val base))) x proof (prove)
goal (1 subgoal):
 1. \<And>f v x. heap_update_list (ptr_val base) (access_ti (map_td (\<lambda>n algn. update_desc user_data_C.words_C (user_data_C.words_C_update \<circ> (\<lambda>x _. x))) (typ_info_t TYPE(32 word[1024]))) (user_data_C.words_C_update f v) (take (size_td (typ_info_t TYPE(32 word[1024]))) (heap_list x 4096 (ptr_val base)))) x = heap_update_list (ptr_val base) (access_ti (typ_info_t TYPE(32 word[1024])) (f (user_data_C.words_C v)) (heap_list x 4096 (ptr_val base))) x proof (prove)
goal (1 subgoal):
 1. \<And>f v x. heap_update_list (ptr_val base) (access_ti_list (map (\<lambda>n. DTPair (adjust_ti (typ_info_t TYPE(32 word)) (\<lambda>x. x.[n]) (\<lambda>x f. Arrays.update f n x)) (replicate n CHR ''1'')) [0..<1024]) (f (user_data_C.words_C v)) (take (size_td_list (map (\<lambda>n. DTPair (adjust_ti (typ_info_t TYPE(32 word)) (\<lambda>x. x.[n]) (\<lambda>x f. Arrays.update f n x)) (replicate n CHR ''1'')) [0..<1024])) (heap_list x 4096 (ptr_val base)))) x = heap_update_list (ptr_val base) (access_ti_list (map (\<lambda>n. DTPair (adjust_ti (typ_info_t TYPE(32 word)) (\<lambda>x. x.[n]) (\<lambda>x f. Arrays.update f n x)) (replicate n CHR ''1'')) [0..<1024]) (f (user_data_C.words_C v)) (heap_list x 4096 (ptr_val base))) x proof (prove)
goal:
No subgoals! proof (state)
this:
heap_update base (user_data_C.words_C_update ?f2 ?v2) = heap_update (PTR_COERCE(user_data_C \<rightarrow> 32 word[1024]) base) (?f2 (user_data_C.words_C ?v2))

goal (1 subgoal):
 1. \<And>\<sigma> s. (\<sigma>, s) \<in> rf_sr \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pointerInUserData ptr \<sigma> \<and> is_aligned ptr 2 \<Longrightarrow> (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>)\<rparr>, s\<lparr>globals := globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>x z. user_data_C.words_C_update (\<lambda>_. x) z = user_data_C x proof (state)
this:
user_data_C.words_C_update (\<lambda>_. ?x3) ?z3 = user_data_C ?x3

goal (1 subgoal):
 1. \<And>\<sigma> s. (\<sigma>, s) \<in> rf_sr \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pointerInUserData ptr \<sigma> \<and> is_aligned ptr 2 \<Longrightarrow> (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>)\<rparr>, s\<lparr>globals := globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>f xs. map_td_list f xs = map (map_td_pair f) xs proof (state)
this:
map_td_list ?f3 ?xs3 = map (map_td_pair ?f3) ?xs3

goal (1 subgoal):
 1. \<And>\<sigma> s. (\<sigma>, s) \<in> rf_sr \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pointerInUserData ptr \<sigma> \<and> is_aligned ptr 2 \<Longrightarrow> (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>)\<rparr>, s\<lparr>globals := globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>Cons upd adjs f v v'. \<lbrakk>v = Cons v'; \<And>a ys v. length ys = size_td_pair a \<Longrightarrow> update_ti_pair (map_td_pair f a) ys (Cons v) = Cons (update_ti_pair a ys v)\<rbrakk> \<Longrightarrow> \<forall>xs. update_ti_list_t (map_td_list f adjs) xs v = Cons (update_ti_list_t adjs xs v') proof (prove)
goal (1 subgoal):
 1. \<And>Cons adjs f v v'. \<lbrakk>v = Cons v'; \<And>a ys v. length ys = size_td_pair a \<Longrightarrow> update_ti_pair (map_td_pair f a) ys (Cons v) = Cons (update_ti_pair a ys v)\<rbrakk> \<Longrightarrow> \<forall>xs. length xs = size_td_list adjs \<longrightarrow> update_ti_list (map_td_list f adjs) xs (Cons v') = Cons (update_ti_list adjs xs v') proof (prove)
goal (2 subgoals):
 1. \<And>Cons adjs f v v'. \<lbrakk>v = Cons v'; \<And>a ys v. length ys = size_td_pair a \<Longrightarrow> update_ti_pair (map_td_pair f a) ys (Cons v) = Cons (update_ti_pair a ys v)\<rbrakk> \<Longrightarrow> \<forall>xs. length xs = size_td_list [] \<longrightarrow> update_ti_list (map_td_list f []) xs (Cons v') = Cons (update_ti_list [] xs v')
 2. \<And>Consa adjs f v v' x1 x2. \<lbrakk>v = Consa v'; \<And>a ys v. length ys = size_td_pair a \<Longrightarrow> update_ti_pair (map_td_pair f a) ys (Consa v) = Consa (update_ti_pair a ys v); \<forall>xs. length xs = size_td_list x2 \<longrightarrow> update_ti_list (map_td_list f x2) xs (Consa v') = Consa (update_ti_list x2 xs v')\<rbrakk> \<Longrightarrow> \<forall>xs. length xs = size_td_list (x1 # x2) \<longrightarrow> update_ti_list (map_td_list f (x1 # x2)) xs (Consa v') = Consa (update_ti_list (x1 # x2) xs v') proof (prove)
goal (1 subgoal):
 1. \<And>Consa adjs f v v' x1 x2. \<lbrakk>v = Consa v'; \<And>a ys v. length ys = size_td_pair a \<Longrightarrow> update_ti_pair (map_td_pair f a) ys (Consa v) = Consa (update_ti_pair a ys v); \<forall>xs. length xs = size_td_list x2 \<longrightarrow> update_ti_list (map_td_list f x2) xs (Consa v') = Consa (update_ti_list x2 xs v')\<rbrakk> \<Longrightarrow> \<forall>xs. length xs = size_td_list (x1 # x2) \<longrightarrow> update_ti_list (map_td_list f (x1 # x2)) xs (Consa v') = Consa (update_ti_list (x1 # x2) xs v') proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrakk>?v4 = ?Cons4 ?v'4; \<And>a ys v. length ys = size_td_pair a \<Longrightarrow> update_ti_pair (map_td_pair ?f4 a) ys (?Cons4 v) = ?Cons4 (update_ti_pair a ys v)\<rbrakk> \<Longrightarrow> \<forall>xs. update_ti_list_t (map_td_list ?f4 ?adjs4) xs ?v4 = ?Cons4 (update_ti_list_t ?adjs4 xs ?v'4)

goal (1 subgoal):
 1. \<And>\<sigma> s. (\<sigma>, s) \<in> rf_sr \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pointerInUserData ptr \<sigma> \<and> is_aligned ptr 2 \<Longrightarrow> (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>)\<rparr>, s\<lparr>globals := globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))\<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> s. (\<sigma>, s) \<in> rf_sr \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pointerInUserData ptr \<sigma> \<and> is_aligned ptr 2 \<Longrightarrow> (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>)\<rparr>, s\<lparr>globals := globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>hp. h_val hp base = user_data_C (h_val hp (PTR_COERCE(user_data_C \<rightarrow> 32 word[1024]) base)) proof (prove)
goal (1 subgoal):
 1. \<And>hp. update_ti_t (typ_info_t TYPE(user_data_C)) (heap_list hp 4096 (ptr && ~~ mask pageBits)) undefined = user_data_C (update_ti_t (typ_info_t TYPE(32 word[1024])) (heap_list hp 4096 (ptr && ~~ mask pageBits)) undefined) proof (prove)
goal (1 subgoal):
 1. \<And>hp. update_ti_t (final_pad (ti_typ_pad_combine TYPE(32 word[1024]) user_data_C.words_C (user_data_C.words_C_update \<circ> (\<lambda>x _. x)) ''words_C'' (empty_typ_info ''user_data_C''))) (heap_list hp 4096 (ptr && ~~ mask pageBits)) undefined = user_data_C (update_ti_t (typ_info_t TYPE(32 word[1024])) (heap_list hp 4096 (ptr && ~~ mask pageBits)) undefined) proof (prove)
goal (1 subgoal):
 1. \<And>hp. update_ti_t (if 0 < padup (2 ^ align_td (typ_info_t TYPE(32 word[1024]))) (size_td (ti_typ_pad_combine TYPE(32 word[1024]) user_data_C.words_C (user_data_C.words_C_update \<circ> (\<lambda>x _. x)) ''words_C'' (empty_typ_info ''user_data_C''))) then ti_pad_combine (padup (2 ^ align_td (typ_info_t TYPE(32 word[1024]))) (size_td (ti_typ_pad_combine TYPE(32 word[1024]) user_data_C.words_C (user_data_C.words_C_update \<circ> (\<lambda>x _. x)) ''words_C'' (empty_typ_info ''user_data_C'')))) (ti_typ_pad_combine TYPE(32 word[1024]) user_data_C.words_C (user_data_C.words_C_update \<circ> (\<lambda>x _. x)) ''words_C'' (empty_typ_info ''user_data_C'')) else ti_typ_pad_combine TYPE(32 word[1024]) user_data_C.words_C (user_data_C.words_C_update \<circ> (\<lambda>x _. x)) ''words_C'' (empty_typ_info ''user_data_C'')) (heap_list hp 4096 (ptr && ~~ mask pageBits)) undefined = user_data_C (update_ti_t (typ_info_t TYPE(32 word[1024])) (heap_list hp 4096 (ptr && ~~ mask pageBits)) undefined) proof (prove)
goal (1 subgoal):
 1. \<And>hp. update_ti_t (if 0 < padup 4 (size_td (ti_typ_pad_combine TYPE(32 word[1024]) user_data_C.words_C (user_data_C.words_C_update \<circ> (\<lambda>x _. x)) ''words_C'' (empty_typ_info ''user_data_C''))) then ti_pad_combine (padup 4 (size_td (ti_typ_pad_combine TYPE(32 word[1024]) user_data_C.words_C (user_data_C.words_C_update \<circ> (\<lambda>x _. x)) ''words_C'' (empty_typ_info ''user_data_C'')))) (ti_typ_pad_combine TYPE(32 word[1024]) user_data_C.words_C (user_data_C.words_C_update \<circ> (\<lambda>x _. x)) ''words_C'' (empty_typ_info ''user_data_C'')) else ti_typ_pad_combine TYPE(32 word[1024]) user_data_C.words_C (user_data_C.words_C_update \<circ> (\<lambda>x _. x)) ''words_C'' (empty_typ_info ''user_data_C'')) (heap_list hp 4096 (ptr && ~~ mask pageBits)) undefined = user_data_C (update_ti_t (typ_info_t TYPE(32 word[1024])) (heap_list hp 4096 (ptr && ~~ mask pageBits)) undefined) proof (prove)
goal (1 subgoal):
 1. \<And>hp. update_ti_t (if 0 < padup 4 4096 then ti_pad_combine (padup 4 4096) (TypDesc (TypAggregate [DTPair (map_td (\<lambda>n algn. update_desc user_data_C.words_C (user_data_C.words_C_update \<circ> (\<lambda>x _. x))) (typ_info_t TYPE(32 word[1024]))) ''words_C'']) ''user_data_C'') else TypDesc (TypAggregate [DTPair (map_td (\<lambda>n algn. update_desc user_data_C.words_C (user_data_C.words_C_update \<circ> (\<lambda>x _. x))) (typ_info_t TYPE(32 word[1024]))) ''words_C'']) ''user_data_C'') (heap_list hp 4096 (ptr && ~~ mask pageBits)) undefined = user_data_C (update_ti_t (typ_info_t TYPE(32 word[1024])) (heap_list hp 4096 (ptr && ~~ mask pageBits)) undefined) proof (prove)
goal (1 subgoal):
 1. \<And>hp. update_ti_list_t (map_td_list (\<lambda>n algn. update_desc user_data_C.words_C (user_data_C.words_C_update \<circ> (\<lambda>x _. x))) (map (\<lambda>n. DTPair (adjust_ti (typ_info_t TYPE(32 word)) (\<lambda>x. x.[n]) (\<lambda>x f. Arrays.update f n x)) (replicate n CHR ''1'')) [0..<1024])) (heap_list hp 4096 (ptr && ~~ mask pageBits)) undefined = user_data_C (update_ti_list_t (map (\<lambda>n. DTPair (adjust_ti (typ_info_t TYPE(32 word)) (\<lambda>x. x.[n]) (\<lambda>x f. Arrays.update f n x)) (replicate n CHR ''1'')) [0..<1024]) (heap_list hp 4096 (ptr && ~~ mask pageBits)) undefined) proof (prove)
goal (1 subgoal):
 1. \<And>hp. update_ti_list_t (map (map_td_pair (\<lambda>n algn. update_desc user_data_C.words_C (user_data_C.words_C_update \<circ> (\<lambda>x _. x))) \<circ> (\<lambda>n. DTPair (adjust_ti (typ_info_t TYPE(32 word)) (\<lambda>x. x.[n]) (\<lambda>x f. Arrays.update f n x)) (replicate n CHR ''1''))) [0..<1024]) (heap_list hp 4096 (ptr && ~~ mask pageBits)) undefined = user_data_C (update_ti_list_t (map (\<lambda>n. DTPair (adjust_ti (typ_info_t TYPE(32 word)) (\<lambda>x. x.[n]) (\<lambda>x f. Arrays.update f n x)) (replicate n CHR ''1'')) [0..<1024]) (heap_list hp 4096 (ptr && ~~ mask pageBits)) undefined) proof (prove)
goal (2 subgoals):
 1. \<And>hp. inj user_data_C.words_C
 2. \<And>hp. user_data_C.words_C (update_ti_list_t (map (map_td_pair (\<lambda>n algn. update_desc user_data_C.words_C (user_data_C.words_C_update \<circ> (\<lambda>x _. x))) \<circ> (\<lambda>n. DTPair (adjust_ti (typ_info_t TYPE(32 word)) (\<lambda>x. x.[n]) (\<lambda>x f. Arrays.update f n x)) (replicate n CHR ''1''))) [0..<1024]) (heap_list hp 4096 (ptr && ~~ mask pageBits)) undefined) = user_data_C.words_C (user_data_C (update_ti_list_t (map (\<lambda>n. DTPair (adjust_ti (typ_info_t TYPE(32 word)) (\<lambda>x. x.[n]) (\<lambda>x f. Arrays.update f n x)) (replicate n CHR ''1'')) [0..<1024]) (heap_list hp 4096 (ptr && ~~ mask pageBits)) undefined)) proof (prove)
goal (2 subgoals):
 1. \<And>hp x y. user_data_C.words_C x = user_data_C.words_C y \<Longrightarrow> x = y
 2. \<And>hp. user_data_C.words_C (update_ti_list_t (map (map_td_pair (\<lambda>n algn. update_desc user_data_C.words_C (user_data_C.words_C_update \<circ> (\<lambda>x _. x))) \<circ> (\<lambda>n. DTPair (adjust_ti (typ_info_t TYPE(32 word)) (\<lambda>x. x.[n]) (\<lambda>x f. Arrays.update f n x)) (replicate n CHR ''1''))) [0..<1024]) (heap_list hp 4096 (ptr && ~~ mask pageBits)) undefined) = user_data_C.words_C (user_data_C (update_ti_list_t (map (\<lambda>n. DTPair (adjust_ti (typ_info_t TYPE(32 word)) (\<lambda>x. x.[n]) (\<lambda>x f. Arrays.update f n x)) (replicate n CHR ''1'')) [0..<1024]) (heap_list hp 4096 (ptr && ~~ mask pageBits)) undefined)) proof (prove)
goal (1 subgoal):
 1. \<And>hp. user_data_C.words_C (update_ti_list_t (map (map_td_pair (\<lambda>n algn. update_desc user_data_C.words_C (user_data_C.words_C_update \<circ> (\<lambda>x _. x))) \<circ> (\<lambda>n. DTPair (adjust_ti (typ_info_t TYPE(32 word)) (\<lambda>x. x.[n]) (\<lambda>x f. Arrays.update f n x)) (replicate n CHR ''1''))) [0..<1024]) (heap_list hp 4096 (ptr && ~~ mask pageBits)) undefined) = user_data_C.words_C (user_data_C (update_ti_list_t (map (\<lambda>n. DTPair (adjust_ti (typ_info_t TYPE(32 word)) (\<lambda>x. x.[n]) (\<lambda>x f. Arrays.update f n x)) (replicate n CHR ''1'')) [0..<1024]) (heap_list hp 4096 (ptr && ~~ mask pageBits)) undefined)) proof (prove)
goal (1 subgoal):
 1. \<And>hp. user_data_C.words_C (update_ti_list_t (map (map_td_pair (\<lambda>n algn. update_desc user_data_C.words_C (user_data_C.words_C_update \<circ> (\<lambda>x _. x))) \<circ> (\<lambda>n. DTPair (adjust_ti (typ_info_t TYPE(32 word)) (\<lambda>x. x.[n]) (\<lambda>x f. Arrays.update f n x)) (replicate n CHR ''1''))) [0..<1024]) (heap_list hp 4096 (ptr && ~~ mask pageBits)) undefined) = update_ti_list_t (map (\<lambda>n. DTPair (adjust_ti (typ_info_t TYPE(32 word)) (\<lambda>x. x.[n]) (\<lambda>x f. Arrays.update f n x)) (replicate n CHR ''1'')) [0..<1024]) (heap_list hp 4096 (ptr && ~~ mask pageBits)) undefined proof (prove)
goal (3 subgoals):
 1. \<And>hp a ys v. \<lbrakk>a \<in> set (map (map_td_pair (\<lambda>n algn. update_desc user_data_C.words_C (user_data_C.words_C_update \<circ> (\<lambda>x _. x))) \<circ> (\<lambda>n. DTPair (adjust_ti (typ_info_t TYPE(32 word)) (\<lambda>x. x.[n]) (\<lambda>x f. Arrays.update f n x)) (replicate n CHR ''1''))) [0..<1024]); length ys = size_td_pair a\<rbrakk> \<Longrightarrow> user_data_C.words_C (update_ti_pair a ys v) = update_ti_pair (map_td_pair (K (K (update_desc user_data_C (\<lambda>a b. user_data_C.words_C a)))) a) ys (user_data_C.words_C v)
 2. \<And>hp a. size_td_pair (map_td_pair (K (K (update_desc user_data_C (\<lambda>a b. user_data_C.words_C a)))) a) = size_td_pair a
 3. \<And>hp. update_ti_list_t (map (map_td_pair (K (K (update_desc user_data_C (\<lambda>a b. user_data_C.words_C a))))) (map (map_td_pair (\<lambda>n algn. update_desc user_data_C.words_C (user_data_C.words_C_update \<circ> (\<lambda>x _. x))) \<circ> (\<lambda>n. DTPair (adjust_ti (typ_info_t TYPE(32 word)) (\<lambda>x. x.[n]) (\<lambda>x f. Arrays.update f n x)) (replicate n CHR ''1''))) [0..<1024])) (heap_list hp 4096 (ptr && ~~ mask pageBits)) (user_data_C.words_C undefined) = update_ti_list_t (map (\<lambda>n. DTPair (adjust_ti (typ_info_t TYPE(32 word)) (\<lambda>x. x.[n]) (\<lambda>x f. Arrays.update f n x)) (replicate n CHR ''1'')) [0..<1024]) (heap_list hp 4096 (ptr && ~~ mask pageBits)) undefined proof (prove)
goal (2 subgoals):
 1. \<And>hp a. size_td_pair (map_td_pair (K (K (update_desc user_data_C (\<lambda>a b. user_data_C.words_C a)))) a) = size_td_pair a
 2. \<And>hp. update_ti_list_t (map (map_td_pair (K (K (update_desc user_data_C (\<lambda>a b. user_data_C.words_C a))))) (map (map_td_pair (\<lambda>n algn. update_desc user_data_C.words_C (user_data_C.words_C_update \<circ> (\<lambda>x _. x))) \<circ> (\<lambda>n. DTPair (adjust_ti (typ_info_t TYPE(32 word)) (\<lambda>x. x.[n]) (\<lambda>x f. Arrays.update f n x)) (replicate n CHR ''1''))) [0..<1024])) (heap_list hp 4096 (ptr && ~~ mask pageBits)) (user_data_C.words_C undefined) = update_ti_list_t (map (\<lambda>n. DTPair (adjust_ti (typ_info_t TYPE(32 word)) (\<lambda>x. x.[n]) (\<lambda>x f. Arrays.update f n x)) (replicate n CHR ''1'')) [0..<1024]) (heap_list hp 4096 (ptr && ~~ mask pageBits)) undefined proof (prove)
goal (1 subgoal):
 1. \<And>hp. update_ti_list_t (map (map_td_pair (K (K (update_desc user_data_C (\<lambda>a b. user_data_C.words_C a))))) (map (map_td_pair (\<lambda>n algn. update_desc user_data_C.words_C (user_data_C.words_C_update \<circ> (\<lambda>x _. x))) \<circ> (\<lambda>n. DTPair (adjust_ti (typ_info_t TYPE(32 word)) (\<lambda>x. x.[n]) (\<lambda>x f. Arrays.update f n x)) (replicate n CHR ''1''))) [0..<1024])) (heap_list hp 4096 (ptr && ~~ mask pageBits)) (user_data_C.words_C undefined) = update_ti_list_t (map (\<lambda>n. DTPair (adjust_ti (typ_info_t TYPE(32 word)) (\<lambda>x. x.[n]) (\<lambda>x f. Arrays.update f n x)) (replicate n CHR ''1'')) [0..<1024]) (heap_list hp 4096 (ptr && ~~ mask pageBits)) undefined proof (prove)
goal (1 subgoal):
 1. \<And>hp. update_ti_list_t (map (map_td_pair (\<lambda>y ya. update_desc user_data_C (\<lambda>a b. user_data_C.words_C a)) \<circ> (map_td_pair (\<lambda>n algn. update_desc user_data_C.words_C (user_data_C.words_C_update \<circ> (\<lambda>x _. x))) \<circ> (\<lambda>n. DTPair (adjust_ti (typ_info_t TYPE(32 word)) (\<lambda>x. x.[n]) (\<lambda>x f. Arrays.update f n x)) (replicate n CHR ''1'')))) [0..<1024]) (heap_list hp 4096 (ptr && ~~ mask pageBits)) (user_data_C.words_C undefined) = update_ti_list_t (map (\<lambda>n. DTPair (adjust_ti (typ_info_t TYPE(32 word)) (\<lambda>x. x.[n]) (\<lambda>x f. Arrays.update f n x)) (replicate n CHR ''1'')) [0..<1024]) (heap_list hp 4096 (ptr && ~~ mask pageBits)) undefined proof (prove)
goal (1 subgoal):
 1. \<And>hp. foldr (\<lambda>n arr. Arrays.update arr n ((if 4 \<le> 4096 - 4 * n then \<lambda>v. word_rcat (rev (take 4 (drop (4 * n) (heap_list hp 4096 (ptr && ~~ mask pageBits))))) else id) (arr.[n]))) [0..<1024] (user_data_C.words_C undefined) = foldr (\<lambda>n arr. Arrays.update arr n ((if 4 \<le> 4096 - 4 * n then \<lambda>v. word_rcat (rev (take 4 (drop (4 * n) (heap_list hp 4096 (ptr && ~~ mask pageBits))))) else id) (arr.[n]))) [0..<1024] undefined proof (prove)
goal (1 subgoal):
 1. \<And>hp i. i < 1024 \<Longrightarrow> foldr (\<lambda>n arr. Arrays.update arr n ((if 4 \<le> 4096 - 4 * n then \<lambda>v. word_rcat (rev (take 4 (drop (4 * n) (heap_list hp 4096 (ptr && ~~ mask pageBits))))) else id) (arr.[n]))) [0..<1024] (user_data_C.words_C undefined).[i] = foldr (\<lambda>n arr. Arrays.update arr n ((if 4 \<le> 4096 - 4 * n then \<lambda>v. word_rcat (rev (take 4 (drop (4 * n) (heap_list hp 4096 (ptr && ~~ mask pageBits))))) else id) (arr.[n]))) [0..<1024] undefined.[i] proof (prove)
goal (1 subgoal):
 1. \<And>hp i. i < 1024 \<Longrightarrow> (if 4 \<le> 4096 - 4 * i then \<lambda>v. word_rcat (rev (take 4 (drop (4 * i) (heap_list hp 4096 (ptr && ~~ mask pageBits))))) else id) (user_data_C.words_C undefined.[i]) = (if 4 \<le> 4096 - 4 * i then \<lambda>v. word_rcat (rev (take 4 (drop (4 * i) (heap_list hp 4096 (ptr && ~~ mask pageBits))))) else id) (undefined.[i]) proof (prove)
goal (1 subgoal):
 1. \<And>hp i. i < 1024 \<Longrightarrow> word_rcat (rev (take 4 (drop (4 * i) (heap_list hp 4096 (ptr && ~~ mask pageBits))))) = word_rcat (rev (take 4 (drop (4 * i) (heap_list hp 4096 (ptr && ~~ mask pageBits))))) proof (prove)
goal:
No subgoals! proof (state)
this:
h_val ?hp5 base = user_data_C (h_val ?hp5 (PTR_COERCE(user_data_C \<rightarrow> 32 word[1024]) base))

goal (1 subgoal):
 1. \<And>\<sigma> s. (\<sigma>, s) \<in> rf_sr \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pointerInUserData ptr \<sigma> \<and> is_aligned ptr 2 \<Longrightarrow> (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>)\<rparr>, s\<lparr>globals := globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))\<rparr>\<rparr>) \<in> rf_sr proof (chain)
picking this:
pageBits < size ptr \<Longrightarrow> ptr && mask pageBits < 2 ^ pageBits proof (prove)
using this:
pageBits < size ptr \<Longrightarrow> ptr && mask pageBits < 2 ^ pageBits

goal (1 subgoal):
 1. ptr && mask pageBits >> 2 < 2 ^ 10 proof (prove)
goal (1 subgoal):
 1. (pageBits < size ptr \<Longrightarrow> ptr && mask pageBits < 2 ^ pageBits) \<Longrightarrow> ptr && mask pageBits >> 2 < 2 ^ 10 proof (prove)
goal (1 subgoal):
 1. (pageBits < size ptr \<Longrightarrow> ptr && mask pageBits < 2 ^ pageBits) \<Longrightarrow> ptr && mask pageBits < 2 ^ (2 + 10) proof (prove)
goal:
No subgoals! proof (state)
this:
ptr && mask pageBits >> 2 < 2 ^ 10

goal (1 subgoal):
 1. \<And>\<sigma> s. (\<sigma>, s) \<in> rf_sr \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pointerInUserData ptr \<sigma> \<and> is_aligned ptr 2 \<Longrightarrow> (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>)\<rparr>, s\<lparr>globals := globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
using this:
ptr && mask pageBits >> 2 < 2 ^ 10

goal (1 subgoal):
 1. unat offset = unat (ptr && mask pageBits >> 2) proof (prove)
goal (1 subgoal):
 1. ptr && mask pageBits >> 2 < 0x400 \<Longrightarrow> unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2)) = unat (ptr && mask pageBits >> 2) proof (prove)
goal (1 subgoal):
 1. ptr && mask pageBits >> 2 < 0x400 \<Longrightarrow> unat (ptr && mask pageBits >> 2) mod 1024 = unat (ptr && mask pageBits >> 2) proof (prove)
goal:
No subgoals! proof (state)
this:
unat offset = unat (ptr && mask pageBits >> 2)

goal (1 subgoal):
 1. \<And>\<sigma> s. (\<sigma>, s) \<in> rf_sr \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pointerInUserData ptr \<sigma> \<and> is_aligned ptr 2 \<Longrightarrow> (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>)\<rparr>, s\<lparr>globals := globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. heap_update (PTR(32 word) ptr) w = (\<lambda>hp. heap_update base (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat offset) w) (h_val hp base)) hp) proof (prove)
goal (1 subgoal):
 1. \<And>hp. heap_update (PTR(32 word) ptr) w hp = heap_update base (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat offset) w) (h_val hp base)) hp proof (prove)
goal (1 subgoal):
 1. \<And>hp. heap_update (PTR(32 word) ptr) w hp = heap_update (PTR_COERCE(user_data_C \<rightarrow> 32 word[1024]) base) (Arrays.update (user_data_C.words_C (h_val hp base)) (unat offset) w) hp proof (prove)
goal (1 subgoal):
 1. \<And>hp. heap_update (PTR(32 word) ptr) w hp = heap_update (PTR_COERCE(user_data_C \<rightarrow> 32 word[1024]) base) (Arrays.update (user_data_C.words_C (user_data_C (h_val hp (PTR_COERCE(user_data_C \<rightarrow> 32 word[1024]) base)))) (unat offset) w) hp proof (prove)
goal (1 subgoal):
 1. \<And>hp. heap_update (PTR(32 word) ptr) w hp = heap_update (PTR_COERCE(user_data_C \<rightarrow> 32 word[1024]) (PTR(user_data_C) (ptr && ~~ mask pageBits))) (Arrays.update (user_data_C.words_C (user_data_C (h_val hp (PTR_COERCE(user_data_C \<rightarrow> 32 word[1024]) (PTR(user_data_C) (ptr && ~~ mask pageBits)))))) (unat (ptr && mask pageBits >> 2)) w) hp proof (prove)
goal (1 subgoal):
 1. \<And>hp. heap_update (PTR(32 word) ptr) w hp = heap_update (PTR(32 word[1024]) (ptr && ~~ mask pageBits)) (Arrays.update (h_val hp (PTR(32 word[1024]) (ptr && ~~ mask pageBits))) (unat (ptr && mask pageBits >> 2)) w) hp proof (prove)
goal (2 subgoals):
 1. \<And>hp. unat (ptr && mask pageBits >> 2) < CARD(1024)
 2. \<And>hp. heap_update (PTR(32 word) ptr) w hp = heap_update (PTR_COERCE(32 word[1024] \<rightarrow> 32 word) (PTR(32 word[1024]) (ptr && ~~ mask pageBits)) +\<^sub>p int (unat (ptr && mask pageBits >> 2))) w hp proof (prove)
goal (2 subgoals):
 1. \<And>hp. ptr && mask pageBits >> 2 < 2 ^ 10 \<Longrightarrow> unat (ptr && mask pageBits >> 2) < CARD(1024)
 2. \<And>hp. heap_update (PTR(32 word) ptr) w hp = heap_update (PTR_COERCE(32 word[1024] \<rightarrow> 32 word) (PTR(32 word[1024]) (ptr && ~~ mask pageBits)) +\<^sub>p int (unat (ptr && mask pageBits >> 2))) w hp proof (prove)
goal (1 subgoal):
 1. \<And>hp. heap_update (PTR(32 word) ptr) w hp = heap_update (PTR_COERCE(32 word[1024] \<rightarrow> 32 word) (PTR(32 word[1024]) (ptr && ~~ mask pageBits)) +\<^sub>p int (unat (ptr && mask pageBits >> 2))) w hp proof (prove)
goal (1 subgoal):
 1. \<And>hp. heap_update (PTR(32 word) ptr) w hp = heap_update (PTR(32 word) ((ptr && ~~ mask pageBits) + ((ptr && mask pageBits) && ~~ mask 2))) w hp proof (prove)
goal (1 subgoal):
 1. \<And>hp. heap_update (PTR(32 word) ptr) w hp = heap_update (PTR(32 word) ((ptr && ~~ mask pageBits) + (ptr && mask pageBits))) w hp proof (prove)
goal:
No subgoals! proof (state)
this:
heap_update (PTR(32 word) ptr) w = (\<lambda>hp. heap_update base (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat offset) w) (h_val hp base)) hp)

goal (1 subgoal):
 1. \<And>\<sigma> s. (\<sigma>, s) \<in> rf_sr \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pointerInUserData ptr \<sigma> \<and> is_aligned ptr 2 \<Longrightarrow> (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>)\<rparr>, s\<lparr>globals := globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>x. UCAST(10 \<rightarrow> 32) x * 4 && ~~ mask pageBits = 0 proof (state)
goal (1 subgoal):
 1. \<And>x. UCAST(10 \<rightarrow> 32) x * 4 && ~~ mask pageBits = 0 proof (state)
goal (1 subgoal):
 1. \<And>x. UCAST(10 \<rightarrow> 32) x * 4 && ~~ mask pageBits = 0 proof (prove)
goal (1 subgoal):
 1. UCAST(10 \<rightarrow> 32) x * 4 = UCAST(10 \<rightarrow> 32) x << 2 proof (state)
this:
UCAST(10 \<rightarrow> 32) x * 4 = UCAST(10 \<rightarrow> 32) x << 2

goal (1 subgoal):
 1. \<And>x. UCAST(10 \<rightarrow> 32) x * 4 && ~~ mask pageBits = 0 proof (prove)
using this:
UCAST(10 \<rightarrow> 32) x * 4 = UCAST(10 \<rightarrow> 32) x << 2

goal (1 subgoal):
 1. UCAST(10 \<rightarrow> 32) x * 4 && ~~ mask pageBits = 0 proof (prove)
goal (1 subgoal):
 1. UCAST(10 \<rightarrow> 32) x * 4 = UCAST(10 \<rightarrow> 32) x << 2 \<Longrightarrow> (UCAST(10 \<rightarrow> 32) x << 2) && ~~ mask pageBits = 0 proof (prove)
goal (1 subgoal):
 1. \<And>n. UCAST(10 \<rightarrow> 32) x * 4 = UCAST(10 \<rightarrow> 32) x << 2 \<Longrightarrow> n < size ((UCAST(10 \<rightarrow> 32) x << 2) && ~~ mask pageBits) \<longrightarrow> ((UCAST(10 \<rightarrow> 32) x << 2) && ~~ mask pageBits) !! n = 0 !! n proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>UCAST(10 \<rightarrow> 32) x * 4 = UCAST(10 \<rightarrow> 32) x << 2; n < 32; x !! (n - 2); n - 2 < 32; 2 \<le> n\<rbrakk> \<Longrightarrow> n < pageBits proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>UCAST(10 \<rightarrow> 32) x * 4 = UCAST(10 \<rightarrow> 32) x << 2; n < 32; n - 2 < 32; 2 \<le> n; n - 2 < size x\<rbrakk> \<Longrightarrow> n < pageBits proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>UCAST(10 \<rightarrow> 32) x * 4 = UCAST(10 \<rightarrow> 32) x << 2; n < 32; 2 \<le> n; n - 2 < 10\<rbrakk> \<Longrightarrow> n < 12 proof (prove)
goal:
No subgoals! proof (state)
this:
UCAST(10 \<rightarrow> 32) x * 4 && ~~ mask pageBits = 0

goal:
No subgoals! proof (state)
this:
UCAST(10 \<rightarrow> 32) ?x5 * 4 && ~~ mask pageBits = 0

goal (1 subgoal):
 1. \<And>\<sigma> s. (\<sigma>, s) \<in> rf_sr \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pointerInUserData ptr \<sigma> \<and> is_aligned ptr 2 \<Longrightarrow> (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>)\<rparr>, s\<lparr>globals := globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>x y. is_aligned x pageBits \<Longrightarrow> x + UCAST(10 \<rightarrow> 32) y * 4 && ~~ mask pageBits = x proof (prove)
goal (1 subgoal):
 1. \<And>x y. is_aligned x pageBits \<Longrightarrow> x + (UCAST(10 \<rightarrow> 32) y * 4 && ~~ mask pageBits) = x proof (prove)
goal:
No subgoals! proof (state)
this:
is_aligned ?x5 pageBits \<Longrightarrow> ?x5 + UCAST(10 \<rightarrow> 32) ?y5 * 4 && ~~ mask pageBits = ?x5

goal (1 subgoal):
 1. \<And>\<sigma> s. (\<sigma>, s) \<in> rf_sr \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pointerInUserData ptr \<sigma> \<and> is_aligned ptr 2 \<Longrightarrow> (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>)\<rparr>, s\<lparr>globals := globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))\<rparr>\<rparr>) \<in> rf_sr proof (chain)
picking this:
pointerInUserData ptr \<sigma>
is_aligned ptr 2 proof (prove)
using this:
pointerInUserData ptr \<sigma>
is_aligned ptr 2

goal (1 subgoal):
 1. cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_C) cuser_user_data_relation \<Longrightarrow> cmap_relation (heap_to_user_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0))) (\<lambda>y. if ptr_val y = ptr_val (PTR(32 word) ptr) && ~~ mask pageBits then Some (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s y))) else cslift s y) PTR(user_data_C) cuser_user_data_relation proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_C) cuser_user_data_relation; pointerInUserData ptr \<sigma>; is_aligned ptr 2\<rbrakk> \<Longrightarrow> cmap_relation (heap_to_user_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0))) (\<lambda>y. if ptr_val y = ptr_val (PTR(32 word) ptr) && ~~ mask pageBits then Some (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s y))) else cslift s y) PTR(user_data_C) cuser_user_data_relation proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_C) cuser_user_data_relation; pointerInUserData ptr \<sigma>; is_aligned ptr 2\<rbrakk> \<Longrightarrow> PTR(user_data_C) ` dom (heap_to_user_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0))) = dom (\<lambda>y. if ptr_val y = ptr_val (PTR(32 word) ptr) && ~~ mask pageBits then Some (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s y))) else cslift s y)
 2. \<And>x v v'. \<lbrakk>cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_C) cuser_user_data_relation; pointerInUserData ptr \<sigma>; is_aligned ptr 2; heap_to_user_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0)) x = Some v; (if ptr_val (PTR(user_data_C) x) = ptr_val (PTR(32 word) ptr) && ~~ mask pageBits then Some (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s (PTR(user_data_C) x)))) else cslift s (PTR(user_data_C) x)) = Some v'\<rbrakk> \<Longrightarrow> cuser_user_data_relation v v' proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>pointerInUserData ptr \<sigma>; is_aligned ptr 2; ptr_val x = ptr && ~~ mask pageBits; PTR(user_data_C) ` dom (map_to_user_data (ksPSpace \<sigma>)) = dom (cslift s); \<forall>x\<in>dom (map_to_user_data (ksPSpace \<sigma>)). cuser_user_data_relation (the (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) x)) (the (cslift s (PTR(user_data_C) x)))\<rbrakk> \<Longrightarrow> \<exists>y. cslift s x = Some y
 2. \<And>x v v'. \<lbrakk>cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_C) cuser_user_data_relation; pointerInUserData ptr \<sigma>; is_aligned ptr 2; heap_to_user_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0)) x = Some v; (if ptr_val (PTR(user_data_C) x) = ptr_val (PTR(32 word) ptr) && ~~ mask pageBits then Some (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s (PTR(user_data_C) x)))) else cslift s (PTR(user_data_C) x)) = Some v'\<rbrakk> \<Longrightarrow> cuser_user_data_relation v v' proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>typ_at' UserDataT (ptr && ~~ mask pageBits) \<sigma>; is_aligned ptr 2; ptr_val x = ptr && ~~ mask pageBits; PTR(user_data_C) ` dom (map_to_user_data (ksPSpace \<sigma>)) = dom (cslift s); \<forall>x\<in>dom (map_to_user_data (ksPSpace \<sigma>)). cuser_user_data_relation (the (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) x)) (the (cslift s (PTR(user_data_C) x)))\<rbrakk> \<Longrightarrow> \<exists>y. cslift s x = Some y
 2. \<And>x v v'. \<lbrakk>cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_C) cuser_user_data_relation; pointerInUserData ptr \<sigma>; is_aligned ptr 2; heap_to_user_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0)) x = Some v; (if ptr_val (PTR(user_data_C) x) = ptr_val (PTR(32 word) ptr) && ~~ mask pageBits then Some (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s (PTR(user_data_C) x)))) else cslift s (PTR(user_data_C) x)) = Some v'\<rbrakk> \<Longrightarrow> cuser_user_data_relation v v' proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>is_aligned ptr 2; ptr_val x = ptr && ~~ mask pageBits; PTR(user_data_C) ` dom (map_to_user_data (ksPSpace \<sigma>)) = dom (cslift s); \<forall>x\<in>dom (map_to_user_data (ksPSpace \<sigma>)). cuser_user_data_relation (the (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) x)) (the (cslift s (PTR(user_data_C) x))); ko_at' UserData (ptr && ~~ mask pageBits) \<sigma>\<rbrakk> \<Longrightarrow> \<exists>y. cslift s x = Some y
 2. \<And>x v v'. \<lbrakk>cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_C) cuser_user_data_relation; pointerInUserData ptr \<sigma>; is_aligned ptr 2; heap_to_user_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0)) x = Some v; (if ptr_val (PTR(user_data_C) x) = ptr_val (PTR(32 word) ptr) && ~~ mask pageBits then Some (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s (PTR(user_data_C) x)))) else cslift s (PTR(user_data_C) x)) = Some v'\<rbrakk> \<Longrightarrow> cuser_user_data_relation v v' proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>is_aligned ptr 2; ptr_val x = ptr && ~~ mask pageBits; PTR(user_data_C) ` dom (map_to_user_data (ksPSpace \<sigma>)) = dom (cslift s); \<forall>x\<in>dom (map_to_user_data (ksPSpace \<sigma>)). cuser_user_data_relation (the (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) x)) (the (cslift s (PTR(user_data_C) x))); map_to_user_data (ksPSpace \<sigma>) (ptr && ~~ mask pageBits) = Some UserData\<rbrakk> \<Longrightarrow> \<exists>y. cslift s x = Some y
 2. \<And>x v v'. \<lbrakk>cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_C) cuser_user_data_relation; pointerInUserData ptr \<sigma>; is_aligned ptr 2; heap_to_user_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0)) x = Some v; (if ptr_val (PTR(user_data_C) x) = ptr_val (PTR(32 word) ptr) && ~~ mask pageBits then Some (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s (PTR(user_data_C) x)))) else cslift s (PTR(user_data_C) x)) = Some v'\<rbrakk> \<Longrightarrow> cuser_user_data_relation v v' proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>is_aligned ptr 2; ptr_val x = ptr && ~~ mask pageBits; PTR(user_data_C) ` dom (map_to_user_data (ksPSpace \<sigma>)) = dom (cslift s); \<forall>x\<in>dom (map_to_user_data (ksPSpace \<sigma>)). cuser_user_data_relation (the (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) x)) (the (cslift s (PTR(user_data_C) x))); map_to_user_data (ksPSpace \<sigma>) (ptr && ~~ mask pageBits) = Some UserData; x = PTR(user_data_C) xa\<rbrakk> \<Longrightarrow> \<exists>y. cslift s x = Some y
 2. \<And>x v v'. \<lbrakk>cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_C) cuser_user_data_relation; pointerInUserData ptr \<sigma>; is_aligned ptr 2; heap_to_user_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0)) x = Some v; (if ptr_val (PTR(user_data_C) x) = ptr_val (PTR(32 word) ptr) && ~~ mask pageBits then Some (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s (PTR(user_data_C) x)))) else cslift s (PTR(user_data_C) x)) = Some v'\<rbrakk> \<Longrightarrow> cuser_user_data_relation v v' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 2; PTR(user_data_C) ` dom (map_to_user_data (ksPSpace \<sigma>)) = dom (cslift s); \<forall>x\<in>dom (map_to_user_data (ksPSpace \<sigma>)). cuser_user_data_relation (the (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) x)) (the (cslift s (PTR(user_data_C) x))); map_to_user_data (ksPSpace \<sigma>) (ptr && ~~ mask pageBits) = Some UserData\<rbrakk> \<Longrightarrow> \<exists>y. cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)) = Some y
 2. \<And>x v v'. \<lbrakk>cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_C) cuser_user_data_relation; pointerInUserData ptr \<sigma>; is_aligned ptr 2; heap_to_user_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0)) x = Some v; (if ptr_val (PTR(user_data_C) x) = ptr_val (PTR(32 word) ptr) && ~~ mask pageBits then Some (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s (PTR(user_data_C) x)))) else cslift s (PTR(user_data_C) x)) = Some v'\<rbrakk> \<Longrightarrow> cuser_user_data_relation v v' proof (prove)
goal (1 subgoal):
 1. \<And>x v v'. \<lbrakk>cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_C) cuser_user_data_relation; pointerInUserData ptr \<sigma>; is_aligned ptr 2; heap_to_user_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0)) x = Some v; (if ptr_val (PTR(user_data_C) x) = ptr_val (PTR(32 word) ptr) && ~~ mask pageBits then Some (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s (PTR(user_data_C) x)))) else cslift s (PTR(user_data_C) x)) = Some v'\<rbrakk> \<Longrightarrow> cuser_user_data_relation v v' proof (prove)
goal (1 subgoal):
 1. \<And>x v v'. \<lbrakk>cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_C) cuser_user_data_relation; pointerInUserData ptr \<sigma>; is_aligned ptr 2; heap_to_user_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) x = Some v; (if x = ptr && ~~ mask pageBits then Some (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits))))) else cslift s (PTR(user_data_C) x)) = Some v'\<rbrakk> \<Longrightarrow> cuser_user_data_relation v v' proof (prove)
goal (2 subgoals):
 1. \<And>x v v'. \<lbrakk>cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_C) cuser_user_data_relation; pointerInUserData ptr \<sigma>; is_aligned ptr 2; heap_to_user_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) x = Some v; (if x = ptr && ~~ mask pageBits then Some (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits))))) else cslift s (PTR(user_data_C) x)) = Some v'; x = ptr && ~~ mask pageBits\<rbrakk> \<Longrightarrow> cuser_user_data_relation v v'
 2. \<And>x v v'. \<lbrakk>cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_C) cuser_user_data_relation; pointerInUserData ptr \<sigma>; is_aligned ptr 2; heap_to_user_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) x = Some v; (if x = ptr && ~~ mask pageBits then Some (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits))))) else cslift s (PTR(user_data_C) x)) = Some v'; x \<noteq> ptr && ~~ mask pageBits\<rbrakk> \<Longrightarrow> cuser_user_data_relation v v' proof (prove)
goal (1 subgoal):
 1. \<And>x v v'. \<lbrakk>cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_C) cuser_user_data_relation; pointerInUserData ptr \<sigma>; is_aligned ptr 2; heap_to_user_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) x = Some v; (if x = ptr && ~~ mask pageBits then Some (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits))))) else cslift s (PTR(user_data_C) x)) = Some v'; x \<noteq> ptr && ~~ mask pageBits\<rbrakk> \<Longrightarrow> cuser_user_data_relation v v' proof (prove)
goal (1 subgoal):
 1. \<And>x v v'. \<lbrakk>cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_C) cuser_user_data_relation; pointerInUserData ptr \<sigma>; is_aligned ptr 2; heap_to_user_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) x = Some v; cslift s (PTR(user_data_C) x) = Some v'; x \<noteq> ptr && ~~ mask pageBits\<rbrakk> \<Longrightarrow> cuser_user_data_relation v v' proof (prove)
goal (2 subgoals):
 1. \<And>x v v'. \<lbrakk>cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_C) cuser_user_data_relation; pointerInUserData ptr \<sigma>; is_aligned ptr 2; heap_to_user_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) x = Some v; cslift s (PTR(user_data_C) x) = Some v'; x \<noteq> ptr && ~~ mask pageBits; Some v = heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) x\<rbrakk> \<Longrightarrow> cuser_user_data_relation v v'
 2. \<And>x v v'. \<lbrakk>cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_C) cuser_user_data_relation; pointerInUserData ptr \<sigma>; is_aligned ptr 2; heap_to_user_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) x = Some v; cslift s (PTR(user_data_C) x) = Some v'; x \<noteq> ptr && ~~ mask pageBits\<rbrakk> \<Longrightarrow> Some v = heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) x proof (prove)
goal (2 subgoals):
 1. \<And>x v' x2. \<lbrakk>cmap_relation (\<lambda>p. case map_to_user_data (ksPSpace \<sigma>) p of None \<Rightarrow> None | Some x \<Rightarrow> Some (byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) p)) (cslift s) PTR(user_data_C) cuser_user_data_relation; pointerInUserData ptr \<sigma>; is_aligned ptr 2; cslift s (PTR(user_data_C) x) = Some v'; x \<noteq> ptr && ~~ mask pageBits; map_to_user_data (ksPSpace \<sigma>) x = Some x2; byte_to_word_heap ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) x = byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) x\<rbrakk> \<Longrightarrow> cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) x) v'
 2. \<And>x v v'. \<lbrakk>cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_C) cuser_user_data_relation; pointerInUserData ptr \<sigma>; is_aligned ptr 2; heap_to_user_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) x = Some v; cslift s (PTR(user_data_C) x) = Some v'; x \<noteq> ptr && ~~ mask pageBits\<rbrakk> \<Longrightarrow> Some v = heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) x proof (prove)
goal (1 subgoal):
 1. \<And>x v v'. \<lbrakk>cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_C) cuser_user_data_relation; pointerInUserData ptr \<sigma>; is_aligned ptr 2; heap_to_user_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) x = Some v; cslift s (PTR(user_data_C) x) = Some v'; x \<noteq> ptr && ~~ mask pageBits\<rbrakk> \<Longrightarrow> Some v = heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) x proof (prove)
goal (1 subgoal):
 1. \<And>x v' z. \<lbrakk>cmap_relation (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) p) (map_to_user_data (ksPSpace \<sigma>) p)) (cslift s) PTR(user_data_C) cuser_user_data_relation; pointerInUserData ptr \<sigma>; is_aligned ptr 2; cslift s (PTR(user_data_C) x) = Some v'; x \<noteq> ptr && ~~ mask pageBits; map_to_user_data (ksPSpace \<sigma>) x = Some z\<rbrakk> \<Longrightarrow> byte_to_word_heap ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) x = byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) x proof (prove)
goal (2 subgoals):
 1. \<And>x v' z. \<lbrakk>cmap_relation (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) p) (map_to_user_data (ksPSpace \<sigma>) p)) (cslift s) PTR(user_data_C) cuser_user_data_relation; pointerInUserData ptr \<sigma>; is_aligned ptr 2; cslift s (PTR(user_data_C) x) = Some v'; x \<noteq> ptr && ~~ mask pageBits; map_to_user_data (ksPSpace \<sigma>) x = Some z\<rbrakk> \<Longrightarrow> inj PTR(user_data_C)
 2. \<And>x v' z. \<lbrakk>cmap_relation (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) p) (map_to_user_data (ksPSpace \<sigma>) p)) (cslift s) PTR(user_data_C) cuser_user_data_relation; pointerInUserData ptr \<sigma>; is_aligned ptr 2; cslift s (PTR(user_data_C) x) = Some v'; x \<noteq> ptr && ~~ mask pageBits; map_to_user_data (ksPSpace \<sigma>) x = Some z; \<exists>ko. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) x) (map_to_user_data (ksPSpace \<sigma>) x) = Some ko \<and> cuser_user_data_relation ko v'\<rbrakk> \<Longrightarrow> byte_to_word_heap ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) x = byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) x proof (prove)
goal (1 subgoal):
 1. \<And>x v' z. \<lbrakk>cmap_relation (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) p) (map_to_user_data (ksPSpace \<sigma>) p)) (cslift s) PTR(user_data_C) cuser_user_data_relation; pointerInUserData ptr \<sigma>; is_aligned ptr 2; cslift s (PTR(user_data_C) x) = Some v'; x \<noteq> ptr && ~~ mask pageBits; map_to_user_data (ksPSpace \<sigma>) x = Some z; \<exists>ko. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) x) (map_to_user_data (ksPSpace \<sigma>) x) = Some ko \<and> cuser_user_data_relation ko v'\<rbrakk> \<Longrightarrow> byte_to_word_heap ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) x = byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) x proof (prove)
goal (1 subgoal):
 1. \<And>x v' z. \<lbrakk>cmap_relation (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) p) (map_to_user_data (ksPSpace \<sigma>) p)) (cslift s) PTR(user_data_C) cuser_user_data_relation; pointerInUserData ptr \<sigma>; is_aligned ptr 2; cslift s (PTR(user_data_C) x) = Some v'; x \<noteq> ptr && ~~ mask pageBits; map_to_user_data (ksPSpace \<sigma>) x = Some z; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) x) v'\<rbrakk> \<Longrightarrow> byte_to_word_heap ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) x = byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) x proof (prove)
goal (3 subgoals):
 1. \<And>x v' z. \<lbrakk>cmap_relation (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) p) (map_to_user_data (ksPSpace \<sigma>) p)) (cslift s) PTR(user_data_C) cuser_user_data_relation; pointerInUserData ptr \<sigma>; is_aligned ptr 2; cslift s (PTR(user_data_C) x) = Some v'; x \<noteq> ptr && ~~ mask pageBits; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) x) v'\<rbrakk> \<Longrightarrow> pspace_aligned' \<sigma>
 2. \<And>x v' z. \<lbrakk>cmap_relation (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) p) (map_to_user_data (ksPSpace \<sigma>) p)) (cslift s) PTR(user_data_C) cuser_user_data_relation; pointerInUserData ptr \<sigma>; is_aligned ptr 2; cslift s (PTR(user_data_C) x) = Some v'; x \<noteq> ptr && ~~ mask pageBits; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) x) v'\<rbrakk> \<Longrightarrow> pspace_distinct' \<sigma>
 3. \<And>x v' z. \<lbrakk>cmap_relation (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) p) (map_to_user_data (ksPSpace \<sigma>) p)) (cslift s) PTR(user_data_C) cuser_user_data_relation; pointerInUserData ptr \<sigma>; is_aligned ptr 2; cslift s (PTR(user_data_C) x) = Some v'; x \<noteq> ptr && ~~ mask pageBits; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) x) v'; ko_at' z x \<sigma>\<rbrakk> \<Longrightarrow> byte_to_word_heap ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) x = byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) x proof (prove)
goal (2 subgoals):
 1. \<And>x v' z. \<lbrakk>cmap_relation (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) p) (map_to_user_data (ksPSpace \<sigma>) p)) (cslift s) PTR(user_data_C) cuser_user_data_relation; pointerInUserData ptr \<sigma>; is_aligned ptr 2; cslift s (PTR(user_data_C) x) = Some v'; x \<noteq> ptr && ~~ mask pageBits; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) x) v'\<rbrakk> \<Longrightarrow> pspace_distinct' \<sigma>
 2. \<And>x v' z. \<lbrakk>cmap_relation (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) p) (map_to_user_data (ksPSpace \<sigma>) p)) (cslift s) PTR(user_data_C) cuser_user_data_relation; pointerInUserData ptr \<sigma>; is_aligned ptr 2; cslift s (PTR(user_data_C) x) = Some v'; x \<noteq> ptr && ~~ mask pageBits; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) x) v'; ko_at' z x \<sigma>\<rbrakk> \<Longrightarrow> byte_to_word_heap ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) x = byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) x proof (prove)
goal (1 subgoal):
 1. \<And>x v' z. \<lbrakk>cmap_relation (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) p) (map_to_user_data (ksPSpace \<sigma>) p)) (cslift s) PTR(user_data_C) cuser_user_data_relation; pointerInUserData ptr \<sigma>; is_aligned ptr 2; cslift s (PTR(user_data_C) x) = Some v'; x \<noteq> ptr && ~~ mask pageBits; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) x) v'; ko_at' z x \<sigma>\<rbrakk> \<Longrightarrow> byte_to_word_heap ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) x = byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) x proof (prove)
goal (2 subgoals):
 1. \<And>x v' z. \<lbrakk>cmap_relation (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) p) (map_to_user_data (ksPSpace \<sigma>) p)) (cslift s) PTR(user_data_C) cuser_user_data_relation; pointerInUserData ptr \<sigma>; is_aligned ptr 2; cslift s (PTR(user_data_C) x) = Some v'; x \<noteq> ptr && ~~ mask pageBits; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) x) v'; ko_at' z x \<sigma>; is_aligned x pageBits\<rbrakk> \<Longrightarrow> byte_to_word_heap ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) x = byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) x
 2. \<And>x v' z. \<lbrakk>cmap_relation (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) p) (map_to_user_data (ksPSpace \<sigma>) p)) (cslift s) PTR(user_data_C) cuser_user_data_relation; pointerInUserData ptr \<sigma>; is_aligned ptr 2; cslift s (PTR(user_data_C) x) = Some v'; x \<noteq> ptr && ~~ mask pageBits; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) x) v'; ko_at' z x \<sigma>\<rbrakk> \<Longrightarrow> is_aligned x pageBits proof (prove)
goal (2 subgoals):
 1. \<And>x v' z. \<lbrakk>cmap_relation (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) p) (map_to_user_data (ksPSpace \<sigma>) p)) (cslift s) PTR(user_data_C) cuser_user_data_relation; pointerInUserData ptr \<sigma>; is_aligned ptr 2; cslift s (PTR(user_data_C) x) = Some v'; x \<noteq> ptr && ~~ mask pageBits; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) x) v'; ko_at' z x \<sigma>\<rbrakk> \<Longrightarrow> is_aligned x pageBits
 2. \<And>x v' z. \<lbrakk>cmap_relation (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) p) (map_to_user_data (ksPSpace \<sigma>) p)) (cslift s) PTR(user_data_C) cuser_user_data_relation; pointerInUserData ptr \<sigma>; is_aligned ptr 2; cslift s (PTR(user_data_C) x) = Some v'; x \<noteq> ptr && ~~ mask pageBits; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) x) v'; ko_at' z x \<sigma>; is_aligned x pageBits\<rbrakk> \<Longrightarrow> byte_to_word_heap ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) x = byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) x proof (prove)
goal (1 subgoal):
 1. \<And>x v' z. \<lbrakk>cmap_relation (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) p) (map_to_user_data (ksPSpace \<sigma>) p)) (cslift s) PTR(user_data_C) cuser_user_data_relation; pointerInUserData ptr \<sigma>; is_aligned ptr 2; cslift s (PTR(user_data_C) x) = Some v'; x \<noteq> ptr && ~~ mask pageBits; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) x) v'; ko_at' z x \<sigma>; is_aligned x pageBits\<rbrakk> \<Longrightarrow> byte_to_word_heap ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) x = byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) x proof (prove)
goal (2 subgoals):
 1. \<And>x v' z. \<lbrakk>cmap_relation (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) p) (map_to_user_data (ksPSpace \<sigma>) p)) (cslift s) PTR(user_data_C) cuser_user_data_relation; pointerInUserData ptr \<sigma>; is_aligned ptr 2; cslift s (PTR(user_data_C) x) = Some v'; x \<noteq> ptr && ~~ mask pageBits; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) x) v'; ko_at' z x \<sigma>; is_aligned x pageBits; is_aligned x 2\<rbrakk> \<Longrightarrow> byte_to_word_heap ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) x = byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) x
 2. \<And>x v' z. \<lbrakk>cmap_relation (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) p) (map_to_user_data (ksPSpace \<sigma>) p)) (cslift s) PTR(user_data_C) cuser_user_data_relation; pointerInUserData ptr \<sigma>; is_aligned ptr 2; cslift s (PTR(user_data_C) x) = Some v'; x \<noteq> ptr && ~~ mask pageBits; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) x) v'; ko_at' z x \<sigma>; is_aligned x pageBits\<rbrakk> \<Longrightarrow> is_aligned x 2 proof (prove)
goal (2 subgoals):
 1. \<And>x v' z. \<lbrakk>cmap_relation (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) p) (map_to_user_data (ksPSpace \<sigma>) p)) (cslift s) PTR(user_data_C) cuser_user_data_relation; pointerInUserData ptr \<sigma>; is_aligned ptr 2; cslift s (PTR(user_data_C) x) = Some v'; x \<noteq> ptr && ~~ mask pageBits; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) x) v'; ko_at' z x \<sigma>; is_aligned x pageBits\<rbrakk> \<Longrightarrow> is_aligned x 2
 2. \<And>x v' z. \<lbrakk>cmap_relation (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) p) (map_to_user_data (ksPSpace \<sigma>) p)) (cslift s) PTR(user_data_C) cuser_user_data_relation; pointerInUserData ptr \<sigma>; is_aligned ptr 2; cslift s (PTR(user_data_C) x) = Some v'; x \<noteq> ptr && ~~ mask pageBits; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) x) v'; ko_at' z x \<sigma>; is_aligned x pageBits; is_aligned x 2\<rbrakk> \<Longrightarrow> byte_to_word_heap ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) x = byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) x proof (prove)
goal (2 subgoals):
 1. \<And>x v' z. \<lbrakk>cmap_relation (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) p) (map_to_user_data (ksPSpace \<sigma>) p)) (cslift s) PTR(user_data_C) cuser_user_data_relation; pointerInUserData ptr \<sigma>; is_aligned ptr 2; cslift s (PTR(user_data_C) x) = Some v'; x \<noteq> ptr && ~~ mask pageBits; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) x) v'; ko_at' z x \<sigma>\<rbrakk> \<Longrightarrow> 2 \<le> pageBits
 2. \<And>x v' z. \<lbrakk>cmap_relation (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) p) (map_to_user_data (ksPSpace \<sigma>) p)) (cslift s) PTR(user_data_C) cuser_user_data_relation; pointerInUserData ptr \<sigma>; is_aligned ptr 2; cslift s (PTR(user_data_C) x) = Some v'; x \<noteq> ptr && ~~ mask pageBits; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) x) v'; ko_at' z x \<sigma>; is_aligned x pageBits; is_aligned x 2\<rbrakk> \<Longrightarrow> byte_to_word_heap ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) x = byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) x proof (prove)
goal (1 subgoal):
 1. \<And>x v' z. \<lbrakk>cmap_relation (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) p) (map_to_user_data (ksPSpace \<sigma>) p)) (cslift s) PTR(user_data_C) cuser_user_data_relation; pointerInUserData ptr \<sigma>; is_aligned ptr 2; cslift s (PTR(user_data_C) x) = Some v'; x \<noteq> ptr && ~~ mask pageBits; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) x) v'; ko_at' z x \<sigma>; is_aligned x pageBits; is_aligned x 2\<rbrakk> \<Longrightarrow> byte_to_word_heap ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) x = byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) x proof (prove)
goal (1 subgoal):
 1. \<And>x v' z xa. \<lbrakk>cmap_relation (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) p) (map_to_user_data (ksPSpace \<sigma>) p)) (cslift s) PTR(user_data_C) cuser_user_data_relation; pointerInUserData ptr \<sigma>; is_aligned ptr 2; cslift s (PTR(user_data_C) x) = Some v'; x \<noteq> ptr && ~~ mask pageBits; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) x) v'; ko_at' z x \<sigma>; is_aligned x pageBits; is_aligned x 2\<rbrakk> \<Longrightarrow> byte_to_word_heap ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) x xa = byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) x xa proof (prove)
goal (1 subgoal):
 1. \<And>x v' z xa. \<lbrakk>cmap_relation (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) p) (map_to_user_data (ksPSpace \<sigma>) p)) (cslift s) PTR(user_data_C) cuser_user_data_relation; pointerInUserData ptr \<sigma>; is_aligned ptr 2; cslift s (PTR(user_data_C) x) = Some v'; x \<noteq> ptr && ~~ mask pageBits; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) x) v'; ko_at' z x \<sigma>; is_aligned x pageBits; is_aligned x 2\<rbrakk> \<Longrightarrow> byte_to_word_heap ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3)) x xa = byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) x xa proof (prove)
goal (2 subgoals):
 1. \<And>x v' z xa. \<lbrakk>cmap_relation (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) p) (map_to_user_data (ksPSpace \<sigma>) p)) (cslift s) PTR(user_data_C) cuser_user_data_relation; pointerInUserData ptr \<sigma>; is_aligned ptr 2; cslift s (PTR(user_data_C) x) = Some v'; x \<noteq> ptr && ~~ mask pageBits; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) x) v'; ko_at' z x \<sigma>; is_aligned x pageBits; is_aligned x 2\<rbrakk> \<Longrightarrow> x + UCAST(10 \<rightarrow> 32) xa * 4 \<noteq> ptr
 2. \<And>x v' z xa. \<lbrakk>cmap_relation (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) p) (map_to_user_data (ksPSpace \<sigma>) p)) (cslift s) PTR(user_data_C) cuser_user_data_relation; pointerInUserData ptr \<sigma>; is_aligned ptr 2; cslift s (PTR(user_data_C) x) = Some v'; x \<noteq> ptr && ~~ mask pageBits; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) x) v'; ko_at' z x \<sigma>; is_aligned x pageBits; is_aligned x 2\<rbrakk> \<Longrightarrow> byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) x xa = byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) x xa proof (prove)
goal (1 subgoal):
 1. \<And>x v' z xa. \<lbrakk>cmap_relation (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) p) (map_to_user_data (ksPSpace \<sigma>) p)) (cslift s) PTR(user_data_C) cuser_user_data_relation; pointerInUserData ptr \<sigma>; is_aligned ptr 2; cslift s (PTR(user_data_C) x) = Some v'; x \<noteq> ptr && ~~ mask pageBits; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) x) v'; ko_at' z x \<sigma>; is_aligned x pageBits; is_aligned x 2\<rbrakk> \<Longrightarrow> byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) x xa = byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) x xa proof (prove)
goal:
No subgoals! proof (state)
this:
cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_C) cuser_user_data_relation \<Longrightarrow> cmap_relation (heap_to_user_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0))) (\<lambda>y. if ptr_val y = ptr_val (PTR(32 word) ptr) && ~~ mask pageBits then Some (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s y))) else cslift s y) PTR(user_data_C) cuser_user_data_relation

goal (1 subgoal):
 1. \<And>\<sigma> s. (\<sigma>, s) \<in> rf_sr \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pointerInUserData ptr \<sigma> \<and> is_aligned ptr 2 \<Longrightarrow> (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>)\<rparr>, s\<lparr>globals := globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>f hp'. hrs_mem_update (\<lambda>hp. heap_update base (f (h_val hp base)) hp) hp' = hrs_mem_update (heap_update base (f (h_val (hrs_mem hp') base))) hp' proof (state)
this:
hrs_mem_update (\<lambda>hp. heap_update base (?f5 (h_val hp base)) hp) ?hp'5 = hrs_mem_update (heap_update base (?f5 (h_val (hrs_mem ?hp'5) base))) ?hp'5

goal (1 subgoal):
 1. \<And>\<sigma> s. (\<sigma>, s) \<in> rf_sr \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pointerInUserData ptr \<sigma> \<and> is_aligned ptr 2 \<Longrightarrow> (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>)\<rparr>, s\<lparr>globals := globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))\<rparr>\<rparr>) \<in> rf_sr proof (chain)
picking this:
cslift s base = Some page proof (prove)
using this:
cslift s base = Some page

goal (1 subgoal):
 1. typ_uinfo_t TYPE(user_data_C) \<bottom>\<^sub>t typ_uinfo_t TYPE('t) \<Longrightarrow> clift (hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))) = cslift s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>typ_uinfo_t TYPE(user_data_C) \<bottom>\<^sub>t typ_uinfo_t TYPE('t); cslift s base = Some page\<rbrakk> \<Longrightarrow> clift (hrs_mem_update (\<lambda>hp. heap_update base (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat offset) w) (h_val hp base)) hp) (t_hrs_' (globals s))) = cslift s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>typ_uinfo_t TYPE(user_data_C) \<bottom>\<^sub>t typ_uinfo_t TYPE('t); cslift s base = Some page\<rbrakk> \<Longrightarrow> clift (hrs_mem_update (heap_update base (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat offset) w) (h_val (hrs_mem (t_hrs_' (globals s))) base))) (t_hrs_' (globals s))) = cslift s proof (prove)
goal:
No subgoals! proof (state)
this:
typ_uinfo_t TYPE(user_data_C) \<bottom>\<^sub>t typ_uinfo_t TYPE(?'t6) \<Longrightarrow> clift (hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))) = cslift s

goal (1 subgoal):
 1. \<And>\<sigma> s. (\<sigma>, s) \<in> rf_sr \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pointerInUserData ptr \<sigma> \<and> is_aligned ptr 2 \<Longrightarrow> (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>)\<rparr>, s\<lparr>globals := globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. {ptr..+2\<^sup>2} \<subseteq> {ptr && ~~ mask pageBits..+2 ^ pageBits} proof (prove)
goal (1 subgoal):
 1. {ptr..ptr + 2\<^sup>2 - 1} \<subseteq> {ptr && ~~ mask pageBits..(ptr && ~~ mask pageBits) + 2 ^ pageBits - 1} proof (prove)
goal (4 subgoals):
 1. is_aligned (ptr && mask pageBits) ?sz'1
 2. ?sz'1 \<le> pageBits
 3. ptr && mask pageBits < 2 ^ pageBits
 4. {(ptr && ~~ mask pageBits) + (ptr && mask pageBits)..(ptr && ~~ mask pageBits) + (ptr && mask pageBits) + 2 ^ ?sz'1 - 1} \<subseteq> {ptr && ~~ mask pageBits..(ptr && ~~ mask pageBits) + 2 ^ pageBits - 1} \<Longrightarrow> {ptr..ptr + 2\<^sup>2 - 1} \<subseteq> {ptr && ~~ mask pageBits..(ptr && ~~ mask pageBits) + 2 ^ pageBits - 1} proof (prove)
goal (3 subgoals):
 1. 2 \<le> pageBits
 2. ptr && mask pageBits < 2 ^ pageBits
 3. {(ptr && ~~ mask pageBits) + (ptr && mask pageBits)..(ptr && ~~ mask pageBits) + (ptr && mask pageBits) + 2\<^sup>2 - 1} \<subseteq> {ptr && ~~ mask pageBits..(ptr && ~~ mask pageBits) + 2 ^ pageBits - 1} \<Longrightarrow> {ptr..ptr + 2\<^sup>2 - 1} \<subseteq> {ptr && ~~ mask pageBits..(ptr && ~~ mask pageBits) + 2 ^ pageBits - 1} proof (prove)
goal (2 subgoals):
 1. ptr && mask pageBits < 2 ^ pageBits
 2. {(ptr && ~~ mask pageBits) + (ptr && mask pageBits)..(ptr && ~~ mask pageBits) + (ptr && mask pageBits) + 2\<^sup>2 - 1} \<subseteq> {ptr && ~~ mask pageBits..(ptr && ~~ mask pageBits) + 2 ^ pageBits - 1} \<Longrightarrow> {ptr..ptr + 2\<^sup>2 - 1} \<subseteq> {ptr && ~~ mask pageBits..(ptr && ~~ mask pageBits) + 2 ^ pageBits - 1} proof (prove)
goal (1 subgoal):
 1. {(ptr && ~~ mask pageBits) + (ptr && mask pageBits)..(ptr && ~~ mask pageBits) + (ptr && mask pageBits) + 2\<^sup>2 - 1} \<subseteq> {ptr && ~~ mask pageBits..(ptr && ~~ mask pageBits) + 2 ^ pageBits - 1} \<Longrightarrow> {ptr..ptr + 2\<^sup>2 - 1} \<subseteq> {ptr && ~~ mask pageBits..(ptr && ~~ mask pageBits) + 2 ^ pageBits - 1} proof (prove)
goal (1 subgoal):
 1. {ptr..ptr + 2\<^sup>2 - 1} \<subseteq> {(ptr && ~~ mask pageBits) + (ptr && mask pageBits)..(ptr && ~~ mask pageBits) + (ptr && mask pageBits) + 2\<^sup>2 - 1} proof (prove)
goal:
No subgoals! proof (state)
this:
{ptr..+2\<^sup>2} \<subseteq> {ptr && ~~ mask pageBits..+2 ^ pageBits}

goal (1 subgoal):
 1. \<And>\<sigma> s. (\<sigma>, s) \<in> rf_sr \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pointerInUserData ptr \<sigma> \<and> is_aligned ptr 2 \<Longrightarrow> (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>)\<rparr>, s\<lparr>globals := globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
using this:
{ptr..+2\<^sup>2} \<subseteq> {ptr && ~~ mask pageBits..+2 ^ pageBits}

goal (1 subgoal):
 1. \<And>rs. zero_ranges_are_zero rs (hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))) = zero_ranges_are_zero rs (t_hrs_' (globals s)) proof (prove)
using this:
{ptr..+2\<^sup>2} \<subseteq> {ptr && ~~ mask pageBits..+2 ^ pageBits}
cslift s base = Some page

goal (1 subgoal):
 1. \<And>rs. zero_ranges_are_zero rs (hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))) = zero_ranges_are_zero rs (t_hrs_' (globals s)) proof (prove)
goal (1 subgoal):
 1. \<And>rs a b. \<lbrakk>{ptr..+4} \<subseteq> {ptr && ~~ mask pageBits..+2 ^ pageBits}; cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)) = Some page; (a, b) \<in> rs; region_actually_is_bytes a (unat (b + 1 - a)) s\<rbrakk> \<Longrightarrow> (heap_list (heap_update_list ptr (to_bytes w (heap_list (hrs_mem (t_hrs_' (globals s))) 4 ptr)) (hrs_mem (t_hrs_' (globals s)))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0) = (heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0) proof (prove)
goal (1 subgoal):
 1. \<And>rs a b. \<lbrakk>{ptr..+4} \<subseteq> {ptr && ~~ mask pageBits..+2 ^ pageBits}; cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)) = Some page; (a, b) \<in> rs; region_is_bytes a (unat (b + 1 - a)) s\<rbrakk> \<Longrightarrow> (heap_list (heap_update_list ptr (to_bytes w (heap_list (hrs_mem (t_hrs_' (globals s))) 4 ptr)) (hrs_mem (t_hrs_' (globals s)))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0) = (heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0) proof (prove)
goal (2 subgoals):
 1. \<And>rs a b. \<lbrakk>{ptr..+4} \<subseteq> {ptr && ~~ mask pageBits..+2 ^ pageBits}; cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)) = Some page; (a, b) \<in> rs; region_is_bytes a (unat (b + 1 - a)) s\<rbrakk> \<Longrightarrow> typ_uinfo_t TYPE(user_data_C) \<noteq> typ_uinfo_t TYPE(8 word)
 2. \<And>rs a b. \<lbrakk>{ptr..+4} \<subseteq> {ptr && ~~ mask pageBits..+2 ^ pageBits}; cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)) = Some page; (a, b) \<in> rs; region_is_bytes a (unat (b + 1 - a)) s; {a..+unat (b + 1 - a)} \<inter> ptr_span (PTR(user_data_C) (ptr && ~~ mask pageBits)) = {}\<rbrakk> \<Longrightarrow> (heap_list (heap_update_list ptr (to_bytes w (heap_list (hrs_mem (t_hrs_' (globals s))) 4 ptr)) (hrs_mem (t_hrs_' (globals s)))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0) = (heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0) proof (prove)
goal (1 subgoal):
 1. \<And>rs a b. \<lbrakk>{ptr..+4} \<subseteq> {ptr && ~~ mask pageBits..+2 ^ pageBits}; cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)) = Some page; (a, b) \<in> rs; region_is_bytes a (unat (b + 1 - a)) s; {a..+unat (b + 1 - a)} \<inter> ptr_span (PTR(user_data_C) (ptr && ~~ mask pageBits)) = {}\<rbrakk> \<Longrightarrow> (heap_list (heap_update_list ptr (to_bytes w (heap_list (hrs_mem (t_hrs_' (globals s))) 4 ptr)) (hrs_mem (t_hrs_' (globals s)))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0) = (heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0) proof (prove)
goal (1 subgoal):
 1. \<And>rs a b. \<lbrakk>{ptr..+4} \<subseteq> {ptr && ~~ mask pageBits..+2 ^ pageBits}; cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)) = Some page; (a, b) \<in> rs; region_is_bytes a (unat (b + 1 - a)) s; {a..+unat (b + 1 - a)} \<inter> {ptr && ~~ mask pageBits..+4096} = {}\<rbrakk> \<Longrightarrow> {ptr..+4} \<inter> {a..+unat (b + 1 - a)} = {} proof (prove)
goal (1 subgoal):
 1. \<And>rs a b. \<lbrakk>{ptr..+4} \<subseteq> {ptr && ~~ mask pageBits..+2 ^ pageBits}; cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)) = Some page; (a, b) \<in> rs; region_is_bytes a (unat (b + 1 - a)) s\<rbrakk> \<Longrightarrow> {ptr..+4} \<subseteq> {ptr && ~~ mask pageBits..+4096} proof (prove)
goal:
No subgoals! proof (state)
this:
zero_ranges_are_zero ?rs6 (hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))) = zero_ranges_are_zero ?rs6 (t_hrs_' (globals s))

goal (1 subgoal):
 1. \<And>\<sigma> s. (\<sigma>, s) \<in> rf_sr \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pointerInUserData ptr \<sigma> \<and> is_aligned ptr 2 \<Longrightarrow> (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>)\<rparr>, s\<lparr>globals := globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>as cs cs' f rel. \<lbrakk>cmap_relation as cs f rel; cs = cs'\<rbrakk> \<Longrightarrow> cmap_relation as cs' f rel proof (state)
this:
\<lbrakk>cmap_relation ?as6 ?cs6 ?f6 ?rel6; ?cs6 = ?cs'6\<rbrakk> \<Longrightarrow> cmap_relation ?as6 ?cs'6 ?f6 ?rel6

goal (1 subgoal):
 1. \<And>\<sigma> s. (\<sigma>, s) \<in> rf_sr \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pointerInUserData ptr \<sigma> \<and> is_aligned ptr 2 \<Longrightarrow> (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>)\<rparr>, s\<lparr>globals := globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))\<rparr>\<rparr>) \<in> rf_sr proof (chain)
picking this:
(\<sigma>, s) \<in> rf_sr proof (prove)
using this:
(\<sigma>, s) \<in> rf_sr

goal (1 subgoal):
 1. cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals s)) proof (prove)
using this:
(\<sigma>, s) \<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 s)) proof (state)
this:
cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals s))

goal (1 subgoal):
 1. \<And>\<sigma> s. (\<sigma>, s) \<in> rf_sr \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pointerInUserData ptr \<sigma> \<and> is_aligned ptr 2 \<Longrightarrow> (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>)\<rparr>, s\<lparr>globals := globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
using this:
cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals s))

goal (1 subgoal):
 1. cpspace_relation (ksPSpace \<sigma>) (underlying_memory (underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>))) (hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))) proof (prove)
using this:
cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation \<and> cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation \<and> cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift s) ep_Ptr (cendpoint_relation (cslift s)) \<and> cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)) \<and> cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift s) pde_Ptr cpde_relation \<and> cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift s) pte_Ptr cpte_relation \<and> cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift s) ap_Ptr casid_pool_relation \<and> cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_C) cuser_user_data_relation \<and> cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation \<and> carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid s) pd_Ptr \<and> carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid s) pt_Ptr

goal (1 subgoal):
 1. cmap_relation (ctes_of \<sigma>) (clift (hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s)))) cte_Ptr ccte_relation \<and> cpspace_tcb_relation (ksPSpace \<sigma>) (hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))) \<and> cmap_relation (map_to_eps (ksPSpace \<sigma>)) (clift (hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s)))) ep_Ptr (cendpoint_relation (clift (hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))))) \<and> cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (clift (hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s)))) ntfn_Ptr (cnotification_relation (clift (hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))))) \<and> cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (clift (hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s)))) pde_Ptr cpde_relation \<and> cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (clift (hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s)))) pte_Ptr cpte_relation \<and> cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (clift (hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s)))) ap_Ptr casid_pool_relation \<and> cpspace_user_data_relation (ksPSpace \<sigma>) (underlying_memory (underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>))) (hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))) \<and> cpspace_device_data_relation (ksPSpace \<sigma>) (underlying_memory (underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>))) (hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))) \<and> cpspace_pde_array_relation (ksPSpace \<sigma>) (hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))) \<and> cpspace_pte_array_relation (ksPSpace \<sigma>) (hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))) proof (prove)
using this:
cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation \<and> cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation \<and> cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift s) ep_Ptr (cendpoint_relation (cslift s)) \<and> cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)) \<and> cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift s) pde_Ptr cpde_relation \<and> cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift s) pte_Ptr cpte_relation \<and> cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift s) ap_Ptr casid_pool_relation \<and> cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_C) cuser_user_data_relation \<and> cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation \<and> carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid s) pd_Ptr \<and> carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid s) pt_Ptr
cslift s base = Some page

goal (1 subgoal):
 1. cmap_relation (ctes_of \<sigma>) (clift (hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s)))) cte_Ptr ccte_relation \<and> cpspace_tcb_relation (ksPSpace \<sigma>) (hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))) \<and> cmap_relation (map_to_eps (ksPSpace \<sigma>)) (clift (hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s)))) ep_Ptr (cendpoint_relation (clift (hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))))) \<and> cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (clift (hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s)))) ntfn_Ptr (cnotification_relation (clift (hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))))) \<and> cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (clift (hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s)))) pde_Ptr cpde_relation \<and> cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (clift (hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s)))) pte_Ptr cpte_relation \<and> cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (clift (hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s)))) ap_Ptr casid_pool_relation \<and> cpspace_user_data_relation (ksPSpace \<sigma>) (underlying_memory (underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>))) (hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))) \<and> cpspace_device_data_relation (ksPSpace \<sigma>) (underlying_memory (underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>))) (hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))) \<and> cpspace_pde_array_relation (ksPSpace \<sigma>) (hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))) \<and> cpspace_pte_array_relation (ksPSpace \<sigma>) (hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation \<and> cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation \<and> cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift s) ep_Ptr (cendpoint_relation (cslift s)) \<and> cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)) \<and> cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift s) pde_Ptr cpde_relation \<and> cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift s) pte_Ptr cpte_relation \<and> cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift s) ap_Ptr casid_pool_relation \<and> cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_C) cuser_user_data_relation \<and> cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation \<and> carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid s) pd_Ptr \<and> carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid s) pt_Ptr; cslift s base = Some page\<rbrakk> \<Longrightarrow> cmap_relation (ctes_of \<sigma>) (clift (hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s)))) cte_Ptr ccte_relation \<and> cpspace_tcb_relation (ksPSpace \<sigma>) (hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))) \<and> cmap_relation (map_to_eps (ksPSpace \<sigma>)) (clift (hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s)))) ep_Ptr (cendpoint_relation (clift (hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))))) \<and> cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (clift (hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s)))) ntfn_Ptr (cnotification_relation (clift (hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))))) \<and> cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (clift (hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s)))) pde_Ptr cpde_relation \<and> cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (clift (hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s)))) pte_Ptr cpte_relation \<and> cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (clift (hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s)))) ap_Ptr casid_pool_relation \<and> cpspace_user_data_relation (ksPSpace \<sigma>) (underlying_memory (underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>))) (hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))) \<and> cpspace_device_data_relation (ksPSpace \<sigma>) (underlying_memory (underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>))) (hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))) \<and> cpspace_pde_array_relation (ksPSpace \<sigma>) (hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))) \<and> cpspace_pte_array_relation (ksPSpace \<sigma>) (hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cslift s base = Some page; cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift s) ep_Ptr (cendpoint_relation (cslift s)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift s) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift s) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift s) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid s) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid s) pt_Ptr\<rbrakk> \<Longrightarrow> cpspace_user_data_relation (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) (hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))) \<and> cmap_relation (heap_to_device_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cslift s base = Some page; cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift s) ep_Ptr (cendpoint_relation (cslift s)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift s) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift s) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift s) ap_Ptr casid_pool_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid s) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid s) pt_Ptr; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0))) (\<lambda>y. if ptr_val y = ptr_val (PTR(32 word) ptr) && ~~ mask pageBits then Some (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s y))) else cslift s y) PTR(user_data_C) cuser_user_data_relation\<rbrakk> \<Longrightarrow> cpspace_user_data_relation (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) (hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))) \<and> cmap_relation (heap_to_device_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cslift s base = Some page; cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift s) ep_Ptr (cendpoint_relation (cslift s)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift s) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift s) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift s) ap_Ptr casid_pool_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid s) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid s) pt_Ptr; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0))) (\<lambda>y. if ptr_val y = ptr && ~~ mask pageBits then Some (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s y))) else cslift s y) PTR(user_data_C) cuser_user_data_relation\<rbrakk> \<Longrightarrow> cpspace_user_data_relation (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) (hrs_mem_update (\<lambda>hp. heap_update base (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat offset) w) (h_val hp base)) hp) (t_hrs_' (globals s))) \<and> cmap_relation (heap_to_device_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cslift s base = Some page; cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift s) ep_Ptr (cendpoint_relation (cslift s)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift s) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift s) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift s) ap_Ptr casid_pool_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid s) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid s) pt_Ptr; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0))) (\<lambda>y. if ptr_val y = ptr && ~~ mask pageBits then Some (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s y))) else cslift s y) PTR(user_data_C) cuser_user_data_relation\<rbrakk> \<Longrightarrow> cpspace_user_data_relation (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) (hrs_mem_update (heap_update base (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat offset) w) (h_val (hrs_mem (t_hrs_' (globals s))) base))) (t_hrs_' (globals s))) \<and> cmap_relation (heap_to_device_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)) = Some page; cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift s) ep_Ptr (cendpoint_relation (cslift s)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift s) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift s) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift s) ap_Ptr casid_pool_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid s) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid s) pt_Ptr; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0))) (\<lambda>y. if ptr_val y = ptr && ~~ mask pageBits then Some (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s y))) else cslift s y) PTR(user_data_C) cuser_user_data_relation\<rbrakk> \<Longrightarrow> cpspace_user_data_relation (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) (hrs_mem_update (heap_update (PTR(user_data_C) (ptr && ~~ mask pageBits)) (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (h_val (hrs_mem (t_hrs_' (globals s))) (PTR(user_data_C) (ptr && ~~ mask pageBits))))) (t_hrs_' (globals s))) \<and> cmap_relation (heap_to_device_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)) = Some page; cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift s) ep_Ptr (cendpoint_relation (cslift s)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift s) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift s) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift s) ap_Ptr casid_pool_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid s) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid s) pt_Ptr; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0))) (\<lambda>y. if ptr_val y = ptr && ~~ mask pageBits then Some (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s y))) else cslift s y) PTR(user_data_C) cuser_user_data_relation\<rbrakk> \<Longrightarrow> cpspace_user_data_relation (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) (hrs_mem_update (heap_update (PTR(user_data_C) (ptr && ~~ mask pageBits)) (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (h_val (hrs_mem (t_hrs_' (globals s))) (PTR(user_data_C) (ptr && ~~ mask pageBits))))) (t_hrs_' (globals s)))
 2. \<lbrakk>cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)) = Some page; cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift s) ep_Ptr (cendpoint_relation (cslift s)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift s) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift s) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift s) ap_Ptr casid_pool_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid s) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid s) pt_Ptr; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0))) (\<lambda>y. if ptr_val y = ptr && ~~ mask pageBits then Some (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s y))) else cslift s y) PTR(user_data_C) cuser_user_data_relation\<rbrakk> \<Longrightarrow> cmap_relation (heap_to_device_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)) = Some page; cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift s) ep_Ptr (cendpoint_relation (cslift s)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift s) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift s) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift s) ap_Ptr casid_pool_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid s) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid s) pt_Ptr\<rbrakk> \<Longrightarrow> (\<lambda>y. if ptr_val y = ptr && ~~ mask pageBits then Some (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s y))) else cslift s y) = clift (hrs_mem_update (heap_update (PTR(user_data_C) (ptr && ~~ mask pageBits)) (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (h_val (hrs_mem (t_hrs_' (globals s))) (PTR(user_data_C) (ptr && ~~ mask pageBits))))) (t_hrs_' (globals s)))
 2. \<lbrakk>cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)) = Some page; cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift s) ep_Ptr (cendpoint_relation (cslift s)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift s) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift s) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift s) ap_Ptr casid_pool_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid s) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid s) pt_Ptr; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0))) (\<lambda>y. if ptr_val y = ptr && ~~ mask pageBits then Some (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s y))) else cslift s y) PTR(user_data_C) cuser_user_data_relation\<rbrakk> \<Longrightarrow> cmap_relation (heap_to_device_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)) = Some page; cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift s) ep_Ptr (cendpoint_relation (cslift s)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift s) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift s) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift s) ap_Ptr casid_pool_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid s) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid s) pt_Ptr\<rbrakk> \<Longrightarrow> (\<lambda>y. if ptr_val y = ptr && ~~ mask pageBits then Some (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s y))) else cslift s y) = (cslift s)(PTR(user_data_C) (ptr && ~~ mask pageBits) \<mapsto> user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) page)
 2. \<lbrakk>cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)) = Some page; cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift s) ep_Ptr (cendpoint_relation (cslift s)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift s) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift s) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift s) ap_Ptr casid_pool_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid s) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid s) pt_Ptr; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0))) (\<lambda>y. if ptr_val y = ptr && ~~ mask pageBits then Some (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s y))) else cslift s y) PTR(user_data_C) cuser_user_data_relation\<rbrakk> \<Longrightarrow> cmap_relation (heap_to_device_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)) = Some page; cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift s) ep_Ptr (cendpoint_relation (cslift s)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift s) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift s) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift s) ap_Ptr casid_pool_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid s) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid s) pt_Ptr\<rbrakk> \<Longrightarrow> (if ptr_val y = ptr && ~~ mask pageBits then Some (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s y))) else cslift s y) = ((cslift s)(PTR(user_data_C) (ptr && ~~ mask pageBits) \<mapsto> user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) page)) y
 2. \<lbrakk>cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)) = Some page; cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift s) ep_Ptr (cendpoint_relation (cslift s)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift s) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift s) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift s) ap_Ptr casid_pool_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid s) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid s) pt_Ptr; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0))) (\<lambda>y. if ptr_val y = ptr && ~~ mask pageBits then Some (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s y))) else cslift s y) PTR(user_data_C) cuser_user_data_relation\<rbrakk> \<Longrightarrow> cmap_relation (heap_to_device_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)) = Some page; cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift s) ep_Ptr (cendpoint_relation (cslift s)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift s) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift s) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift s) ap_Ptr casid_pool_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid s) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid s) pt_Ptr\<rbrakk> \<Longrightarrow> (if ptr_val y = ptr && ~~ mask pageBits then Some (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s y))) else cslift s y) = (if y = PTR(user_data_C) (ptr && ~~ mask pageBits) then Some (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) page) else cslift s y)
 2. \<lbrakk>cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)) = Some page; cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift s) ep_Ptr (cendpoint_relation (cslift s)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift s) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift s) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift s) ap_Ptr casid_pool_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid s) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid s) pt_Ptr; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0))) (\<lambda>y. if ptr_val y = ptr && ~~ mask pageBits then Some (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s y))) else cslift s y) PTR(user_data_C) cuser_user_data_relation\<rbrakk> \<Longrightarrow> cmap_relation (heap_to_device_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation proof (prove)
goal (2 subgoals):
 1. \<And>y x. \<lbrakk>cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)) = Some page; cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift s) ep_Ptr (cendpoint_relation (cslift s)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift s) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift s) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift s) ap_Ptr casid_pool_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid s) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid s) pt_Ptr; y = PTR(user_data_C) x\<rbrakk> \<Longrightarrow> (if ptr_val y = ptr && ~~ mask pageBits then Some (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s y))) else cslift s y) = (if y = PTR(user_data_C) (ptr && ~~ mask pageBits) then Some (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) page) else cslift s y)
 2. \<lbrakk>cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)) = Some page; cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift s) ep_Ptr (cendpoint_relation (cslift s)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift s) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift s) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift s) ap_Ptr casid_pool_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid s) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid s) pt_Ptr; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0))) (\<lambda>y. if ptr_val y = ptr && ~~ mask pageBits then Some (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s y))) else cslift s y) PTR(user_data_C) cuser_user_data_relation\<rbrakk> \<Longrightarrow> cmap_relation (heap_to_device_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)) = Some page; cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift s) ep_Ptr (cendpoint_relation (cslift s)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift s) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift s) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift s) ap_Ptr casid_pool_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid s) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid s) pt_Ptr; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0))) (\<lambda>y. if ptr_val y = ptr && ~~ mask pageBits then Some (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s y))) else cslift s y) PTR(user_data_C) cuser_user_data_relation\<rbrakk> \<Longrightarrow> cmap_relation (heap_to_device_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)) = Some page; cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift s) ep_Ptr (cendpoint_relation (cslift s)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift s) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift s) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift s) ap_Ptr casid_pool_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid s) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid s) pt_Ptr; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0))) (\<lambda>y. if ptr_val y = ptr && ~~ mask pageBits then Some (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s y))) else cslift s y) PTR(user_data_C) cuser_user_data_relation\<rbrakk> \<Longrightarrow> PTR(user_data_device_C) ` dom (heap_to_device_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0))) = dom (cslift s)
 2. \<And>x v v'. \<lbrakk>cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)) = Some page; cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift s) ep_Ptr (cendpoint_relation (cslift s)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift s) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift s) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift s) ap_Ptr casid_pool_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid s) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid s) pt_Ptr; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0))) (\<lambda>y. if ptr_val y = ptr && ~~ mask pageBits then Some (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s y))) else cslift s y) PTR(user_data_C) cuser_user_data_relation; heap_to_device_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) x = Some v; cslift s (PTR(user_data_device_C) x) = Some v'\<rbrakk> \<Longrightarrow> cuser_user_data_device_relation v v' proof (prove)
goal (1 subgoal):
 1. \<And>x v v'. \<lbrakk>cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)) = Some page; cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift s) ep_Ptr (cendpoint_relation (cslift s)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift s) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift s) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift s) ap_Ptr casid_pool_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid s) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid s) pt_Ptr; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0))) (\<lambda>y. if ptr_val y = ptr && ~~ mask pageBits then Some (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s y))) else cslift s y) PTR(user_data_C) cuser_user_data_relation; heap_to_device_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) x = Some v; cslift s (PTR(user_data_device_C) x) = Some v'\<rbrakk> \<Longrightarrow> cuser_user_data_device_relation v v' proof (prove)
using this:
pspace_aligned' \<sigma>

goal (1 subgoal):
 1. \<And>x v v'. \<lbrakk>cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)) = Some page; cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift s) ep_Ptr (cendpoint_relation (cslift s)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift s) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift s) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift s) ap_Ptr casid_pool_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid s) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid s) pt_Ptr; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0))) (\<lambda>y. if ptr_val y = ptr && ~~ mask pageBits then Some (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s y))) else cslift s y) PTR(user_data_C) cuser_user_data_relation; heap_to_device_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) x = Some v; cslift s (PTR(user_data_device_C) x) = Some v'\<rbrakk> \<Longrightarrow> cuser_user_data_device_relation v v' proof (prove)
goal (4 subgoals):
 1. \<And>x v v'. \<lbrakk>cslift s (PTR(user_data_device_C) x) = Some v'; pspace_aligned' \<sigma>; cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)) = Some page; cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift s) ep_Ptr (cendpoint_relation (cslift s)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift s) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift s) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift s) ap_Ptr casid_pool_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid s) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid s) pt_Ptr; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0))) (\<lambda>y. if ptr_val y = ptr && ~~ mask pageBits then Some (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s y))) else cslift s y) PTR(user_data_C) cuser_user_data_relation\<rbrakk> \<Longrightarrow> \<not> pointerInDeviceData (ptr + 3) \<sigma>
 2. \<And>x v v'. \<lbrakk>cslift s (PTR(user_data_device_C) x) = Some v'; pspace_aligned' \<sigma>; cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)) = Some page; cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift s) ep_Ptr (cendpoint_relation (cslift s)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift s) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift s) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift s) ap_Ptr casid_pool_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid s) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid s) pt_Ptr; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0))) (\<lambda>y. if ptr_val y = ptr && ~~ mask pageBits then Some (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s y))) else cslift s y) PTR(user_data_C) cuser_user_data_relation\<rbrakk> \<Longrightarrow> pspace_distinct' \<sigma>
 3. \<And>x v v'. \<lbrakk>cslift s (PTR(user_data_device_C) x) = Some v'; pspace_aligned' \<sigma>; cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)) = Some page; cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift s) ep_Ptr (cendpoint_relation (cslift s)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift s) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift s) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift s) ap_Ptr casid_pool_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid s) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid s) pt_Ptr; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0))) (\<lambda>y. if ptr_val y = ptr && ~~ mask pageBits then Some (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s y))) else cslift s y) PTR(user_data_C) cuser_user_data_relation\<rbrakk> \<Longrightarrow> pspace_aligned' \<sigma>
 4. \<And>x v v'. \<lbrakk>cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)) = Some page; cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift s) ep_Ptr (cendpoint_relation (cslift s)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift s) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift s) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift s) ap_Ptr casid_pool_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid s) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid s) pt_Ptr; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0))) (\<lambda>y. if ptr_val y = ptr && ~~ mask pageBits then Some (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s y))) else cslift s y) PTR(user_data_C) cuser_user_data_relation; heap_to_device_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0)) x = Some v; cslift s (PTR(user_data_device_C) x) = Some v'; pspace_aligned' \<sigma>\<rbrakk> \<Longrightarrow> cuser_user_data_device_relation v v' proof (prove)
goal (1 subgoal):
 1. \<And>x v v'. \<lbrakk>cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)) = Some page; cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift s) ep_Ptr (cendpoint_relation (cslift s)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift s) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift s) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift s) ap_Ptr casid_pool_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid s) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid s) pt_Ptr; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0))) (\<lambda>y. if ptr_val y = ptr && ~~ mask pageBits then Some (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s y))) else cslift s y) PTR(user_data_C) cuser_user_data_relation; heap_to_device_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0)) x = Some v; cslift s (PTR(user_data_device_C) x) = Some v'\<rbrakk> \<Longrightarrow> cuser_user_data_device_relation v v' proof (prove)
goal (4 subgoals):
 1. \<And>x v v'. \<lbrakk>cslift s (PTR(user_data_device_C) x) = Some v'; cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)) = Some page; cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift s) ep_Ptr (cendpoint_relation (cslift s)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift s) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift s) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift s) ap_Ptr casid_pool_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid s) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid s) pt_Ptr; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0))) (\<lambda>y. if ptr_val y = ptr && ~~ mask pageBits then Some (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s y))) else cslift s y) PTR(user_data_C) cuser_user_data_relation\<rbrakk> \<Longrightarrow> \<not> pointerInDeviceData (ptr + 2) \<sigma>
 2. \<And>x v v'. \<lbrakk>cslift s (PTR(user_data_device_C) x) = Some v'; cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)) = Some page; cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift s) ep_Ptr (cendpoint_relation (cslift s)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift s) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift s) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift s) ap_Ptr casid_pool_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid s) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid s) pt_Ptr; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0))) (\<lambda>y. if ptr_val y = ptr && ~~ mask pageBits then Some (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s y))) else cslift s y) PTR(user_data_C) cuser_user_data_relation\<rbrakk> \<Longrightarrow> pspace_distinct' \<sigma>
 3. \<And>x v v'. \<lbrakk>cslift s (PTR(user_data_device_C) x) = Some v'; cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)) = Some page; cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift s) ep_Ptr (cendpoint_relation (cslift s)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift s) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift s) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift s) ap_Ptr casid_pool_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid s) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid s) pt_Ptr; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0))) (\<lambda>y. if ptr_val y = ptr && ~~ mask pageBits then Some (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s y))) else cslift s y) PTR(user_data_C) cuser_user_data_relation\<rbrakk> \<Longrightarrow> pspace_aligned' \<sigma>
 4. \<And>x v v'. \<lbrakk>cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)) = Some page; cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift s) ep_Ptr (cendpoint_relation (cslift s)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift s) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift s) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift s) ap_Ptr casid_pool_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid s) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid s) pt_Ptr; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0))) (\<lambda>y. if ptr_val y = ptr && ~~ mask pageBits then Some (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s y))) else cslift s y) PTR(user_data_C) cuser_user_data_relation; heap_to_device_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2)) x = Some v; cslift s (PTR(user_data_device_C) x) = Some v'\<rbrakk> \<Longrightarrow> cuser_user_data_device_relation v v' proof (prove)
goal (1 subgoal):
 1. \<And>x v v'. \<lbrakk>cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)) = Some page; cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift s) ep_Ptr (cendpoint_relation (cslift s)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift s) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift s) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift s) ap_Ptr casid_pool_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid s) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid s) pt_Ptr; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0))) (\<lambda>y. if ptr_val y = ptr && ~~ mask pageBits then Some (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s y))) else cslift s y) PTR(user_data_C) cuser_user_data_relation; heap_to_device_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2)) x = Some v; cslift s (PTR(user_data_device_C) x) = Some v'\<rbrakk> \<Longrightarrow> cuser_user_data_device_relation v v' proof (prove)
goal (4 subgoals):
 1. \<And>x v v'. \<lbrakk>cslift s (PTR(user_data_device_C) x) = Some v'; cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)) = Some page; cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift s) ep_Ptr (cendpoint_relation (cslift s)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift s) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift s) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift s) ap_Ptr casid_pool_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid s) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid s) pt_Ptr; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0))) (\<lambda>y. if ptr_val y = ptr && ~~ mask pageBits then Some (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s y))) else cslift s y) PTR(user_data_C) cuser_user_data_relation\<rbrakk> \<Longrightarrow> \<not> pointerInDeviceData (ptr + 1) \<sigma>
 2. \<And>x v v'. \<lbrakk>cslift s (PTR(user_data_device_C) x) = Some v'; cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)) = Some page; cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift s) ep_Ptr (cendpoint_relation (cslift s)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift s) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift s) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift s) ap_Ptr casid_pool_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid s) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid s) pt_Ptr; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0))) (\<lambda>y. if ptr_val y = ptr && ~~ mask pageBits then Some (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s y))) else cslift s y) PTR(user_data_C) cuser_user_data_relation\<rbrakk> \<Longrightarrow> pspace_distinct' \<sigma>
 3. \<And>x v v'. \<lbrakk>cslift s (PTR(user_data_device_C) x) = Some v'; cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)) = Some page; cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift s) ep_Ptr (cendpoint_relation (cslift s)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift s) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift s) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift s) ap_Ptr casid_pool_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid s) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid s) pt_Ptr; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0))) (\<lambda>y. if ptr_val y = ptr && ~~ mask pageBits then Some (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s y))) else cslift s y) PTR(user_data_C) cuser_user_data_relation\<rbrakk> \<Longrightarrow> pspace_aligned' \<sigma>
 4. \<And>x v v'. \<lbrakk>cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)) = Some page; cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift s) ep_Ptr (cendpoint_relation (cslift s)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift s) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift s) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift s) ap_Ptr casid_pool_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid s) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid s) pt_Ptr; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0))) (\<lambda>y. if ptr_val y = ptr && ~~ mask pageBits then Some (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s y))) else cslift s y) PTR(user_data_C) cuser_user_data_relation; heap_to_device_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3)) x = Some v; cslift s (PTR(user_data_device_C) x) = Some v'\<rbrakk> \<Longrightarrow> cuser_user_data_device_relation v v' proof (prove)
goal (1 subgoal):
 1. \<And>x v v'. \<lbrakk>cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)) = Some page; cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift s) ep_Ptr (cendpoint_relation (cslift s)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift s) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift s) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift s) ap_Ptr casid_pool_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid s) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid s) pt_Ptr; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0))) (\<lambda>y. if ptr_val y = ptr && ~~ mask pageBits then Some (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s y))) else cslift s y) PTR(user_data_C) cuser_user_data_relation; heap_to_device_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3)) x = Some v; cslift s (PTR(user_data_device_C) x) = Some v'\<rbrakk> \<Longrightarrow> cuser_user_data_device_relation v v' proof (prove)
goal (4 subgoals):
 1. \<And>x v v'. \<lbrakk>cslift s (PTR(user_data_device_C) x) = Some v'; cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)) = Some page; cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift s) ep_Ptr (cendpoint_relation (cslift s)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift s) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift s) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift s) ap_Ptr casid_pool_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid s) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid s) pt_Ptr; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0))) (\<lambda>y. if ptr_val y = ptr && ~~ mask pageBits then Some (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s y))) else cslift s y) PTR(user_data_C) cuser_user_data_relation\<rbrakk> \<Longrightarrow> \<not> pointerInDeviceData ptr \<sigma>
 2. \<And>x v v'. \<lbrakk>cslift s (PTR(user_data_device_C) x) = Some v'; cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)) = Some page; cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift s) ep_Ptr (cendpoint_relation (cslift s)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift s) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift s) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift s) ap_Ptr casid_pool_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid s) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid s) pt_Ptr; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0))) (\<lambda>y. if ptr_val y = ptr && ~~ mask pageBits then Some (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s y))) else cslift s y) PTR(user_data_C) cuser_user_data_relation\<rbrakk> \<Longrightarrow> pspace_distinct' \<sigma>
 3. \<And>x v v'. \<lbrakk>cslift s (PTR(user_data_device_C) x) = Some v'; cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)) = Some page; cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift s) ep_Ptr (cendpoint_relation (cslift s)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift s) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift s) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift s) ap_Ptr casid_pool_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid s) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid s) pt_Ptr; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0))) (\<lambda>y. if ptr_val y = ptr && ~~ mask pageBits then Some (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s y))) else cslift s y) PTR(user_data_C) cuser_user_data_relation\<rbrakk> \<Longrightarrow> pspace_aligned' \<sigma>
 4. \<And>x v v'. \<lbrakk>cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)) = Some page; cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift s) ep_Ptr (cendpoint_relation (cslift s)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift s) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift s) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift s) ap_Ptr casid_pool_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid s) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid s) pt_Ptr; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0))) (\<lambda>y. if ptr_val y = ptr && ~~ mask pageBits then Some (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s y))) else cslift s y) PTR(user_data_C) cuser_user_data_relation; heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) x = Some v; cslift s (PTR(user_data_device_C) x) = Some v'\<rbrakk> \<Longrightarrow> cuser_user_data_device_relation v v' proof (prove)
goal (1 subgoal):
 1. \<And>x v v'. \<lbrakk>cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)) = Some page; cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift s) ep_Ptr (cendpoint_relation (cslift s)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift s) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift s) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift s) ap_Ptr casid_pool_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid s) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid s) pt_Ptr; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0))) (\<lambda>y. if ptr_val y = ptr && ~~ mask pageBits then Some (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s y))) else cslift s y) PTR(user_data_C) cuser_user_data_relation; heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) x = Some v; cslift s (PTR(user_data_device_C) x) = Some v'\<rbrakk> \<Longrightarrow> cuser_user_data_device_relation v v' proof (prove)
goal (2 subgoals):
 1. \<And>x v v'. \<lbrakk>cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)) = Some page; cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift s) ep_Ptr (cendpoint_relation (cslift s)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift s) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift s) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift s) ap_Ptr casid_pool_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid s) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid s) pt_Ptr; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0))) (\<lambda>y. if ptr_val y = ptr && ~~ mask pageBits then Some (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s y))) else cslift s y) PTR(user_data_C) cuser_user_data_relation; heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) x = Some v; cslift s (PTR(user_data_device_C) x) = Some v'\<rbrakk> \<Longrightarrow> heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (?x48 x v v') = Some v
 2. \<And>x v v'. \<lbrakk>cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)) = Some page; cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift s) ep_Ptr (cendpoint_relation (cslift s)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift s) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift s) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift s) ap_Ptr casid_pool_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid s) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid s) pt_Ptr; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0))) (\<lambda>y. if ptr_val y = ptr && ~~ mask pageBits then Some (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s y))) else cslift s y) PTR(user_data_C) cuser_user_data_relation; heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) x = Some v; cslift s (PTR(user_data_device_C) x) = Some v'\<rbrakk> \<Longrightarrow> cslift s (PTR(user_data_device_C) (?x48 x v v')) = Some v' proof (prove)
goal:
No subgoals! proof (state)
this:
cpspace_relation (ksPSpace \<sigma>) (underlying_memory (underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>))) (hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s)))

goal (1 subgoal):
 1. \<And>\<sigma> s. (\<sigma>, s) \<in> rf_sr \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pointerInUserData ptr \<sigma> \<and> is_aligned ptr 2 \<Longrightarrow> (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>)\<rparr>, s\<lparr>globals := globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
using this:
cpspace_relation (ksPSpace \<sigma>) (underlying_memory (underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>))) (hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s)))

goal (1 subgoal):
 1. (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>)\<rparr>, s\<lparr>globals := globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
using this:
cpspace_relation (ksPSpace \<sigma>) (underlying_memory (underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>))) (hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s)))
(\<sigma>, s) \<in> rf_sr

goal (1 subgoal):
 1. (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>)\<rparr>, s\<lparr>globals := globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cpspace_relation (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) (hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))); cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals s)) \<and> cready_queues_relation (cslift s) (ksReadyQueues_' (globals s)) (ksReadyQueues \<sigma>) \<and> zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals s)) \<and> cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s)) (ksReadyQueuesL1Bitmap \<sigma>) \<and> cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s)) (ksReadyQueuesL2Bitmap \<sigma>) \<and> ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>) \<and> ksIdleThread_' (globals s) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>) \<and> cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s)) \<and> cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals s)) \<and> carch_state_relation (ksArchState \<sigma>) (globals s) \<and> cmachine_state_relation (ksMachineState \<sigma>) (globals s) \<and> cte_array_relation \<sigma> (globals s) \<and> tcb_cte_array_relation \<sigma> (globals s) \<and> apsnd fst (ghost'state_' (globals s)) = (gsUserPages \<sigma>, gsCNodes \<sigma>) \<and> ghost_size_rel (ghost'state_' (globals s)) (gsMaxObjectSize \<sigma>) \<and> ksWorkUnitsCompleted_' (globals s) = ksWorkUnitsCompleted \<sigma> \<and> s \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr \<and> {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs \<and> s \<Turnstile>\<^sub>c armKSGlobalPD_Ptr \<and> {symbol_table ''armKSGlobalPD''..+16384} \<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 \<sigma>) kernel_all_global_addresses.ksDomSchedule \<and> ksDomScheduleIdx_' (globals s) = word_of_nat (ksDomScheduleIdx \<sigma>) \<and> ksCurDomain_' (globals s) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>) \<and> ksDomainTime_' (globals s) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))) \<and> carch_state_relation (ksArchState \<sigma>) (globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))\<rparr>) \<and> cmachine_state_relation (underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>)) (globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cpspace_relation (ksPSpace \<sigma>) ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) (hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))); cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals s)) \<and> cready_queues_relation (cslift s) (ksReadyQueues_' (globals s)) (ksReadyQueues \<sigma>) \<and> zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals s)) \<and> cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s)) (ksReadyQueuesL1Bitmap \<sigma>) \<and> cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s)) (ksReadyQueuesL2Bitmap \<sigma>) \<and> ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>) \<and> ksIdleThread_' (globals s) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>) \<and> cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s)) \<and> cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals s)) \<and> armKSNextASID_' (globals s) = armKSNextASID (ksArchState \<sigma>) \<and> armKSKernelVSpace (ksArchState \<sigma>) = armKSKernelVSpace_C \<and> array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState \<sigma>)) (armKSHWASIDTable_' (globals s)) \<and> array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState \<sigma>)) (armKSASIDTable_' (globals s)) \<and> asid_map_pd_to_hwasids (armKSASIDMap (ksArchState \<sigma>)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift s \<circ>\<^sub>m pd_pointer_to_asid_slot) \<and> armKSGlobalPD (ksArchState \<sigma>) = symbol_table ''armKSGlobalPD'' \<and> armKSGlobalPTs (ksArchState \<sigma>) = [symbol_table ''armKSGlobalPT''] \<and> irq_masks (ksMachineState \<sigma>) = irq_masks (phantom_machine_state_' (globals s)) \<and> irq_state (ksMachineState \<sigma>) = irq_state (phantom_machine_state_' (globals s)) \<and> device_state (ksMachineState \<sigma>) = device_state (phantom_machine_state_' (globals s)) \<and> exclusive_state (ksMachineState \<sigma>) = exclusive_state (phantom_machine_state_' (globals s)) \<and> machine_state_rest (ksMachineState \<sigma>) = machine_state_rest (phantom_machine_state_' (globals s)) \<and> cte_array_relation \<sigma> (globals s) \<and> tcb_cte_array_relation \<sigma> (globals s) \<and> apsnd fst (ghost'state_' (globals s)) = (gsUserPages \<sigma>, gsCNodes \<sigma>) \<and> ghost_size_rel (ghost'state_' (globals s)) (gsMaxObjectSize \<sigma>) \<and> ksWorkUnitsCompleted_' (globals s) = ksWorkUnitsCompleted \<sigma> \<and> s \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr \<and> {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs \<and> s \<Turnstile>\<^sub>c armKSGlobalPD_Ptr \<and> {symbol_table ''armKSGlobalPD''..+16384} \<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 \<sigma>) kernel_all_global_addresses.ksDomSchedule \<and> ksDomScheduleIdx_' (globals s) = word_of_nat (ksDomScheduleIdx \<sigma>) \<and> ksCurDomain_' (globals s) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>) \<and> ksDomainTime_' (globals s) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))) \<and> set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift s \<circ>\<^sub>m pd_pointer_to_asid_slot) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))) \<circ>\<^sub>m pd_pointer_to_asid_slot) proof (prove)
goal:
No subgoals! proof (state)
this:
(\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>)\<rparr>, s\<lparr>globals := globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))\<rparr>\<rparr>) \<in> rf_sr

goal:
No subgoals!