theory StoreWord_C

lemma heap_to_user_data_seperate:
  "\<lbrakk> \<not> pointerInUserData ptr \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>\<rbrakk>
      \<Longrightarrow> heap_to_user_data (ksPSpace \<sigma>) (fun_upd ms ptr a) x
      = heap_to_user_data (ksPSpace \<sigma>) ms x" apply (simp add : heap_to_user_data_def) apply (case_tac "map_to_user_data (ksPSpace \<sigma>) x") apply simp apply simp apply (clarsimp simp add: projectKO_opt_user_data map_comp_def
                     split: option.split_asm kernel_object.splits) apply (frule userDataSeperate) apply simp+ apply (frule(1) pspace_alignedD') apply (simp add:objBits_simps) apply (rule ext) apply (subst AND_NOT_mask_plus_AND_mask_eq[symmetric,where n =2]) apply (subst byte_to_word_heap_upd_neq[where n = "ptr && mask 2",simplified]) apply (erule is_aligned_weaken, simp add: pageBits_def) apply simp+ apply (clarsimp simp: pointerInUserData_def pageBits_def) apply (subst(asm) and_not_mask_twice[symmetric,where m = 12 and n =2,simplified]) apply (drule sym[where t=" ptr && ~~ mask 2"]) apply simp apply (subst(asm) neg_mask_add_aligned,assumption) apply (rule word_less_power_trans2[where k = 2,simplified]) apply (simp add: pageBits_def) apply (rule less_le_trans[OF ucast_less],simp+) apply (clarsimp simp: typ_at'_def ko_wp_at'_def pageBits_def objBits_simps
                   dest!: pspace_distinctD') apply (rule word_and_less') apply (simp add:mask_def) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> pointerInUserData ptr \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>\<rbrakk> \<Longrightarrow> heap_to_user_data (ksPSpace \<sigma>) (ms(ptr := a)) x = heap_to_user_data (ksPSpace \<sigma>) ms x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> pointerInUserData ptr \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>\<rbrakk> \<Longrightarrow> map_option (\<lambda>_. byte_to_word_heap (ms(ptr := a)) x) (map_to_user_data (ksPSpace \<sigma>) x) = map_option (\<lambda>_. byte_to_word_heap ms x) (map_to_user_data (ksPSpace \<sigma>) x) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<not> pointerInUserData ptr \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; map_to_user_data (ksPSpace \<sigma>) x = None\<rbrakk> \<Longrightarrow> map_option (\<lambda>_. byte_to_word_heap (ms(ptr := a)) x) (map_to_user_data (ksPSpace \<sigma>) x) = map_option (\<lambda>_. byte_to_word_heap ms x) (map_to_user_data (ksPSpace \<sigma>) x)
 2. \<And>aa. \<lbrakk>\<not> pointerInUserData ptr \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; map_to_user_data (ksPSpace \<sigma>) x = Some aa\<rbrakk> \<Longrightarrow> map_option (\<lambda>_. byte_to_word_heap (ms(ptr := a)) x) (map_to_user_data (ksPSpace \<sigma>) x) = map_option (\<lambda>_. byte_to_word_heap ms x) (map_to_user_data (ksPSpace \<sigma>) x) proof (prove)
goal (1 subgoal):
 1. \<And>aa. \<lbrakk>\<not> pointerInUserData ptr \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; map_to_user_data (ksPSpace \<sigma>) x = Some aa\<rbrakk> \<Longrightarrow> map_option (\<lambda>_. byte_to_word_heap (ms(ptr := a)) x) (map_to_user_data (ksPSpace \<sigma>) x) = map_option (\<lambda>_. byte_to_word_heap ms x) (map_to_user_data (ksPSpace \<sigma>) x) proof (prove)
goal (1 subgoal):
 1. \<And>aa. \<lbrakk>\<not> pointerInUserData ptr \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; map_to_user_data (ksPSpace \<sigma>) x = Some aa\<rbrakk> \<Longrightarrow> byte_to_word_heap (ms(ptr := a)) x = byte_to_word_heap ms x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> pointerInUserData ptr \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData\<rbrakk> \<Longrightarrow> byte_to_word_heap (ms(ptr := a)) x = byte_to_word_heap ms x proof (prove)
goal (4 subgoals):
 1. \<lbrakk>\<not> pointerInUserData ptr \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData\<rbrakk> \<Longrightarrow> pspace_distinct' \<sigma>
 2. \<lbrakk>\<not> pointerInUserData ptr \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData\<rbrakk> \<Longrightarrow> pspace_aligned' \<sigma>
 3. \<lbrakk>\<not> pointerInUserData ptr \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData\<rbrakk> \<Longrightarrow> ksPSpace \<sigma> ?x48 = Some KOUserData
 4. \<lbrakk>\<not> pointerInUserData ptr \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData; ptr \<noteq> ?x48\<rbrakk> \<Longrightarrow> byte_to_word_heap (ms(ptr := a)) x = byte_to_word_heap ms x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> pointerInUserData ptr \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData; ptr \<noteq> x\<rbrakk> \<Longrightarrow> byte_to_word_heap (ms(ptr := a)) x = byte_to_word_heap ms x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> pointerInUserData ptr \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData; ptr \<noteq> x; is_aligned x (objBitsKO KOUserData)\<rbrakk> \<Longrightarrow> byte_to_word_heap (ms(ptr := a)) x = byte_to_word_heap ms x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> pointerInUserData ptr \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData; ptr \<noteq> x; is_aligned x pageBits\<rbrakk> \<Longrightarrow> byte_to_word_heap (ms(ptr := a)) x = byte_to_word_heap ms x proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>\<not> pointerInUserData ptr \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData; ptr \<noteq> x; is_aligned x pageBits\<rbrakk> \<Longrightarrow> byte_to_word_heap (ms(ptr := a)) x xa = byte_to_word_heap ms x xa proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>\<not> pointerInUserData ptr \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData; ptr \<noteq> x; is_aligned x pageBits\<rbrakk> \<Longrightarrow> byte_to_word_heap (ms((ptr && ~~ mask 2) + (ptr && mask 2) := a)) x xa = byte_to_word_heap ms x xa proof (prove)
goal (5 subgoals):
 1. \<And>xa. \<lbrakk>\<not> pointerInUserData ptr \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData; ptr \<noteq> x; is_aligned x pageBits\<rbrakk> \<Longrightarrow> is_aligned x 2
 2. \<And>xa. \<lbrakk>\<not> pointerInUserData ptr \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData; ptr \<noteq> x; is_aligned x pageBits\<rbrakk> \<Longrightarrow> is_aligned (ptr && ~~ mask 2) 2
 3. \<And>xa. \<lbrakk>\<not> pointerInUserData ptr \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData; ptr \<noteq> x; is_aligned x pageBits\<rbrakk> \<Longrightarrow> x + UCAST(10 \<rightarrow> 32) xa * 4 \<noteq> ptr && ~~ mask 2
 4. \<And>xa. \<lbrakk>\<not> pointerInUserData ptr \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData; ptr \<noteq> x; is_aligned x pageBits\<rbrakk> \<Longrightarrow> ptr && mask 2 < 4
 5. \<And>xa. \<lbrakk>\<not> pointerInUserData ptr \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData; ptr \<noteq> x; is_aligned x pageBits\<rbrakk> \<Longrightarrow> byte_to_word_heap ms x xa = byte_to_word_heap ms x xa proof (prove)
goal (4 subgoals):
 1. \<And>xa. \<lbrakk>\<not> pointerInUserData ptr \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData; ptr \<noteq> x; is_aligned x pageBits\<rbrakk> \<Longrightarrow> is_aligned (ptr && ~~ mask 2) 2
 2. \<And>xa. \<lbrakk>\<not> pointerInUserData ptr \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData; ptr \<noteq> x; is_aligned x pageBits\<rbrakk> \<Longrightarrow> x + UCAST(10 \<rightarrow> 32) xa * 4 \<noteq> ptr && ~~ mask 2
 3. \<And>xa. \<lbrakk>\<not> pointerInUserData ptr \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData; ptr \<noteq> x; is_aligned x pageBits\<rbrakk> \<Longrightarrow> ptr && mask 2 < 4
 4. \<And>xa. \<lbrakk>\<not> pointerInUserData ptr \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData; ptr \<noteq> x; is_aligned x pageBits\<rbrakk> \<Longrightarrow> byte_to_word_heap ms x xa = byte_to_word_heap ms x xa proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>\<not> pointerInUserData ptr \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData; ptr \<noteq> x; is_aligned x pageBits\<rbrakk> \<Longrightarrow> x + UCAST(10 \<rightarrow> 32) xa * 4 \<noteq> ptr && ~~ mask 2
 2. \<And>xa. \<lbrakk>\<not> pointerInUserData ptr \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData; ptr \<noteq> x; is_aligned x pageBits\<rbrakk> \<Longrightarrow> ptr && mask 2 < 4
 3. \<And>xa. \<lbrakk>\<not> pointerInUserData ptr \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData; ptr \<noteq> x; is_aligned x pageBits\<rbrakk> \<Longrightarrow> byte_to_word_heap ms x xa = byte_to_word_heap ms x xa proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>\<not> typ_at' UserDataT (ptr && ~~ mask 12) \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData; ptr \<noteq> x; is_aligned x 12; x + UCAST(10 \<rightarrow> 32) xa * 4 = ptr && ~~ mask 2\<rbrakk> \<Longrightarrow> False
 2. \<And>xa. \<lbrakk>\<not> pointerInUserData ptr \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData; ptr \<noteq> x; is_aligned x pageBits\<rbrakk> \<Longrightarrow> ptr && mask 2 < 4
 3. \<And>xa. \<lbrakk>\<not> pointerInUserData ptr \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData; ptr \<noteq> x; is_aligned x pageBits\<rbrakk> \<Longrightarrow> byte_to_word_heap ms x xa = byte_to_word_heap ms x xa proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>\<not> typ_at' UserDataT ((ptr && ~~ mask 2) && ~~ mask 12) \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData; ptr \<noteq> x; is_aligned x 12; x + UCAST(10 \<rightarrow> 32) xa * 4 = ptr && ~~ mask 2\<rbrakk> \<Longrightarrow> False
 2. \<And>xa. \<lbrakk>\<not> pointerInUserData ptr \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData; ptr \<noteq> x; is_aligned x pageBits\<rbrakk> \<Longrightarrow> ptr && mask 2 < 4
 3. \<And>xa. \<lbrakk>\<not> pointerInUserData ptr \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData; ptr \<noteq> x; is_aligned x pageBits\<rbrakk> \<Longrightarrow> byte_to_word_heap ms x xa = byte_to_word_heap ms x xa proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>\<not> typ_at' UserDataT ((ptr && ~~ mask 2) && ~~ mask 12) \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData; ptr \<noteq> x; is_aligned x 12; ptr && ~~ mask 2 = x + UCAST(10 \<rightarrow> 32) xa * 4\<rbrakk> \<Longrightarrow> False
 2. \<And>xa. \<lbrakk>\<not> pointerInUserData ptr \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData; ptr \<noteq> x; is_aligned x pageBits\<rbrakk> \<Longrightarrow> ptr && mask 2 < 4
 3. \<And>xa. \<lbrakk>\<not> pointerInUserData ptr \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData; ptr \<noteq> x; is_aligned x pageBits\<rbrakk> \<Longrightarrow> byte_to_word_heap ms x xa = byte_to_word_heap ms x xa proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>\<not> typ_at' UserDataT (x + UCAST(10 \<rightarrow> 32) xa * 4 && ~~ mask 12) \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData; ptr \<noteq> x; is_aligned x 12; ptr && ~~ mask 2 = x + UCAST(10 \<rightarrow> 32) xa * 4\<rbrakk> \<Longrightarrow> False
 2. \<And>xa. \<lbrakk>\<not> pointerInUserData ptr \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData; ptr \<noteq> x; is_aligned x pageBits\<rbrakk> \<Longrightarrow> ptr && mask 2 < 4
 3. \<And>xa. \<lbrakk>\<not> pointerInUserData ptr \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData; ptr \<noteq> x; is_aligned x pageBits\<rbrakk> \<Longrightarrow> byte_to_word_heap ms x xa = byte_to_word_heap ms x xa proof (prove)
goal (4 subgoals):
 1. \<And>xa. \<lbrakk>pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData; ptr \<noteq> x; is_aligned x 12; ptr && ~~ mask 2 = x + UCAST(10 \<rightarrow> 32) xa * 4\<rbrakk> \<Longrightarrow> UCAST(10 \<rightarrow> 32) xa * 4 < 2 ^ 12
 2. \<And>xa. \<lbrakk>\<not> typ_at' UserDataT (x && ~~ mask 12) \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData; ptr \<noteq> x; is_aligned x 12; ptr && ~~ mask 2 = x + UCAST(10 \<rightarrow> 32) xa * 4\<rbrakk> \<Longrightarrow> False
 3. \<And>xa. \<lbrakk>\<not> pointerInUserData ptr \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData; ptr \<noteq> x; is_aligned x pageBits\<rbrakk> \<Longrightarrow> ptr && mask 2 < 4
 4. \<And>xa. \<lbrakk>\<not> pointerInUserData ptr \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData; ptr \<noteq> x; is_aligned x pageBits\<rbrakk> \<Longrightarrow> byte_to_word_heap ms x xa = byte_to_word_heap ms x xa proof (prove)
goal (6 subgoals):
 1. \<And>xa. \<lbrakk>pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData; ptr \<noteq> x; is_aligned x 12; ptr && ~~ mask 2 = x + UCAST(10 \<rightarrow> 32) xa * 4\<rbrakk> \<Longrightarrow> UCAST(10 \<rightarrow> 32) xa < 2 ^ (12 - 2)
 2. \<And>xa. \<lbrakk>pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData; ptr \<noteq> x; is_aligned x 12; ptr && ~~ mask 2 = x + UCAST(10 \<rightarrow> 32) xa * 4\<rbrakk> \<Longrightarrow> 2 \<le> 12
 3. \<And>xa. \<lbrakk>pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData; ptr \<noteq> x; is_aligned x 12; ptr && ~~ mask 2 = x + UCAST(10 \<rightarrow> 32) xa * 4\<rbrakk> \<Longrightarrow> 12 < LENGTH(32)
 4. \<And>xa. \<lbrakk>\<not> typ_at' UserDataT (x && ~~ mask 12) \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData; ptr \<noteq> x; is_aligned x 12; ptr && ~~ mask 2 = x + UCAST(10 \<rightarrow> 32) xa * 4\<rbrakk> \<Longrightarrow> False
 5. \<And>xa. \<lbrakk>\<not> pointerInUserData ptr \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData; ptr \<noteq> x; is_aligned x pageBits\<rbrakk> \<Longrightarrow> ptr && mask 2 < 4
 6. \<And>xa. \<lbrakk>\<not> pointerInUserData ptr \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData; ptr \<noteq> x; is_aligned x pageBits\<rbrakk> \<Longrightarrow> byte_to_word_heap ms x xa = byte_to_word_heap ms x xa proof (prove)
goal (6 subgoals):
 1. \<And>xa. \<lbrakk>pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData; ptr \<noteq> x; is_aligned x 12; ptr && ~~ mask 2 = x + UCAST(10 \<rightarrow> 32) xa * 4\<rbrakk> \<Longrightarrow> UCAST(10 \<rightarrow> 32) xa < 0x400
 2. \<And>xa. \<lbrakk>pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData; ptr \<noteq> x; is_aligned x 12; ptr && ~~ mask 2 = x + UCAST(10 \<rightarrow> 32) xa * 4\<rbrakk> \<Longrightarrow> 2 \<le> 12
 3. \<And>xa. \<lbrakk>pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData; ptr \<noteq> x; is_aligned x 12; ptr && ~~ mask 2 = x + UCAST(10 \<rightarrow> 32) xa * 4\<rbrakk> \<Longrightarrow> 12 < LENGTH(32)
 4. \<And>xa. \<lbrakk>\<not> typ_at' UserDataT (x && ~~ mask 12) \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData; ptr \<noteq> x; is_aligned x 12; ptr && ~~ mask 2 = x + UCAST(10 \<rightarrow> 32) xa * 4\<rbrakk> \<Longrightarrow> False
 5. \<And>xa. \<lbrakk>\<not> pointerInUserData ptr \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData; ptr \<noteq> x; is_aligned x pageBits\<rbrakk> \<Longrightarrow> ptr && mask 2 < 4
 6. \<And>xa. \<lbrakk>\<not> pointerInUserData ptr \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData; ptr \<noteq> x; is_aligned x pageBits\<rbrakk> \<Longrightarrow> byte_to_word_heap ms x xa = byte_to_word_heap ms x xa proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>\<not> typ_at' UserDataT x \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData; ptr \<noteq> x; is_aligned x 12; ptr && ~~ mask 2 = x + UCAST(10 \<rightarrow> 32) xa * 4\<rbrakk> \<Longrightarrow> False
 2. \<And>xa. \<lbrakk>\<not> pointerInUserData ptr \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData; ptr \<noteq> x; is_aligned x pageBits\<rbrakk> \<Longrightarrow> ptr && mask 2 < 4
 3. \<And>xa. \<lbrakk>\<not> pointerInUserData ptr \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData; ptr \<noteq> x; is_aligned x pageBits\<rbrakk> \<Longrightarrow> byte_to_word_heap ms x xa = byte_to_word_heap ms x xa proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>\<not> pointerInUserData ptr \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData; ptr \<noteq> x; is_aligned x pageBits\<rbrakk> \<Longrightarrow> ptr && mask 2 < 4
 2. \<And>xa. \<lbrakk>\<not> pointerInUserData ptr \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData; ptr \<noteq> x; is_aligned x pageBits\<rbrakk> \<Longrightarrow> byte_to_word_heap ms x xa = byte_to_word_heap ms x xa proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>\<not> pointerInUserData ptr \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData; ptr \<noteq> x; is_aligned x pageBits\<rbrakk> \<Longrightarrow> mask 2 < 4
 2. \<And>xa. \<lbrakk>\<not> pointerInUserData ptr \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData; ptr \<noteq> x; is_aligned x pageBits\<rbrakk> \<Longrightarrow> byte_to_word_heap ms x xa = byte_to_word_heap ms x xa proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>\<not> pointerInUserData ptr \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData; ptr \<noteq> x; is_aligned x pageBits\<rbrakk> \<Longrightarrow> byte_to_word_heap ms x xa = byte_to_word_heap ms x xa proof (prove)
goal:
No subgoals!