theory ArchADT_IF_Refine_C

lemma obs_cpspace_user_data_relation[ADT_IF_Refine_assms]:
  "\<lbrakk> pspace_aligned' bd; pspace_distinct' bd;
     cpspace_user_data_relation (ksPSpace bd) (underlying_memory (ksMachineState bd)) hgs \<rbrakk>
     \<Longrightarrow> cpspace_user_data_relation (ksPSpace bd)
           (underlying_memory (observable_memory (ksMachineState bd) (user_mem' bd))) hgs" apply (clarsimp simp: cmap_relation_def dom_heap_to_user_data) apply (drule bspec, fastforce) apply (clarsimp simp: cuser_user_data_relation_def observable_memory_def
                         heap_to_user_data_def map_comp_def Let_def
                  split: option.split_asm) apply (drule_tac x = off in spec) apply (subst option_to_0_user_mem') apply (subst map_option_byte_to_word_heap) apply (clarsimp simp: projectKO_opt_user_data pointerInUserData_def field_simps
                   split: kernel_object.split_asm option.split_asm) apply (frule(1) pspace_alignedD') apply (subst neg_mask_add_aligned) apply (simp add: objBits_simps) apply (simp add: word_less_nat_alt) apply (rule le_less_trans[OF unat_plus_gt]) apply (subst add.commute) apply (subst unat_mult_simple) apply (simp add: word_bits_def) apply (rule less_le_trans[OF unat_lt2p]) apply simp apply simp apply (rule nat_add_offset_less [where n = 2, simplified]) apply simp apply (rule unat_lt2p) apply (simp add: pageBits_def objBits_simps) apply (frule(1) pspace_distinctD') apply (clarsimp simp: obj_at'_def typ_at'_def ko_wp_at'_def objBits_simps) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_aligned' bd; pspace_distinct' bd; cpspace_user_data_relation (ksPSpace bd) (underlying_memory (ksMachineState bd)) hgs\<rbrakk> \<Longrightarrow> cpspace_user_data_relation (ksPSpace bd) (underlying_memory (observable_memory (ksMachineState bd) (user_mem' bd))) hgs proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>pspace_aligned' bd; pspace_distinct' bd; map_to_user_data (ksPSpace bd) x = Some y; PTR(user_data_C) ` dom (map_to_user_data (ksPSpace bd)) = dom (clift hgs); \<forall>x\<in>dom (map_to_user_data (ksPSpace bd)). cuser_user_data_relation (the (heap_to_user_data (ksPSpace bd) (underlying_memory (ksMachineState bd)) x)) (the (clift hgs (PTR(user_data_C) x)))\<rbrakk> \<Longrightarrow> cuser_user_data_relation (the (heap_to_user_data (ksPSpace bd) (underlying_memory (observable_memory (ksMachineState bd) (user_mem' bd))) x)) (the (clift hgs (PTR(user_data_C) x))) proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>pspace_aligned' bd; pspace_distinct' bd; map_to_user_data (ksPSpace bd) x = Some y; PTR(user_data_C) ` dom (map_to_user_data (ksPSpace bd)) = dom (clift hgs); cuser_user_data_relation (the (heap_to_user_data (ksPSpace bd) (underlying_memory (ksMachineState bd)) x)) (the (clift hgs (PTR(user_data_C) x)))\<rbrakk> \<Longrightarrow> cuser_user_data_relation (the (heap_to_user_data (ksPSpace bd) (underlying_memory (observable_memory (ksMachineState bd) (user_mem' bd))) x)) (the (clift hgs (PTR(user_data_C) x))) proof (prove)
goal (1 subgoal):
 1. \<And>x y x2 off. \<lbrakk>PTR(user_data_C) ` dom (\<lambda>k. case ksPSpace bd k of None \<Rightarrow> None | Some v \<Rightarrow> projectKO_opt v) = dom (clift hgs); \<forall>off. byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off]; pspace_aligned' bd; pspace_distinct' bd; ksPSpace bd x = Some x2; projectKO_opt x2 = Some y\<rbrakk> \<Longrightarrow> byte_to_word_heap (option_to_0 \<circ> user_mem' bd) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off] proof (prove)
goal (1 subgoal):
 1. \<And>x y x2 off. \<lbrakk>PTR(user_data_C) ` dom (\<lambda>k. case ksPSpace bd k of None \<Rightarrow> None | Some v \<Rightarrow> projectKO_opt v) = dom (clift hgs); pspace_aligned' bd; pspace_distinct' bd; ksPSpace bd x = Some x2; projectKO_opt x2 = Some y; byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off]\<rbrakk> \<Longrightarrow> byte_to_word_heap (option_to_0 \<circ> user_mem' bd) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off] proof (prove)
goal (1 subgoal):
 1. \<And>x y x2 off. \<lbrakk>PTR(user_data_C) ` dom (\<lambda>k. case ksPSpace bd k of None \<Rightarrow> None | Some v \<Rightarrow> projectKO_opt v) = dom (clift hgs); pspace_aligned' bd; pspace_distinct' bd; ksPSpace bd x = Some x2; projectKO_opt x2 = Some y; byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off]\<rbrakk> \<Longrightarrow> byte_to_word_heap (\<lambda>x. if x \<in> {y. \<not> pointerInUserData y bd} then 0 else underlying_memory (ksMachineState bd) x) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off] proof (prove)
goal (2 subgoals):
 1. \<And>x y x2 off offa xa. \<lbrakk>PTR(user_data_C) ` dom (\<lambda>k. case ksPSpace bd k of None \<Rightarrow> None | Some v \<Rightarrow> projectKO_opt v) = dom (clift hgs); pspace_aligned' bd; pspace_distinct' bd; ksPSpace bd x = Some x2; projectKO_opt x2 = Some y; byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off]; xa < 4\<rbrakk> \<Longrightarrow> x + UCAST(10 \<rightarrow> 32) offa * 4 + xa \<notin> {y. \<not> pointerInUserData y bd}
 2. \<And>x y x2 off. \<lbrakk>PTR(user_data_C) ` dom (\<lambda>k. case ksPSpace bd k of None \<Rightarrow> None | Some v \<Rightarrow> projectKO_opt v) = dom (clift hgs); pspace_aligned' bd; pspace_distinct' bd; ksPSpace bd x = Some x2; projectKO_opt x2 = Some y; byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off]\<rbrakk> \<Longrightarrow> byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off] proof (prove)
goal (2 subgoals):
 1. \<And>x off offa xa. \<lbrakk>byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off]; xa < 4; PTR(user_data_C) ` dom (\<lambda>k. case ksPSpace bd k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) = dom (clift hgs); pspace_aligned' bd; pspace_distinct' bd; ksPSpace bd x = Some KOUserData\<rbrakk> \<Longrightarrow> typ_at' UserDataT (x + (xa + UCAST(10 \<rightarrow> 32) offa * 4) && ~~ mask pageBits) bd
 2. \<And>x y x2 off. \<lbrakk>PTR(user_data_C) ` dom (\<lambda>k. case ksPSpace bd k of None \<Rightarrow> None | Some v \<Rightarrow> projectKO_opt v) = dom (clift hgs); pspace_aligned' bd; pspace_distinct' bd; ksPSpace bd x = Some x2; projectKO_opt x2 = Some y; byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off]\<rbrakk> \<Longrightarrow> byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off] proof (prove)
goal (2 subgoals):
 1. \<And>x off offa xa. \<lbrakk>byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off]; xa < 4; PTR(user_data_C) ` dom (\<lambda>k. case ksPSpace bd k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) = dom (clift hgs); pspace_aligned' bd; pspace_distinct' bd; ksPSpace bd x = Some KOUserData; is_aligned x (objBitsKO KOUserData)\<rbrakk> \<Longrightarrow> typ_at' UserDataT (x + (xa + UCAST(10 \<rightarrow> 32) offa * 4) && ~~ mask pageBits) bd
 2. \<And>x y x2 off. \<lbrakk>PTR(user_data_C) ` dom (\<lambda>k. case ksPSpace bd k of None \<Rightarrow> None | Some v \<Rightarrow> projectKO_opt v) = dom (clift hgs); pspace_aligned' bd; pspace_distinct' bd; ksPSpace bd x = Some x2; projectKO_opt x2 = Some y; byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off]\<rbrakk> \<Longrightarrow> byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off] proof (prove)
goal (4 subgoals):
 1. \<And>x off offa xa. \<lbrakk>byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off]; xa < 4; PTR(user_data_C) ` dom (\<lambda>k. case ksPSpace bd k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) = dom (clift hgs); pspace_aligned' bd; pspace_distinct' bd; ksPSpace bd x = Some KOUserData; is_aligned x (objBitsKO KOUserData)\<rbrakk> \<Longrightarrow> is_aligned x pageBits
 2. \<And>x off offa xa. \<lbrakk>byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off]; xa < 4; PTR(user_data_C) ` dom (\<lambda>k. case ksPSpace bd k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) = dom (clift hgs); pspace_aligned' bd; pspace_distinct' bd; ksPSpace bd x = Some KOUserData; is_aligned x (objBitsKO KOUserData)\<rbrakk> \<Longrightarrow> xa + UCAST(10 \<rightarrow> 32) offa * 4 < 2 ^ pageBits
 3. \<And>x off offa xa. \<lbrakk>byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off]; xa < 4; PTR(user_data_C) ` dom (\<lambda>k. case ksPSpace bd k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) = dom (clift hgs); pspace_aligned' bd; pspace_distinct' bd; ksPSpace bd x = Some KOUserData; is_aligned x (objBitsKO KOUserData)\<rbrakk> \<Longrightarrow> typ_at' UserDataT (x && ~~ mask pageBits) bd
 4. \<And>x y x2 off. \<lbrakk>PTR(user_data_C) ` dom (\<lambda>k. case ksPSpace bd k of None \<Rightarrow> None | Some v \<Rightarrow> projectKO_opt v) = dom (clift hgs); pspace_aligned' bd; pspace_distinct' bd; ksPSpace bd x = Some x2; projectKO_opt x2 = Some y; byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off]\<rbrakk> \<Longrightarrow> byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off] proof (prove)
goal (3 subgoals):
 1. \<And>x off offa xa. \<lbrakk>byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off]; xa < 4; PTR(user_data_C) ` dom (\<lambda>k. case ksPSpace bd k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) = dom (clift hgs); pspace_aligned' bd; pspace_distinct' bd; ksPSpace bd x = Some KOUserData; is_aligned x (objBitsKO KOUserData)\<rbrakk> \<Longrightarrow> xa + UCAST(10 \<rightarrow> 32) offa * 4 < 2 ^ pageBits
 2. \<And>x off offa xa. \<lbrakk>byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off]; xa < 4; PTR(user_data_C) ` dom (\<lambda>k. case ksPSpace bd k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) = dom (clift hgs); pspace_aligned' bd; pspace_distinct' bd; ksPSpace bd x = Some KOUserData; is_aligned x (objBitsKO KOUserData)\<rbrakk> \<Longrightarrow> typ_at' UserDataT (x && ~~ mask pageBits) bd
 3. \<And>x y x2 off. \<lbrakk>PTR(user_data_C) ` dom (\<lambda>k. case ksPSpace bd k of None \<Rightarrow> None | Some v \<Rightarrow> projectKO_opt v) = dom (clift hgs); pspace_aligned' bd; pspace_distinct' bd; ksPSpace bd x = Some x2; projectKO_opt x2 = Some y; byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off]\<rbrakk> \<Longrightarrow> byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off] proof (prove)
goal (3 subgoals):
 1. \<And>x off offa xa. \<lbrakk>byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off]; unat xa < 4; PTR(user_data_C) ` dom (\<lambda>k. case ksPSpace bd k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) = dom (clift hgs); pspace_aligned' bd; pspace_distinct' bd; ksPSpace bd x = Some KOUserData; is_aligned x (objBitsKO KOUserData)\<rbrakk> \<Longrightarrow> unat (xa + UCAST(10 \<rightarrow> 32) offa * 4) < 2 ^ pageBits
 2. \<And>x off offa xa. \<lbrakk>byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off]; xa < 4; PTR(user_data_C) ` dom (\<lambda>k. case ksPSpace bd k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) = dom (clift hgs); pspace_aligned' bd; pspace_distinct' bd; ksPSpace bd x = Some KOUserData; is_aligned x (objBitsKO KOUserData)\<rbrakk> \<Longrightarrow> typ_at' UserDataT (x && ~~ mask pageBits) bd
 3. \<And>x y x2 off. \<lbrakk>PTR(user_data_C) ` dom (\<lambda>k. case ksPSpace bd k of None \<Rightarrow> None | Some v \<Rightarrow> projectKO_opt v) = dom (clift hgs); pspace_aligned' bd; pspace_distinct' bd; ksPSpace bd x = Some x2; projectKO_opt x2 = Some y; byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off]\<rbrakk> \<Longrightarrow> byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off] proof (prove)
goal (3 subgoals):
 1. \<And>x off offa xa. \<lbrakk>byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off]; unat xa < 4; PTR(user_data_C) ` dom (\<lambda>k. case ksPSpace bd k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) = dom (clift hgs); pspace_aligned' bd; pspace_distinct' bd; ksPSpace bd x = Some KOUserData; is_aligned x (objBitsKO KOUserData)\<rbrakk> \<Longrightarrow> unat xa + unat (UCAST(10 \<rightarrow> 32) offa * 4) < 2 ^ pageBits
 2. \<And>x off offa xa. \<lbrakk>byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off]; xa < 4; PTR(user_data_C) ` dom (\<lambda>k. case ksPSpace bd k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) = dom (clift hgs); pspace_aligned' bd; pspace_distinct' bd; ksPSpace bd x = Some KOUserData; is_aligned x (objBitsKO KOUserData)\<rbrakk> \<Longrightarrow> typ_at' UserDataT (x && ~~ mask pageBits) bd
 3. \<And>x y x2 off. \<lbrakk>PTR(user_data_C) ` dom (\<lambda>k. case ksPSpace bd k of None \<Rightarrow> None | Some v \<Rightarrow> projectKO_opt v) = dom (clift hgs); pspace_aligned' bd; pspace_distinct' bd; ksPSpace bd x = Some x2; projectKO_opt x2 = Some y; byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off]\<rbrakk> \<Longrightarrow> byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off] proof (prove)
goal (3 subgoals):
 1. \<And>x off offa xa. \<lbrakk>byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off]; unat xa < 4; PTR(user_data_C) ` dom (\<lambda>k. case ksPSpace bd k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) = dom (clift hgs); pspace_aligned' bd; pspace_distinct' bd; ksPSpace bd x = Some KOUserData; is_aligned x (objBitsKO KOUserData)\<rbrakk> \<Longrightarrow> unat (UCAST(10 \<rightarrow> 32) offa * 4) + unat xa < 2 ^ pageBits
 2. \<And>x off offa xa. \<lbrakk>byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off]; xa < 4; PTR(user_data_C) ` dom (\<lambda>k. case ksPSpace bd k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) = dom (clift hgs); pspace_aligned' bd; pspace_distinct' bd; ksPSpace bd x = Some KOUserData; is_aligned x (objBitsKO KOUserData)\<rbrakk> \<Longrightarrow> typ_at' UserDataT (x && ~~ mask pageBits) bd
 3. \<And>x y x2 off. \<lbrakk>PTR(user_data_C) ` dom (\<lambda>k. case ksPSpace bd k of None \<Rightarrow> None | Some v \<Rightarrow> projectKO_opt v) = dom (clift hgs); pspace_aligned' bd; pspace_distinct' bd; ksPSpace bd x = Some x2; projectKO_opt x2 = Some y; byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off]\<rbrakk> \<Longrightarrow> byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off] proof (prove)
goal (4 subgoals):
 1. \<And>x off offa xa. \<lbrakk>byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off]; unat xa < 4; PTR(user_data_C) ` dom (\<lambda>k. case ksPSpace bd k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) = dom (clift hgs); pspace_aligned' bd; pspace_distinct' bd; ksPSpace bd x = Some KOUserData; is_aligned x (objBitsKO KOUserData)\<rbrakk> \<Longrightarrow> unat (UCAST(10 \<rightarrow> 32) offa) * unat 4 < 2 ^ LENGTH(32)
 2. \<And>x off offa xa. \<lbrakk>byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off]; unat xa < 4; PTR(user_data_C) ` dom (\<lambda>k. case ksPSpace bd k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) = dom (clift hgs); pspace_aligned' bd; pspace_distinct' bd; ksPSpace bd x = Some KOUserData; is_aligned x (objBitsKO KOUserData)\<rbrakk> \<Longrightarrow> unat (UCAST(10 \<rightarrow> 32) offa) * unat 4 + unat xa < 2 ^ pageBits
 3. \<And>x off offa xa. \<lbrakk>byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off]; xa < 4; PTR(user_data_C) ` dom (\<lambda>k. case ksPSpace bd k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) = dom (clift hgs); pspace_aligned' bd; pspace_distinct' bd; ksPSpace bd x = Some KOUserData; is_aligned x (objBitsKO KOUserData)\<rbrakk> \<Longrightarrow> typ_at' UserDataT (x && ~~ mask pageBits) bd
 4. \<And>x y x2 off. \<lbrakk>PTR(user_data_C) ` dom (\<lambda>k. case ksPSpace bd k of None \<Rightarrow> None | Some v \<Rightarrow> projectKO_opt v) = dom (clift hgs); pspace_aligned' bd; pspace_distinct' bd; ksPSpace bd x = Some x2; projectKO_opt x2 = Some y; byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off]\<rbrakk> \<Longrightarrow> byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off] proof (prove)
goal (4 subgoals):
 1. \<And>x off offa xa. \<lbrakk>byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off]; unat xa < 4; PTR(user_data_C) ` dom (\<lambda>k. case ksPSpace bd k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) = dom (clift hgs); pspace_aligned' bd; pspace_distinct' bd; ksPSpace bd x = Some KOUserData; is_aligned x (objBitsKO KOUserData)\<rbrakk> \<Longrightarrow> unat offa < 1073741824
 2. \<And>x off offa xa. \<lbrakk>byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off]; unat xa < 4; PTR(user_data_C) ` dom (\<lambda>k. case ksPSpace bd k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) = dom (clift hgs); pspace_aligned' bd; pspace_distinct' bd; ksPSpace bd x = Some KOUserData; is_aligned x (objBitsKO KOUserData)\<rbrakk> \<Longrightarrow> unat (UCAST(10 \<rightarrow> 32) offa) * unat 4 + unat xa < 2 ^ pageBits
 3. \<And>x off offa xa. \<lbrakk>byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off]; xa < 4; PTR(user_data_C) ` dom (\<lambda>k. case ksPSpace bd k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) = dom (clift hgs); pspace_aligned' bd; pspace_distinct' bd; ksPSpace bd x = Some KOUserData; is_aligned x (objBitsKO KOUserData)\<rbrakk> \<Longrightarrow> typ_at' UserDataT (x && ~~ mask pageBits) bd
 4. \<And>x y x2 off. \<lbrakk>PTR(user_data_C) ` dom (\<lambda>k. case ksPSpace bd k of None \<Rightarrow> None | Some v \<Rightarrow> projectKO_opt v) = dom (clift hgs); pspace_aligned' bd; pspace_distinct' bd; ksPSpace bd x = Some x2; projectKO_opt x2 = Some y; byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off]\<rbrakk> \<Longrightarrow> byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off] proof (prove)
goal (4 subgoals):
 1. \<And>x off offa xa. \<lbrakk>byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off]; unat xa < 4; PTR(user_data_C) ` dom (\<lambda>k. case ksPSpace bd k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) = dom (clift hgs); pspace_aligned' bd; pspace_distinct' bd; ksPSpace bd x = Some KOUserData; is_aligned x (objBitsKO KOUserData)\<rbrakk> \<Longrightarrow> 2 ^ LENGTH(10) \<le> 1073741824
 2. \<And>x off offa xa. \<lbrakk>byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off]; unat xa < 4; PTR(user_data_C) ` dom (\<lambda>k. case ksPSpace bd k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) = dom (clift hgs); pspace_aligned' bd; pspace_distinct' bd; ksPSpace bd x = Some KOUserData; is_aligned x (objBitsKO KOUserData)\<rbrakk> \<Longrightarrow> unat (UCAST(10 \<rightarrow> 32) offa) * unat 4 + unat xa < 2 ^ pageBits
 3. \<And>x off offa xa. \<lbrakk>byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off]; xa < 4; PTR(user_data_C) ` dom (\<lambda>k. case ksPSpace bd k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) = dom (clift hgs); pspace_aligned' bd; pspace_distinct' bd; ksPSpace bd x = Some KOUserData; is_aligned x (objBitsKO KOUserData)\<rbrakk> \<Longrightarrow> typ_at' UserDataT (x && ~~ mask pageBits) bd
 4. \<And>x y x2 off. \<lbrakk>PTR(user_data_C) ` dom (\<lambda>k. case ksPSpace bd k of None \<Rightarrow> None | Some v \<Rightarrow> projectKO_opt v) = dom (clift hgs); pspace_aligned' bd; pspace_distinct' bd; ksPSpace bd x = Some x2; projectKO_opt x2 = Some y; byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off]\<rbrakk> \<Longrightarrow> byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off] proof (prove)
goal (3 subgoals):
 1. \<And>x off offa xa. \<lbrakk>byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off]; unat xa < 4; PTR(user_data_C) ` dom (\<lambda>k. case ksPSpace bd k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) = dom (clift hgs); pspace_aligned' bd; pspace_distinct' bd; ksPSpace bd x = Some KOUserData; is_aligned x (objBitsKO KOUserData)\<rbrakk> \<Longrightarrow> unat (UCAST(10 \<rightarrow> 32) offa) * unat 4 + unat xa < 2 ^ pageBits
 2. \<And>x off offa xa. \<lbrakk>byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off]; xa < 4; PTR(user_data_C) ` dom (\<lambda>k. case ksPSpace bd k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) = dom (clift hgs); pspace_aligned' bd; pspace_distinct' bd; ksPSpace bd x = Some KOUserData; is_aligned x (objBitsKO KOUserData)\<rbrakk> \<Longrightarrow> typ_at' UserDataT (x && ~~ mask pageBits) bd
 3. \<And>x y x2 off. \<lbrakk>PTR(user_data_C) ` dom (\<lambda>k. case ksPSpace bd k of None \<Rightarrow> None | Some v \<Rightarrow> projectKO_opt v) = dom (clift hgs); pspace_aligned' bd; pspace_distinct' bd; ksPSpace bd x = Some x2; projectKO_opt x2 = Some y; byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off]\<rbrakk> \<Longrightarrow> byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off] proof (prove)
goal (3 subgoals):
 1. \<And>x off offa xa. \<lbrakk>byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off]; unat xa < 4; PTR(user_data_C) ` dom (\<lambda>k. case ksPSpace bd k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) = dom (clift hgs); pspace_aligned' bd; pspace_distinct' bd; ksPSpace bd x = Some KOUserData; is_aligned x (objBitsKO KOUserData)\<rbrakk> \<Longrightarrow> unat offa * 4 + unat xa < 2 ^ pageBits
 2. \<And>x off offa xa. \<lbrakk>byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off]; xa < 4; PTR(user_data_C) ` dom (\<lambda>k. case ksPSpace bd k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) = dom (clift hgs); pspace_aligned' bd; pspace_distinct' bd; ksPSpace bd x = Some KOUserData; is_aligned x (objBitsKO KOUserData)\<rbrakk> \<Longrightarrow> typ_at' UserDataT (x && ~~ mask pageBits) bd
 3. \<And>x y x2 off. \<lbrakk>PTR(user_data_C) ` dom (\<lambda>k. case ksPSpace bd k of None \<Rightarrow> None | Some v \<Rightarrow> projectKO_opt v) = dom (clift hgs); pspace_aligned' bd; pspace_distinct' bd; ksPSpace bd x = Some x2; projectKO_opt x2 = Some y; byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off]\<rbrakk> \<Longrightarrow> byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off] proof (prove)
goal (5 subgoals):
 1. \<And>x off offa xa. \<lbrakk>byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off]; unat xa < 4; PTR(user_data_C) ` dom (\<lambda>k. case ksPSpace bd k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) = dom (clift hgs); pspace_aligned' bd; pspace_distinct' bd; ksPSpace bd x = Some KOUserData; is_aligned x (objBitsKO KOUserData)\<rbrakk> \<Longrightarrow> unat xa < 4
 2. \<And>x off offa xa. \<lbrakk>byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off]; unat xa < 4; PTR(user_data_C) ` dom (\<lambda>k. case ksPSpace bd k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) = dom (clift hgs); pspace_aligned' bd; pspace_distinct' bd; ksPSpace bd x = Some KOUserData; is_aligned x (objBitsKO KOUserData)\<rbrakk> \<Longrightarrow> unat offa < 2 ^ ?m89 x off offa xa
 3. \<And>x off offa xa. \<lbrakk>byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off]; unat xa < 4; PTR(user_data_C) ` dom (\<lambda>k. case ksPSpace bd k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) = dom (clift hgs); pspace_aligned' bd; pspace_distinct' bd; ksPSpace bd x = Some KOUserData; is_aligned x (objBitsKO KOUserData)\<rbrakk> \<Longrightarrow> pageBits = Suc (Suc (?m89 x off offa xa))
 4. \<And>x off offa xa. \<lbrakk>byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off]; xa < 4; PTR(user_data_C) ` dom (\<lambda>k. case ksPSpace bd k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) = dom (clift hgs); pspace_aligned' bd; pspace_distinct' bd; ksPSpace bd x = Some KOUserData; is_aligned x (objBitsKO KOUserData)\<rbrakk> \<Longrightarrow> typ_at' UserDataT (x && ~~ mask pageBits) bd
 5. \<And>x y x2 off. \<lbrakk>PTR(user_data_C) ` dom (\<lambda>k. case ksPSpace bd k of None \<Rightarrow> None | Some v \<Rightarrow> projectKO_opt v) = dom (clift hgs); pspace_aligned' bd; pspace_distinct' bd; ksPSpace bd x = Some x2; projectKO_opt x2 = Some y; byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off]\<rbrakk> \<Longrightarrow> byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off] proof (prove)
goal (4 subgoals):
 1. \<And>x off offa xa. \<lbrakk>byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off]; unat xa < 4; PTR(user_data_C) ` dom (\<lambda>k. case ksPSpace bd k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) = dom (clift hgs); pspace_aligned' bd; pspace_distinct' bd; ksPSpace bd x = Some KOUserData; is_aligned x (objBitsKO KOUserData)\<rbrakk> \<Longrightarrow> unat offa < 2 ^ ?m89 x off offa xa
 2. \<And>x off offa xa. \<lbrakk>byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off]; unat xa < 4; PTR(user_data_C) ` dom (\<lambda>k. case ksPSpace bd k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) = dom (clift hgs); pspace_aligned' bd; pspace_distinct' bd; ksPSpace bd x = Some KOUserData; is_aligned x (objBitsKO KOUserData)\<rbrakk> \<Longrightarrow> pageBits = Suc (Suc (?m89 x off offa xa))
 3. \<And>x off offa xa. \<lbrakk>byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off]; xa < 4; PTR(user_data_C) ` dom (\<lambda>k. case ksPSpace bd k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) = dom (clift hgs); pspace_aligned' bd; pspace_distinct' bd; ksPSpace bd x = Some KOUserData; is_aligned x (objBitsKO KOUserData)\<rbrakk> \<Longrightarrow> typ_at' UserDataT (x && ~~ mask pageBits) bd
 4. \<And>x y x2 off. \<lbrakk>PTR(user_data_C) ` dom (\<lambda>k. case ksPSpace bd k of None \<Rightarrow> None | Some v \<Rightarrow> projectKO_opt v) = dom (clift hgs); pspace_aligned' bd; pspace_distinct' bd; ksPSpace bd x = Some x2; projectKO_opt x2 = Some y; byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off]\<rbrakk> \<Longrightarrow> byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off] proof (prove)
goal (3 subgoals):
 1. \<And>x off offa xa. \<lbrakk>byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off]; unat xa < 4; PTR(user_data_C) ` dom (\<lambda>k. case ksPSpace bd k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) = dom (clift hgs); pspace_aligned' bd; pspace_distinct' bd; ksPSpace bd x = Some KOUserData; is_aligned x (objBitsKO KOUserData)\<rbrakk> \<Longrightarrow> pageBits = Suc (Suc LENGTH(10))
 2. \<And>x off offa xa. \<lbrakk>byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off]; xa < 4; PTR(user_data_C) ` dom (\<lambda>k. case ksPSpace bd k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) = dom (clift hgs); pspace_aligned' bd; pspace_distinct' bd; ksPSpace bd x = Some KOUserData; is_aligned x (objBitsKO KOUserData)\<rbrakk> \<Longrightarrow> typ_at' UserDataT (x && ~~ mask pageBits) bd
 3. \<And>x y x2 off. \<lbrakk>PTR(user_data_C) ` dom (\<lambda>k. case ksPSpace bd k of None \<Rightarrow> None | Some v \<Rightarrow> projectKO_opt v) = dom (clift hgs); pspace_aligned' bd; pspace_distinct' bd; ksPSpace bd x = Some x2; projectKO_opt x2 = Some y; byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off]\<rbrakk> \<Longrightarrow> byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off] proof (prove)
goal (2 subgoals):
 1. \<And>x off offa xa. \<lbrakk>byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off]; xa < 4; PTR(user_data_C) ` dom (\<lambda>k. case ksPSpace bd k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) = dom (clift hgs); pspace_aligned' bd; pspace_distinct' bd; ksPSpace bd x = Some KOUserData; is_aligned x (objBitsKO KOUserData)\<rbrakk> \<Longrightarrow> typ_at' UserDataT (x && ~~ mask pageBits) bd
 2. \<And>x y x2 off. \<lbrakk>PTR(user_data_C) ` dom (\<lambda>k. case ksPSpace bd k of None \<Rightarrow> None | Some v \<Rightarrow> projectKO_opt v) = dom (clift hgs); pspace_aligned' bd; pspace_distinct' bd; ksPSpace bd x = Some x2; projectKO_opt x2 = Some y; byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off]\<rbrakk> \<Longrightarrow> byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off] proof (prove)
goal (2 subgoals):
 1. \<And>x off offa xa. \<lbrakk>byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off]; xa < 4; PTR(user_data_C) ` dom (\<lambda>k. case ksPSpace bd k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) = dom (clift hgs); pspace_aligned' bd; pspace_distinct' bd; ksPSpace bd x = Some KOUserData; is_aligned x (objBitsKO KOUserData); ps_clear x (objBitsKO KOUserData) bd\<rbrakk> \<Longrightarrow> typ_at' UserDataT (x && ~~ mask pageBits) bd
 2. \<And>x y x2 off. \<lbrakk>PTR(user_data_C) ` dom (\<lambda>k. case ksPSpace bd k of None \<Rightarrow> None | Some v \<Rightarrow> projectKO_opt v) = dom (clift hgs); pspace_aligned' bd; pspace_distinct' bd; ksPSpace bd x = Some x2; projectKO_opt x2 = Some y; byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off]\<rbrakk> \<Longrightarrow> byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off] proof (prove)
goal (1 subgoal):
 1. \<And>x y x2 off. \<lbrakk>PTR(user_data_C) ` dom (\<lambda>k. case ksPSpace bd k of None \<Rightarrow> None | Some v \<Rightarrow> projectKO_opt v) = dom (clift hgs); pspace_aligned' bd; pspace_distinct' bd; ksPSpace bd x = Some x2; projectKO_opt x2 = Some y; byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off]\<rbrakk> \<Longrightarrow> byte_to_word_heap (underlying_memory (ksMachineState bd)) x off = user_data_C.words_C (the (clift hgs (PTR(user_data_C) x))).[unat off] proof (prove)
goal:
No subgoals!