theory ArchVSpaceEntries_AI

lemma copy_global_mappings_valid_pdpt_objs[wp]:
  notes hoare_pre [wp_pre del]
  shows
  "\<lbrace>valid_pdpt_objs and valid_arch_state and pspace_aligned
            and K (is_aligned p pd_bits)\<rbrace>
       copy_global_mappings p \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>" apply (rule hoare_gen_asm) apply (simp add: copy_global_mappings_def) apply wp apply (rule_tac P="is_aligned global_pd pd_bits" in hoare_gen_asm) apply (rule mapM_x_copy_pde_updates, simp_all) apply (clarsimp simp: mask_eq_x_eq_0[symmetric]) apply (rule less_mask_eq, rule shiftl_less_t2n,
          simp_all add: pd_bits_def pageBits_def)[1] apply (drule plus_one_helper2, simp+) apply wp apply (clarsimp simp: invs_aligned_pdD ranI
                 elim!: ranE split: if_split_asm) apply (intro conjI) apply (rule_tac S="{x. ucast x \<ge> (kernel_base >> 20)}"
                 in valid_entries_partial_copy) apply (fastforce simp: obj_at_def ran_def) apply (fastforce simp: obj_at_def ran_def) apply (clarsimp simp:image_def) apply (subst (asm) less_mask_eq) apply (rule shiftl_less_t2n) apply (simp add:pd_bits_def pageBits_def word_le_make_less) apply (simp add:pd_bits_def pageBits_def) apply (subst (asm) shiftl_shiftr1) apply simp apply (simp add:word_size) apply (subst (asm) less_mask_eq) apply (simp add:pd_bits_def pageBits_def le_less_trans) apply (case_tac v) apply (simp add:ucast_ucast_len pd_bits_def pageBits_def le_less_trans)+ apply (clarsimp split:if_splits) apply (simp add:kernel_base_shift_cast_le) apply (simp add:kernel_base_def) apply (cut_tac y1 = xb and x1 = "0xE00::12 word" in ucast_le_migrate[THEN iffD1,rotated -1]) apply simp apply (simp add:word_size le_less_trans) apply (simp add:word_size) apply (drule aligned_le_sharp[where n = 4 and a = "0xE00::12 word"]) apply (simp add:kernel_base_def is_aligned_def) apply (erule order_trans) apply (erule subst) apply (simp add:word_and_le2) apply (subst ucast_ucast_len) apply (simp,word_bitwise) apply simp apply (clarsimp simp:image_def) apply (rule disjointI) apply clarsimp apply (drule_tac x = "ucast x" in spec) apply (erule impE) apply (simp add:pd_bits_def pageBits_def) apply word_bitwise apply (subgoal_tac "kernel_base >> 20 \<le> ucast x") apply simp apply (subst (asm) less_mask_eq) apply (rule shiftl_less_t2n) apply (simp add:pd_bits_def pageBits_def word_le_make_less) apply word_bitwise apply (simp add:pd_bits_def pageBits_def) apply (subst (asm) shiftl_shiftr1) apply simp apply (simp add:word_size) apply (subst (asm) less_mask_eq) apply (rule less_le_trans[OF ucast_less]) apply simp apply simp apply word_bitwise apply (case_tac v,simp_all) apply (clarsimp split:if_splits) apply (drule aligned_le_sharp[where n = 4]) apply (simp add:kernel_base_def is_aligned_def) apply (simp add:word_size kernel_base_def pd_bits_def pageBits_def) apply word_bitwise apply simp apply (clarsimp simp:obj_at_def) apply (subst (asm) is_aligned_neg_mask_eq
    [where p = p and n = pd_bits,symmetric]) apply simp apply (drule(1) valid_pdpt_objs_pdD[rotated])+ apply (clarsimp simp:entries_align_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_arch_state and pspace_aligned and K (is_aligned p pd_bits)\<rbrace> copy_global_mappings p \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (1 subgoal):
 1. is_aligned p pd_bits \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_arch_state and pspace_aligned\<rbrace> copy_global_mappings p \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (1 subgoal):
 1. is_aligned p pd_bits \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_arch_state and pspace_aligned\<rbrace> do global_pd <- gets (arm_global_pd \<circ> arch_state);
mapM_x (\<lambda>index. get_pde (global_pd + (index << 2)) >>= store_pde (p + (index << 2))) [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]
od \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>global_pd. is_aligned p pd_bits \<Longrightarrow> \<lbrace>?B2 global_pd\<rbrace> mapM_x (\<lambda>index. get_pde (global_pd + (index << 2)) >>= store_pde (p + (index << 2))) [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1] \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace>
 2. is_aligned p pd_bits \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_arch_state and pspace_aligned\<rbrace> gets (arm_global_pd \<circ> arch_state) \<lbrace>?B2\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>global_pd. \<lbrakk>is_aligned p pd_bits; is_aligned global_pd pd_bits\<rbrakk> \<Longrightarrow> \<lbrace>?P'3 global_pd\<rbrace> mapM_x (\<lambda>index. get_pde (global_pd + (index << 2)) >>= store_pde (p + (index << 2))) [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1] \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace>
 2. is_aligned p pd_bits \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_arch_state and pspace_aligned\<rbrace> gets (arm_global_pd \<circ> arch_state) \<lbrace>\<lambda>global_pd. ?P'3 global_pd and K (is_aligned global_pd pd_bits)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>global_pd. \<lbrakk>is_aligned p pd_bits; is_aligned global_pd pd_bits\<rbrakk> \<Longrightarrow> \<forall>x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1 \<longrightarrow> (x << 2) && ~~ mask pd_bits = 0
 2. is_aligned p pd_bits \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_arch_state and pspace_aligned\<rbrace> gets (arm_global_pd \<circ> arch_state) \<lbrace>\<lambda>global_pd. (\<lambda>s. (\<not> typ_at (AArch APageDirectory) global_pd s \<longrightarrow> (\<forall>x\<in>ran (kheap s). obj_valid_pdpt x)) \<and> (\<not> typ_at (AArch APageDirectory) p s \<longrightarrow> (\<forall>x\<in>ran (kheap s). obj_valid_pdpt x)) \<and> (\<forall>pd pd'. ako_at (PageDirectory pd) global_pd s \<and> ako_at (PageDirectory pd') p s \<longrightarrow> (\<forall>x\<in>ran ((kheap s)(p \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y)))). obj_valid_pdpt x))) and (\<lambda>y. is_aligned global_pd pd_bits)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>global_pd x. \<lbrakk>is_aligned p pd_bits; is_aligned global_pd pd_bits; kernel_base >> 20 \<le> x; x \<le> 2 ^ (pd_bits - 2) - 1\<rbrakk> \<Longrightarrow> (x << 2) && mask pd_bits = x << 2
 2. is_aligned p pd_bits \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_arch_state and pspace_aligned\<rbrace> gets (arm_global_pd \<circ> arch_state) \<lbrace>\<lambda>global_pd. (\<lambda>s. (\<not> typ_at (AArch APageDirectory) global_pd s \<longrightarrow> (\<forall>x\<in>ran (kheap s). obj_valid_pdpt x)) \<and> (\<not> typ_at (AArch APageDirectory) p s \<longrightarrow> (\<forall>x\<in>ran (kheap s). obj_valid_pdpt x)) \<and> (\<forall>pd pd'. ako_at (PageDirectory pd) global_pd s \<and> ako_at (PageDirectory pd') p s \<longrightarrow> (\<forall>x\<in>ran ((kheap s)(p \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y)))). obj_valid_pdpt x))) and (\<lambda>y. is_aligned global_pd pd_bits)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>global_pd x. \<lbrakk>is_aligned p 14; is_aligned global_pd 14; kernel_base >> 20 \<le> x; x \<le> 0xFFF\<rbrakk> \<Longrightarrow> x < 0x1000
 2. is_aligned p pd_bits \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_arch_state and pspace_aligned\<rbrace> gets (arm_global_pd \<circ> arch_state) \<lbrace>\<lambda>global_pd. (\<lambda>s. (\<not> typ_at (AArch APageDirectory) global_pd s \<longrightarrow> (\<forall>x\<in>ran (kheap s). obj_valid_pdpt x)) \<and> (\<not> typ_at (AArch APageDirectory) p s \<longrightarrow> (\<forall>x\<in>ran (kheap s). obj_valid_pdpt x)) \<and> (\<forall>pd pd'. ako_at (PageDirectory pd) global_pd s \<and> ako_at (PageDirectory pd') p s \<longrightarrow> (\<forall>x\<in>ran ((kheap s)(p \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y)))). obj_valid_pdpt x))) and (\<lambda>y. is_aligned global_pd pd_bits)\<rbrace> proof (prove)
goal (1 subgoal):
 1. is_aligned p pd_bits \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_arch_state and pspace_aligned\<rbrace> gets (arm_global_pd \<circ> arch_state) \<lbrace>\<lambda>global_pd. (\<lambda>s. (\<not> typ_at (AArch APageDirectory) global_pd s \<longrightarrow> (\<forall>x\<in>ran (kheap s). obj_valid_pdpt x)) \<and> (\<not> typ_at (AArch APageDirectory) p s \<longrightarrow> (\<forall>x\<in>ran (kheap s). obj_valid_pdpt x)) \<and> (\<forall>pd pd'. ako_at (PageDirectory pd) global_pd s \<and> ako_at (PageDirectory pd') p s \<longrightarrow> (\<forall>x\<in>ran ((kheap s)(p \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y)))). obj_valid_pdpt x))) and (\<lambda>y. is_aligned global_pd pd_bits)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_aligned p pd_bits; ((\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_arch_state and pspace_aligned) s\<rbrakk> \<Longrightarrow> ((\<lambda>sa. (\<not> typ_at (AArch APageDirectory) ((arm_global_pd \<circ> arch_state) s) sa \<longrightarrow> (\<forall>x\<in>ran (kheap sa). obj_valid_pdpt x)) \<and> (\<not> typ_at (AArch APageDirectory) p sa \<longrightarrow> (\<forall>x\<in>ran (kheap sa). obj_valid_pdpt x)) \<and> (\<forall>pd pd'. ako_at (PageDirectory pd) ((arm_global_pd \<circ> arch_state) s) sa \<and> ako_at (PageDirectory pd') p sa \<longrightarrow> (\<forall>x\<in>ran ((kheap sa)(p \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y)))). obj_valid_pdpt x))) and (\<lambda>y. is_aligned ((arm_global_pd \<circ> arch_state) s) pd_bits)) s proof (prove)
goal (1 subgoal):
 1. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> valid_entries pde_range (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) \<and> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal (2 subgoals):
 1. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> valid_entries pde_range (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y)
 2. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal (5 subgoals):
 1. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> valid_entries pde_range pd
 2. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> valid_entries pde_range pd'
 3. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> \<forall>v x. x \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} \<longrightarrow> pde_range v x \<subseteq> {x. kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x}
 4. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> \<forall>v x. x \<notin> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} \<longrightarrow> pde_range v x \<inter> {x. kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x} = {}
 5. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal (4 subgoals):
 1. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> valid_entries pde_range pd'
 2. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> \<forall>v x. x \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} \<longrightarrow> pde_range v x \<subseteq> {x. kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x}
 3. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> \<forall>v x. x \<notin> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} \<longrightarrow> pde_range v x \<inter> {x. kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x} = {}
 4. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal (3 subgoals):
 1. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> \<forall>v x. x \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} \<longrightarrow> pde_range v x \<subseteq> {x. kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x}
 2. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> \<forall>v x. x \<notin> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} \<longrightarrow> pde_range v x \<inter> {x. kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x} = {}
 3. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal (3 subgoals):
 1. \<And>s pd pd' v xa xb. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; xa \<in> pde_range v (UCAST(32 \<rightarrow> 12) ((xb << 2) && mask pd_bits >> 2)); kernel_base >> 20 \<le> xb; xb \<le> 2 ^ (pd_bits - 2) - 1\<rbrakk> \<Longrightarrow> kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) xa
 2. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> \<forall>v x. x \<notin> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} \<longrightarrow> pde_range v x \<inter> {x. kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x} = {}
 3. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal (4 subgoals):
 1. \<And>s pd pd' v xa xb. \<lbrakk>kernel_base >> 20 \<le> xb; xb \<le> 2 ^ (pd_bits - 2) - 1; ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> xb << 2 < 2 ^ pd_bits
 2. \<And>s pd pd' v xa xb. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; xa \<in> pde_range v (UCAST(32 \<rightarrow> 12) (xb << 2 >> 2)); kernel_base >> 20 \<le> xb; xb \<le> 2 ^ (pd_bits - 2) - 1\<rbrakk> \<Longrightarrow> kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) xa
 3. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> \<forall>v x. x \<notin> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} \<longrightarrow> pde_range v x \<inter> {x. kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x} = {}
 4. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal (5 subgoals):
 1. \<And>s pd pd' v xa xb. \<lbrakk>kernel_base >> 20 \<le> xb; xb \<le> 2 ^ (pd_bits - 2) - 1; ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> xb < 2 ^ (pd_bits - 2)
 2. \<And>s pd pd' v xa xb. \<lbrakk>kernel_base >> 20 \<le> xb; xb \<le> 2 ^ (pd_bits - 2) - 1; ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> pd_bits < LENGTH(32)
 3. \<And>s pd pd' v xa xb. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; xa \<in> pde_range v (UCAST(32 \<rightarrow> 12) (xb << 2 >> 2)); kernel_base >> 20 \<le> xb; xb \<le> 2 ^ (pd_bits - 2) - 1\<rbrakk> \<Longrightarrow> kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) xa
 4. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> \<forall>v x. x \<notin> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} \<longrightarrow> pde_range v x \<inter> {x. kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x} = {}
 5. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal (4 subgoals):
 1. \<And>s pd pd' v xa xb. \<lbrakk>kernel_base >> 20 \<le> xb; xb \<le> 2 ^ (pd_bits - 2) - 1; ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> pd_bits < LENGTH(32)
 2. \<And>s pd pd' v xa xb. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; xa \<in> pde_range v (UCAST(32 \<rightarrow> 12) (xb << 2 >> 2)); kernel_base >> 20 \<le> xb; xb \<le> 2 ^ (pd_bits - 2) - 1\<rbrakk> \<Longrightarrow> kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) xa
 3. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> \<forall>v x. x \<notin> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} \<longrightarrow> pde_range v x \<inter> {x. kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x} = {}
 4. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal (3 subgoals):
 1. \<And>s pd pd' v xa xb. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; xa \<in> pde_range v (UCAST(32 \<rightarrow> 12) (xb << 2 >> 2)); kernel_base >> 20 \<le> xb; xb \<le> 2 ^ (pd_bits - 2) - 1\<rbrakk> \<Longrightarrow> kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) xa
 2. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> \<forall>v x. x \<notin> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} \<longrightarrow> pde_range v x \<inter> {x. kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x} = {}
 3. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal (4 subgoals):
 1. \<And>s pd pd' v xa xb. \<lbrakk>kernel_base >> 20 \<le> xb; xb \<le> 2 ^ (pd_bits - 2) - 1; ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> 2 \<le> 2
 2. \<And>s pd pd' v xa xb. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; xa \<in> pde_range v (UCAST(32 \<rightarrow> 12) (xb && mask (size xb - 2) << 2 - 2)); kernel_base >> 20 \<le> xb; xb \<le> 2 ^ (pd_bits - 2) - 1\<rbrakk> \<Longrightarrow> kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) xa
 3. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> \<forall>v x. x \<notin> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} \<longrightarrow> pde_range v x \<inter> {x. kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x} = {}
 4. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal (3 subgoals):
 1. \<And>s pd pd' v xa xb. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; xa \<in> pde_range v (UCAST(32 \<rightarrow> 12) (xb && mask (size xb - 2) << 2 - 2)); kernel_base >> 20 \<le> xb; xb \<le> 2 ^ (pd_bits - 2) - 1\<rbrakk> \<Longrightarrow> kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) xa
 2. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> \<forall>v x. x \<notin> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} \<longrightarrow> pde_range v x \<inter> {x. kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x} = {}
 3. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal (3 subgoals):
 1. \<And>s pd pd' v xa xb. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; xa \<in> pde_range v (UCAST(32 \<rightarrow> 12) (xb && mask 30)); kernel_base >> 20 \<le> xb; xb \<le> 2 ^ (pd_bits - 2) - 1\<rbrakk> \<Longrightarrow> kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) xa
 2. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> \<forall>v x. x \<notin> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} \<longrightarrow> pde_range v x \<inter> {x. kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x} = {}
 3. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal (4 subgoals):
 1. \<And>s pd pd' v xa xb. \<lbrakk>kernel_base >> 20 \<le> xb; xb \<le> 2 ^ (pd_bits - 2) - 1; ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> xb < 2 ^ 30
 2. \<And>s pd pd' v xa xb. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; xa \<in> pde_range v (UCAST(32 \<rightarrow> 12) xb); kernel_base >> 20 \<le> xb; xb \<le> 2 ^ (pd_bits - 2) - 1\<rbrakk> \<Longrightarrow> kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) xa
 3. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> \<forall>v x. x \<notin> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} \<longrightarrow> pde_range v x \<inter> {x. kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x} = {}
 4. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal (3 subgoals):
 1. \<And>s pd pd' v xa xb. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; xa \<in> pde_range v (UCAST(32 \<rightarrow> 12) xb); kernel_base >> 20 \<le> xb; xb \<le> 2 ^ (pd_bits - 2) - 1\<rbrakk> \<Longrightarrow> kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) xa
 2. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> \<forall>v x. x \<notin> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} \<longrightarrow> pde_range v x \<inter> {x. kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x} = {}
 3. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal (6 subgoals):
 1. \<And>s pd pd' v xa xb. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; xa \<in> pde_range v (UCAST(32 \<rightarrow> 12) xb); kernel_base >> 20 \<le> xb; xb \<le> 2 ^ (pd_bits - 2) - 1; v = InvalidPDE\<rbrakk> \<Longrightarrow> kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) xa
 2. \<And>s pd pd' v xa xb x21 x22 x23. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; xa \<in> pde_range v (UCAST(32 \<rightarrow> 12) xb); kernel_base >> 20 \<le> xb; xb \<le> 2 ^ (pd_bits - 2) - 1; v = PageTablePDE x21 x22 x23\<rbrakk> \<Longrightarrow> kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) xa
 3. \<And>s pd pd' v xa xb x31 x32 x33 x34. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; xa \<in> pde_range v (UCAST(32 \<rightarrow> 12) xb); kernel_base >> 20 \<le> xb; xb \<le> 2 ^ (pd_bits - 2) - 1; v = SectionPDE x31 x32 x33 x34\<rbrakk> \<Longrightarrow> kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) xa
 4. \<And>s pd pd' v xa xb x41 x42 x43. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; xa \<in> pde_range v (UCAST(32 \<rightarrow> 12) xb); kernel_base >> 20 \<le> xb; xb \<le> 2 ^ (pd_bits - 2) - 1; v = SuperSectionPDE x41 x42 x43\<rbrakk> \<Longrightarrow> kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) xa
 5. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> \<forall>v x. x \<notin> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} \<longrightarrow> pde_range v x \<inter> {x. kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x} = {}
 6. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal (3 subgoals):
 1. \<And>s pd pd' v xa xb x41 x42 x43. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p 14; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; xa \<in> (if is_aligned (UCAST(32 \<rightarrow> 12) xb) 4 then {x. x && ~~ mask 4 = UCAST(32 \<rightarrow> 12) xb} else {UCAST(32 \<rightarrow> 12) xb}); kernel_base >> 20 \<le> xb; xb \<le> 0xFFF; v = SuperSectionPDE x41 x42 x43\<rbrakk> \<Longrightarrow> kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) xa
 2. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> \<forall>v x. x \<notin> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} \<longrightarrow> pde_range v x \<inter> {x. kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x} = {}
 3. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal (4 subgoals):
 1. \<And>s pd pd' xa xb. \<lbrakk>kernel_base >> 20 \<le> xb; xb \<le> 0xFFF; ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p 14; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; is_aligned (UCAST(32 \<rightarrow> 12) xb) 4; xa && ~~ mask 4 = UCAST(32 \<rightarrow> 12) xb\<rbrakk> \<Longrightarrow> kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) xa
 2. \<And>s pd pd' xb. \<lbrakk>kernel_base >> 20 \<le> xb; xb \<le> 0xFFF; ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p 14; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; \<not> is_aligned (UCAST(32 \<rightarrow> 12) xb) 4\<rbrakk> \<Longrightarrow> kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) xb)
 3. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> \<forall>v x. x \<notin> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} \<longrightarrow> pde_range v x \<inter> {x. kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x} = {}
 4. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal (4 subgoals):
 1. \<And>s pd pd' xa xb. \<lbrakk>kernel_base >> 20 \<le> xb; xb \<le> 0xFFF; ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p 14; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; is_aligned (UCAST(32 \<rightarrow> 12) xb) 4; xa && ~~ mask 4 = UCAST(32 \<rightarrow> 12) xb\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> xa
 2. \<And>s pd pd' xb. \<lbrakk>kernel_base >> 20 \<le> xb; xb \<le> 0xFFF; ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p 14; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; \<not> is_aligned (UCAST(32 \<rightarrow> 12) xb) 4\<rbrakk> \<Longrightarrow> kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) xb)
 3. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> \<forall>v x. x \<notin> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} \<longrightarrow> pde_range v x \<inter> {x. kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x} = {}
 4. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal (4 subgoals):
 1. \<And>s pd pd' xa xb. \<lbrakk>0xE00 \<le> xb; xb \<le> 0xFFF; ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p 14; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; is_aligned (UCAST(32 \<rightarrow> 12) xb) 4; xa && ~~ mask 4 = UCAST(32 \<rightarrow> 12) xb\<rbrakk> \<Longrightarrow> 0xE00 \<le> xa
 2. \<And>s pd pd' xb. \<lbrakk>kernel_base >> 20 \<le> xb; xb \<le> 0xFFF; ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p 14; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; \<not> is_aligned (UCAST(32 \<rightarrow> 12) xb) 4\<rbrakk> \<Longrightarrow> kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) xb)
 3. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> \<forall>v x. x \<notin> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} \<longrightarrow> pde_range v x \<inter> {x. kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x} = {}
 4. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal (7 subgoals):
 1. \<And>s pd pd' xa xb. \<lbrakk>0xE00 \<le> xb; xb \<le> 0xFFF; ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p 14; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; is_aligned (UCAST(32 \<rightarrow> 12) xb) 4; xa && ~~ mask 4 = UCAST(32 \<rightarrow> 12) xb\<rbrakk> \<Longrightarrow> UCAST(12 \<rightarrow> 32) 0xE00 \<le> xb
 2. \<And>s pd pd' xa xb. \<lbrakk>0xE00 \<le> xb; xb \<le> 0xFFF; ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p 14; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; is_aligned (UCAST(32 \<rightarrow> 12) xb) 4; xa && ~~ mask 4 = UCAST(32 \<rightarrow> 12) xb\<rbrakk> \<Longrightarrow> xb < 2 ^ size 0xE00
 3. \<And>s pd pd' xa xb. \<lbrakk>0xE00 \<le> xb; xb \<le> 0xFFF; ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p 14; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; is_aligned (UCAST(32 \<rightarrow> 12) xb) 4; xa && ~~ mask 4 = UCAST(32 \<rightarrow> 12) xb\<rbrakk> \<Longrightarrow> size 0xE00 < size xb
 4. \<And>s pd pd' xa xb. \<lbrakk>0xE00 \<le> xb; xb \<le> 0xFFF; ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p 14; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; is_aligned (UCAST(32 \<rightarrow> 12) xb) 4; xa && ~~ mask 4 = UCAST(32 \<rightarrow> 12) xb; 0xE00 \<le> UCAST(32 \<rightarrow> 12) xb\<rbrakk> \<Longrightarrow> 0xE00 \<le> xa
 5. \<And>s pd pd' xb. \<lbrakk>kernel_base >> 20 \<le> xb; xb \<le> 0xFFF; ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p 14; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; \<not> is_aligned (UCAST(32 \<rightarrow> 12) xb) 4\<rbrakk> \<Longrightarrow> kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) xb)
 6. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> \<forall>v x. x \<notin> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} \<longrightarrow> pde_range v x \<inter> {x. kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x} = {}
 7. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal (6 subgoals):
 1. \<And>s pd pd' xa xb. \<lbrakk>0xE00 \<le> xb; xb \<le> 0xFFF; ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p 14; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; is_aligned (UCAST(32 \<rightarrow> 12) xb) 4; xa && ~~ mask 4 = UCAST(32 \<rightarrow> 12) xb\<rbrakk> \<Longrightarrow> xb < 2 ^ size 0xE00
 2. \<And>s pd pd' xa xb. \<lbrakk>0xE00 \<le> xb; xb \<le> 0xFFF; ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p 14; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; is_aligned (UCAST(32 \<rightarrow> 12) xb) 4; xa && ~~ mask 4 = UCAST(32 \<rightarrow> 12) xb\<rbrakk> \<Longrightarrow> size 0xE00 < size xb
 3. \<And>s pd pd' xa xb. \<lbrakk>0xE00 \<le> xb; xb \<le> 0xFFF; ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p 14; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; is_aligned (UCAST(32 \<rightarrow> 12) xb) 4; xa && ~~ mask 4 = UCAST(32 \<rightarrow> 12) xb; 0xE00 \<le> UCAST(32 \<rightarrow> 12) xb\<rbrakk> \<Longrightarrow> 0xE00 \<le> xa
 4. \<And>s pd pd' xb. \<lbrakk>kernel_base >> 20 \<le> xb; xb \<le> 0xFFF; ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p 14; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; \<not> is_aligned (UCAST(32 \<rightarrow> 12) xb) 4\<rbrakk> \<Longrightarrow> kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) xb)
 5. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> \<forall>v x. x \<notin> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} \<longrightarrow> pde_range v x \<inter> {x. kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x} = {}
 6. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal (5 subgoals):
 1. \<And>s pd pd' xa xb. \<lbrakk>0xE00 \<le> xb; xb \<le> 0xFFF; ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p 14; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; is_aligned (UCAST(32 \<rightarrow> 12) xb) 4; xa && ~~ mask 4 = UCAST(32 \<rightarrow> 12) xb\<rbrakk> \<Longrightarrow> size 0xE00 < size xb
 2. \<And>s pd pd' xa xb. \<lbrakk>0xE00 \<le> xb; xb \<le> 0xFFF; ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p 14; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; is_aligned (UCAST(32 \<rightarrow> 12) xb) 4; xa && ~~ mask 4 = UCAST(32 \<rightarrow> 12) xb; 0xE00 \<le> UCAST(32 \<rightarrow> 12) xb\<rbrakk> \<Longrightarrow> 0xE00 \<le> xa
 3. \<And>s pd pd' xb. \<lbrakk>kernel_base >> 20 \<le> xb; xb \<le> 0xFFF; ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p 14; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; \<not> is_aligned (UCAST(32 \<rightarrow> 12) xb) 4\<rbrakk> \<Longrightarrow> kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) xb)
 4. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> \<forall>v x. x \<notin> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} \<longrightarrow> pde_range v x \<inter> {x. kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x} = {}
 5. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal (4 subgoals):
 1. \<And>s pd pd' xa xb. \<lbrakk>0xE00 \<le> xb; xb \<le> 0xFFF; ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p 14; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; is_aligned (UCAST(32 \<rightarrow> 12) xb) 4; xa && ~~ mask 4 = UCAST(32 \<rightarrow> 12) xb; 0xE00 \<le> UCAST(32 \<rightarrow> 12) xb\<rbrakk> \<Longrightarrow> 0xE00 \<le> xa
 2. \<And>s pd pd' xb. \<lbrakk>kernel_base >> 20 \<le> xb; xb \<le> 0xFFF; ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p 14; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; \<not> is_aligned (UCAST(32 \<rightarrow> 12) xb) 4\<rbrakk> \<Longrightarrow> kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) xb)
 3. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> \<forall>v x. x \<notin> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} \<longrightarrow> pde_range v x \<inter> {x. kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x} = {}
 4. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal (5 subgoals):
 1. \<And>s pd pd' xa xb. \<lbrakk>0xE00 \<le> xb; xb \<le> 0xFFF; ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p 14; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; is_aligned (UCAST(32 \<rightarrow> 12) xb) 4; xa && ~~ mask 4 = UCAST(32 \<rightarrow> 12) xb\<rbrakk> \<Longrightarrow> is_aligned 0xE00 4
 2. \<And>s pd pd' xa xb. \<lbrakk>0xE00 \<le> xb; xb \<le> 0xFFF; ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p 14; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; is_aligned (UCAST(32 \<rightarrow> 12) xb) 4; xa && ~~ mask 4 = UCAST(32 \<rightarrow> 12) xb; 0xE00 \<le> UCAST(32 \<rightarrow> 12) xb && ~~ mask 4\<rbrakk> \<Longrightarrow> 0xE00 \<le> xa
 3. \<And>s pd pd' xb. \<lbrakk>kernel_base >> 20 \<le> xb; xb \<le> 0xFFF; ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p 14; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; \<not> is_aligned (UCAST(32 \<rightarrow> 12) xb) 4\<rbrakk> \<Longrightarrow> kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) xb)
 4. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> \<forall>v x. x \<notin> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} \<longrightarrow> pde_range v x \<inter> {x. kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x} = {}
 5. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal (4 subgoals):
 1. \<And>s pd pd' xa xb. \<lbrakk>0xE00 \<le> xb; xb \<le> 0xFFF; ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p 14; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; is_aligned (UCAST(32 \<rightarrow> 12) xb) 4; xa && ~~ mask 4 = UCAST(32 \<rightarrow> 12) xb; 0xE00 \<le> UCAST(32 \<rightarrow> 12) xb && ~~ mask 4\<rbrakk> \<Longrightarrow> 0xE00 \<le> xa
 2. \<And>s pd pd' xb. \<lbrakk>kernel_base >> 20 \<le> xb; xb \<le> 0xFFF; ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p 14; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; \<not> is_aligned (UCAST(32 \<rightarrow> 12) xb) 4\<rbrakk> \<Longrightarrow> kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) xb)
 3. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> \<forall>v x. x \<notin> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} \<longrightarrow> pde_range v x \<inter> {x. kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x} = {}
 4. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal (4 subgoals):
 1. \<And>s pd pd' xa xb. \<lbrakk>0xE00 \<le> xb; xb \<le> 0xFFF; ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p 14; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; is_aligned (UCAST(32 \<rightarrow> 12) xb) 4; xa && ~~ mask 4 = UCAST(32 \<rightarrow> 12) xb\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) xb && ~~ mask 4 \<le> xa
 2. \<And>s pd pd' xb. \<lbrakk>kernel_base >> 20 \<le> xb; xb \<le> 0xFFF; ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p 14; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; \<not> is_aligned (UCAST(32 \<rightarrow> 12) xb) 4\<rbrakk> \<Longrightarrow> kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) xb)
 3. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> \<forall>v x. x \<notin> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} \<longrightarrow> pde_range v x \<inter> {x. kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x} = {}
 4. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal (4 subgoals):
 1. \<And>s pd pd' xa xb. \<lbrakk>0xE00 \<le> xb; xb \<le> 0xFFF; ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p 14; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; is_aligned (UCAST(32 \<rightarrow> 12) xb) 4\<rbrakk> \<Longrightarrow> (xa && ~~ mask 4) && ~~ mask 4 \<le> xa
 2. \<And>s pd pd' xb. \<lbrakk>kernel_base >> 20 \<le> xb; xb \<le> 0xFFF; ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p 14; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; \<not> is_aligned (UCAST(32 \<rightarrow> 12) xb) 4\<rbrakk> \<Longrightarrow> kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) xb)
 3. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> \<forall>v x. x \<notin> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} \<longrightarrow> pde_range v x \<inter> {x. kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x} = {}
 4. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal (3 subgoals):
 1. \<And>s pd pd' xb. \<lbrakk>kernel_base >> 20 \<le> xb; xb \<le> 0xFFF; ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p 14; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; \<not> is_aligned (UCAST(32 \<rightarrow> 12) xb) 4\<rbrakk> \<Longrightarrow> kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) xb)
 2. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> \<forall>v x. x \<notin> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} \<longrightarrow> pde_range v x \<inter> {x. kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x} = {}
 3. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal (4 subgoals):
 1. \<And>s pd pd' xb. \<lbrakk>kernel_base >> 20 \<le> xb; xb \<le> 0xFFF; ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p 14; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; \<not> is_aligned (UCAST(32 \<rightarrow> 12) xb) 4\<rbrakk> \<Longrightarrow> xb < 2 ^ LENGTH(12)
 2. \<And>s pd pd' xb. \<lbrakk>kernel_base >> 20 \<le> xb; xb \<le> 0xFFF; ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p 14; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; \<not> is_aligned (UCAST(32 \<rightarrow> 12) xb) 4\<rbrakk> \<Longrightarrow> kernel_base >> 20 \<le> xb
 3. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> \<forall>v x. x \<notin> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} \<longrightarrow> pde_range v x \<inter> {x. kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x} = {}
 4. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal (3 subgoals):
 1. \<And>s pd pd' xb. \<lbrakk>kernel_base >> 20 \<le> xb; xb \<le> 0xFFF; ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p 14; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; \<not> is_aligned (UCAST(32 \<rightarrow> 12) xb) 4\<rbrakk> \<Longrightarrow> kernel_base >> 20 \<le> xb
 2. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> \<forall>v x. x \<notin> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} \<longrightarrow> pde_range v x \<inter> {x. kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x} = {}
 3. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal (2 subgoals):
 1. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> \<forall>v x. x \<notin> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} \<longrightarrow> pde_range v x \<inter> {x. kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x} = {}
 2. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal (2 subgoals):
 1. \<And>s pd pd' v x. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; \<forall>xa\<le>2 ^ (pd_bits - 2) - 1. kernel_base >> 20 \<le> xa \<longrightarrow> x \<noteq> UCAST(32 \<rightarrow> 12) ((xa << 2) && mask pd_bits >> 2)\<rbrakk> \<Longrightarrow> pde_range v x \<inter> {x. kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x} = {}
 2. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal (2 subgoals):
 1. \<And>s pd pd' v x xa y. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; \<forall>xa\<le>2 ^ (pd_bits - 2) - 1. kernel_base >> 20 \<le> xa \<longrightarrow> x \<noteq> UCAST(32 \<rightarrow> 12) ((xa << 2) && mask pd_bits >> 2); xa \<in> pde_range v x; y \<in> {x. kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x}\<rbrakk> \<Longrightarrow> xa \<noteq> y
 2. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal (2 subgoals):
 1. \<And>s pd pd' v x y. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; \<forall>xa\<le>2 ^ (pd_bits - 2) - 1. kernel_base >> 20 \<le> xa \<longrightarrow> x \<noteq> UCAST(32 \<rightarrow> 12) ((xa << 2) && mask pd_bits >> 2); y \<in> pde_range v x; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) y\<rbrakk> \<Longrightarrow> False
 2. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal (2 subgoals):
 1. \<And>s pd pd' v x y. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; y \<in> pde_range v x; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) y; UCAST(12 \<rightarrow> 32) x \<le> 2 ^ (pd_bits - 2) - 1 \<longrightarrow> kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x \<longrightarrow> x \<noteq> UCAST(32 \<rightarrow> 12) ((UCAST(12 \<rightarrow> 32) x << 2) && mask pd_bits >> 2)\<rbrakk> \<Longrightarrow> False
 2. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal (3 subgoals):
 1. \<And>s pd pd' v x y. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; y \<in> pde_range v x; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) y\<rbrakk> \<Longrightarrow> UCAST(12 \<rightarrow> 32) x \<le> 2 ^ (pd_bits - 2) - 1
 2. \<And>s pd pd' v x y. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; y \<in> pde_range v x; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) y; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x \<longrightarrow> x \<noteq> UCAST(32 \<rightarrow> 12) ((UCAST(12 \<rightarrow> 32) x << 2) && mask pd_bits >> 2)\<rbrakk> \<Longrightarrow> False
 3. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal (3 subgoals):
 1. \<And>s pd pd' v x y. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p 14; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; y \<in> pde_range v x; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) y\<rbrakk> \<Longrightarrow> UCAST(12 \<rightarrow> 32) x \<le> 0xFFF
 2. \<And>s pd pd' v x y. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; y \<in> pde_range v x; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) y; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x \<longrightarrow> x \<noteq> UCAST(32 \<rightarrow> 12) ((UCAST(12 \<rightarrow> 32) x << 2) && mask pd_bits >> 2)\<rbrakk> \<Longrightarrow> False
 3. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal (2 subgoals):
 1. \<And>s pd pd' v x y. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; y \<in> pde_range v x; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) y; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x \<longrightarrow> x \<noteq> UCAST(32 \<rightarrow> 12) ((UCAST(12 \<rightarrow> 32) x << 2) && mask pd_bits >> 2)\<rbrakk> \<Longrightarrow> False
 2. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal (3 subgoals):
 1. \<And>s pd pd' v x y. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; y \<in> pde_range v x; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) y; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x \<longrightarrow> x \<noteq> UCAST(32 \<rightarrow> 12) ((UCAST(12 \<rightarrow> 32) x << 2) && mask pd_bits >> 2); kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x\<rbrakk> \<Longrightarrow> False
 2. \<And>s pd pd' v x y. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; y \<in> pde_range v x; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) y; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x \<longrightarrow> x \<noteq> UCAST(32 \<rightarrow> 12) ((UCAST(12 \<rightarrow> 32) x << 2) && mask pd_bits >> 2)\<rbrakk> \<Longrightarrow> kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x
 3. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal (3 subgoals):
 1. \<And>s pd pd' v x y. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; y \<in> pde_range v x; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) y; x \<noteq> UCAST(32 \<rightarrow> 12) ((UCAST(12 \<rightarrow> 32) x << 2) && mask pd_bits >> 2); kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x\<rbrakk> \<Longrightarrow> False
 2. \<And>s pd pd' v x y. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; y \<in> pde_range v x; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) y; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x \<longrightarrow> x \<noteq> UCAST(32 \<rightarrow> 12) ((UCAST(12 \<rightarrow> 32) x << 2) && mask pd_bits >> 2)\<rbrakk> \<Longrightarrow> kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x
 3. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal (4 subgoals):
 1. \<And>s pd pd' v x y. \<lbrakk>kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x; ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; y \<in> pde_range v x; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) y\<rbrakk> \<Longrightarrow> UCAST(12 \<rightarrow> 32) x << 2 < 2 ^ pd_bits
 2. \<And>s pd pd' v x y. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; y \<in> pde_range v x; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) y; x \<noteq> UCAST(32 \<rightarrow> 12) (UCAST(12 \<rightarrow> 32) x << 2 >> 2); kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x\<rbrakk> \<Longrightarrow> False
 3. \<And>s pd pd' v x y. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; y \<in> pde_range v x; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) y; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x \<longrightarrow> x \<noteq> UCAST(32 \<rightarrow> 12) ((UCAST(12 \<rightarrow> 32) x << 2) && mask pd_bits >> 2)\<rbrakk> \<Longrightarrow> kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x
 4. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal (5 subgoals):
 1. \<And>s pd pd' v x y. \<lbrakk>kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x; ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; y \<in> pde_range v x; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) y\<rbrakk> \<Longrightarrow> UCAST(12 \<rightarrow> 32) x < 2 ^ (pd_bits - 2)
 2. \<And>s pd pd' v x y. \<lbrakk>kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x; ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; y \<in> pde_range v x; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) y\<rbrakk> \<Longrightarrow> pd_bits < LENGTH(32)
 3. \<And>s pd pd' v x y. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; y \<in> pde_range v x; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) y; x \<noteq> UCAST(32 \<rightarrow> 12) (UCAST(12 \<rightarrow> 32) x << 2 >> 2); kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x\<rbrakk> \<Longrightarrow> False
 4. \<And>s pd pd' v x y. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; y \<in> pde_range v x; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) y; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x \<longrightarrow> x \<noteq> UCAST(32 \<rightarrow> 12) ((UCAST(12 \<rightarrow> 32) x << 2) && mask pd_bits >> 2)\<rbrakk> \<Longrightarrow> kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x
 5. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal (5 subgoals):
 1. \<And>s pd pd' v x y. \<lbrakk>kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x; ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p 14; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; y \<in> pde_range v x; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) y\<rbrakk> \<Longrightarrow> UCAST(12 \<rightarrow> 32) x < 0x1000
 2. \<And>s pd pd' v x y. \<lbrakk>kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x; ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; y \<in> pde_range v x; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) y\<rbrakk> \<Longrightarrow> pd_bits < LENGTH(32)
 3. \<And>s pd pd' v x y. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; y \<in> pde_range v x; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) y; x \<noteq> UCAST(32 \<rightarrow> 12) (UCAST(12 \<rightarrow> 32) x << 2 >> 2); kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x\<rbrakk> \<Longrightarrow> False
 4. \<And>s pd pd' v x y. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; y \<in> pde_range v x; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) y; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x \<longrightarrow> x \<noteq> UCAST(32 \<rightarrow> 12) ((UCAST(12 \<rightarrow> 32) x << 2) && mask pd_bits >> 2)\<rbrakk> \<Longrightarrow> kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x
 5. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal (4 subgoals):
 1. \<And>s pd pd' v x y. \<lbrakk>kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x; ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; y \<in> pde_range v x; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) y\<rbrakk> \<Longrightarrow> pd_bits < LENGTH(32)
 2. \<And>s pd pd' v x y. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; y \<in> pde_range v x; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) y; x \<noteq> UCAST(32 \<rightarrow> 12) (UCAST(12 \<rightarrow> 32) x << 2 >> 2); kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x\<rbrakk> \<Longrightarrow> False
 3. \<And>s pd pd' v x y. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; y \<in> pde_range v x; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) y; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x \<longrightarrow> x \<noteq> UCAST(32 \<rightarrow> 12) ((UCAST(12 \<rightarrow> 32) x << 2) && mask pd_bits >> 2)\<rbrakk> \<Longrightarrow> kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x
 4. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal (3 subgoals):
 1. \<And>s pd pd' v x y. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; y \<in> pde_range v x; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) y; x \<noteq> UCAST(32 \<rightarrow> 12) (UCAST(12 \<rightarrow> 32) x << 2 >> 2); kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x\<rbrakk> \<Longrightarrow> False
 2. \<And>s pd pd' v x y. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; y \<in> pde_range v x; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) y; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x \<longrightarrow> x \<noteq> UCAST(32 \<rightarrow> 12) ((UCAST(12 \<rightarrow> 32) x << 2) && mask pd_bits >> 2)\<rbrakk> \<Longrightarrow> kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x
 3. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal (4 subgoals):
 1. \<And>s pd pd' v x y. \<lbrakk>kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x; ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; y \<in> pde_range v x; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) y\<rbrakk> \<Longrightarrow> 2 \<le> 2
 2. \<And>s pd pd' v x y. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; y \<in> pde_range v x; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) y; x \<noteq> UCAST(32 \<rightarrow> 12) (UCAST(12 \<rightarrow> 32) x && mask (size (UCAST(12 \<rightarrow> 32) x) - 2) << 2 - 2); kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x\<rbrakk> \<Longrightarrow> False
 3. \<And>s pd pd' v x y. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; y \<in> pde_range v x; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) y; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x \<longrightarrow> x \<noteq> UCAST(32 \<rightarrow> 12) ((UCAST(12 \<rightarrow> 32) x << 2) && mask pd_bits >> 2)\<rbrakk> \<Longrightarrow> kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x
 4. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal (3 subgoals):
 1. \<And>s pd pd' v x y. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; y \<in> pde_range v x; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) y; x \<noteq> UCAST(32 \<rightarrow> 12) (UCAST(12 \<rightarrow> 32) x && mask (size (UCAST(12 \<rightarrow> 32) x) - 2) << 2 - 2); kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x\<rbrakk> \<Longrightarrow> False
 2. \<And>s pd pd' v x y. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; y \<in> pde_range v x; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) y; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x \<longrightarrow> x \<noteq> UCAST(32 \<rightarrow> 12) ((UCAST(12 \<rightarrow> 32) x << 2) && mask pd_bits >> 2)\<rbrakk> \<Longrightarrow> kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x
 3. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal (3 subgoals):
 1. \<And>s pd pd' v x y. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; y \<in> pde_range v x; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) y; x \<noteq> UCAST(32 \<rightarrow> 12) (UCAST(12 \<rightarrow> 32) x && mask 30); kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x\<rbrakk> \<Longrightarrow> False
 2. \<And>s pd pd' v x y. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; y \<in> pde_range v x; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) y; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x \<longrightarrow> x \<noteq> UCAST(32 \<rightarrow> 12) ((UCAST(12 \<rightarrow> 32) x << 2) && mask pd_bits >> 2)\<rbrakk> \<Longrightarrow> kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x
 3. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal (4 subgoals):
 1. \<And>s pd pd' v x y. \<lbrakk>kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x; ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; y \<in> pde_range v x; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) y\<rbrakk> \<Longrightarrow> UCAST(12 \<rightarrow> 32) x < 2 ^ 30
 2. \<And>s pd pd' v x y. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; y \<in> pde_range v x; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) y; x \<noteq> UCAST(32 \<rightarrow> 12) (UCAST(12 \<rightarrow> 32) x); kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x\<rbrakk> \<Longrightarrow> False
 3. \<And>s pd pd' v x y. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; y \<in> pde_range v x; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) y; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x \<longrightarrow> x \<noteq> UCAST(32 \<rightarrow> 12) ((UCAST(12 \<rightarrow> 32) x << 2) && mask pd_bits >> 2)\<rbrakk> \<Longrightarrow> kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x
 4. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal (5 subgoals):
 1. \<And>s pd pd' v x y. \<lbrakk>kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x; ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; y \<in> pde_range v x; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) y\<rbrakk> \<Longrightarrow> LENGTH(12) < LENGTH(32)
 2. \<And>s pd pd' v x y. \<lbrakk>kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x; ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; y \<in> pde_range v x; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) y\<rbrakk> \<Longrightarrow> 2 ^ LENGTH(12) \<le> 2 ^ 30
 3. \<And>s pd pd' v x y. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; y \<in> pde_range v x; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) y; x \<noteq> UCAST(32 \<rightarrow> 12) (UCAST(12 \<rightarrow> 32) x); kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x\<rbrakk> \<Longrightarrow> False
 4. \<And>s pd pd' v x y. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; y \<in> pde_range v x; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) y; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x \<longrightarrow> x \<noteq> UCAST(32 \<rightarrow> 12) ((UCAST(12 \<rightarrow> 32) x << 2) && mask pd_bits >> 2)\<rbrakk> \<Longrightarrow> kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x
 5. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal (4 subgoals):
 1. \<And>s pd pd' v x y. \<lbrakk>kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x; ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; y \<in> pde_range v x; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) y\<rbrakk> \<Longrightarrow> 2 ^ LENGTH(12) \<le> 2 ^ 30
 2. \<And>s pd pd' v x y. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; y \<in> pde_range v x; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) y; x \<noteq> UCAST(32 \<rightarrow> 12) (UCAST(12 \<rightarrow> 32) x); kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x\<rbrakk> \<Longrightarrow> False
 3. \<And>s pd pd' v x y. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; y \<in> pde_range v x; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) y; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x \<longrightarrow> x \<noteq> UCAST(32 \<rightarrow> 12) ((UCAST(12 \<rightarrow> 32) x << 2) && mask pd_bits >> 2)\<rbrakk> \<Longrightarrow> kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x
 4. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal (3 subgoals):
 1. \<And>s pd pd' v x y. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; y \<in> pde_range v x; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) y; x \<noteq> UCAST(32 \<rightarrow> 12) (UCAST(12 \<rightarrow> 32) x); kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x\<rbrakk> \<Longrightarrow> False
 2. \<And>s pd pd' v x y. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; y \<in> pde_range v x; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) y; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x \<longrightarrow> x \<noteq> UCAST(32 \<rightarrow> 12) ((UCAST(12 \<rightarrow> 32) x << 2) && mask pd_bits >> 2)\<rbrakk> \<Longrightarrow> kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x
 3. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal (2 subgoals):
 1. \<And>s pd pd' v x y. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; y \<in> pde_range v x; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) y; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x \<longrightarrow> x \<noteq> UCAST(32 \<rightarrow> 12) ((UCAST(12 \<rightarrow> 32) x << 2) && mask pd_bits >> 2)\<rbrakk> \<Longrightarrow> kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x
 2. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal (2 subgoals):
 1. \<And>s pd pd' v x y x41 x42 x43. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; y \<in> (if is_aligned x 4 then {xa. xa && ~~ mask 4 = x} else {x}); kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) y; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x \<longrightarrow> x \<noteq> UCAST(32 \<rightarrow> 12) ((UCAST(12 \<rightarrow> 32) x << 2) && mask pd_bits >> 2); v = SuperSectionPDE x41 x42 x43\<rbrakk> \<Longrightarrow> kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x
 2. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal (2 subgoals):
 1. \<And>s pd pd' y. \<lbrakk>kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) y; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) (y && ~~ mask 4) \<longrightarrow> y && ~~ mask 4 \<noteq> UCAST(32 \<rightarrow> 12) ((UCAST(12 \<rightarrow> 32) (y && ~~ mask 4) << 2) && mask pd_bits >> 2); ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) (y && ~~ mask 4)
 2. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal (3 subgoals):
 1. \<And>s pd pd' y. \<lbrakk>kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) (y && ~~ mask 4) \<longrightarrow> y && ~~ mask 4 \<noteq> UCAST(32 \<rightarrow> 12) ((UCAST(12 \<rightarrow> 32) (y && ~~ mask 4) << 2) && mask pd_bits >> 2); ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> is_aligned (kernel_base >> 20) 4
 2. \<And>s pd pd' y. \<lbrakk>kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) (y && ~~ mask 4) \<longrightarrow> y && ~~ mask 4 \<noteq> UCAST(32 \<rightarrow> 12) ((UCAST(12 \<rightarrow> 32) (y && ~~ mask 4) << 2) && mask pd_bits >> 2); ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) y && ~~ mask 4\<rbrakk> \<Longrightarrow> kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) (y && ~~ mask 4)
 3. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal (2 subgoals):
 1. \<And>s pd pd' y. \<lbrakk>kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) (y && ~~ mask 4) \<longrightarrow> y && ~~ mask 4 \<noteq> UCAST(32 \<rightarrow> 12) ((UCAST(12 \<rightarrow> 32) (y && ~~ mask 4) << 2) && mask pd_bits >> 2); ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) y && ~~ mask 4\<rbrakk> \<Longrightarrow> kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) (y && ~~ mask 4)
 2. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal (2 subgoals):
 1. \<And>s pd pd' y. \<lbrakk>0xE00 \<le> UCAST(12 \<rightarrow> 32) (y && ~~ mask 4) \<longrightarrow> y && ~~ mask 4 \<noteq> UCAST(32 \<rightarrow> 12) ((UCAST(12 \<rightarrow> 32) (y && ~~ mask 4) << 2) && mask 14 >> 2); ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p 14; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; 0xE00 \<le> UCAST(12 \<rightarrow> 32) y && ~~ mask 4\<rbrakk> \<Longrightarrow> 0xE00 \<le> UCAST(12 \<rightarrow> 32) (y && ~~ mask 4)
 2. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal (2 subgoals):
 1. \<And>s pd pd' y. \<lbrakk>y !! 11 \<and> \<not> mask 4 !! 11 \<and> y !! 10 \<and> \<not> mask 4 !! 10 \<and> y !! 9 \<and> \<not> mask 4 !! 9 \<longrightarrow> mask 14 !! 12 \<longrightarrow> mask 14 !! 11 \<longrightarrow> (y !! 0 \<and> \<not> mask 4 !! 0) = (y !! 0 \<longrightarrow> mask 4 !! 0 \<or> \<not> mask 14 !! 2) \<or> (y !! 1 \<and> \<not> mask 4 !! 1) = (y !! 1 \<longrightarrow> mask 4 !! 1 \<or> \<not> mask 14 !! 3) \<or> (y !! 2 \<and> \<not> mask 4 !! 2) = (y !! 2 \<longrightarrow> mask 4 !! 2 \<or> \<not> mask 14 !! 4) \<or> (y !! 3 \<and> \<not> mask 4 !! 3) = (y !! 3 \<longrightarrow> mask 4 !! 3 \<or> \<not> mask 14 !! 5) \<or> (y !! 4 \<and> \<not> mask 4 !! 4) = (y !! 4 \<longrightarrow> mask 4 !! 4 \<or> \<not> mask 14 !! 6) \<or> (y !! 5 \<and> \<not> mask 4 !! 5) = (y !! 5 \<longrightarrow> mask 4 !! 5 \<or> \<not> mask 14 !! 7) \<or> (y !! 6 \<and> \<not> mask 4 !! 6) = (y !! 6 \<longrightarrow> mask 4 !! 6 \<or> \<not> mask 14 !! 8) \<or> (y !! 7 \<and> \<not> mask 4 !! 7) = (y !! 7 \<longrightarrow> mask 4 !! 7 \<or> \<not> mask 14 !! 9) \<or> (y !! 8 \<and> \<not> mask 4 !! 8) = (y !! 8 \<longrightarrow> mask 4 !! 8 \<or> \<not> mask 14 !! 10) \<or> \<not> mask 14 !! 13; ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p 14; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; y !! 11 \<and> \<not> mask 4 !! 11 \<and> y !! 10 \<and> \<not> mask 4 !! 10 \<and> y !! 9 \<and> \<not> mask 4 !! 9\<rbrakk> \<Longrightarrow> y !! 11 \<and> \<not> mask 4 !! 11 \<and> y !! 10 \<and> \<not> mask 4 !! 10 \<and> y !! 9 \<and> \<not> mask 4 !! 9
 2. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal (1 subgoal):
 1. \<And>s pd pd'. \<lbrakk>ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s; ako_at (PageDirectory pd') p s; is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal (1 subgoal):
 1. \<And>s pd pd'. \<lbrakk>kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pd)); kheap s p = Some (ArchObj (PageDirectory pd')); is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal (2 subgoals):
 1. \<And>s pd pd'. \<lbrakk>is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> is_aligned p pd_bits
 2. \<And>s pd pd'. \<lbrakk>kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pd)); kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd')); is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal (1 subgoal):
 1. \<And>s pd pd'. \<lbrakk>kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pd)); kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd')); is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal (1 subgoal):
 1. \<And>s pd pd'. \<lbrakk>is_aligned p pd_bits; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_arch_state s; pspace_aligned s; valid_entries pde_range pd \<and> entries_align pde_range_sz pd; valid_entries pde_range pd' \<and> entries_align pde_range_sz pd'\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) ((x << 2) && mask pd_bits >> 2)) ` {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} then pd y else pd' y) proof (prove)
goal:
No subgoals!