theory SR_lemmas_C

lemma memory_cross_over:
  "\<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>;
    pointerInUserData ptr \<sigma>\<rbrakk>
   \<Longrightarrow> fst (t_hrs_' (globals s)) ptr = underlying_memory (ksMachineState \<sigma>) ptr" apply (subgoal_tac " c_guard (Ptr (ptr && ~~ mask 2)::32 word ptr) \<and>
    s \<Turnstile>\<^sub>c (Ptr (ptr && ~~ mask 2)::32 word ptr) \<and> h_val (hrs_mem (t_hrs_' (globals s))) (Ptr (ptr && ~~ mask 2)) = x" for x) prefer 2 apply (drule_tac p="ptr && ~~ mask 2" in user_word_at_cross_over[rotated]) apply simp apply (simp add: user_word_at_def Aligned.is_aligned_neg_mask
                     pointerInUserData_def pageBits_def mask_lower_twice) apply assumption apply (clarsimp simp: h_val_def from_bytes_def typ_info_word) apply (drule_tac f="word_rsplit :: word32 \<Rightarrow> word8 list" in arg_cong) apply (simp add: word_rsplit_rcat_size word_size) apply (drule_tac f="\<lambda>xs. xs ! unat (ptr && mask 2)" in arg_cong) apply (simp add: heap_list_nth unat_mask_2_less_4
                   word_plus_and_or_coroll2 add.commute
                   hrs_mem_def) apply (cut_tac p=ptr in unat_mask_2_less_4) apply (subgoal_tac "(ptr && ~~ mask 2) + (ptr && mask 2) = ptr") apply (subgoal_tac "!n x. n < 4 \<longrightarrow> (unat (x::word32) = n) = (x = of_nat n)") apply (clarsimp simp: eval_nat_numeral) apply (fastforce simp: add.commute elim!: less_SucE) apply (clarsimp simp: unat32_eq_of_nat word_bits_def) apply (simp add: add.commute word_plus_and_or_coroll2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>\<rbrakk> \<Longrightarrow> fst (t_hrs_' (globals s)) ptr = underlying_memory (ksMachineState \<sigma>) ptr proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; c_guard (PTR(32 word) (ptr && ~~ mask 2)) \<and> s \<Turnstile>\<^sub>c PTR(32 word) (ptr && ~~ mask 2) \<and> h_val (hrs_mem (t_hrs_' (globals s))) (PTR(?'a1) (ptr && ~~ mask 2)) = ?x4\<rbrakk> \<Longrightarrow> fst (t_hrs_' (globals s)) ptr = underlying_memory (ksMachineState \<sigma>) ptr
 2. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>\<rbrakk> \<Longrightarrow> c_guard (PTR(32 word) (ptr && ~~ mask 2)) \<and> s \<Turnstile>\<^sub>c PTR(32 word) (ptr && ~~ mask 2) \<and> h_val (hrs_mem (t_hrs_' (globals s))) (PTR(?'a1) (ptr && ~~ mask 2)) = ?x4 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>\<rbrakk> \<Longrightarrow> c_guard (PTR(32 word) (ptr && ~~ mask 2)) \<and> s \<Turnstile>\<^sub>c PTR(32 word) (ptr && ~~ mask 2) \<and> h_val (hrs_mem (t_hrs_' (globals s))) (PTR(?'a1) (ptr && ~~ mask 2)) = ?x4
 2. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; c_guard (PTR(32 word) (ptr && ~~ mask 2)) \<and> s \<Turnstile>\<^sub>c PTR(32 word) (ptr && ~~ mask 2) \<and> h_val (hrs_mem (t_hrs_' (globals s))) (PTR(?'a1) (ptr && ~~ mask 2)) = ?x4\<rbrakk> \<Longrightarrow> fst (t_hrs_' (globals s)) ptr = underlying_memory (ksMachineState \<sigma>) ptr proof (prove)
goal (4 subgoals):
 1. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>\<rbrakk> \<Longrightarrow> ?p'5 = PTR(32 word) (ptr && ~~ mask 2)
 2. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>\<rbrakk> \<Longrightarrow> user_word_at ?x5 (ptr && ~~ mask 2) \<sigma>
 3. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; c_guard ?p'5 \<and> s \<Turnstile>\<^sub>c ?p'5 \<and> h_val (hrs_mem (t_hrs_' (globals s))) ?p'5 = ?x5\<rbrakk> \<Longrightarrow> c_guard (PTR(32 word) (ptr && ~~ mask 2)) \<and> s \<Turnstile>\<^sub>c PTR(32 word) (ptr && ~~ mask 2) \<and> h_val (hrs_mem (t_hrs_' (globals s))) (PTR(?'a1) (ptr && ~~ mask 2)) = ?x4
 4. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; c_guard (PTR(32 word) (ptr && ~~ mask 2)) \<and> s \<Turnstile>\<^sub>c PTR(32 word) (ptr && ~~ mask 2) \<and> h_val (hrs_mem (t_hrs_' (globals s))) (PTR(?'a1) (ptr && ~~ mask 2)) = ?x4\<rbrakk> \<Longrightarrow> fst (t_hrs_' (globals s)) ptr = underlying_memory (ksMachineState \<sigma>) ptr proof (prove)
goal (3 subgoals):
 1. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>\<rbrakk> \<Longrightarrow> user_word_at ?x5 (ptr && ~~ mask 2) \<sigma>
 2. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; c_guard (PTR(32 word) (ptr && ~~ mask 2)) \<and> s \<Turnstile>\<^sub>c PTR(32 word) (ptr && ~~ mask 2) \<and> h_val (hrs_mem (t_hrs_' (globals s))) (PTR(32 word) (ptr && ~~ mask 2)) = ?x5\<rbrakk> \<Longrightarrow> c_guard (PTR(32 word) (ptr && ~~ mask 2)) \<and> s \<Turnstile>\<^sub>c PTR(32 word) (ptr && ~~ mask 2) \<and> h_val (hrs_mem (t_hrs_' (globals s))) (PTR(?'a1) (ptr && ~~ mask 2)) = ?x4
 3. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; c_guard (PTR(32 word) (ptr && ~~ mask 2)) \<and> s \<Turnstile>\<^sub>c PTR(32 word) (ptr && ~~ mask 2) \<and> h_val (hrs_mem (t_hrs_' (globals s))) (PTR(?'a1) (ptr && ~~ mask 2)) = ?x4\<rbrakk> \<Longrightarrow> fst (t_hrs_' (globals s)) ptr = underlying_memory (ksMachineState \<sigma>) ptr proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; c_guard (PTR(32 word) (ptr && ~~ mask 2)) \<and> s \<Turnstile>\<^sub>c PTR(32 word) (ptr && ~~ mask 2) \<and> h_val (hrs_mem (t_hrs_' (globals s))) (PTR(32 word) (ptr && ~~ mask 2)) = word_rcat [underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 3), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 2), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 1), underlying_memory (ksMachineState \<sigma>) (ptr && ~~ mask 2)]\<rbrakk> \<Longrightarrow> c_guard (PTR(32 word) (ptr && ~~ mask 2)) \<and> s \<Turnstile>\<^sub>c PTR(32 word) (ptr && ~~ mask 2) \<and> h_val (hrs_mem (t_hrs_' (globals s))) (PTR(?'a1) (ptr && ~~ mask 2)) = ?x4
 2. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; c_guard (PTR(32 word) (ptr && ~~ mask 2)) \<and> s \<Turnstile>\<^sub>c PTR(32 word) (ptr && ~~ mask 2) \<and> h_val (hrs_mem (t_hrs_' (globals s))) (PTR(?'a1) (ptr && ~~ mask 2)) = ?x4\<rbrakk> \<Longrightarrow> fst (t_hrs_' (globals s)) ptr = underlying_memory (ksMachineState \<sigma>) ptr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; c_guard (PTR(32 word) (ptr && ~~ mask 2)) \<and> s \<Turnstile>\<^sub>c PTR(32 word) (ptr && ~~ mask 2) \<and> h_val (hrs_mem (t_hrs_' (globals s))) (PTR(32 word) (ptr && ~~ mask 2)) = word_rcat [underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 3), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 2), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 1), underlying_memory (ksMachineState \<sigma>) (ptr && ~~ mask 2)]\<rbrakk> \<Longrightarrow> fst (t_hrs_' (globals s)) ptr = underlying_memory (ksMachineState \<sigma>) ptr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; c_guard (PTR(32 word) (ptr && ~~ mask 2)); s \<Turnstile>\<^sub>c PTR(32 word) (ptr && ~~ mask 2); word_rcat (rev (heap_list (hrs_mem (t_hrs_' (globals s))) 4 (ptr && ~~ mask 2))) = word_rcat [underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 3), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 2), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 1), underlying_memory (ksMachineState \<sigma>) (ptr && ~~ mask 2)]\<rbrakk> \<Longrightarrow> fst (t_hrs_' (globals s)) ptr = underlying_memory (ksMachineState \<sigma>) ptr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; c_guard (PTR(32 word) (ptr && ~~ mask 2)); s \<Turnstile>\<^sub>c PTR(32 word) (ptr && ~~ mask 2); word_rsplit (word_rcat (rev (heap_list (hrs_mem (t_hrs_' (globals s))) 4 (ptr && ~~ mask 2)))) = word_rsplit (word_rcat [underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 3), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 2), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 1), underlying_memory (ksMachineState \<sigma>) (ptr && ~~ mask 2)])\<rbrakk> \<Longrightarrow> fst (t_hrs_' (globals s)) ptr = underlying_memory (ksMachineState \<sigma>) ptr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; c_guard (PTR(32 word) (ptr && ~~ mask 2)); s \<Turnstile>\<^sub>c PTR(32 word) (ptr && ~~ mask 2); heap_list (hrs_mem (t_hrs_' (globals s))) 4 (ptr && ~~ mask 2) = [underlying_memory (ksMachineState \<sigma>) (ptr && ~~ mask 2), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 1), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 2), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 3)]\<rbrakk> \<Longrightarrow> fst (t_hrs_' (globals s)) ptr = underlying_memory (ksMachineState \<sigma>) ptr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; c_guard (PTR(32 word) (ptr && ~~ mask 2)); s \<Turnstile>\<^sub>c PTR(32 word) (ptr && ~~ mask 2); heap_list (hrs_mem (t_hrs_' (globals s))) 4 (ptr && ~~ mask 2) ! unat (ptr && mask 2) = [underlying_memory (ksMachineState \<sigma>) (ptr && ~~ mask 2), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 1), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 2), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 3)] ! unat (ptr && mask 2)\<rbrakk> \<Longrightarrow> fst (t_hrs_' (globals s)) ptr = underlying_memory (ksMachineState \<sigma>) ptr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; c_guard (PTR(32 word) (ptr && ~~ mask 2)); s \<Turnstile>\<^sub>c PTR(32 word) (ptr && ~~ mask 2); fst (t_hrs_' (globals s)) ptr = [underlying_memory (ksMachineState \<sigma>) (ptr && ~~ mask 2), underlying_memory (ksMachineState \<sigma>) (1 + (ptr && ~~ mask 2)), underlying_memory (ksMachineState \<sigma>) (2 + (ptr && ~~ mask 2)), underlying_memory (ksMachineState \<sigma>) (3 + (ptr && ~~ mask 2))] ! unat (ptr && mask 2)\<rbrakk> \<Longrightarrow> [underlying_memory (ksMachineState \<sigma>) (ptr && ~~ mask 2), underlying_memory (ksMachineState \<sigma>) (1 + (ptr && ~~ mask 2)), underlying_memory (ksMachineState \<sigma>) (2 + (ptr && ~~ mask 2)), underlying_memory (ksMachineState \<sigma>) (3 + (ptr && ~~ mask 2))] ! unat (ptr && mask 2) = underlying_memory (ksMachineState \<sigma>) ptr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; c_guard (PTR(32 word) (ptr && ~~ mask 2)); s \<Turnstile>\<^sub>c PTR(32 word) (ptr && ~~ mask 2); fst (t_hrs_' (globals s)) ptr = [underlying_memory (ksMachineState \<sigma>) (ptr && ~~ mask 2), underlying_memory (ksMachineState \<sigma>) (1 + (ptr && ~~ mask 2)), underlying_memory (ksMachineState \<sigma>) (2 + (ptr && ~~ mask 2)), underlying_memory (ksMachineState \<sigma>) (3 + (ptr && ~~ mask 2))] ! unat (ptr && mask 2); unat (ptr && mask 2) < 4\<rbrakk> \<Longrightarrow> [underlying_memory (ksMachineState \<sigma>) (ptr && ~~ mask 2), underlying_memory (ksMachineState \<sigma>) (1 + (ptr && ~~ mask 2)), underlying_memory (ksMachineState \<sigma>) (2 + (ptr && ~~ mask 2)), underlying_memory (ksMachineState \<sigma>) (3 + (ptr && ~~ mask 2))] ! unat (ptr && mask 2) = underlying_memory (ksMachineState \<sigma>) ptr proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; c_guard (PTR(32 word) (ptr && ~~ mask 2)); s \<Turnstile>\<^sub>c PTR(32 word) (ptr && ~~ mask 2); fst (t_hrs_' (globals s)) ptr = [underlying_memory (ksMachineState \<sigma>) (ptr && ~~ mask 2), underlying_memory (ksMachineState \<sigma>) (1 + (ptr && ~~ mask 2)), underlying_memory (ksMachineState \<sigma>) (2 + (ptr && ~~ mask 2)), underlying_memory (ksMachineState \<sigma>) (3 + (ptr && ~~ mask 2))] ! unat (ptr && mask 2); unat (ptr && mask 2) < 4; (ptr && ~~ mask 2) + (ptr && mask 2) = ptr\<rbrakk> \<Longrightarrow> [underlying_memory (ksMachineState \<sigma>) (ptr && ~~ mask 2), underlying_memory (ksMachineState \<sigma>) (1 + (ptr && ~~ mask 2)), underlying_memory (ksMachineState \<sigma>) (2 + (ptr && ~~ mask 2)), underlying_memory (ksMachineState \<sigma>) (3 + (ptr && ~~ mask 2))] ! unat (ptr && mask 2) = underlying_memory (ksMachineState \<sigma>) ptr
 2. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; c_guard (PTR(32 word) (ptr && ~~ mask 2)); s \<Turnstile>\<^sub>c PTR(32 word) (ptr && ~~ mask 2); fst (t_hrs_' (globals s)) ptr = [underlying_memory (ksMachineState \<sigma>) (ptr && ~~ mask 2), underlying_memory (ksMachineState \<sigma>) (1 + (ptr && ~~ mask 2)), underlying_memory (ksMachineState \<sigma>) (2 + (ptr && ~~ mask 2)), underlying_memory (ksMachineState \<sigma>) (3 + (ptr && ~~ mask 2))] ! unat (ptr && mask 2); unat (ptr && mask 2) < 4\<rbrakk> \<Longrightarrow> (ptr && ~~ mask 2) + (ptr && mask 2) = ptr proof (prove)
goal (3 subgoals):
 1. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; c_guard (PTR(32 word) (ptr && ~~ mask 2)); s \<Turnstile>\<^sub>c PTR(32 word) (ptr && ~~ mask 2); fst (t_hrs_' (globals s)) ptr = [underlying_memory (ksMachineState \<sigma>) (ptr && ~~ mask 2), underlying_memory (ksMachineState \<sigma>) (1 + (ptr && ~~ mask 2)), underlying_memory (ksMachineState \<sigma>) (2 + (ptr && ~~ mask 2)), underlying_memory (ksMachineState \<sigma>) (3 + (ptr && ~~ mask 2))] ! unat (ptr && mask 2); unat (ptr && mask 2) < 4; (ptr && ~~ mask 2) + (ptr && mask 2) = ptr; \<forall>n x. n < 4 \<longrightarrow> (unat x = n) = (x = word_of_nat n)\<rbrakk> \<Longrightarrow> [underlying_memory (ksMachineState \<sigma>) (ptr && ~~ mask 2), underlying_memory (ksMachineState \<sigma>) (1 + (ptr && ~~ mask 2)), underlying_memory (ksMachineState \<sigma>) (2 + (ptr && ~~ mask 2)), underlying_memory (ksMachineState \<sigma>) (3 + (ptr && ~~ mask 2))] ! unat (ptr && mask 2) = underlying_memory (ksMachineState \<sigma>) ptr
 2. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; c_guard (PTR(32 word) (ptr && ~~ mask 2)); s \<Turnstile>\<^sub>c PTR(32 word) (ptr && ~~ mask 2); fst (t_hrs_' (globals s)) ptr = [underlying_memory (ksMachineState \<sigma>) (ptr && ~~ mask 2), underlying_memory (ksMachineState \<sigma>) (1 + (ptr && ~~ mask 2)), underlying_memory (ksMachineState \<sigma>) (2 + (ptr && ~~ mask 2)), underlying_memory (ksMachineState \<sigma>) (3 + (ptr && ~~ mask 2))] ! unat (ptr && mask 2); unat (ptr && mask 2) < 4; (ptr && ~~ mask 2) + (ptr && mask 2) = ptr\<rbrakk> \<Longrightarrow> \<forall>n x. n < 4 \<longrightarrow> (unat x = n) = (x = word_of_nat n)
 3. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; c_guard (PTR(32 word) (ptr && ~~ mask 2)); s \<Turnstile>\<^sub>c PTR(32 word) (ptr && ~~ mask 2); fst (t_hrs_' (globals s)) ptr = [underlying_memory (ksMachineState \<sigma>) (ptr && ~~ mask 2), underlying_memory (ksMachineState \<sigma>) (1 + (ptr && ~~ mask 2)), underlying_memory (ksMachineState \<sigma>) (2 + (ptr && ~~ mask 2)), underlying_memory (ksMachineState \<sigma>) (3 + (ptr && ~~ mask 2))] ! unat (ptr && mask 2); unat (ptr && mask 2) < 4\<rbrakk> \<Longrightarrow> (ptr && ~~ mask 2) + (ptr && mask 2) = ptr proof (prove)
goal (3 subgoals):
 1. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; c_guard (PTR(32 word) (ptr && ~~ mask (Suc (Suc 0)))); s \<Turnstile>\<^sub>c PTR(32 word) (ptr && ~~ mask (Suc (Suc 0))); fst (t_hrs_' (globals s)) ptr = [underlying_memory (ksMachineState \<sigma>) (ptr && ~~ mask (Suc (Suc 0))), underlying_memory (ksMachineState \<sigma>) (1 + (ptr && ~~ mask (Suc (Suc 0)))), underlying_memory (ksMachineState \<sigma>) (2 + (ptr && ~~ mask (Suc (Suc 0)))), underlying_memory (ksMachineState \<sigma>) (3 + (ptr && ~~ mask (Suc (Suc 0))))] ! unat (ptr && mask (Suc (Suc 0))); unat (ptr && mask (Suc (Suc 0))) < Suc (Suc (Suc (Suc 0))); (ptr && ~~ mask (Suc (Suc 0))) + (ptr && mask (Suc (Suc 0))) = ptr; \<forall>n<Suc (Suc (Suc (Suc 0))). \<forall>x. (unat x = n) = (x = word_of_nat n)\<rbrakk> \<Longrightarrow> [underlying_memory (ksMachineState \<sigma>) (ptr && ~~ mask (Suc (Suc 0))), underlying_memory (ksMachineState \<sigma>) (1 + (ptr && ~~ mask (Suc (Suc 0)))), underlying_memory (ksMachineState \<sigma>) (2 + (ptr && ~~ mask (Suc (Suc 0)))), underlying_memory (ksMachineState \<sigma>) (3 + (ptr && ~~ mask (Suc (Suc 0))))] ! unat (ptr && mask (Suc (Suc 0))) = underlying_memory (ksMachineState \<sigma>) ptr
 2. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; c_guard (PTR(32 word) (ptr && ~~ mask 2)); s \<Turnstile>\<^sub>c PTR(32 word) (ptr && ~~ mask 2); fst (t_hrs_' (globals s)) ptr = [underlying_memory (ksMachineState \<sigma>) (ptr && ~~ mask 2), underlying_memory (ksMachineState \<sigma>) (1 + (ptr && ~~ mask 2)), underlying_memory (ksMachineState \<sigma>) (2 + (ptr && ~~ mask 2)), underlying_memory (ksMachineState \<sigma>) (3 + (ptr && ~~ mask 2))] ! unat (ptr && mask 2); unat (ptr && mask 2) < 4; (ptr && ~~ mask 2) + (ptr && mask 2) = ptr\<rbrakk> \<Longrightarrow> \<forall>n x. n < 4 \<longrightarrow> (unat x = n) = (x = word_of_nat n)
 3. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; c_guard (PTR(32 word) (ptr && ~~ mask 2)); s \<Turnstile>\<^sub>c PTR(32 word) (ptr && ~~ mask 2); fst (t_hrs_' (globals s)) ptr = [underlying_memory (ksMachineState \<sigma>) (ptr && ~~ mask 2), underlying_memory (ksMachineState \<sigma>) (1 + (ptr && ~~ mask 2)), underlying_memory (ksMachineState \<sigma>) (2 + (ptr && ~~ mask 2)), underlying_memory (ksMachineState \<sigma>) (3 + (ptr && ~~ mask 2))] ! unat (ptr && mask 2); unat (ptr && mask 2) < 4\<rbrakk> \<Longrightarrow> (ptr && ~~ mask 2) + (ptr && mask 2) = ptr proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; c_guard (PTR(32 word) (ptr && ~~ mask 2)); s \<Turnstile>\<^sub>c PTR(32 word) (ptr && ~~ mask 2); fst (t_hrs_' (globals s)) ptr = [underlying_memory (ksMachineState \<sigma>) (ptr && ~~ mask 2), underlying_memory (ksMachineState \<sigma>) (1 + (ptr && ~~ mask 2)), underlying_memory (ksMachineState \<sigma>) (2 + (ptr && ~~ mask 2)), underlying_memory (ksMachineState \<sigma>) (3 + (ptr && ~~ mask 2))] ! unat (ptr && mask 2); unat (ptr && mask 2) < 4; (ptr && ~~ mask 2) + (ptr && mask 2) = ptr\<rbrakk> \<Longrightarrow> \<forall>n x. n < 4 \<longrightarrow> (unat x = n) = (x = word_of_nat n)
 2. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; c_guard (PTR(32 word) (ptr && ~~ mask 2)); s \<Turnstile>\<^sub>c PTR(32 word) (ptr && ~~ mask 2); fst (t_hrs_' (globals s)) ptr = [underlying_memory (ksMachineState \<sigma>) (ptr && ~~ mask 2), underlying_memory (ksMachineState \<sigma>) (1 + (ptr && ~~ mask 2)), underlying_memory (ksMachineState \<sigma>) (2 + (ptr && ~~ mask 2)), underlying_memory (ksMachineState \<sigma>) (3 + (ptr && ~~ mask 2))] ! unat (ptr && mask 2); unat (ptr && mask 2) < 4\<rbrakk> \<Longrightarrow> (ptr && ~~ mask 2) + (ptr && mask 2) = ptr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; c_guard (PTR(32 word) (ptr && ~~ mask 2)); s \<Turnstile>\<^sub>c PTR(32 word) (ptr && ~~ mask 2); fst (t_hrs_' (globals s)) ptr = [underlying_memory (ksMachineState \<sigma>) (ptr && ~~ mask 2), underlying_memory (ksMachineState \<sigma>) (1 + (ptr && ~~ mask 2)), underlying_memory (ksMachineState \<sigma>) (2 + (ptr && ~~ mask 2)), underlying_memory (ksMachineState \<sigma>) (3 + (ptr && ~~ mask 2))] ! unat (ptr && mask 2); unat (ptr && mask 2) < 4\<rbrakk> \<Longrightarrow> (ptr && ~~ mask 2) + (ptr && mask 2) = ptr proof (prove)
goal:
No subgoals!