theory Detype_R

lemma obj_relation_cuts_in_obj_range:
  "\<lbrakk> (y, P) \<in> obj_relation_cuts ko x; x \<in> obj_range x ko;
       kheap s x = Some ko; valid_objs s; pspace_aligned s \<rbrakk> \<Longrightarrow> y \<in> obj_range x ko" apply (cases ko, simp_all) apply (clarsimp split: if_split_asm) apply (subgoal_tac "cte_at (x, ya) s") apply (drule(2) cte_at_cte_map_in_obj_bits) apply (simp add: obj_range_def) apply (fastforce intro: cte_wp_at_cteI) apply (frule(1) pspace_alignedD) apply (frule valid_obj_sizes, erule ranI) apply (rename_tac arch_kernel_obj) apply (case_tac arch_kernel_obj, simp_all) apply (clarsimp simp only: obj_range_def field_simps atLeastAtMost_iff
                                obj_bits.simps arch_kobj_size.simps) apply (rule context_conjI) apply (erule is_aligned_no_wrap') apply simp apply (simp add: ucast_less_shiftl_helper) apply (subst add_diff_eq[symmetric]) apply (rule word_plus_mono_right) apply (subst word_less_sub_le, simp) apply (simp add: ucast_less_shiftl_helper) apply (simp add: field_simps) apply (clarsimp simp only: obj_range_def field_simps atLeastAtMost_iff
                              obj_bits.simps arch_kobj_size.simps) apply (rule context_conjI) apply (erule is_aligned_no_wrap') apply simp apply (simp add: ucast_less_shiftl_helper) apply (subst add_diff_eq[symmetric]) apply (rule word_plus_mono_right) apply (subst word_less_sub_le, simp) apply (simp add: ucast_less_shiftl_helper) apply (simp add: field_simps) apply (rename_tac vmpage_size) apply (clarsimp simp only: obj_range_def field_simps atLeastAtMost_iff
                             obj_bits.simps arch_kobj_size.simps) apply (subgoal_tac "n * 2 ^ pageBits < 2 ^ pageBitsForSize vmpage_size") apply (rule context_conjI) apply (erule is_aligned_no_wrap') apply assumption apply (subst add_diff_eq[symmetric]) apply (rule word_plus_mono_right) apply (subst word_less_sub_le, simp add: word_bits_def) apply assumption apply (simp add: field_simps) apply (erule word_less_power_trans2) apply (case_tac vmpage_size, simp_all add: pageBits_def)[1] apply (simp add: word_bits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(y, P) \<in> obj_relation_cuts ko x; x \<in> obj_range x ko; kheap s x = Some ko; valid_objs s; pspace_aligned s\<rbrakk> \<Longrightarrow> y \<in> obj_range x ko proof (prove)
goal (2 subgoals):
 1. \<And>x11 x12. \<lbrakk>(y, P) \<in> (if well_formed_cnode_n x11 x12 then {(cte_map (x, y), cte_relation y) |y. y \<in> dom x12} else {(x, \<lambda>_ _. False)}); x \<in> obj_range x (CNode x11 x12); kheap s x = Some (CNode x11 x12); valid_objs s; pspace_aligned s; ko = CNode x11 x12\<rbrakk> \<Longrightarrow> y \<in> obj_range x (CNode x11 x12)
 2. \<And>x5. \<lbrakk>(y, P) \<in> aobj_relation_cuts x5 x; x \<in> obj_range x (ArchObj x5); kheap s x = Some (ArchObj x5); valid_objs s; pspace_aligned s; ko = ArchObj x5\<rbrakk> \<Longrightarrow> y \<in> obj_range x (ArchObj x5) proof (prove)
goal (2 subgoals):
 1. \<And>x11 x12 ya yaa. \<lbrakk>x \<in> obj_range x (CNode x11 x12); kheap s x = Some (CNode x11 x12); valid_objs s; pspace_aligned s; ko = CNode x11 x12; well_formed_cnode_n x11 x12; y = cte_map (x, ya); P = cte_relation ya; x12 ya = Some yaa\<rbrakk> \<Longrightarrow> cte_map (x, ya) \<in> obj_range x (CNode x11 x12)
 2. \<And>x5. \<lbrakk>(y, P) \<in> aobj_relation_cuts x5 x; x \<in> obj_range x (ArchObj x5); kheap s x = Some (ArchObj x5); valid_objs s; pspace_aligned s; ko = ArchObj x5\<rbrakk> \<Longrightarrow> y \<in> obj_range x (ArchObj x5) proof (prove)
goal (3 subgoals):
 1. \<And>x11 x12 ya yaa. \<lbrakk>x \<in> obj_range x (CNode x11 x12); kheap s x = Some (CNode x11 x12); valid_objs s; pspace_aligned s; ko = CNode x11 x12; well_formed_cnode_n x11 x12; y = cte_map (x, ya); P = cte_relation ya; x12 ya = Some yaa; cte_wp_at (\<lambda>_. True) (x, ya) s\<rbrakk> \<Longrightarrow> cte_map (x, ya) \<in> obj_range x (CNode x11 x12)
 2. \<And>x11 x12 ya yaa. \<lbrakk>x \<in> obj_range x (CNode x11 x12); kheap s x = Some (CNode x11 x12); valid_objs s; pspace_aligned s; ko = CNode x11 x12; well_formed_cnode_n x11 x12; y = cte_map (x, ya); P = cte_relation ya; x12 ya = Some yaa\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (x, ya) s
 3. \<And>x5. \<lbrakk>(y, P) \<in> aobj_relation_cuts x5 x; x \<in> obj_range x (ArchObj x5); kheap s x = Some (ArchObj x5); valid_objs s; pspace_aligned s; ko = ArchObj x5\<rbrakk> \<Longrightarrow> y \<in> obj_range x (ArchObj x5) proof (prove)
goal (3 subgoals):
 1. \<And>x11 x12 ya yaa. \<lbrakk>x \<in> obj_range x (CNode x11 x12); kheap s x = Some (CNode x11 x12); valid_objs s; pspace_aligned s; ko = CNode x11 x12; well_formed_cnode_n x11 x12; y = cte_map (x, ya); P = cte_relation ya; x12 ya = Some yaa; cte_map (x, ya) \<in> {fst (x, ya)..fst (x, ya) + 2 ^ obj_bits (the (kheap s (fst (x, ya)))) - 1} \<and> kheap s (fst (x, ya)) \<noteq> None\<rbrakk> \<Longrightarrow> cte_map (x, ya) \<in> obj_range x (CNode x11 x12)
 2. \<And>x11 x12 ya yaa. \<lbrakk>x \<in> obj_range x (CNode x11 x12); kheap s x = Some (CNode x11 x12); valid_objs s; pspace_aligned s; ko = CNode x11 x12; well_formed_cnode_n x11 x12; y = cte_map (x, ya); P = cte_relation ya; x12 ya = Some yaa\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (x, ya) s
 3. \<And>x5. \<lbrakk>(y, P) \<in> aobj_relation_cuts x5 x; x \<in> obj_range x (ArchObj x5); kheap s x = Some (ArchObj x5); valid_objs s; pspace_aligned s; ko = ArchObj x5\<rbrakk> \<Longrightarrow> y \<in> obj_range x (ArchObj x5) proof (prove)
goal (2 subgoals):
 1. \<And>x11 x12 ya yaa. \<lbrakk>x \<in> obj_range x (CNode x11 x12); kheap s x = Some (CNode x11 x12); valid_objs s; pspace_aligned s; ko = CNode x11 x12; well_formed_cnode_n x11 x12; y = cte_map (x, ya); P = cte_relation ya; x12 ya = Some yaa\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (x, ya) s
 2. \<And>x5. \<lbrakk>(y, P) \<in> aobj_relation_cuts x5 x; x \<in> obj_range x (ArchObj x5); kheap s x = Some (ArchObj x5); valid_objs s; pspace_aligned s; ko = ArchObj x5\<rbrakk> \<Longrightarrow> y \<in> obj_range x (ArchObj x5) proof (prove)
goal (1 subgoal):
 1. \<And>x5. \<lbrakk>(y, P) \<in> aobj_relation_cuts x5 x; x \<in> obj_range x (ArchObj x5); kheap s x = Some (ArchObj x5); valid_objs s; pspace_aligned s; ko = ArchObj x5\<rbrakk> \<Longrightarrow> y \<in> obj_range x (ArchObj x5) proof (prove)
goal (1 subgoal):
 1. \<And>x5. \<lbrakk>(y, P) \<in> aobj_relation_cuts x5 x; x \<in> obj_range x (ArchObj x5); kheap s x = Some (ArchObj x5); valid_objs s; pspace_aligned s; ko = ArchObj x5; is_aligned x (obj_bits (ArchObj x5))\<rbrakk> \<Longrightarrow> y \<in> obj_range x (ArchObj x5) proof (prove)
goal (1 subgoal):
 1. \<And>x5. \<lbrakk>(y, P) \<in> aobj_relation_cuts x5 x; x \<in> obj_range x (ArchObj x5); kheap s x = Some (ArchObj x5); valid_objs s; pspace_aligned s; ko = ArchObj x5; is_aligned x (obj_bits (ArchObj x5)); obj_bits (ArchObj x5) < word_bits\<rbrakk> \<Longrightarrow> y \<in> obj_range x (ArchObj x5) proof (prove)
goal (1 subgoal):
 1. \<And>arch_kernel_obj. \<lbrakk>(y, P) \<in> aobj_relation_cuts arch_kernel_obj x; x \<in> obj_range x (ArchObj arch_kernel_obj); kheap s x = Some (ArchObj arch_kernel_obj); valid_objs s; pspace_aligned s; ko = ArchObj arch_kernel_obj; is_aligned x (obj_bits (ArchObj arch_kernel_obj)); obj_bits (ArchObj arch_kernel_obj) < word_bits\<rbrakk> \<Longrightarrow> y \<in> obj_range x (ArchObj arch_kernel_obj) proof (prove)
goal (3 subgoals):
 1. \<And>arch_kernel_obj x2. \<lbrakk>(y, P) \<in> range (\<lambda>y. (x + (UCAST(8 \<rightarrow> 32) y << 2), pte_relation y)); x \<in> obj_range x (ArchObj (PageTable x2)); kheap s x = Some (ArchObj (PageTable x2)); valid_objs s; pspace_aligned s; ko = ArchObj (PageTable x2); is_aligned x 10; 10 < word_bits; arch_kernel_obj = PageTable x2\<rbrakk> \<Longrightarrow> y \<in> obj_range x (ArchObj (PageTable x2))
 2. \<And>arch_kernel_obj x3. \<lbrakk>(y, P) \<in> range (\<lambda>y. (x + (UCAST(12 \<rightarrow> 32) y << 2), pde_relation y)); x \<in> obj_range x (ArchObj (PageDirectory x3)); kheap s x = Some (ArchObj (PageDirectory x3)); valid_objs s; pspace_aligned s; ko = ArchObj (PageDirectory x3); is_aligned x 14; 14 < word_bits; arch_kernel_obj = PageDirectory x3\<rbrakk> \<Longrightarrow> y \<in> obj_range x (ArchObj (PageDirectory x3))
 3. \<And>arch_kernel_obj x41 x42. \<lbrakk>\<exists>n. y = x + n * 2 ^ pageBits \<and> P = (\<lambda>_ obj. obj = (if x41 then KOUserDataDevice else KOUserData)) \<and> n < 2 ^ (pageBitsForSize x42 - pageBits); x \<in> obj_range x (ArchObj (DataPage x41 x42)); kheap s x = Some (ArchObj (DataPage x41 x42)); valid_objs s; pspace_aligned s; ko = ArchObj (DataPage x41 x42); is_aligned x (pageBitsForSize x42); pageBitsForSize x42 < word_bits; arch_kernel_obj = DataPage x41 x42\<rbrakk> \<Longrightarrow> y \<in> obj_range x (ArchObj (DataPage x41 x42)) proof (prove)
goal (3 subgoals):
 1. \<And>arch_kernel_obj x2 ya. \<lbrakk>kheap s x = Some (ArchObj (PageTable x2)); valid_objs s; pspace_aligned s; ko = ArchObj (PageTable x2); is_aligned x 10; 10 < word_bits; ya \<in> UNIV; x \<le> x; x \<le> x + 2 ^ 10 - 1; P = pte_relation ya; y = x + (UCAST(8 \<rightarrow> 32) ya << 2)\<rbrakk> \<Longrightarrow> x \<le> x + (UCAST(8 \<rightarrow> 32) ya << 2) \<and> x + (UCAST(8 \<rightarrow> 32) ya << 2) \<le> x + 2 ^ 10 - 1
 2. \<And>arch_kernel_obj x3. \<lbrakk>(y, P) \<in> range (\<lambda>y. (x + (UCAST(12 \<rightarrow> 32) y << 2), pde_relation y)); x \<in> obj_range x (ArchObj (PageDirectory x3)); kheap s x = Some (ArchObj (PageDirectory x3)); valid_objs s; pspace_aligned s; ko = ArchObj (PageDirectory x3); is_aligned x 14; 14 < word_bits; arch_kernel_obj = PageDirectory x3\<rbrakk> \<Longrightarrow> y \<in> obj_range x (ArchObj (PageDirectory x3))
 3. \<And>arch_kernel_obj x41 x42. \<lbrakk>\<exists>n. y = x + n * 2 ^ pageBits \<and> P = (\<lambda>_ obj. obj = (if x41 then KOUserDataDevice else KOUserData)) \<and> n < 2 ^ (pageBitsForSize x42 - pageBits); x \<in> obj_range x (ArchObj (DataPage x41 x42)); kheap s x = Some (ArchObj (DataPage x41 x42)); valid_objs s; pspace_aligned s; ko = ArchObj (DataPage x41 x42); is_aligned x (pageBitsForSize x42); pageBitsForSize x42 < word_bits; arch_kernel_obj = DataPage x41 x42\<rbrakk> \<Longrightarrow> y \<in> obj_range x (ArchObj (DataPage x41 x42)) proof (prove)
goal (4 subgoals):
 1. \<And>arch_kernel_obj x2 ya. \<lbrakk>kheap s x = Some (ArchObj (PageTable x2)); valid_objs s; pspace_aligned s; ko = ArchObj (PageTable x2); is_aligned x 10; 10 < word_bits; ya \<in> UNIV; x \<le> x; x \<le> x + 2 ^ 10 - 1; P = pte_relation ya; y = x + (UCAST(8 \<rightarrow> 32) ya << 2)\<rbrakk> \<Longrightarrow> x \<le> x + (UCAST(8 \<rightarrow> 32) ya << 2)
 2. \<And>arch_kernel_obj x2 ya. \<lbrakk>kheap s x = Some (ArchObj (PageTable x2)); valid_objs s; pspace_aligned s; ko = ArchObj (PageTable x2); is_aligned x 10; 10 < word_bits; ya \<in> UNIV; x \<le> x; x \<le> x + 2 ^ 10 - 1; P = pte_relation ya; y = x + (UCAST(8 \<rightarrow> 32) ya << 2); x \<le> x + (UCAST(8 \<rightarrow> 32) ya << 2)\<rbrakk> \<Longrightarrow> x + (UCAST(8 \<rightarrow> 32) ya << 2) \<le> x + 2 ^ 10 - 1
 3. \<And>arch_kernel_obj x3. \<lbrakk>(y, P) \<in> range (\<lambda>y. (x + (UCAST(12 \<rightarrow> 32) y << 2), pde_relation y)); x \<in> obj_range x (ArchObj (PageDirectory x3)); kheap s x = Some (ArchObj (PageDirectory x3)); valid_objs s; pspace_aligned s; ko = ArchObj (PageDirectory x3); is_aligned x 14; 14 < word_bits; arch_kernel_obj = PageDirectory x3\<rbrakk> \<Longrightarrow> y \<in> obj_range x (ArchObj (PageDirectory x3))
 4. \<And>arch_kernel_obj x41 x42. \<lbrakk>\<exists>n. y = x + n * 2 ^ pageBits \<and> P = (\<lambda>_ obj. obj = (if x41 then KOUserDataDevice else KOUserData)) \<and> n < 2 ^ (pageBitsForSize x42 - pageBits); x \<in> obj_range x (ArchObj (DataPage x41 x42)); kheap s x = Some (ArchObj (DataPage x41 x42)); valid_objs s; pspace_aligned s; ko = ArchObj (DataPage x41 x42); is_aligned x (pageBitsForSize x42); pageBitsForSize x42 < word_bits; arch_kernel_obj = DataPage x41 x42\<rbrakk> \<Longrightarrow> y \<in> obj_range x (ArchObj (DataPage x41 x42)) proof (prove)
goal (4 subgoals):
 1. \<And>arch_kernel_obj x2 ya. \<lbrakk>kheap s x = Some (ArchObj (PageTable x2)); valid_objs s; pspace_aligned s; ko = ArchObj (PageTable x2); 10 < word_bits; ya \<in> UNIV; x \<le> x; x \<le> x + 2 ^ 10 - 1; P = pte_relation ya; y = x + (UCAST(8 \<rightarrow> 32) ya << 2)\<rbrakk> \<Longrightarrow> UCAST(8 \<rightarrow> 32) ya << 2 < 2 ^ 10
 2. \<And>arch_kernel_obj x2 ya. \<lbrakk>kheap s x = Some (ArchObj (PageTable x2)); valid_objs s; pspace_aligned s; ko = ArchObj (PageTable x2); is_aligned x 10; 10 < word_bits; ya \<in> UNIV; x \<le> x; x \<le> x + 2 ^ 10 - 1; P = pte_relation ya; y = x + (UCAST(8 \<rightarrow> 32) ya << 2); x \<le> x + (UCAST(8 \<rightarrow> 32) ya << 2)\<rbrakk> \<Longrightarrow> x + (UCAST(8 \<rightarrow> 32) ya << 2) \<le> x + 2 ^ 10 - 1
 3. \<And>arch_kernel_obj x3. \<lbrakk>(y, P) \<in> range (\<lambda>y. (x + (UCAST(12 \<rightarrow> 32) y << 2), pde_relation y)); x \<in> obj_range x (ArchObj (PageDirectory x3)); kheap s x = Some (ArchObj (PageDirectory x3)); valid_objs s; pspace_aligned s; ko = ArchObj (PageDirectory x3); is_aligned x 14; 14 < word_bits; arch_kernel_obj = PageDirectory x3\<rbrakk> \<Longrightarrow> y \<in> obj_range x (ArchObj (PageDirectory x3))
 4. \<And>arch_kernel_obj x41 x42. \<lbrakk>\<exists>n. y = x + n * 2 ^ pageBits \<and> P = (\<lambda>_ obj. obj = (if x41 then KOUserDataDevice else KOUserData)) \<and> n < 2 ^ (pageBitsForSize x42 - pageBits); x \<in> obj_range x (ArchObj (DataPage x41 x42)); kheap s x = Some (ArchObj (DataPage x41 x42)); valid_objs s; pspace_aligned s; ko = ArchObj (DataPage x41 x42); is_aligned x (pageBitsForSize x42); pageBitsForSize x42 < word_bits; arch_kernel_obj = DataPage x41 x42\<rbrakk> \<Longrightarrow> y \<in> obj_range x (ArchObj (DataPage x41 x42)) proof (prove)
goal (4 subgoals):
 1. \<And>x2 ya. \<lbrakk>kheap s x = Some (ArchObj (PageTable x2)); valid_objs s; pspace_aligned s; ko = ArchObj (PageTable x2); 10 < word_bits; x \<le> 0x3FF + x; P = pte_relation ya; y = x + (UCAST(8 \<rightarrow> 32) ya << 2)\<rbrakk> \<Longrightarrow> UCAST(8 \<rightarrow> 32) ya << 2 < 0x400
 2. \<And>arch_kernel_obj x2 ya. \<lbrakk>kheap s x = Some (ArchObj (PageTable x2)); valid_objs s; pspace_aligned s; ko = ArchObj (PageTable x2); is_aligned x 10; 10 < word_bits; ya \<in> UNIV; x \<le> x; x \<le> x + 2 ^ 10 - 1; P = pte_relation ya; y = x + (UCAST(8 \<rightarrow> 32) ya << 2); x \<le> x + (UCAST(8 \<rightarrow> 32) ya << 2)\<rbrakk> \<Longrightarrow> x + (UCAST(8 \<rightarrow> 32) ya << 2) \<le> x + 2 ^ 10 - 1
 3. \<And>arch_kernel_obj x3. \<lbrakk>(y, P) \<in> range (\<lambda>y. (x + (UCAST(12 \<rightarrow> 32) y << 2), pde_relation y)); x \<in> obj_range x (ArchObj (PageDirectory x3)); kheap s x = Some (ArchObj (PageDirectory x3)); valid_objs s; pspace_aligned s; ko = ArchObj (PageDirectory x3); is_aligned x 14; 14 < word_bits; arch_kernel_obj = PageDirectory x3\<rbrakk> \<Longrightarrow> y \<in> obj_range x (ArchObj (PageDirectory x3))
 4. \<And>arch_kernel_obj x41 x42. \<lbrakk>\<exists>n. y = x + n * 2 ^ pageBits \<and> P = (\<lambda>_ obj. obj = (if x41 then KOUserDataDevice else KOUserData)) \<and> n < 2 ^ (pageBitsForSize x42 - pageBits); x \<in> obj_range x (ArchObj (DataPage x41 x42)); kheap s x = Some (ArchObj (DataPage x41 x42)); valid_objs s; pspace_aligned s; ko = ArchObj (DataPage x41 x42); is_aligned x (pageBitsForSize x42); pageBitsForSize x42 < word_bits; arch_kernel_obj = DataPage x41 x42\<rbrakk> \<Longrightarrow> y \<in> obj_range x (ArchObj (DataPage x41 x42)) proof (prove)
goal (3 subgoals):
 1. \<And>arch_kernel_obj x2 ya. \<lbrakk>kheap s x = Some (ArchObj (PageTable x2)); valid_objs s; pspace_aligned s; ko = ArchObj (PageTable x2); is_aligned x 10; 10 < word_bits; ya \<in> UNIV; x \<le> x; x \<le> x + 2 ^ 10 - 1; P = pte_relation ya; y = x + (UCAST(8 \<rightarrow> 32) ya << 2); x \<le> x + (UCAST(8 \<rightarrow> 32) ya << 2)\<rbrakk> \<Longrightarrow> x + (UCAST(8 \<rightarrow> 32) ya << 2) \<le> x + 2 ^ 10 - 1
 2. \<And>arch_kernel_obj x3. \<lbrakk>(y, P) \<in> range (\<lambda>y. (x + (UCAST(12 \<rightarrow> 32) y << 2), pde_relation y)); x \<in> obj_range x (ArchObj (PageDirectory x3)); kheap s x = Some (ArchObj (PageDirectory x3)); valid_objs s; pspace_aligned s; ko = ArchObj (PageDirectory x3); is_aligned x 14; 14 < word_bits; arch_kernel_obj = PageDirectory x3\<rbrakk> \<Longrightarrow> y \<in> obj_range x (ArchObj (PageDirectory x3))
 3. \<And>arch_kernel_obj x41 x42. \<lbrakk>\<exists>n. y = x + n * 2 ^ pageBits \<and> P = (\<lambda>_ obj. obj = (if x41 then KOUserDataDevice else KOUserData)) \<and> n < 2 ^ (pageBitsForSize x42 - pageBits); x \<in> obj_range x (ArchObj (DataPage x41 x42)); kheap s x = Some (ArchObj (DataPage x41 x42)); valid_objs s; pspace_aligned s; ko = ArchObj (DataPage x41 x42); is_aligned x (pageBitsForSize x42); pageBitsForSize x42 < word_bits; arch_kernel_obj = DataPage x41 x42\<rbrakk> \<Longrightarrow> y \<in> obj_range x (ArchObj (DataPage x41 x42)) proof (prove)
goal (3 subgoals):
 1. \<And>arch_kernel_obj x2 ya. \<lbrakk>kheap s x = Some (ArchObj (PageTable x2)); valid_objs s; pspace_aligned s; ko = ArchObj (PageTable x2); is_aligned x 10; 10 < word_bits; ya \<in> UNIV; x \<le> x; x \<le> x + 2 ^ 10 - 1; P = pte_relation ya; y = x + (UCAST(8 \<rightarrow> 32) ya << 2); x \<le> x + (UCAST(8 \<rightarrow> 32) ya << 2)\<rbrakk> \<Longrightarrow> x + (UCAST(8 \<rightarrow> 32) ya << 2) \<le> x + (2 ^ 10 - 1)
 2. \<And>arch_kernel_obj x3. \<lbrakk>(y, P) \<in> range (\<lambda>y. (x + (UCAST(12 \<rightarrow> 32) y << 2), pde_relation y)); x \<in> obj_range x (ArchObj (PageDirectory x3)); kheap s x = Some (ArchObj (PageDirectory x3)); valid_objs s; pspace_aligned s; ko = ArchObj (PageDirectory x3); is_aligned x 14; 14 < word_bits; arch_kernel_obj = PageDirectory x3\<rbrakk> \<Longrightarrow> y \<in> obj_range x (ArchObj (PageDirectory x3))
 3. \<And>arch_kernel_obj x41 x42. \<lbrakk>\<exists>n. y = x + n * 2 ^ pageBits \<and> P = (\<lambda>_ obj. obj = (if x41 then KOUserDataDevice else KOUserData)) \<and> n < 2 ^ (pageBitsForSize x42 - pageBits); x \<in> obj_range x (ArchObj (DataPage x41 x42)); kheap s x = Some (ArchObj (DataPage x41 x42)); valid_objs s; pspace_aligned s; ko = ArchObj (DataPage x41 x42); is_aligned x (pageBitsForSize x42); pageBitsForSize x42 < word_bits; arch_kernel_obj = DataPage x41 x42\<rbrakk> \<Longrightarrow> y \<in> obj_range x (ArchObj (DataPage x41 x42)) proof (prove)
goal (4 subgoals):
 1. \<And>arch_kernel_obj x2 ya. \<lbrakk>kheap s x = Some (ArchObj (PageTable x2)); valid_objs s; pspace_aligned s; ko = ArchObj (PageTable x2); is_aligned x 10; 10 < word_bits; ya \<in> UNIV; x \<le> x; x \<le> x + 2 ^ 10 - 1; P = pte_relation ya; y = x + (UCAST(8 \<rightarrow> 32) ya << 2); x \<le> x + (UCAST(8 \<rightarrow> 32) ya << 2)\<rbrakk> \<Longrightarrow> UCAST(8 \<rightarrow> 32) ya << 2 \<le> 2 ^ 10 - 1
 2. \<And>arch_kernel_obj x2 ya. \<lbrakk>kheap s x = Some (ArchObj (PageTable x2)); valid_objs s; pspace_aligned s; ko = ArchObj (PageTable x2); is_aligned x 10; 10 < word_bits; ya \<in> UNIV; x \<le> x; x \<le> x + 2 ^ 10 - 1; P = pte_relation ya; y = x + (UCAST(8 \<rightarrow> 32) ya << 2); x \<le> x + (UCAST(8 \<rightarrow> 32) ya << 2)\<rbrakk> \<Longrightarrow> x \<le> x + (2 ^ 10 - 1)
 3. \<And>arch_kernel_obj x3. \<lbrakk>(y, P) \<in> range (\<lambda>y. (x + (UCAST(12 \<rightarrow> 32) y << 2), pde_relation y)); x \<in> obj_range x (ArchObj (PageDirectory x3)); kheap s x = Some (ArchObj (PageDirectory x3)); valid_objs s; pspace_aligned s; ko = ArchObj (PageDirectory x3); is_aligned x 14; 14 < word_bits; arch_kernel_obj = PageDirectory x3\<rbrakk> \<Longrightarrow> y \<in> obj_range x (ArchObj (PageDirectory x3))
 4. \<And>arch_kernel_obj x41 x42. \<lbrakk>\<exists>n. y = x + n * 2 ^ pageBits \<and> P = (\<lambda>_ obj. obj = (if x41 then KOUserDataDevice else KOUserData)) \<and> n < 2 ^ (pageBitsForSize x42 - pageBits); x \<in> obj_range x (ArchObj (DataPage x41 x42)); kheap s x = Some (ArchObj (DataPage x41 x42)); valid_objs s; pspace_aligned s; ko = ArchObj (DataPage x41 x42); is_aligned x (pageBitsForSize x42); pageBitsForSize x42 < word_bits; arch_kernel_obj = DataPage x41 x42\<rbrakk> \<Longrightarrow> y \<in> obj_range x (ArchObj (DataPage x41 x42)) proof (prove)
goal (4 subgoals):
 1. \<And>arch_kernel_obj x2 ya. \<lbrakk>kheap s x = Some (ArchObj (PageTable x2)); valid_objs s; pspace_aligned s; ko = ArchObj (PageTable x2); is_aligned x 10; 10 < word_bits; ya \<in> UNIV; x \<le> x; x \<le> x + 2 ^ 10 - 1; P = pte_relation ya; y = x + (UCAST(8 \<rightarrow> 32) ya << 2); x \<le> x + (UCAST(8 \<rightarrow> 32) ya << 2)\<rbrakk> \<Longrightarrow> UCAST(8 \<rightarrow> 32) ya << 2 < 2 ^ 10
 2. \<And>arch_kernel_obj x2 ya. \<lbrakk>kheap s x = Some (ArchObj (PageTable x2)); valid_objs s; pspace_aligned s; ko = ArchObj (PageTable x2); is_aligned x 10; 10 < word_bits; ya \<in> UNIV; x \<le> x; x \<le> x + 2 ^ 10 - 1; P = pte_relation ya; y = x + (UCAST(8 \<rightarrow> 32) ya << 2); x \<le> x + (UCAST(8 \<rightarrow> 32) ya << 2)\<rbrakk> \<Longrightarrow> x \<le> x + (2 ^ 10 - 1)
 3. \<And>arch_kernel_obj x3. \<lbrakk>(y, P) \<in> range (\<lambda>y. (x + (UCAST(12 \<rightarrow> 32) y << 2), pde_relation y)); x \<in> obj_range x (ArchObj (PageDirectory x3)); kheap s x = Some (ArchObj (PageDirectory x3)); valid_objs s; pspace_aligned s; ko = ArchObj (PageDirectory x3); is_aligned x 14; 14 < word_bits; arch_kernel_obj = PageDirectory x3\<rbrakk> \<Longrightarrow> y \<in> obj_range x (ArchObj (PageDirectory x3))
 4. \<And>arch_kernel_obj x41 x42. \<lbrakk>\<exists>n. y = x + n * 2 ^ pageBits \<and> P = (\<lambda>_ obj. obj = (if x41 then KOUserDataDevice else KOUserData)) \<and> n < 2 ^ (pageBitsForSize x42 - pageBits); x \<in> obj_range x (ArchObj (DataPage x41 x42)); kheap s x = Some (ArchObj (DataPage x41 x42)); valid_objs s; pspace_aligned s; ko = ArchObj (DataPage x41 x42); is_aligned x (pageBitsForSize x42); pageBitsForSize x42 < word_bits; arch_kernel_obj = DataPage x41 x42\<rbrakk> \<Longrightarrow> y \<in> obj_range x (ArchObj (DataPage x41 x42)) proof (prove)
goal (3 subgoals):
 1. \<And>arch_kernel_obj x2 ya. \<lbrakk>kheap s x = Some (ArchObj (PageTable x2)); valid_objs s; pspace_aligned s; ko = ArchObj (PageTable x2); is_aligned x 10; 10 < word_bits; ya \<in> UNIV; x \<le> x; x \<le> x + 2 ^ 10 - 1; P = pte_relation ya; y = x + (UCAST(8 \<rightarrow> 32) ya << 2); x \<le> x + (UCAST(8 \<rightarrow> 32) ya << 2)\<rbrakk> \<Longrightarrow> x \<le> x + (2 ^ 10 - 1)
 2. \<And>arch_kernel_obj x3. \<lbrakk>(y, P) \<in> range (\<lambda>y. (x + (UCAST(12 \<rightarrow> 32) y << 2), pde_relation y)); x \<in> obj_range x (ArchObj (PageDirectory x3)); kheap s x = Some (ArchObj (PageDirectory x3)); valid_objs s; pspace_aligned s; ko = ArchObj (PageDirectory x3); is_aligned x 14; 14 < word_bits; arch_kernel_obj = PageDirectory x3\<rbrakk> \<Longrightarrow> y \<in> obj_range x (ArchObj (PageDirectory x3))
 3. \<And>arch_kernel_obj x41 x42. \<lbrakk>\<exists>n. y = x + n * 2 ^ pageBits \<and> P = (\<lambda>_ obj. obj = (if x41 then KOUserDataDevice else KOUserData)) \<and> n < 2 ^ (pageBitsForSize x42 - pageBits); x \<in> obj_range x (ArchObj (DataPage x41 x42)); kheap s x = Some (ArchObj (DataPage x41 x42)); valid_objs s; pspace_aligned s; ko = ArchObj (DataPage x41 x42); is_aligned x (pageBitsForSize x42); pageBitsForSize x42 < word_bits; arch_kernel_obj = DataPage x41 x42\<rbrakk> \<Longrightarrow> y \<in> obj_range x (ArchObj (DataPage x41 x42)) proof (prove)
goal (2 subgoals):
 1. \<And>arch_kernel_obj x3. \<lbrakk>(y, P) \<in> range (\<lambda>y. (x + (UCAST(12 \<rightarrow> 32) y << 2), pde_relation y)); x \<in> obj_range x (ArchObj (PageDirectory x3)); kheap s x = Some (ArchObj (PageDirectory x3)); valid_objs s; pspace_aligned s; ko = ArchObj (PageDirectory x3); is_aligned x 14; 14 < word_bits; arch_kernel_obj = PageDirectory x3\<rbrakk> \<Longrightarrow> y \<in> obj_range x (ArchObj (PageDirectory x3))
 2. \<And>arch_kernel_obj x41 x42. \<lbrakk>\<exists>n. y = x + n * 2 ^ pageBits \<and> P = (\<lambda>_ obj. obj = (if x41 then KOUserDataDevice else KOUserData)) \<and> n < 2 ^ (pageBitsForSize x42 - pageBits); x \<in> obj_range x (ArchObj (DataPage x41 x42)); kheap s x = Some (ArchObj (DataPage x41 x42)); valid_objs s; pspace_aligned s; ko = ArchObj (DataPage x41 x42); is_aligned x (pageBitsForSize x42); pageBitsForSize x42 < word_bits; arch_kernel_obj = DataPage x41 x42\<rbrakk> \<Longrightarrow> y \<in> obj_range x (ArchObj (DataPage x41 x42)) proof (prove)
goal (2 subgoals):
 1. \<And>arch_kernel_obj x3 ya. \<lbrakk>kheap s x = Some (ArchObj (PageDirectory x3)); valid_objs s; pspace_aligned s; ko = ArchObj (PageDirectory x3); is_aligned x 14; 14 < word_bits; ya \<in> UNIV; x \<le> x; x \<le> x + 2 ^ 14 - 1; P = pde_relation ya; y = x + (UCAST(12 \<rightarrow> 32) ya << 2)\<rbrakk> \<Longrightarrow> x \<le> x + (UCAST(12 \<rightarrow> 32) ya << 2) \<and> x + (UCAST(12 \<rightarrow> 32) ya << 2) \<le> x + 2 ^ 14 - 1
 2. \<And>arch_kernel_obj x41 x42. \<lbrakk>\<exists>n. y = x + n * 2 ^ pageBits \<and> P = (\<lambda>_ obj. obj = (if x41 then KOUserDataDevice else KOUserData)) \<and> n < 2 ^ (pageBitsForSize x42 - pageBits); x \<in> obj_range x (ArchObj (DataPage x41 x42)); kheap s x = Some (ArchObj (DataPage x41 x42)); valid_objs s; pspace_aligned s; ko = ArchObj (DataPage x41 x42); is_aligned x (pageBitsForSize x42); pageBitsForSize x42 < word_bits; arch_kernel_obj = DataPage x41 x42\<rbrakk> \<Longrightarrow> y \<in> obj_range x (ArchObj (DataPage x41 x42)) proof (prove)
goal (3 subgoals):
 1. \<And>arch_kernel_obj x3 ya. \<lbrakk>kheap s x = Some (ArchObj (PageDirectory x3)); valid_objs s; pspace_aligned s; ko = ArchObj (PageDirectory x3); is_aligned x 14; 14 < word_bits; ya \<in> UNIV; x \<le> x; x \<le> x + 2 ^ 14 - 1; P = pde_relation ya; y = x + (UCAST(12 \<rightarrow> 32) ya << 2)\<rbrakk> \<Longrightarrow> x \<le> x + (UCAST(12 \<rightarrow> 32) ya << 2)
 2. \<And>arch_kernel_obj x3 ya. \<lbrakk>kheap s x = Some (ArchObj (PageDirectory x3)); valid_objs s; pspace_aligned s; ko = ArchObj (PageDirectory x3); is_aligned x 14; 14 < word_bits; ya \<in> UNIV; x \<le> x; x \<le> x + 2 ^ 14 - 1; P = pde_relation ya; y = x + (UCAST(12 \<rightarrow> 32) ya << 2); x \<le> x + (UCAST(12 \<rightarrow> 32) ya << 2)\<rbrakk> \<Longrightarrow> x + (UCAST(12 \<rightarrow> 32) ya << 2) \<le> x + 2 ^ 14 - 1
 3. \<And>arch_kernel_obj x41 x42. \<lbrakk>\<exists>n. y = x + n * 2 ^ pageBits \<and> P = (\<lambda>_ obj. obj = (if x41 then KOUserDataDevice else KOUserData)) \<and> n < 2 ^ (pageBitsForSize x42 - pageBits); x \<in> obj_range x (ArchObj (DataPage x41 x42)); kheap s x = Some (ArchObj (DataPage x41 x42)); valid_objs s; pspace_aligned s; ko = ArchObj (DataPage x41 x42); is_aligned x (pageBitsForSize x42); pageBitsForSize x42 < word_bits; arch_kernel_obj = DataPage x41 x42\<rbrakk> \<Longrightarrow> y \<in> obj_range x (ArchObj (DataPage x41 x42)) proof (prove)
goal (3 subgoals):
 1. \<And>arch_kernel_obj x3 ya. \<lbrakk>kheap s x = Some (ArchObj (PageDirectory x3)); valid_objs s; pspace_aligned s; ko = ArchObj (PageDirectory x3); 14 < word_bits; ya \<in> UNIV; x \<le> x; x \<le> x + 2 ^ 14 - 1; P = pde_relation ya; y = x + (UCAST(12 \<rightarrow> 32) ya << 2)\<rbrakk> \<Longrightarrow> UCAST(12 \<rightarrow> 32) ya << 2 < 2 ^ 14
 2. \<And>arch_kernel_obj x3 ya. \<lbrakk>kheap s x = Some (ArchObj (PageDirectory x3)); valid_objs s; pspace_aligned s; ko = ArchObj (PageDirectory x3); is_aligned x 14; 14 < word_bits; ya \<in> UNIV; x \<le> x; x \<le> x + 2 ^ 14 - 1; P = pde_relation ya; y = x + (UCAST(12 \<rightarrow> 32) ya << 2); x \<le> x + (UCAST(12 \<rightarrow> 32) ya << 2)\<rbrakk> \<Longrightarrow> x + (UCAST(12 \<rightarrow> 32) ya << 2) \<le> x + 2 ^ 14 - 1
 3. \<And>arch_kernel_obj x41 x42. \<lbrakk>\<exists>n. y = x + n * 2 ^ pageBits \<and> P = (\<lambda>_ obj. obj = (if x41 then KOUserDataDevice else KOUserData)) \<and> n < 2 ^ (pageBitsForSize x42 - pageBits); x \<in> obj_range x (ArchObj (DataPage x41 x42)); kheap s x = Some (ArchObj (DataPage x41 x42)); valid_objs s; pspace_aligned s; ko = ArchObj (DataPage x41 x42); is_aligned x (pageBitsForSize x42); pageBitsForSize x42 < word_bits; arch_kernel_obj = DataPage x41 x42\<rbrakk> \<Longrightarrow> y \<in> obj_range x (ArchObj (DataPage x41 x42)) proof (prove)
goal (3 subgoals):
 1. \<And>x3 ya. \<lbrakk>kheap s x = Some (ArchObj (PageDirectory x3)); valid_objs s; pspace_aligned s; ko = ArchObj (PageDirectory x3); 14 < word_bits; x \<le> 0x3FFF + x; P = pde_relation ya; y = x + (UCAST(12 \<rightarrow> 32) ya << 2)\<rbrakk> \<Longrightarrow> UCAST(12 \<rightarrow> 32) ya << 2 < 0x4000
 2. \<And>arch_kernel_obj x3 ya. \<lbrakk>kheap s x = Some (ArchObj (PageDirectory x3)); valid_objs s; pspace_aligned s; ko = ArchObj (PageDirectory x3); is_aligned x 14; 14 < word_bits; ya \<in> UNIV; x \<le> x; x \<le> x + 2 ^ 14 - 1; P = pde_relation ya; y = x + (UCAST(12 \<rightarrow> 32) ya << 2); x \<le> x + (UCAST(12 \<rightarrow> 32) ya << 2)\<rbrakk> \<Longrightarrow> x + (UCAST(12 \<rightarrow> 32) ya << 2) \<le> x + 2 ^ 14 - 1
 3. \<And>arch_kernel_obj x41 x42. \<lbrakk>\<exists>n. y = x + n * 2 ^ pageBits \<and> P = (\<lambda>_ obj. obj = (if x41 then KOUserDataDevice else KOUserData)) \<and> n < 2 ^ (pageBitsForSize x42 - pageBits); x \<in> obj_range x (ArchObj (DataPage x41 x42)); kheap s x = Some (ArchObj (DataPage x41 x42)); valid_objs s; pspace_aligned s; ko = ArchObj (DataPage x41 x42); is_aligned x (pageBitsForSize x42); pageBitsForSize x42 < word_bits; arch_kernel_obj = DataPage x41 x42\<rbrakk> \<Longrightarrow> y \<in> obj_range x (ArchObj (DataPage x41 x42)) proof (prove)
goal (2 subgoals):
 1. \<And>arch_kernel_obj x3 ya. \<lbrakk>kheap s x = Some (ArchObj (PageDirectory x3)); valid_objs s; pspace_aligned s; ko = ArchObj (PageDirectory x3); is_aligned x 14; 14 < word_bits; ya \<in> UNIV; x \<le> x; x \<le> x + 2 ^ 14 - 1; P = pde_relation ya; y = x + (UCAST(12 \<rightarrow> 32) ya << 2); x \<le> x + (UCAST(12 \<rightarrow> 32) ya << 2)\<rbrakk> \<Longrightarrow> x + (UCAST(12 \<rightarrow> 32) ya << 2) \<le> x + 2 ^ 14 - 1
 2. \<And>arch_kernel_obj x41 x42. \<lbrakk>\<exists>n. y = x + n * 2 ^ pageBits \<and> P = (\<lambda>_ obj. obj = (if x41 then KOUserDataDevice else KOUserData)) \<and> n < 2 ^ (pageBitsForSize x42 - pageBits); x \<in> obj_range x (ArchObj (DataPage x41 x42)); kheap s x = Some (ArchObj (DataPage x41 x42)); valid_objs s; pspace_aligned s; ko = ArchObj (DataPage x41 x42); is_aligned x (pageBitsForSize x42); pageBitsForSize x42 < word_bits; arch_kernel_obj = DataPage x41 x42\<rbrakk> \<Longrightarrow> y \<in> obj_range x (ArchObj (DataPage x41 x42)) proof (prove)
goal (2 subgoals):
 1. \<And>arch_kernel_obj x3 ya. \<lbrakk>kheap s x = Some (ArchObj (PageDirectory x3)); valid_objs s; pspace_aligned s; ko = ArchObj (PageDirectory x3); is_aligned x 14; 14 < word_bits; ya \<in> UNIV; x \<le> x; x \<le> x + 2 ^ 14 - 1; P = pde_relation ya; y = x + (UCAST(12 \<rightarrow> 32) ya << 2); x \<le> x + (UCAST(12 \<rightarrow> 32) ya << 2)\<rbrakk> \<Longrightarrow> x + (UCAST(12 \<rightarrow> 32) ya << 2) \<le> x + (2 ^ 14 - 1)
 2. \<And>arch_kernel_obj x41 x42. \<lbrakk>\<exists>n. y = x + n * 2 ^ pageBits \<and> P = (\<lambda>_ obj. obj = (if x41 then KOUserDataDevice else KOUserData)) \<and> n < 2 ^ (pageBitsForSize x42 - pageBits); x \<in> obj_range x (ArchObj (DataPage x41 x42)); kheap s x = Some (ArchObj (DataPage x41 x42)); valid_objs s; pspace_aligned s; ko = ArchObj (DataPage x41 x42); is_aligned x (pageBitsForSize x42); pageBitsForSize x42 < word_bits; arch_kernel_obj = DataPage x41 x42\<rbrakk> \<Longrightarrow> y \<in> obj_range x (ArchObj (DataPage x41 x42)) proof (prove)
goal (3 subgoals):
 1. \<And>arch_kernel_obj x3 ya. \<lbrakk>kheap s x = Some (ArchObj (PageDirectory x3)); valid_objs s; pspace_aligned s; ko = ArchObj (PageDirectory x3); is_aligned x 14; 14 < word_bits; ya \<in> UNIV; x \<le> x; x \<le> x + 2 ^ 14 - 1; P = pde_relation ya; y = x + (UCAST(12 \<rightarrow> 32) ya << 2); x \<le> x + (UCAST(12 \<rightarrow> 32) ya << 2)\<rbrakk> \<Longrightarrow> UCAST(12 \<rightarrow> 32) ya << 2 \<le> 2 ^ 14 - 1
 2. \<And>arch_kernel_obj x3 ya. \<lbrakk>kheap s x = Some (ArchObj (PageDirectory x3)); valid_objs s; pspace_aligned s; ko = ArchObj (PageDirectory x3); is_aligned x 14; 14 < word_bits; ya \<in> UNIV; x \<le> x; x \<le> x + 2 ^ 14 - 1; P = pde_relation ya; y = x + (UCAST(12 \<rightarrow> 32) ya << 2); x \<le> x + (UCAST(12 \<rightarrow> 32) ya << 2)\<rbrakk> \<Longrightarrow> x \<le> x + (2 ^ 14 - 1)
 3. \<And>arch_kernel_obj x41 x42. \<lbrakk>\<exists>n. y = x + n * 2 ^ pageBits \<and> P = (\<lambda>_ obj. obj = (if x41 then KOUserDataDevice else KOUserData)) \<and> n < 2 ^ (pageBitsForSize x42 - pageBits); x \<in> obj_range x (ArchObj (DataPage x41 x42)); kheap s x = Some (ArchObj (DataPage x41 x42)); valid_objs s; pspace_aligned s; ko = ArchObj (DataPage x41 x42); is_aligned x (pageBitsForSize x42); pageBitsForSize x42 < word_bits; arch_kernel_obj = DataPage x41 x42\<rbrakk> \<Longrightarrow> y \<in> obj_range x (ArchObj (DataPage x41 x42)) proof (prove)
goal (3 subgoals):
 1. \<And>arch_kernel_obj x3 ya. \<lbrakk>kheap s x = Some (ArchObj (PageDirectory x3)); valid_objs s; pspace_aligned s; ko = ArchObj (PageDirectory x3); is_aligned x 14; 14 < word_bits; ya \<in> UNIV; x \<le> x; x \<le> x + 2 ^ 14 - 1; P = pde_relation ya; y = x + (UCAST(12 \<rightarrow> 32) ya << 2); x \<le> x + (UCAST(12 \<rightarrow> 32) ya << 2)\<rbrakk> \<Longrightarrow> UCAST(12 \<rightarrow> 32) ya << 2 < 2 ^ 14
 2. \<And>arch_kernel_obj x3 ya. \<lbrakk>kheap s x = Some (ArchObj (PageDirectory x3)); valid_objs s; pspace_aligned s; ko = ArchObj (PageDirectory x3); is_aligned x 14; 14 < word_bits; ya \<in> UNIV; x \<le> x; x \<le> x + 2 ^ 14 - 1; P = pde_relation ya; y = x + (UCAST(12 \<rightarrow> 32) ya << 2); x \<le> x + (UCAST(12 \<rightarrow> 32) ya << 2)\<rbrakk> \<Longrightarrow> x \<le> x + (2 ^ 14 - 1)
 3. \<And>arch_kernel_obj x41 x42. \<lbrakk>\<exists>n. y = x + n * 2 ^ pageBits \<and> P = (\<lambda>_ obj. obj = (if x41 then KOUserDataDevice else KOUserData)) \<and> n < 2 ^ (pageBitsForSize x42 - pageBits); x \<in> obj_range x (ArchObj (DataPage x41 x42)); kheap s x = Some (ArchObj (DataPage x41 x42)); valid_objs s; pspace_aligned s; ko = ArchObj (DataPage x41 x42); is_aligned x (pageBitsForSize x42); pageBitsForSize x42 < word_bits; arch_kernel_obj = DataPage x41 x42\<rbrakk> \<Longrightarrow> y \<in> obj_range x (ArchObj (DataPage x41 x42)) proof (prove)
goal (2 subgoals):
 1. \<And>arch_kernel_obj x3 ya. \<lbrakk>kheap s x = Some (ArchObj (PageDirectory x3)); valid_objs s; pspace_aligned s; ko = ArchObj (PageDirectory x3); is_aligned x 14; 14 < word_bits; ya \<in> UNIV; x \<le> x; x \<le> x + 2 ^ 14 - 1; P = pde_relation ya; y = x + (UCAST(12 \<rightarrow> 32) ya << 2); x \<le> x + (UCAST(12 \<rightarrow> 32) ya << 2)\<rbrakk> \<Longrightarrow> x \<le> x + (2 ^ 14 - 1)
 2. \<And>arch_kernel_obj x41 x42. \<lbrakk>\<exists>n. y = x + n * 2 ^ pageBits \<and> P = (\<lambda>_ obj. obj = (if x41 then KOUserDataDevice else KOUserData)) \<and> n < 2 ^ (pageBitsForSize x42 - pageBits); x \<in> obj_range x (ArchObj (DataPage x41 x42)); kheap s x = Some (ArchObj (DataPage x41 x42)); valid_objs s; pspace_aligned s; ko = ArchObj (DataPage x41 x42); is_aligned x (pageBitsForSize x42); pageBitsForSize x42 < word_bits; arch_kernel_obj = DataPage x41 x42\<rbrakk> \<Longrightarrow> y \<in> obj_range x (ArchObj (DataPage x41 x42)) proof (prove)
goal (1 subgoal):
 1. \<And>arch_kernel_obj x41 x42. \<lbrakk>\<exists>n. y = x + n * 2 ^ pageBits \<and> P = (\<lambda>_ obj. obj = (if x41 then KOUserDataDevice else KOUserData)) \<and> n < 2 ^ (pageBitsForSize x42 - pageBits); x \<in> obj_range x (ArchObj (DataPage x41 x42)); kheap s x = Some (ArchObj (DataPage x41 x42)); valid_objs s; pspace_aligned s; ko = ArchObj (DataPage x41 x42); is_aligned x (pageBitsForSize x42); pageBitsForSize x42 < word_bits; arch_kernel_obj = DataPage x41 x42\<rbrakk> \<Longrightarrow> y \<in> obj_range x (ArchObj (DataPage x41 x42)) proof (prove)
goal (1 subgoal):
 1. \<And>arch_kernel_obj x41 vmpage_size. \<lbrakk>\<exists>n. y = x + n * 2 ^ pageBits \<and> P = (\<lambda>_ obj. obj = (if x41 then KOUserDataDevice else KOUserData)) \<and> n < 2 ^ (pageBitsForSize vmpage_size - pageBits); x \<in> obj_range x (ArchObj (DataPage x41 vmpage_size)); kheap s x = Some (ArchObj (DataPage x41 vmpage_size)); valid_objs s; pspace_aligned s; ko = ArchObj (DataPage x41 vmpage_size); is_aligned x (pageBitsForSize vmpage_size); pageBitsForSize vmpage_size < word_bits; arch_kernel_obj = DataPage x41 vmpage_size\<rbrakk> \<Longrightarrow> y \<in> obj_range x (ArchObj (DataPage x41 vmpage_size)) proof (prove)
goal (1 subgoal):
 1. \<And>arch_kernel_obj x41 vmpage_size n. \<lbrakk>kheap s x = Some (ArchObj (DataPage x41 vmpage_size)); valid_objs s; pspace_aligned s; ko = ArchObj (DataPage x41 vmpage_size); is_aligned x (pageBitsForSize vmpage_size); pageBitsForSize vmpage_size < word_bits; x \<le> x; x \<le> x + 2 ^ pageBitsForSize vmpage_size - 1; y = x + n * 2 ^ pageBits; P = (\<lambda>_ obj. obj = (if x41 then KOUserDataDevice else KOUserData)); n < 2 ^ (pageBitsForSize vmpage_size - pageBits)\<rbrakk> \<Longrightarrow> x \<le> x + n * 2 ^ pageBits \<and> x + n * 2 ^ pageBits \<le> x + 2 ^ pageBitsForSize vmpage_size - 1 proof (prove)
goal (2 subgoals):
 1. \<And>arch_kernel_obj x41 vmpage_size n. \<lbrakk>kheap s x = Some (ArchObj (DataPage x41 vmpage_size)); valid_objs s; pspace_aligned s; ko = ArchObj (DataPage x41 vmpage_size); is_aligned x (pageBitsForSize vmpage_size); pageBitsForSize vmpage_size < word_bits; x \<le> x; x \<le> x + 2 ^ pageBitsForSize vmpage_size - 1; y = x + n * 2 ^ pageBits; P = (\<lambda>_ obj. obj = (if x41 then KOUserDataDevice else KOUserData)); n < 2 ^ (pageBitsForSize vmpage_size - pageBits); n * 2 ^ pageBits < 2 ^ pageBitsForSize vmpage_size\<rbrakk> \<Longrightarrow> x \<le> x + n * 2 ^ pageBits \<and> x + n * 2 ^ pageBits \<le> x + 2 ^ pageBitsForSize vmpage_size - 1
 2. \<And>arch_kernel_obj x41 vmpage_size n. \<lbrakk>kheap s x = Some (ArchObj (DataPage x41 vmpage_size)); valid_objs s; pspace_aligned s; ko = ArchObj (DataPage x41 vmpage_size); is_aligned x (pageBitsForSize vmpage_size); pageBitsForSize vmpage_size < word_bits; x \<le> x; x \<le> x + 2 ^ pageBitsForSize vmpage_size - 1; y = x + n * 2 ^ pageBits; P = (\<lambda>_ obj. obj = (if x41 then KOUserDataDevice else KOUserData)); n < 2 ^ (pageBitsForSize vmpage_size - pageBits)\<rbrakk> \<Longrightarrow> n * 2 ^ pageBits < 2 ^ pageBitsForSize vmpage_size proof (prove)
goal (3 subgoals):
 1. \<And>arch_kernel_obj x41 vmpage_size n. \<lbrakk>kheap s x = Some (ArchObj (DataPage x41 vmpage_size)); valid_objs s; pspace_aligned s; ko = ArchObj (DataPage x41 vmpage_size); is_aligned x (pageBitsForSize vmpage_size); pageBitsForSize vmpage_size < word_bits; x \<le> x; x \<le> x + 2 ^ pageBitsForSize vmpage_size - 1; y = x + n * 2 ^ pageBits; P = (\<lambda>_ obj. obj = (if x41 then KOUserDataDevice else KOUserData)); n < 2 ^ (pageBitsForSize vmpage_size - pageBits); n * 2 ^ pageBits < 2 ^ pageBitsForSize vmpage_size\<rbrakk> \<Longrightarrow> x \<le> x + n * 2 ^ pageBits
 2. \<And>arch_kernel_obj x41 vmpage_size n. \<lbrakk>kheap s x = Some (ArchObj (DataPage x41 vmpage_size)); valid_objs s; pspace_aligned s; ko = ArchObj (DataPage x41 vmpage_size); is_aligned x (pageBitsForSize vmpage_size); pageBitsForSize vmpage_size < word_bits; x \<le> x; x \<le> x + 2 ^ pageBitsForSize vmpage_size - 1; y = x + n * 2 ^ pageBits; P = (\<lambda>_ obj. obj = (if x41 then KOUserDataDevice else KOUserData)); n < 2 ^ (pageBitsForSize vmpage_size - pageBits); n * 2 ^ pageBits < 2 ^ pageBitsForSize vmpage_size; x \<le> x + n * 2 ^ pageBits\<rbrakk> \<Longrightarrow> x + n * 2 ^ pageBits \<le> x + 2 ^ pageBitsForSize vmpage_size - 1
 3. \<And>arch_kernel_obj x41 vmpage_size n. \<lbrakk>kheap s x = Some (ArchObj (DataPage x41 vmpage_size)); valid_objs s; pspace_aligned s; ko = ArchObj (DataPage x41 vmpage_size); is_aligned x (pageBitsForSize vmpage_size); pageBitsForSize vmpage_size < word_bits; x \<le> x; x \<le> x + 2 ^ pageBitsForSize vmpage_size - 1; y = x + n * 2 ^ pageBits; P = (\<lambda>_ obj. obj = (if x41 then KOUserDataDevice else KOUserData)); n < 2 ^ (pageBitsForSize vmpage_size - pageBits)\<rbrakk> \<Longrightarrow> n * 2 ^ pageBits < 2 ^ pageBitsForSize vmpage_size proof (prove)
goal (3 subgoals):
 1. \<And>arch_kernel_obj x41 vmpage_size n. \<lbrakk>kheap s x = Some (ArchObj (DataPage x41 vmpage_size)); valid_objs s; pspace_aligned s; ko = ArchObj (DataPage x41 vmpage_size); pageBitsForSize vmpage_size < word_bits; x \<le> x; x \<le> x + 2 ^ pageBitsForSize vmpage_size - 1; y = x + n * 2 ^ pageBits; P = (\<lambda>_ obj. obj = (if x41 then KOUserDataDevice else KOUserData)); n < 2 ^ (pageBitsForSize vmpage_size - pageBits); n * 2 ^ pageBits < 2 ^ pageBitsForSize vmpage_size\<rbrakk> \<Longrightarrow> n * 2 ^ pageBits < 2 ^ pageBitsForSize vmpage_size
 2. \<And>arch_kernel_obj x41 vmpage_size n. \<lbrakk>kheap s x = Some (ArchObj (DataPage x41 vmpage_size)); valid_objs s; pspace_aligned s; ko = ArchObj (DataPage x41 vmpage_size); is_aligned x (pageBitsForSize vmpage_size); pageBitsForSize vmpage_size < word_bits; x \<le> x; x \<le> x + 2 ^ pageBitsForSize vmpage_size - 1; y = x + n * 2 ^ pageBits; P = (\<lambda>_ obj. obj = (if x41 then KOUserDataDevice else KOUserData)); n < 2 ^ (pageBitsForSize vmpage_size - pageBits); n * 2 ^ pageBits < 2 ^ pageBitsForSize vmpage_size; x \<le> x + n * 2 ^ pageBits\<rbrakk> \<Longrightarrow> x + n * 2 ^ pageBits \<le> x + 2 ^ pageBitsForSize vmpage_size - 1
 3. \<And>arch_kernel_obj x41 vmpage_size n. \<lbrakk>kheap s x = Some (ArchObj (DataPage x41 vmpage_size)); valid_objs s; pspace_aligned s; ko = ArchObj (DataPage x41 vmpage_size); is_aligned x (pageBitsForSize vmpage_size); pageBitsForSize vmpage_size < word_bits; x \<le> x; x \<le> x + 2 ^ pageBitsForSize vmpage_size - 1; y = x + n * 2 ^ pageBits; P = (\<lambda>_ obj. obj = (if x41 then KOUserDataDevice else KOUserData)); n < 2 ^ (pageBitsForSize vmpage_size - pageBits)\<rbrakk> \<Longrightarrow> n * 2 ^ pageBits < 2 ^ pageBitsForSize vmpage_size proof (prove)
goal (2 subgoals):
 1. \<And>arch_kernel_obj x41 vmpage_size n. \<lbrakk>kheap s x = Some (ArchObj (DataPage x41 vmpage_size)); valid_objs s; pspace_aligned s; ko = ArchObj (DataPage x41 vmpage_size); is_aligned x (pageBitsForSize vmpage_size); pageBitsForSize vmpage_size < word_bits; x \<le> x; x \<le> x + 2 ^ pageBitsForSize vmpage_size - 1; y = x + n * 2 ^ pageBits; P = (\<lambda>_ obj. obj = (if x41 then KOUserDataDevice else KOUserData)); n < 2 ^ (pageBitsForSize vmpage_size - pageBits); n * 2 ^ pageBits < 2 ^ pageBitsForSize vmpage_size; x \<le> x + n * 2 ^ pageBits\<rbrakk> \<Longrightarrow> x + n * 2 ^ pageBits \<le> x + 2 ^ pageBitsForSize vmpage_size - 1
 2. \<And>arch_kernel_obj x41 vmpage_size n. \<lbrakk>kheap s x = Some (ArchObj (DataPage x41 vmpage_size)); valid_objs s; pspace_aligned s; ko = ArchObj (DataPage x41 vmpage_size); is_aligned x (pageBitsForSize vmpage_size); pageBitsForSize vmpage_size < word_bits; x \<le> x; x \<le> x + 2 ^ pageBitsForSize vmpage_size - 1; y = x + n * 2 ^ pageBits; P = (\<lambda>_ obj. obj = (if x41 then KOUserDataDevice else KOUserData)); n < 2 ^ (pageBitsForSize vmpage_size - pageBits)\<rbrakk> \<Longrightarrow> n * 2 ^ pageBits < 2 ^ pageBitsForSize vmpage_size proof (prove)
goal (2 subgoals):
 1. \<And>arch_kernel_obj x41 vmpage_size n. \<lbrakk>kheap s x = Some (ArchObj (DataPage x41 vmpage_size)); valid_objs s; pspace_aligned s; ko = ArchObj (DataPage x41 vmpage_size); is_aligned x (pageBitsForSize vmpage_size); pageBitsForSize vmpage_size < word_bits; x \<le> x; x \<le> x + 2 ^ pageBitsForSize vmpage_size - 1; y = x + n * 2 ^ pageBits; P = (\<lambda>_ obj. obj = (if x41 then KOUserDataDevice else KOUserData)); n < 2 ^ (pageBitsForSize vmpage_size - pageBits); n * 2 ^ pageBits < 2 ^ pageBitsForSize vmpage_size; x \<le> x + n * 2 ^ pageBits\<rbrakk> \<Longrightarrow> x + n * 2 ^ pageBits \<le> x + (2 ^ pageBitsForSize vmpage_size - 1)
 2. \<And>arch_kernel_obj x41 vmpage_size n. \<lbrakk>kheap s x = Some (ArchObj (DataPage x41 vmpage_size)); valid_objs s; pspace_aligned s; ko = ArchObj (DataPage x41 vmpage_size); is_aligned x (pageBitsForSize vmpage_size); pageBitsForSize vmpage_size < word_bits; x \<le> x; x \<le> x + 2 ^ pageBitsForSize vmpage_size - 1; y = x + n * 2 ^ pageBits; P = (\<lambda>_ obj. obj = (if x41 then KOUserDataDevice else KOUserData)); n < 2 ^ (pageBitsForSize vmpage_size - pageBits)\<rbrakk> \<Longrightarrow> n * 2 ^ pageBits < 2 ^ pageBitsForSize vmpage_size proof (prove)
goal (3 subgoals):
 1. \<And>arch_kernel_obj x41 vmpage_size n. \<lbrakk>kheap s x = Some (ArchObj (DataPage x41 vmpage_size)); valid_objs s; pspace_aligned s; ko = ArchObj (DataPage x41 vmpage_size); is_aligned x (pageBitsForSize vmpage_size); pageBitsForSize vmpage_size < word_bits; x \<le> x; x \<le> x + 2 ^ pageBitsForSize vmpage_size - 1; y = x + n * 2 ^ pageBits; P = (\<lambda>_ obj. obj = (if x41 then KOUserDataDevice else KOUserData)); n < 2 ^ (pageBitsForSize vmpage_size - pageBits); n * 2 ^ pageBits < 2 ^ pageBitsForSize vmpage_size; x \<le> x + n * 2 ^ pageBits\<rbrakk> \<Longrightarrow> n * 2 ^ pageBits \<le> 2 ^ pageBitsForSize vmpage_size - 1
 2. \<And>arch_kernel_obj x41 vmpage_size n. \<lbrakk>kheap s x = Some (ArchObj (DataPage x41 vmpage_size)); valid_objs s; pspace_aligned s; ko = ArchObj (DataPage x41 vmpage_size); is_aligned x (pageBitsForSize vmpage_size); pageBitsForSize vmpage_size < word_bits; x \<le> x; x \<le> x + 2 ^ pageBitsForSize vmpage_size - 1; y = x + n * 2 ^ pageBits; P = (\<lambda>_ obj. obj = (if x41 then KOUserDataDevice else KOUserData)); n < 2 ^ (pageBitsForSize vmpage_size - pageBits); n * 2 ^ pageBits < 2 ^ pageBitsForSize vmpage_size; x \<le> x + n * 2 ^ pageBits\<rbrakk> \<Longrightarrow> x \<le> x + (2 ^ pageBitsForSize vmpage_size - 1)
 3. \<And>arch_kernel_obj x41 vmpage_size n. \<lbrakk>kheap s x = Some (ArchObj (DataPage x41 vmpage_size)); valid_objs s; pspace_aligned s; ko = ArchObj (DataPage x41 vmpage_size); is_aligned x (pageBitsForSize vmpage_size); pageBitsForSize vmpage_size < word_bits; x \<le> x; x \<le> x + 2 ^ pageBitsForSize vmpage_size - 1; y = x + n * 2 ^ pageBits; P = (\<lambda>_ obj. obj = (if x41 then KOUserDataDevice else KOUserData)); n < 2 ^ (pageBitsForSize vmpage_size - pageBits)\<rbrakk> \<Longrightarrow> n * 2 ^ pageBits < 2 ^ pageBitsForSize vmpage_size proof (prove)
goal (3 subgoals):
 1. \<And>arch_kernel_obj x41 vmpage_size n. \<lbrakk>kheap s x = Some (ArchObj (DataPage x41 vmpage_size)); valid_objs s; pspace_aligned s; ko = ArchObj (DataPage x41 vmpage_size); is_aligned x (pageBitsForSize vmpage_size); pageBitsForSize vmpage_size < word_bits; x \<le> x; x \<le> x + 2 ^ pageBitsForSize vmpage_size - 1; y = x + n * 2 ^ pageBits; P = (\<lambda>_ obj. obj = (if x41 then KOUserDataDevice else KOUserData)); n < 2 ^ (pageBitsForSize vmpage_size - pageBits); n * 2 ^ pageBits < 2 ^ pageBitsForSize vmpage_size; x \<le> x + n * 2 ^ pageBits\<rbrakk> \<Longrightarrow> n * 2 ^ pageBits < 2 ^ pageBitsForSize vmpage_size
 2. \<And>arch_kernel_obj x41 vmpage_size n. \<lbrakk>kheap s x = Some (ArchObj (DataPage x41 vmpage_size)); valid_objs s; pspace_aligned s; ko = ArchObj (DataPage x41 vmpage_size); is_aligned x (pageBitsForSize vmpage_size); pageBitsForSize vmpage_size < word_bits; x \<le> x; x \<le> x + 2 ^ pageBitsForSize vmpage_size - 1; y = x + n * 2 ^ pageBits; P = (\<lambda>_ obj. obj = (if x41 then KOUserDataDevice else KOUserData)); n < 2 ^ (pageBitsForSize vmpage_size - pageBits); n * 2 ^ pageBits < 2 ^ pageBitsForSize vmpage_size; x \<le> x + n * 2 ^ pageBits\<rbrakk> \<Longrightarrow> x \<le> x + (2 ^ pageBitsForSize vmpage_size - 1)
 3. \<And>arch_kernel_obj x41 vmpage_size n. \<lbrakk>kheap s x = Some (ArchObj (DataPage x41 vmpage_size)); valid_objs s; pspace_aligned s; ko = ArchObj (DataPage x41 vmpage_size); is_aligned x (pageBitsForSize vmpage_size); pageBitsForSize vmpage_size < word_bits; x \<le> x; x \<le> x + 2 ^ pageBitsForSize vmpage_size - 1; y = x + n * 2 ^ pageBits; P = (\<lambda>_ obj. obj = (if x41 then KOUserDataDevice else KOUserData)); n < 2 ^ (pageBitsForSize vmpage_size - pageBits)\<rbrakk> \<Longrightarrow> n * 2 ^ pageBits < 2 ^ pageBitsForSize vmpage_size proof (prove)
goal (2 subgoals):
 1. \<And>arch_kernel_obj x41 vmpage_size n. \<lbrakk>kheap s x = Some (ArchObj (DataPage x41 vmpage_size)); valid_objs s; pspace_aligned s; ko = ArchObj (DataPage x41 vmpage_size); is_aligned x (pageBitsForSize vmpage_size); pageBitsForSize vmpage_size < word_bits; x \<le> x; x \<le> x + 2 ^ pageBitsForSize vmpage_size - 1; y = x + n * 2 ^ pageBits; P = (\<lambda>_ obj. obj = (if x41 then KOUserDataDevice else KOUserData)); n < 2 ^ (pageBitsForSize vmpage_size - pageBits); n * 2 ^ pageBits < 2 ^ pageBitsForSize vmpage_size; x \<le> x + n * 2 ^ pageBits\<rbrakk> \<Longrightarrow> x \<le> x + (2 ^ pageBitsForSize vmpage_size - 1)
 2. \<And>arch_kernel_obj x41 vmpage_size n. \<lbrakk>kheap s x = Some (ArchObj (DataPage x41 vmpage_size)); valid_objs s; pspace_aligned s; ko = ArchObj (DataPage x41 vmpage_size); is_aligned x (pageBitsForSize vmpage_size); pageBitsForSize vmpage_size < word_bits; x \<le> x; x \<le> x + 2 ^ pageBitsForSize vmpage_size - 1; y = x + n * 2 ^ pageBits; P = (\<lambda>_ obj. obj = (if x41 then KOUserDataDevice else KOUserData)); n < 2 ^ (pageBitsForSize vmpage_size - pageBits)\<rbrakk> \<Longrightarrow> n * 2 ^ pageBits < 2 ^ pageBitsForSize vmpage_size proof (prove)
goal (1 subgoal):
 1. \<And>arch_kernel_obj x41 vmpage_size n. \<lbrakk>kheap s x = Some (ArchObj (DataPage x41 vmpage_size)); valid_objs s; pspace_aligned s; ko = ArchObj (DataPage x41 vmpage_size); is_aligned x (pageBitsForSize vmpage_size); pageBitsForSize vmpage_size < word_bits; x \<le> x; x \<le> x + 2 ^ pageBitsForSize vmpage_size - 1; y = x + n * 2 ^ pageBits; P = (\<lambda>_ obj. obj = (if x41 then KOUserDataDevice else KOUserData)); n < 2 ^ (pageBitsForSize vmpage_size - pageBits)\<rbrakk> \<Longrightarrow> n * 2 ^ pageBits < 2 ^ pageBitsForSize vmpage_size proof (prove)
goal (2 subgoals):
 1. \<And>arch_kernel_obj x41 vmpage_size n. \<lbrakk>kheap s x = Some (ArchObj (DataPage x41 vmpage_size)); valid_objs s; pspace_aligned s; ko = ArchObj (DataPage x41 vmpage_size); is_aligned x (pageBitsForSize vmpage_size); pageBitsForSize vmpage_size < word_bits; x \<le> x; x \<le> x + 2 ^ pageBitsForSize vmpage_size - 1; y = x + n * 2 ^ pageBits; P = (\<lambda>_ obj. obj = (if x41 then KOUserDataDevice else KOUserData))\<rbrakk> \<Longrightarrow> pageBits \<le> pageBitsForSize vmpage_size
 2. \<And>arch_kernel_obj x41 vmpage_size n. \<lbrakk>kheap s x = Some (ArchObj (DataPage x41 vmpage_size)); valid_objs s; pspace_aligned s; ko = ArchObj (DataPage x41 vmpage_size); is_aligned x (pageBitsForSize vmpage_size); pageBitsForSize vmpage_size < word_bits; x \<le> x; x \<le> x + 2 ^ pageBitsForSize vmpage_size - 1; y = x + n * 2 ^ pageBits; P = (\<lambda>_ obj. obj = (if x41 then KOUserDataDevice else KOUserData))\<rbrakk> \<Longrightarrow> pageBitsForSize vmpage_size < LENGTH(32) proof (prove)
goal (1 subgoal):
 1. \<And>arch_kernel_obj x41 vmpage_size n. \<lbrakk>kheap s x = Some (ArchObj (DataPage x41 vmpage_size)); valid_objs s; pspace_aligned s; ko = ArchObj (DataPage x41 vmpage_size); is_aligned x (pageBitsForSize vmpage_size); pageBitsForSize vmpage_size < word_bits; x \<le> x; x \<le> x + 2 ^ pageBitsForSize vmpage_size - 1; y = x + n * 2 ^ pageBits; P = (\<lambda>_ obj. obj = (if x41 then KOUserDataDevice else KOUserData))\<rbrakk> \<Longrightarrow> pageBitsForSize vmpage_size < LENGTH(32) proof (prove)
goal:
No subgoals!