theory SR_lemmas_C

lemma user_word_at_cross_over:
  "\<lbrakk> user_word_at x p s; (s, s') \<in> rf_sr; p' = Ptr p \<rbrakk>
   \<Longrightarrow> c_guard p' \<and> hrs_htd (t_hrs_' (globals s')) \<Turnstile>\<^sub>t p'
         \<and> h_val (hrs_mem (t_hrs_' (globals s'))) p' = x" apply (drule rf_sr_heap_user_data_relation) apply (erule cmap_relationE1) apply (clarsimp simp: heap_to_user_data_def Let_def
                         user_word_at_def pointerInUserData_def
                         typ_at_to_obj_at'[where 'a=user_data, simplified]) apply (drule obj_at_ko_at', clarsimp) apply (rule conjI, rule exI, erule ko_at_projectKO_opt) apply (rule refl) apply (thin_tac "heap_to_user_data a b c = d" for a b c d) apply (cut_tac x=p and w="~~ mask pageBits" in word_plus_and_or_coroll2) apply (rule conjI) apply (clarsimp simp: user_word_at_def pointerInUserData_def) apply (simp add: c_guard_def c_null_guard_def ptr_aligned_def) apply (drule lift_t_g) apply (clarsimp simp: ) apply (simp add: align_of_def size_of_def) apply (fold is_aligned_def[where n=2, simplified], simp) apply (erule contra_subsetD[rotated]) apply (rule order_trans[rotated]) apply (rule_tac x="p && mask pageBits" and y=4 in intvl_sub_offset) apply (cut_tac y=p and a="mask pageBits && (~~ mask 2)" in word_and_le1) apply (subst(asm) word_bw_assocs[symmetric], subst(asm) is_aligned_neg_mask_eq,
           erule is_aligned_andI1) apply (simp add: word_le_nat_alt mask_def pageBits_def) apply simp apply (clarsimp simp: cuser_user_data_relation_def user_word_at_def) apply (frule_tac f="[''words_C'']" in h_t_valid_field[OF h_t_valid_clift],
         simp+) apply (drule_tac n="uint (p && mask pageBits >> 2)" in h_t_valid_Array_element) apply simp apply (simp add: shiftr_over_and_dist mask_def pageBits_def uint_and) apply (insert int_and_leR [where a="uint (p >> 2)" and b=1023], clarsimp)[1] apply (simp add: field_lvalue_def
            field_lookup_offset_eq[OF trans, OF _ arg_cong[where f=Some, symmetric], OF _ prod.collapse]
            word_shift_by_2 shiftr_shiftl1 is_aligned_andI1) apply (drule_tac x="ucast (p >> 2)" in spec) apply (simp add: byte_to_word_heap_def Let_def ucast_ucast_mask) apply (fold shiftl_t2n[where n=2, simplified, simplified mult.commute mult.left_commute]) apply (simp add: aligned_shiftr_mask_shiftl pageBits_def) apply (rule trans[rotated], rule_tac hp="hrs_mem (t_hrs_' (globals s'))"
                                   and x="Ptr &(Ptr (p && ~~ mask 12) \<rightarrow> [''words_C''])"
                                    in access_in_array) apply (rule trans) apply (erule typ_heap_simps) apply simp+ apply (rule order_less_le_trans, rule unat_lt2p) apply simp apply (fastforce simp add: typ_info_word) apply simp apply (rule_tac f="h_val hp" for hp in arg_cong) apply simp apply (simp add: field_lvalue_def) apply (simp add: ucast_nat_def ucast_ucast_mask) apply (fold shiftl_t2n[where n=2, simplified, simplified mult.commute mult.left_commute]) apply (simp add: aligned_shiftr_mask_shiftl) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>user_word_at x p s; (s, s') \<in> rf_sr; p' = PTR(32 word) p\<rbrakk> \<Longrightarrow> c_guard p' \<and> s' \<Turnstile>\<^sub>c p' \<and> h_val (hrs_mem (t_hrs_' (globals s'))) p' = x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>user_word_at x p s; p' = PTR(32 word) p; cmap_relation (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_C) cuser_user_data_relation\<rbrakk> \<Longrightarrow> c_guard p' \<and> s' \<Turnstile>\<^sub>c p' \<and> h_val (hrs_mem (t_hrs_' (globals s'))) p' = x proof (prove)
goal (2 subgoals):
 1. \<lbrakk>user_word_at x p s; p' = PTR(32 word) p\<rbrakk> \<Longrightarrow> heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s)) ?x2 = Some ?y2
 2. \<And>y'. \<lbrakk>user_word_at x p s; p' = PTR(32 word) p; heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s)) ?x2 = Some ?y2; cuser_user_data_relation ?y2 y'; cslift s' (PTR(user_data_C) ?x2) = Some y'\<rbrakk> \<Longrightarrow> c_guard p' \<and> s' \<Turnstile>\<^sub>c p' \<and> h_val (hrs_mem (t_hrs_' (globals s'))) p' = x proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p' = PTR(32 word) p; is_aligned p 2; obj_at' (\<lambda>_. True) (p && ~~ mask pageBits) s; x = word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p]\<rbrakk> \<Longrightarrow> (\<exists>z. map_to_user_data (ksPSpace s) ?x2 = Some z) \<and> byte_to_word_heap (underlying_memory (ksMachineState s)) ?x2 = ?y2
 2. \<And>y'. \<lbrakk>user_word_at x p s; p' = PTR(32 word) p; heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s)) ?x2 = Some ?y2; cuser_user_data_relation ?y2 y'; cslift s' (PTR(user_data_C) ?x2) = Some y'\<rbrakk> \<Longrightarrow> c_guard p' \<and> s' \<Turnstile>\<^sub>c p' \<and> h_val (hrs_mem (t_hrs_' (globals s'))) p' = x proof (prove)
goal (2 subgoals):
 1. \<And>ko. \<lbrakk>p' = PTR(32 word) p; is_aligned p 2; x = word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p]; ko_at' ko (p && ~~ mask pageBits) s\<rbrakk> \<Longrightarrow> (\<exists>z. map_to_user_data (ksPSpace s) ?x2 = Some z) \<and> byte_to_word_heap (underlying_memory (ksMachineState s)) ?x2 = ?y2
 2. \<And>y'. \<lbrakk>user_word_at x p s; p' = PTR(32 word) p; heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s)) ?x2 = Some ?y2; cuser_user_data_relation ?y2 y'; cslift s' (PTR(user_data_C) ?x2) = Some y'\<rbrakk> \<Longrightarrow> c_guard p' \<and> s' \<Turnstile>\<^sub>c p' \<and> h_val (hrs_mem (t_hrs_' (globals s'))) p' = x proof (prove)
goal (2 subgoals):
 1. \<And>ko. \<lbrakk>p' = PTR(32 word) p; is_aligned p 2; x = word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p]; ko_at' ko (p && ~~ mask pageBits) s\<rbrakk> \<Longrightarrow> byte_to_word_heap (underlying_memory (ksMachineState s)) (p && ~~ mask pageBits) = ?y2
 2. \<And>y'. \<lbrakk>user_word_at x p s; p' = PTR(32 word) p; heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s)) (p && ~~ mask pageBits) = Some ?y2; cuser_user_data_relation ?y2 y'; cslift s' (PTR(user_data_C) (p && ~~ mask pageBits)) = Some y'\<rbrakk> \<Longrightarrow> c_guard p' \<and> s' \<Turnstile>\<^sub>c p' \<and> h_val (hrs_mem (t_hrs_' (globals s'))) p' = x proof (prove)
goal (1 subgoal):
 1. \<And>y'. \<lbrakk>user_word_at x p s; p' = PTR(32 word) p; heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s)) (p && ~~ mask pageBits) = Some (byte_to_word_heap (underlying_memory (ksMachineState s)) (p && ~~ mask pageBits)); cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState s)) (p && ~~ mask pageBits)) y'; cslift s' (PTR(user_data_C) (p && ~~ mask pageBits)) = Some y'\<rbrakk> \<Longrightarrow> c_guard p' \<and> s' \<Turnstile>\<^sub>c p' \<and> h_val (hrs_mem (t_hrs_' (globals s'))) p' = x proof (prove)
goal (1 subgoal):
 1. \<And>y'. \<lbrakk>user_word_at x p s; p' = PTR(32 word) p; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState s)) (p && ~~ mask pageBits)) y'; cslift s' (PTR(user_data_C) (p && ~~ mask pageBits)) = Some y'\<rbrakk> \<Longrightarrow> c_guard p' \<and> s' \<Turnstile>\<^sub>c p' \<and> h_val (hrs_mem (t_hrs_' (globals s'))) p' = x proof (prove)
goal (1 subgoal):
 1. \<And>y'. \<lbrakk>user_word_at x p s; p' = PTR(32 word) p; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState s)) (p && ~~ mask pageBits)) y'; cslift s' (PTR(user_data_C) (p && ~~ mask pageBits)) = Some y'; (p && ~~ mask pageBits) + (p && ~~ ~~ mask pageBits) = p\<rbrakk> \<Longrightarrow> c_guard p' \<and> s' \<Turnstile>\<^sub>c p' \<and> h_val (hrs_mem (t_hrs_' (globals s'))) p' = x proof (prove)
goal (2 subgoals):
 1. \<And>y'. \<lbrakk>user_word_at x p s; p' = PTR(32 word) p; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState s)) (p && ~~ mask pageBits)) y'; cslift s' (PTR(user_data_C) (p && ~~ mask pageBits)) = Some y'; (p && ~~ mask pageBits) + (p && ~~ ~~ mask pageBits) = p\<rbrakk> \<Longrightarrow> c_guard p'
 2. \<And>y'. \<lbrakk>user_word_at x p s; p' = PTR(32 word) p; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState s)) (p && ~~ mask pageBits)) y'; cslift s' (PTR(user_data_C) (p && ~~ mask pageBits)) = Some y'; (p && ~~ mask pageBits) + (p && ~~ ~~ mask pageBits) = p\<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c p' \<and> h_val (hrs_mem (t_hrs_' (globals s'))) p' = x proof (prove)
goal (2 subgoals):
 1. \<And>y'. \<lbrakk>p' = PTR(32 word) p; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState s)) (p && ~~ mask pageBits)) y'; cslift s' (PTR(user_data_C) (p && ~~ mask pageBits)) = Some y'; (p && ~~ mask pageBits) + (p && mask pageBits) = p; is_aligned p 2; typ_at' UserDataT (p && ~~ mask pageBits) s; x = word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p]\<rbrakk> \<Longrightarrow> c_guard (PTR(32 word) p)
 2. \<And>y'. \<lbrakk>user_word_at x p s; p' = PTR(32 word) p; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState s)) (p && ~~ mask pageBits)) y'; cslift s' (PTR(user_data_C) (p && ~~ mask pageBits)) = Some y'; (p && ~~ mask pageBits) + (p && ~~ ~~ mask pageBits) = p\<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c p' \<and> h_val (hrs_mem (t_hrs_' (globals s'))) p' = x proof (prove)
goal (2 subgoals):
 1. \<And>y'. \<lbrakk>p' = PTR(32 word) p; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState s)) (p && ~~ mask pageBits)) y'; lift_t (\<lambda>p. align_of TYPE(user_data_C) dvd unat (ptr_val p) \<and> 0 \<notin> {ptr_val p..+4096}) (t_hrs_' (globals s')) (PTR(user_data_C) (p && ~~ mask pageBits)) = Some y'; (p && ~~ mask pageBits) + (p && mask pageBits) = p; is_aligned p 2; typ_at' UserDataT (p && ~~ mask pageBits) s; x = word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p]\<rbrakk> \<Longrightarrow> 4 dvd unat p \<and> 0 \<notin> {p..+4}
 2. \<And>y'. \<lbrakk>user_word_at x p s; p' = PTR(32 word) p; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState s)) (p && ~~ mask pageBits)) y'; cslift s' (PTR(user_data_C) (p && ~~ mask pageBits)) = Some y'; (p && ~~ mask pageBits) + (p && ~~ ~~ mask pageBits) = p\<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c p' \<and> h_val (hrs_mem (t_hrs_' (globals s'))) p' = x proof (prove)
goal (2 subgoals):
 1. \<And>y'. \<lbrakk>p' = PTR(32 word) p; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState s)) (p && ~~ mask pageBits)) y'; (p && ~~ mask pageBits) + (p && mask pageBits) = p; is_aligned p 2; typ_at' UserDataT (p && ~~ mask pageBits) s; x = word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p]; align_of TYPE(user_data_C) dvd unat (ptr_val (PTR(user_data_C) (p && ~~ mask pageBits))) \<and> 0 \<notin> {ptr_val (PTR(user_data_C) (p && ~~ mask pageBits))..+4096}\<rbrakk> \<Longrightarrow> 4 dvd unat p \<and> 0 \<notin> {p..+4}
 2. \<And>y'. \<lbrakk>user_word_at x p s; p' = PTR(32 word) p; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState s)) (p && ~~ mask pageBits)) y'; cslift s' (PTR(user_data_C) (p && ~~ mask pageBits)) = Some y'; (p && ~~ mask pageBits) + (p && ~~ ~~ mask pageBits) = p\<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c p' \<and> h_val (hrs_mem (t_hrs_' (globals s'))) p' = x proof (prove)
goal (2 subgoals):
 1. \<And>y'. \<lbrakk>p' = PTR(32 word) p; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState s)) (p && ~~ mask pageBits)) y'; (p && ~~ mask pageBits) + (p && mask pageBits) = p; is_aligned p 2; typ_at' UserDataT (p && ~~ mask pageBits) s; x = word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p]; align_of TYPE(user_data_C) dvd unat (p && ~~ mask pageBits); 0 \<notin> {p && ~~ mask pageBits..+4096}\<rbrakk> \<Longrightarrow> 4 dvd unat p \<and> 0 \<notin> {p..+4}
 2. \<And>y'. \<lbrakk>user_word_at x p s; p' = PTR(32 word) p; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState s)) (p && ~~ mask pageBits)) y'; cslift s' (PTR(user_data_C) (p && ~~ mask pageBits)) = Some y'; (p && ~~ mask pageBits) + (p && ~~ ~~ mask pageBits) = p\<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c p' \<and> h_val (hrs_mem (t_hrs_' (globals s'))) p' = x proof (prove)
goal (2 subgoals):
 1. \<And>y'. \<lbrakk>p' = PTR(32 word) p; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState s)) (p && ~~ mask pageBits)) y'; (p && ~~ mask pageBits) + (p && mask pageBits) = p; is_aligned p 2; typ_at' UserDataT (p && ~~ mask pageBits) s; x = word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p]; 4 dvd unat (p && ~~ mask pageBits); 0 \<notin> {p && ~~ mask pageBits..+4096}\<rbrakk> \<Longrightarrow> 4 dvd unat p \<and> 0 \<notin> {p..+4}
 2. \<And>y'. \<lbrakk>user_word_at x p s; p' = PTR(32 word) p; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState s)) (p && ~~ mask pageBits)) y'; cslift s' (PTR(user_data_C) (p && ~~ mask pageBits)) = Some y'; (p && ~~ mask pageBits) + (p && ~~ ~~ mask pageBits) = p\<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c p' \<and> h_val (hrs_mem (t_hrs_' (globals s'))) p' = x proof (prove)
goal (2 subgoals):
 1. \<And>y'. \<lbrakk>p' = PTR(32 word) p; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState s)) (p && ~~ mask pageBits)) y'; (p && ~~ mask pageBits) + (p && mask pageBits) = p; is_aligned p 2; typ_at' UserDataT (p && ~~ mask pageBits) s; x = word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p]; is_aligned (p && ~~ mask pageBits) 2; 0 \<notin> {p && ~~ mask pageBits..+4096}\<rbrakk> \<Longrightarrow> 0 \<notin> {p..+4}
 2. \<And>y'. \<lbrakk>user_word_at x p s; p' = PTR(32 word) p; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState s)) (p && ~~ mask pageBits)) y'; cslift s' (PTR(user_data_C) (p && ~~ mask pageBits)) = Some y'; (p && ~~ mask pageBits) + (p && ~~ ~~ mask pageBits) = p\<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c p' \<and> h_val (hrs_mem (t_hrs_' (globals s'))) p' = x proof (prove)
goal (2 subgoals):
 1. \<And>y'. \<lbrakk>p' = PTR(32 word) p; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState s)) (p && ~~ mask pageBits)) y'; (p && ~~ mask pageBits) + (p && mask pageBits) = p; is_aligned p 2; typ_at' UserDataT (p && ~~ mask pageBits) s; x = word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p]; is_aligned (p && ~~ mask pageBits) 2\<rbrakk> \<Longrightarrow> {p..+4} \<subseteq> {p && ~~ mask pageBits..+4096}
 2. \<And>y'. \<lbrakk>user_word_at x p s; p' = PTR(32 word) p; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState s)) (p && ~~ mask pageBits)) y'; cslift s' (PTR(user_data_C) (p && ~~ mask pageBits)) = Some y'; (p && ~~ mask pageBits) + (p && ~~ ~~ mask pageBits) = p\<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c p' \<and> h_val (hrs_mem (t_hrs_' (globals s'))) p' = x proof (prove)
goal (3 subgoals):
 1. \<And>y'. \<lbrakk>p' = PTR(32 word) p; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState s)) (p && ~~ mask pageBits)) y'; (p && ~~ mask pageBits) + (p && mask pageBits) = p; is_aligned p 2; typ_at' UserDataT (p && ~~ mask pageBits) s; x = word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p]; is_aligned (p && ~~ mask pageBits) 2\<rbrakk> \<Longrightarrow> ?y41 y' \<subseteq> {p && ~~ mask pageBits..+4096}
 2. \<And>y'. \<lbrakk>p' = PTR(32 word) p; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState s)) (p && ~~ mask pageBits)) y'; (p && ~~ mask pageBits) + (p && mask pageBits) = p; is_aligned p 2; typ_at' UserDataT (p && ~~ mask pageBits) s; x = word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p]; is_aligned (p && ~~ mask pageBits) 2\<rbrakk> \<Longrightarrow> {p..+4} \<subseteq> ?y41 y'
 3. \<And>y'. \<lbrakk>user_word_at x p s; p' = PTR(32 word) p; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState s)) (p && ~~ mask pageBits)) y'; cslift s' (PTR(user_data_C) (p && ~~ mask pageBits)) = Some y'; (p && ~~ mask pageBits) + (p && ~~ ~~ mask pageBits) = p\<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c p' \<and> h_val (hrs_mem (t_hrs_' (globals s'))) p' = x proof (prove)
goal (3 subgoals):
 1. \<And>y'. \<lbrakk>p' = PTR(32 word) p; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState s)) (p && ~~ mask pageBits)) y'; (p && ~~ mask pageBits) + (p && mask pageBits) = p; is_aligned p 2; typ_at' UserDataT (p && ~~ mask pageBits) s; x = word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p]; is_aligned (p && ~~ mask pageBits) 2\<rbrakk> \<Longrightarrow> unat (p && mask pageBits) + 4 \<le> 4096
 2. \<And>y'. \<lbrakk>p' = PTR(32 word) p; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState s)) (p && ~~ mask pageBits)) y'; (p && ~~ mask pageBits) + (p && mask pageBits) = p; is_aligned p 2; typ_at' UserDataT (p && ~~ mask pageBits) s; x = word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p]; is_aligned (p && ~~ mask pageBits) 2\<rbrakk> \<Longrightarrow> {p..+4} \<subseteq> {(p && ~~ mask pageBits) + (p && mask pageBits)..+4}
 3. \<And>y'. \<lbrakk>user_word_at x p s; p' = PTR(32 word) p; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState s)) (p && ~~ mask pageBits)) y'; cslift s' (PTR(user_data_C) (p && ~~ mask pageBits)) = Some y'; (p && ~~ mask pageBits) + (p && ~~ ~~ mask pageBits) = p\<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c p' \<and> h_val (hrs_mem (t_hrs_' (globals s'))) p' = x proof (prove)
goal (3 subgoals):
 1. \<And>y'. \<lbrakk>p' = PTR(32 word) p; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState s)) (p && ~~ mask pageBits)) y'; (p && ~~ mask pageBits) + (p && mask pageBits) = p; is_aligned p 2; typ_at' UserDataT (p && ~~ mask pageBits) s; x = word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p]; is_aligned (p && ~~ mask pageBits) 2; p && mask pageBits && ~~ mask 2 \<le> mask pageBits && ~~ mask 2\<rbrakk> \<Longrightarrow> unat (p && mask pageBits) + 4 \<le> 4096
 2. \<And>y'. \<lbrakk>p' = PTR(32 word) p; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState s)) (p && ~~ mask pageBits)) y'; (p && ~~ mask pageBits) + (p && mask pageBits) = p; is_aligned p 2; typ_at' UserDataT (p && ~~ mask pageBits) s; x = word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p]; is_aligned (p && ~~ mask pageBits) 2\<rbrakk> \<Longrightarrow> {p..+4} \<subseteq> {(p && ~~ mask pageBits) + (p && mask pageBits)..+4}
 3. \<And>y'. \<lbrakk>user_word_at x p s; p' = PTR(32 word) p; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState s)) (p && ~~ mask pageBits)) y'; cslift s' (PTR(user_data_C) (p && ~~ mask pageBits)) = Some y'; (p && ~~ mask pageBits) + (p && ~~ ~~ mask pageBits) = p\<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c p' \<and> h_val (hrs_mem (t_hrs_' (globals s'))) p' = x proof (prove)
goal (3 subgoals):
 1. \<And>y'. \<lbrakk>p' = PTR(32 word) p; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState s)) (p && ~~ mask pageBits)) y'; (p && ~~ mask pageBits) + (p && mask pageBits) = p; is_aligned p 2; typ_at' UserDataT (p && ~~ mask pageBits) s; x = word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p]; is_aligned (p && ~~ mask pageBits) 2; p && mask pageBits \<le> mask pageBits && ~~ mask 2\<rbrakk> \<Longrightarrow> unat (p && mask pageBits) + 4 \<le> 4096
 2. \<And>y'. \<lbrakk>p' = PTR(32 word) p; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState s)) (p && ~~ mask pageBits)) y'; (p && ~~ mask pageBits) + (p && mask pageBits) = p; is_aligned p 2; typ_at' UserDataT (p && ~~ mask pageBits) s; x = word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p]; is_aligned (p && ~~ mask pageBits) 2\<rbrakk> \<Longrightarrow> {p..+4} \<subseteq> {(p && ~~ mask pageBits) + (p && mask pageBits)..+4}
 3. \<And>y'. \<lbrakk>user_word_at x p s; p' = PTR(32 word) p; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState s)) (p && ~~ mask pageBits)) y'; cslift s' (PTR(user_data_C) (p && ~~ mask pageBits)) = Some y'; (p && ~~ mask pageBits) + (p && ~~ ~~ mask pageBits) = p\<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c p' \<and> h_val (hrs_mem (t_hrs_' (globals s'))) p' = x proof (prove)
goal (2 subgoals):
 1. \<And>y'. \<lbrakk>p' = PTR(32 word) p; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState s)) (p && ~~ mask pageBits)) y'; (p && ~~ mask pageBits) + (p && mask pageBits) = p; is_aligned p 2; typ_at' UserDataT (p && ~~ mask pageBits) s; x = word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p]; is_aligned (p && ~~ mask pageBits) 2\<rbrakk> \<Longrightarrow> {p..+4} \<subseteq> {(p && ~~ mask pageBits) + (p && mask pageBits)..+4}
 2. \<And>y'. \<lbrakk>user_word_at x p s; p' = PTR(32 word) p; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState s)) (p && ~~ mask pageBits)) y'; cslift s' (PTR(user_data_C) (p && ~~ mask pageBits)) = Some y'; (p && ~~ mask pageBits) + (p && ~~ ~~ mask pageBits) = p\<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c p' \<and> h_val (hrs_mem (t_hrs_' (globals s'))) p' = x proof (prove)
goal (1 subgoal):
 1. \<And>y'. \<lbrakk>user_word_at x p s; p' = PTR(32 word) p; cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState s)) (p && ~~ mask pageBits)) y'; cslift s' (PTR(user_data_C) (p && ~~ mask pageBits)) = Some y'; (p && ~~ mask pageBits) + (p && ~~ ~~ mask pageBits) = p\<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c p' \<and> h_val (hrs_mem (t_hrs_' (globals s'))) p' = x proof (prove)
goal (1 subgoal):
 1. \<And>y'. \<lbrakk>p' = PTR(32 word) p; \<forall>off. byte_to_word_heap (underlying_memory (ksMachineState s)) (p && ~~ mask pageBits) off = user_data_C.words_C y'.[unat off]; cslift s' (PTR(user_data_C) (p && ~~ mask pageBits)) = Some y'; (p && ~~ mask pageBits) + (p && mask pageBits) = p; is_aligned p 2; pointerInUserData p s; x = word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p]\<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c PTR(32 word) p \<and> h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(32 word) p) = word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p] proof (prove)
goal (1 subgoal):
 1. \<And>y'. \<lbrakk>p' = PTR(32 word) p; \<forall>off. byte_to_word_heap (underlying_memory (ksMachineState s)) (p && ~~ mask pageBits) off = user_data_C.words_C y'.[unat off]; cslift s' (PTR(user_data_C) (p && ~~ mask pageBits)) = Some y'; (p && ~~ mask pageBits) + (p && mask pageBits) = p; is_aligned p 2; pointerInUserData p s; x = word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p]; s' \<Turnstile>\<^sub>c PTR(32 word[1024]) &(PTR(user_data_C) (p && ~~ mask pageBits)\<rightarrow>[''words_C''])\<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c PTR(32 word) p \<and> h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(32 word) p) = word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p] proof (prove)
goal (3 subgoals):
 1. \<And>y'. \<lbrakk>p' = PTR(32 word) p; \<forall>off. byte_to_word_heap (underlying_memory (ksMachineState s)) (p && ~~ mask pageBits) off = user_data_C.words_C y'.[unat off]; cslift s' (PTR(user_data_C) (p && ~~ mask pageBits)) = Some y'; (p && ~~ mask pageBits) + (p && mask pageBits) = p; is_aligned p 2; pointerInUserData p s; x = word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p]\<rbrakk> \<Longrightarrow> 0 \<le> uint (p && mask pageBits >> 2)
 2. \<And>y'. \<lbrakk>p' = PTR(32 word) p; \<forall>off. byte_to_word_heap (underlying_memory (ksMachineState s)) (p && ~~ mask pageBits) off = user_data_C.words_C y'.[unat off]; cslift s' (PTR(user_data_C) (p && ~~ mask pageBits)) = Some y'; (p && ~~ mask pageBits) + (p && mask pageBits) = p; is_aligned p 2; pointerInUserData p s; x = word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p]\<rbrakk> \<Longrightarrow> uint (p && mask pageBits >> 2) < int CARD(1024)
 3. \<And>y'. \<lbrakk>p' = PTR(32 word) p; \<forall>off. byte_to_word_heap (underlying_memory (ksMachineState s)) (p && ~~ mask pageBits) off = user_data_C.words_C y'.[unat off]; cslift s' (PTR(user_data_C) (p && ~~ mask pageBits)) = Some y'; (p && ~~ mask pageBits) + (p && mask pageBits) = p; is_aligned p 2; pointerInUserData p s; x = word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p]; s' \<Turnstile>\<^sub>c (PTR_COERCE(32 word[1024] \<rightarrow> 32 word) (PTR(32 word[1024]) &(PTR(user_data_C) (p && ~~ mask pageBits)\<rightarrow>[''words_C''])) +\<^sub>p uint (p && mask pageBits >> 2))\<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c PTR(32 word) p \<and> h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(32 word) p) = word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p] proof (prove)
goal (2 subgoals):
 1. \<And>y'. \<lbrakk>p' = PTR(32 word) p; \<forall>off. byte_to_word_heap (underlying_memory (ksMachineState s)) (p && ~~ mask pageBits) off = user_data_C.words_C y'.[unat off]; cslift s' (PTR(user_data_C) (p && ~~ mask pageBits)) = Some y'; (p && ~~ mask pageBits) + (p && mask pageBits) = p; is_aligned p 2; pointerInUserData p s; x = word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p]\<rbrakk> \<Longrightarrow> uint (p && mask pageBits >> 2) < int CARD(1024)
 2. \<And>y'. \<lbrakk>p' = PTR(32 word) p; \<forall>off. byte_to_word_heap (underlying_memory (ksMachineState s)) (p && ~~ mask pageBits) off = user_data_C.words_C y'.[unat off]; cslift s' (PTR(user_data_C) (p && ~~ mask pageBits)) = Some y'; (p && ~~ mask pageBits) + (p && mask pageBits) = p; is_aligned p 2; pointerInUserData p s; x = word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p]; s' \<Turnstile>\<^sub>c (PTR_COERCE(32 word[1024] \<rightarrow> 32 word) (PTR(32 word[1024]) &(PTR(user_data_C) (p && ~~ mask pageBits)\<rightarrow>[''words_C''])) +\<^sub>p uint (p && mask pageBits >> 2))\<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c PTR(32 word) p \<and> h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(32 word) p) = word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p] proof (prove)
goal (1 subgoal):
 1. \<And>y'. \<lbrakk>p' = PTR(32 word) p; \<forall>off. byte_to_word_heap (underlying_memory (ksMachineState s)) (p && ~~ mask pageBits) off = user_data_C.words_C y'.[unat off]; cslift s' (PTR(user_data_C) (p && ~~ mask pageBits)) = Some y'; (p && ~~ mask pageBits) + (p && mask pageBits) = p; is_aligned p 2; pointerInUserData p s; x = word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p]; s' \<Turnstile>\<^sub>c (PTR_COERCE(32 word[1024] \<rightarrow> 32 word) (PTR(32 word[1024]) &(PTR(user_data_C) (p && ~~ mask pageBits)\<rightarrow>[''words_C''])) +\<^sub>p uint (p && mask pageBits >> 2))\<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c PTR(32 word) p \<and> h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(32 word) p) = word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p] proof (prove)
goal (1 subgoal):
 1. \<And>y'. \<lbrakk>p' = PTR(32 word) p; \<forall>off. byte_to_word_heap (underlying_memory (ksMachineState s)) (p && ~~ mask pageBits) off = user_data_C.words_C y'.[unat off]; cslift s' (PTR(user_data_C) (p && ~~ mask pageBits)) = Some y'; (p && ~~ mask pageBits) + (p && mask pageBits) = p; is_aligned p 2; pointerInUserData p s; x = word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p]; s' \<Turnstile>\<^sub>c PTR(32 word) (&(PTR(user_data_C) (p && ~~ mask pageBits)\<rightarrow>[''words_C'']) + (p && mask pageBits >> 2) * 4)\<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c PTR(32 word) p \<and> h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(32 word) p) = word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p] proof (prove)
goal (1 subgoal):
 1. \<And>y'. \<lbrakk>p' = PTR(32 word) p; \<forall>off. byte_to_word_heap (underlying_memory (ksMachineState s)) (p && ~~ mask pageBits) off = user_data_C.words_C y'.[unat off]; cslift s' (PTR(user_data_C) (p && ~~ mask pageBits)) = Some y'; (p && ~~ mask pageBits) + (p && mask pageBits) = p; is_aligned p 2; pointerInUserData p s; x = word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p]; s' \<Turnstile>\<^sub>c PTR(32 word) p\<rbrakk> \<Longrightarrow> h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(32 word) p) = word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p] proof (prove)
goal (1 subgoal):
 1. \<And>y'. \<lbrakk>p' = PTR(32 word) p; cslift s' (PTR(user_data_C) (p && ~~ mask pageBits)) = Some y'; (p && ~~ mask pageBits) + (p && mask pageBits) = p; is_aligned p 2; pointerInUserData p s; x = word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p]; s' \<Turnstile>\<^sub>c PTR(32 word) p; byte_to_word_heap (underlying_memory (ksMachineState s)) (p && ~~ mask pageBits) (UCAST(32 \<rightarrow> 10) (p >> 2)) = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]\<rbrakk> \<Longrightarrow> h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(32 word) p) = word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p] proof (prove)
goal (1 subgoal):
 1. \<And>y'. \<lbrakk>p' = PTR(32 word) p; cslift s' (PTR(user_data_C) (p && ~~ mask pageBits)) = Some y'; (p && ~~ mask pageBits) + (p && mask pageBits) = p; is_aligned p 2; pointerInUserData p s; x = word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p]; s' \<Turnstile>\<^sub>c PTR(32 word) p; word_rcat [underlying_memory (ksMachineState s) ((p && ~~ mask pageBits) + ((p >> 2) && mask 10) * 4 + 3), underlying_memory (ksMachineState s) ((p && ~~ mask pageBits) + ((p >> 2) && mask 10) * 4 + 2), underlying_memory (ksMachineState s) ((p && ~~ mask pageBits) + ((p >> 2) && mask 10) * 4 + 1), underlying_memory (ksMachineState s) ((p && ~~ mask pageBits) + ((p >> 2) && mask 10) * 4)] = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]\<rbrakk> \<Longrightarrow> h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(32 word) p) = word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p] proof (prove)
goal (1 subgoal):
 1. \<And>y'. \<lbrakk>p' = PTR(32 word) p; cslift s' (PTR(user_data_C) (p && ~~ mask pageBits)) = Some y'; (p && ~~ mask pageBits) + (p && mask pageBits) = p; is_aligned p 2; pointerInUserData p s; x = word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p]; s' \<Turnstile>\<^sub>c PTR(32 word) p; word_rcat [underlying_memory (ksMachineState s) ((p && ~~ mask pageBits) + ((p >> 2) && mask 10 << 2) + 3), underlying_memory (ksMachineState s) ((p && ~~ mask pageBits) + ((p >> 2) && mask 10 << 2) + 2), underlying_memory (ksMachineState s) ((p && ~~ mask pageBits) + ((p >> 2) && mask 10 << 2) + 1), underlying_memory (ksMachineState s) ((p && ~~ mask pageBits) + ((p >> 2) && mask 10 << 2))] = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]\<rbrakk> \<Longrightarrow> h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(32 word) p) = word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p] proof (prove)
goal (1 subgoal):
 1. \<And>y'. \<lbrakk>p' = PTR(32 word) p; cslift s' (PTR(user_data_C) (p && ~~ mask 12)) = Some y'; (p && ~~ mask 12) + (p && mask 12) = p; is_aligned p 2; pointerInUserData p s; x = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]; s' \<Turnstile>\<^sub>c PTR(32 word) p; word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p] = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]\<rbrakk> \<Longrightarrow> h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(32 word) p) = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))] proof (prove)
goal (4 subgoals):
 1. \<And>y'. \<lbrakk>p' = PTR(32 word) p; cslift s' (PTR(user_data_C) (p && ~~ mask 12)) = Some y'; (p && ~~ mask 12) + (p && mask 12) = p; is_aligned p 2; pointerInUserData p s; x = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]; s' \<Turnstile>\<^sub>c PTR(32 word) p; word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p] = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]\<rbrakk> \<Longrightarrow> h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(32 word[1024]) &(PTR(?'c73) (p && ~~ mask 12)\<rightarrow>[''words_C''])) = user_data_C.words_C y'
 2. \<And>y'. \<lbrakk>p' = PTR(32 word) p; cslift s' (PTR(user_data_C) (p && ~~ mask 12)) = Some y'; (p && ~~ mask 12) + (p && mask 12) = p; is_aligned p 2; pointerInUserData p s; x = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]; s' \<Turnstile>\<^sub>c PTR(32 word) p; word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p] = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]\<rbrakk> \<Longrightarrow> unat (UCAST(32 \<rightarrow> 10) (p >> 2)) < CARD(1024)
 3. \<And>y'. \<lbrakk>p' = PTR(32 word) p; cslift s' (PTR(user_data_C) (p && ~~ mask 12)) = Some y'; (p && ~~ mask 12) + (p && mask 12) = p; is_aligned p 2; pointerInUserData p s; x = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]; s' \<Turnstile>\<^sub>c PTR(32 word) p; word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p] = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]\<rbrakk> \<Longrightarrow> \<forall>xs v. length xs = size_of TYPE(32 word) \<longrightarrow> update_ti_t (typ_info_t TYPE(32 word)) xs v = ?f72 y' xs
 4. \<And>y'. \<lbrakk>p' = PTR(32 word) p; cslift s' (PTR(user_data_C) (p && ~~ mask 12)) = Some y'; (p && ~~ mask 12) + (p && mask 12) = p; is_aligned p 2; pointerInUserData p s; x = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]; s' \<Turnstile>\<^sub>c PTR(32 word) p; word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p] = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]\<rbrakk> \<Longrightarrow> h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(32 word) p) = h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(32 word) (ptr_val (PTR(32 word[1024]) &(PTR(?'c73) (p && ~~ mask 12)\<rightarrow>[''words_C''])) + word_of_nat (unat (UCAST(32 \<rightarrow> 10) (p >> 2)) * size_of TYPE(32 word)))) proof (prove)
goal (5 subgoals):
 1. \<And>y'. \<lbrakk>p' = PTR(32 word) p; cslift s' (PTR(user_data_C) (p && ~~ mask 12)) = Some y'; (p && ~~ mask 12) + (p && mask 12) = p; is_aligned p 2; pointerInUserData p s; x = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]; s' \<Turnstile>\<^sub>c PTR(32 word) p; word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p] = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]\<rbrakk> \<Longrightarrow> h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(32 word[1024]) &(PTR(?'c73) (p && ~~ mask 12)\<rightarrow>[''words_C''])) = ?s74 y'
 2. \<And>y'. \<lbrakk>p' = PTR(32 word) p; cslift s' (PTR(user_data_C) (p && ~~ mask 12)) = Some y'; (p && ~~ mask 12) + (p && mask 12) = p; is_aligned p 2; pointerInUserData p s; x = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]; s' \<Turnstile>\<^sub>c PTR(32 word) p; word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p] = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]\<rbrakk> \<Longrightarrow> ?s74 y' = user_data_C.words_C y'
 3. \<And>y'. \<lbrakk>p' = PTR(32 word) p; cslift s' (PTR(user_data_C) (p && ~~ mask 12)) = Some y'; (p && ~~ mask 12) + (p && mask 12) = p; is_aligned p 2; pointerInUserData p s; x = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]; s' \<Turnstile>\<^sub>c PTR(32 word) p; word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p] = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]\<rbrakk> \<Longrightarrow> unat (UCAST(32 \<rightarrow> 10) (p >> 2)) < CARD(1024)
 4. \<And>y'. \<lbrakk>p' = PTR(32 word) p; cslift s' (PTR(user_data_C) (p && ~~ mask 12)) = Some y'; (p && ~~ mask 12) + (p && mask 12) = p; is_aligned p 2; pointerInUserData p s; x = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]; s' \<Turnstile>\<^sub>c PTR(32 word) p; word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p] = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]\<rbrakk> \<Longrightarrow> \<forall>xs v. length xs = size_of TYPE(32 word) \<longrightarrow> update_ti_t (typ_info_t TYPE(32 word)) xs v = ?f72 y' xs
 5. \<And>y'. \<lbrakk>p' = PTR(32 word) p; cslift s' (PTR(user_data_C) (p && ~~ mask 12)) = Some y'; (p && ~~ mask 12) + (p && mask 12) = p; is_aligned p 2; pointerInUserData p s; x = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]; s' \<Turnstile>\<^sub>c PTR(32 word) p; word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p] = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]\<rbrakk> \<Longrightarrow> h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(32 word) p) = h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(32 word) (ptr_val (PTR(32 word[1024]) &(PTR(?'c73) (p && ~~ mask 12)\<rightarrow>[''words_C''])) + word_of_nat (unat (UCAST(32 \<rightarrow> 10) (p >> 2)) * size_of TYPE(32 word)))) proof (prove)
goal (6 subgoals):
 1. \<And>y'. \<lbrakk>p' = PTR(32 word) p; (p && ~~ mask 12) + (p && mask 12) = p; is_aligned p 2; pointerInUserData p s; x = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]; s' \<Turnstile>\<^sub>c PTR(32 word) p; word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p] = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]\<rbrakk> \<Longrightarrow> field_ti TYPE(user_data_C) [''words_C''] = Some (?t77 y')
 2. \<And>y'. \<lbrakk>p' = PTR(32 word) p; (p && ~~ mask 12) + (p && mask 12) = p; is_aligned p 2; pointerInUserData p s; x = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]; s' \<Turnstile>\<^sub>c PTR(32 word) p; word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p] = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]\<rbrakk> \<Longrightarrow> export_uinfo (?t77 y') = export_uinfo (typ_info_t TYPE(32 word[1024]))
 3. \<And>y'. \<lbrakk>p' = PTR(32 word) p; cslift s' (PTR(user_data_C) (p && ~~ mask 12)) = Some y'; (p && ~~ mask 12) + (p && mask 12) = p; is_aligned p 2; pointerInUserData p s; x = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]; s' \<Turnstile>\<^sub>c PTR(32 word) p; word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p] = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]\<rbrakk> \<Longrightarrow> from_bytes (access_ti\<^sub>0 (?t77 y') y') = user_data_C.words_C y'
 4. \<And>y'. \<lbrakk>p' = PTR(32 word) p; cslift s' (PTR(user_data_C) (p && ~~ mask 12)) = Some y'; (p && ~~ mask 12) + (p && mask 12) = p; is_aligned p 2; pointerInUserData p s; x = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]; s' \<Turnstile>\<^sub>c PTR(32 word) p; word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p] = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]\<rbrakk> \<Longrightarrow> unat (UCAST(32 \<rightarrow> 10) (p >> 2)) < CARD(1024)
 5. \<And>y'. \<lbrakk>p' = PTR(32 word) p; cslift s' (PTR(user_data_C) (p && ~~ mask 12)) = Some y'; (p && ~~ mask 12) + (p && mask 12) = p; is_aligned p 2; pointerInUserData p s; x = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]; s' \<Turnstile>\<^sub>c PTR(32 word) p; word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p] = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]\<rbrakk> \<Longrightarrow> \<forall>xs v. length xs = size_of TYPE(32 word) \<longrightarrow> update_ti_t (typ_info_t TYPE(32 word)) xs v = ?f72 y' xs
 6. \<And>y'. \<lbrakk>p' = PTR(32 word) p; cslift s' (PTR(user_data_C) (p && ~~ mask 12)) = Some y'; (p && ~~ mask 12) + (p && mask 12) = p; is_aligned p 2; pointerInUserData p s; x = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]; s' \<Turnstile>\<^sub>c PTR(32 word) p; word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p] = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]\<rbrakk> \<Longrightarrow> h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(32 word) p) = h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(32 word) (ptr_val (PTR(32 word[1024]) &(PTR(user_data_C) (p && ~~ mask 12)\<rightarrow>[''words_C''])) + word_of_nat (unat (UCAST(32 \<rightarrow> 10) (p >> 2)) * size_of TYPE(32 word)))) proof (prove)
goal (3 subgoals):
 1. \<And>y'. \<lbrakk>p' = PTR(32 word) p; cslift s' (PTR(user_data_C) (p && ~~ mask 12)) = Some y'; (p && ~~ mask 12) + (p && mask 12) = p; is_aligned p 2; pointerInUserData p s; x = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]; s' \<Turnstile>\<^sub>c PTR(32 word) p; word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p] = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]\<rbrakk> \<Longrightarrow> unat (UCAST(32 \<rightarrow> 10) (p >> 2)) < 1024
 2. \<And>y'. \<lbrakk>p' = PTR(32 word) p; cslift s' (PTR(user_data_C) (p && ~~ mask 12)) = Some y'; (p && ~~ mask 12) + (p && mask 12) = p; is_aligned p 2; pointerInUserData p s; x = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]; s' \<Turnstile>\<^sub>c PTR(32 word) p; word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p] = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]\<rbrakk> \<Longrightarrow> \<forall>xs v. length xs = size_of TYPE(32 word) \<longrightarrow> update_ti_t (typ_info_t TYPE(32 word)) xs v = ?f72 y' xs
 3. \<And>y'. \<lbrakk>p' = PTR(32 word) p; cslift s' (PTR(user_data_C) (p && ~~ mask 12)) = Some y'; (p && ~~ mask 12) + (p && mask 12) = p; is_aligned p 2; pointerInUserData p s; x = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]; s' \<Turnstile>\<^sub>c PTR(32 word) p; word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p] = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]\<rbrakk> \<Longrightarrow> h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(32 word) p) = h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(32 word) (ptr_val (PTR(32 word[1024]) &(PTR(user_data_C) (p && ~~ mask 12)\<rightarrow>[''words_C''])) + word_of_nat (unat (UCAST(32 \<rightarrow> 10) (p >> 2)) * size_of TYPE(32 word)))) proof (prove)
goal (3 subgoals):
 1. \<And>y'. \<lbrakk>p' = PTR(32 word) p; cslift s' (PTR(user_data_C) (p && ~~ mask 12)) = Some y'; (p && ~~ mask 12) + (p && mask 12) = p; is_aligned p 2; pointerInUserData p s; x = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]; s' \<Turnstile>\<^sub>c PTR(32 word) p; word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p] = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]\<rbrakk> \<Longrightarrow> 2 ^ LENGTH(10) \<le> 1024
 2. \<And>y'. \<lbrakk>p' = PTR(32 word) p; cslift s' (PTR(user_data_C) (p && ~~ mask 12)) = Some y'; (p && ~~ mask 12) + (p && mask 12) = p; is_aligned p 2; pointerInUserData p s; x = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]; s' \<Turnstile>\<^sub>c PTR(32 word) p; word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p] = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]\<rbrakk> \<Longrightarrow> \<forall>xs v. length xs = size_of TYPE(32 word) \<longrightarrow> update_ti_t (typ_info_t TYPE(32 word)) xs v = ?f72 y' xs
 3. \<And>y'. \<lbrakk>p' = PTR(32 word) p; cslift s' (PTR(user_data_C) (p && ~~ mask 12)) = Some y'; (p && ~~ mask 12) + (p && mask 12) = p; is_aligned p 2; pointerInUserData p s; x = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]; s' \<Turnstile>\<^sub>c PTR(32 word) p; word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p] = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]\<rbrakk> \<Longrightarrow> h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(32 word) p) = h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(32 word) (ptr_val (PTR(32 word[1024]) &(PTR(user_data_C) (p && ~~ mask 12)\<rightarrow>[''words_C''])) + word_of_nat (unat (UCAST(32 \<rightarrow> 10) (p >> 2)) * size_of TYPE(32 word)))) proof (prove)
goal (2 subgoals):
 1. \<And>y'. \<lbrakk>p' = PTR(32 word) p; cslift s' (PTR(user_data_C) (p && ~~ mask 12)) = Some y'; (p && ~~ mask 12) + (p && mask 12) = p; is_aligned p 2; pointerInUserData p s; x = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]; s' \<Turnstile>\<^sub>c PTR(32 word) p; word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p] = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]\<rbrakk> \<Longrightarrow> \<forall>xs v. length xs = size_of TYPE(32 word) \<longrightarrow> update_ti_t (typ_info_t TYPE(32 word)) xs v = ?f72 y' xs
 2. \<And>y'. \<lbrakk>p' = PTR(32 word) p; cslift s' (PTR(user_data_C) (p && ~~ mask 12)) = Some y'; (p && ~~ mask 12) + (p && mask 12) = p; is_aligned p 2; pointerInUserData p s; x = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]; s' \<Turnstile>\<^sub>c PTR(32 word) p; word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p] = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]\<rbrakk> \<Longrightarrow> h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(32 word) p) = h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(32 word) (ptr_val (PTR(32 word[1024]) &(PTR(user_data_C) (p && ~~ mask 12)\<rightarrow>[''words_C''])) + word_of_nat (unat (UCAST(32 \<rightarrow> 10) (p >> 2)) * size_of TYPE(32 word)))) proof (prove)
goal (1 subgoal):
 1. \<And>y'. \<lbrakk>p' = PTR(32 word) p; cslift s' (PTR(user_data_C) (p && ~~ mask 12)) = Some y'; (p && ~~ mask 12) + (p && mask 12) = p; is_aligned p 2; pointerInUserData p s; x = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]; s' \<Turnstile>\<^sub>c PTR(32 word) p; word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p] = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]\<rbrakk> \<Longrightarrow> h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(32 word) p) = h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(32 word) (ptr_val (PTR(32 word[1024]) &(PTR(user_data_C) (p && ~~ mask 12)\<rightarrow>[''words_C''])) + word_of_nat (unat (UCAST(32 \<rightarrow> 10) (p >> 2)) * size_of TYPE(32 word)))) proof (prove)
goal (1 subgoal):
 1. \<And>y'. \<lbrakk>p' = PTR(32 word) p; cslift s' (PTR(user_data_C) (p && ~~ mask 12)) = Some y'; (p && ~~ mask 12) + (p && mask 12) = p; is_aligned p 2; pointerInUserData p s; x = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]; s' \<Turnstile>\<^sub>c PTR(32 word) p; word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p] = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]\<rbrakk> \<Longrightarrow> h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(32 word) p) = h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(32 word) (&(PTR(user_data_C) (p && ~~ mask 12)\<rightarrow>[''words_C'']) + UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) (p >> 2)) * 4)) proof (prove)
goal (1 subgoal):
 1. \<And>y'. \<lbrakk>p' = PTR(32 word) p; cslift s' (PTR(user_data_C) (p && ~~ mask 12)) = Some y'; (p && ~~ mask 12) + (p && mask 12) = p; is_aligned p 2; pointerInUserData p s; x = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]; s' \<Turnstile>\<^sub>c PTR(32 word) p; word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p] = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]\<rbrakk> \<Longrightarrow> PTR(32 word) p = PTR(32 word) (&(PTR(user_data_C) (p && ~~ mask 12)\<rightarrow>[''words_C'']) + UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) (p >> 2)) * 4) proof (prove)
goal (1 subgoal):
 1. \<And>y'. \<lbrakk>p' = PTR(32 word) p; cslift s' (PTR(user_data_C) (p && ~~ mask 12)) = Some y'; (p && ~~ mask 12) + (p && mask 12) = p; is_aligned p 2; pointerInUserData p s; x = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]; s' \<Turnstile>\<^sub>c PTR(32 word) p; word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p] = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]\<rbrakk> \<Longrightarrow> p = &(PTR(user_data_C) (p && ~~ mask 12)\<rightarrow>[''words_C'']) + UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) (p >> 2)) * 4 proof (prove)
goal (1 subgoal):
 1. \<And>y'. \<lbrakk>p' = PTR(32 word) p; cslift s' (PTR(user_data_C) (p && ~~ mask 12)) = Some y'; (p && ~~ mask 12) + (p && mask 12) = p; is_aligned p 2; pointerInUserData p s; x = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]; s' \<Turnstile>\<^sub>c PTR(32 word) p; word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p] = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]\<rbrakk> \<Longrightarrow> p = (p && ~~ mask 12) + UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) (p >> 2)) * 4 proof (prove)
goal (1 subgoal):
 1. \<And>y'. \<lbrakk>p' = PTR(32 word) p; cslift s' (PTR(user_data_C) (p && ~~ mask 12)) = Some y'; (p && ~~ mask 12) + (p && mask 12) = p; is_aligned p 2; pointerInUserData p s; x = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]; s' \<Turnstile>\<^sub>c PTR(32 word) p; word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p] = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]\<rbrakk> \<Longrightarrow> p = (p && ~~ mask 12) + ((p >> 2) && mask 10) * 4 proof (prove)
goal (1 subgoal):
 1. \<And>y'. \<lbrakk>p' = PTR(32 word) p; cslift s' (PTR(user_data_C) (p && ~~ mask 12)) = Some y'; (p && ~~ mask 12) + (p && mask 12) = p; is_aligned p 2; pointerInUserData p s; x = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]; s' \<Turnstile>\<^sub>c PTR(32 word) p; word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p] = user_data_C.words_C y'.[unat (UCAST(32 \<rightarrow> 10) (p >> 2))]\<rbrakk> \<Longrightarrow> p = (p && ~~ mask 12) + ((p >> 2) && mask 10 << 2) proof (prove)
goal:
No subgoals!