theory ArchVSpaceEntries_AI

lemma mapM_x_store_pde_valid_pdpt_objs:
  "\<lbrace>valid_pdpt_objs and K (is_aligned p 6)\<rbrace>
     mapM_x (\<lambda>x. store_pde (x + p) InvalidPDE) [0, 4 .e. 0x3C]
   \<lbrace>\<lambda>_. valid_pdpt_objs\<rbrace>" apply (rule hoare_gen_asm)+ apply (rule hoare_pre, rule_tac p="p && ~~ mask pd_bits" in mapM_x_store_pde_updates) apply clarsimp apply (rule mask_out_first_mask_some[where n=6]) apply (drule_tac d=x in is_aligned_add_helper) apply (drule subsetD[OF upto_enum_step_subset]) apply simp apply (erule order_le_less_trans, simp) apply (simp add: field_simps) apply (simp add: pd_bits_def pageBits_def) apply (clarsimp simp: ranI elim!: ranE split: if_split_asm) apply (simp add: shift_0x3C_set pd_bits_def pageBits_def) apply (rule conjI) apply (rule_tac valid_entries_overwrite_groups
    [where S = "{x. x && ~~ mask 4 = ucast (p && mask 14 >> 2)}"]) apply (fastforce simp add: obj_at_def ran_def) apply fastforce apply clarsimp apply (case_tac v, simp_all split:if_splits) apply clarsimp apply (case_tac v, simp_all split:if_splits) apply (intro conjI impI allI) apply (rule disjointI) apply clarsimp apply (rule entries_align_pde_update) apply (clarsimp simp:obj_at_def) apply (drule valid_pdpt_objs_pdD) apply (simp add:pd_bits_def pageBits_def) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and K (is_aligned p 6)\<rbrace> mapM_x (\<lambda>x. store_pde (x + p) InvalidPDE) [0 , 4 .e. 0x3C] \<lbrace>\<lambda>_ s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (1 subgoal):
 1. is_aligned p 6 \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> mapM_x (\<lambda>x. store_pde (x + p) InvalidPDE) [0 , 4 .e. 0x3C] \<lbrace>\<lambda>_ s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (2 subgoals):
 1. is_aligned p 6 \<Longrightarrow> \<forall>x\<in>set [0 , 4 .e. 0x3C]. x + p && ~~ mask pd_bits = p && ~~ mask pd_bits
 2. \<And>s. \<lbrakk>is_aligned p 6; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrakk> \<Longrightarrow> (\<not> typ_at (AArch APageDirectory) (p && ~~ mask pd_bits) s \<longrightarrow> (\<forall>x\<in>ran (kheap s). obj_valid_pdpt x)) \<and> (\<forall>pd. ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s \<longrightarrow> (\<forall>x\<in>ran (kheap (s\<lparr>kheap := (kheap s)(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (x + p && mask pd_bits >> 2)) ` set [0 , 4 .e. 0x3C] then InvalidPDE else pd y)))\<rparr>)). obj_valid_pdpt x)) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>is_aligned p 6; x \<in> set [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> x + p && ~~ mask pd_bits = p && ~~ mask pd_bits
 2. \<And>s. \<lbrakk>is_aligned p 6; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrakk> \<Longrightarrow> (\<not> typ_at (AArch APageDirectory) (p && ~~ mask pd_bits) s \<longrightarrow> (\<forall>x\<in>ran (kheap s). obj_valid_pdpt x)) \<and> (\<forall>pd. ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s \<longrightarrow> (\<forall>x\<in>ran (kheap (s\<lparr>kheap := (kheap s)(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (x + p && mask pd_bits >> 2)) ` set [0 , 4 .e. 0x3C] then InvalidPDE else pd y)))\<rparr>)). obj_valid_pdpt x)) proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>is_aligned p 6; x \<in> set [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> x + p && ~~ mask 6 = p
 2. \<And>x. \<lbrakk>is_aligned p 6; x \<in> set [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> 6 \<le> pd_bits
 3. \<And>s. \<lbrakk>is_aligned p 6; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrakk> \<Longrightarrow> (\<not> typ_at (AArch APageDirectory) (p && ~~ mask pd_bits) s \<longrightarrow> (\<forall>x\<in>ran (kheap s). obj_valid_pdpt x)) \<and> (\<forall>pd. ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s \<longrightarrow> (\<forall>x\<in>ran (kheap (s\<lparr>kheap := (kheap s)(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (x + p && mask pd_bits >> 2)) ` set [0 , 4 .e. 0x3C] then InvalidPDE else pd y)))\<rparr>)). obj_valid_pdpt x)) proof (prove)
goal (4 subgoals):
 1. \<And>x. x \<in> set [0 , 4 .e. 0x3C] \<Longrightarrow> x < 2 ^ 6
 2. \<And>x. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; p + x && mask 6 = x \<and> p + x && ~~ mask 6 = p\<rbrakk> \<Longrightarrow> x + p && ~~ mask 6 = p
 3. \<And>x. \<lbrakk>is_aligned p 6; x \<in> set [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> 6 \<le> pd_bits
 4. \<And>s. \<lbrakk>is_aligned p 6; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrakk> \<Longrightarrow> (\<not> typ_at (AArch APageDirectory) (p && ~~ mask pd_bits) s \<longrightarrow> (\<forall>x\<in>ran (kheap s). obj_valid_pdpt x)) \<and> (\<forall>pd. ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s \<longrightarrow> (\<forall>x\<in>ran (kheap (s\<lparr>kheap := (kheap s)(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (x + p && mask pd_bits >> 2)) ` set [0 , 4 .e. 0x3C] then InvalidPDE else pd y)))\<rparr>)). obj_valid_pdpt x)) proof (prove)
goal (4 subgoals):
 1. \<And>x. x \<in> {0..0x3C} \<Longrightarrow> x < 2 ^ 6
 2. \<And>x. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; p + x && mask 6 = x \<and> p + x && ~~ mask 6 = p\<rbrakk> \<Longrightarrow> x + p && ~~ mask 6 = p
 3. \<And>x. \<lbrakk>is_aligned p 6; x \<in> set [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> 6 \<le> pd_bits
 4. \<And>s. \<lbrakk>is_aligned p 6; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrakk> \<Longrightarrow> (\<not> typ_at (AArch APageDirectory) (p && ~~ mask pd_bits) s \<longrightarrow> (\<forall>x\<in>ran (kheap s). obj_valid_pdpt x)) \<and> (\<forall>pd. ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s \<longrightarrow> (\<forall>x\<in>ran (kheap (s\<lparr>kheap := (kheap s)(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (x + p && mask pd_bits >> 2)) ` set [0 , 4 .e. 0x3C] then InvalidPDE else pd y)))\<rparr>)). obj_valid_pdpt x)) proof (prove)
goal (4 subgoals):
 1. \<And>x. x \<le> 0x3C \<Longrightarrow> x < 0x40
 2. \<And>x. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; p + x && mask 6 = x \<and> p + x && ~~ mask 6 = p\<rbrakk> \<Longrightarrow> x + p && ~~ mask 6 = p
 3. \<And>x. \<lbrakk>is_aligned p 6; x \<in> set [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> 6 \<le> pd_bits
 4. \<And>s. \<lbrakk>is_aligned p 6; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrakk> \<Longrightarrow> (\<not> typ_at (AArch APageDirectory) (p && ~~ mask pd_bits) s \<longrightarrow> (\<forall>x\<in>ran (kheap s). obj_valid_pdpt x)) \<and> (\<forall>pd. ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s \<longrightarrow> (\<forall>x\<in>ran (kheap (s\<lparr>kheap := (kheap s)(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (x + p && mask pd_bits >> 2)) ` set [0 , 4 .e. 0x3C] then InvalidPDE else pd y)))\<rparr>)). obj_valid_pdpt x)) proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; p + x && mask 6 = x \<and> p + x && ~~ mask 6 = p\<rbrakk> \<Longrightarrow> x + p && ~~ mask 6 = p
 2. \<And>x. \<lbrakk>is_aligned p 6; x \<in> set [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> 6 \<le> pd_bits
 3. \<And>s. \<lbrakk>is_aligned p 6; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrakk> \<Longrightarrow> (\<not> typ_at (AArch APageDirectory) (p && ~~ mask pd_bits) s \<longrightarrow> (\<forall>x\<in>ran (kheap s). obj_valid_pdpt x)) \<and> (\<forall>pd. ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s \<longrightarrow> (\<forall>x\<in>ran (kheap (s\<lparr>kheap := (kheap s)(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (x + p && mask pd_bits >> 2)) ` set [0 , 4 .e. 0x3C] then InvalidPDE else pd y)))\<rparr>)). obj_valid_pdpt x)) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>is_aligned p 6; x \<in> set [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> 6 \<le> pd_bits
 2. \<And>s. \<lbrakk>is_aligned p 6; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrakk> \<Longrightarrow> (\<not> typ_at (AArch APageDirectory) (p && ~~ mask pd_bits) s \<longrightarrow> (\<forall>x\<in>ran (kheap s). obj_valid_pdpt x)) \<and> (\<forall>pd. ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s \<longrightarrow> (\<forall>x\<in>ran (kheap (s\<lparr>kheap := (kheap s)(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (x + p && mask pd_bits >> 2)) ` set [0 , 4 .e. 0x3C] then InvalidPDE else pd y)))\<rparr>)). obj_valid_pdpt x)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_aligned p 6; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrakk> \<Longrightarrow> (\<not> typ_at (AArch APageDirectory) (p && ~~ mask pd_bits) s \<longrightarrow> (\<forall>x\<in>ran (kheap s). obj_valid_pdpt x)) \<and> (\<forall>pd. ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s \<longrightarrow> (\<forall>x\<in>ran (kheap (s\<lparr>kheap := (kheap s)(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (x + p && mask pd_bits >> 2)) ` set [0 , 4 .e. 0x3C] then InvalidPDE else pd y)))\<rparr>)). obj_valid_pdpt x)) proof (prove)
goal (1 subgoal):
 1. \<And>s pd. \<lbrakk>is_aligned p 6; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s\<rbrakk> \<Longrightarrow> valid_entries pde_range (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (x + p && mask pd_bits >> 2)) ` set [0 , 4 .e. 0x3C] then InvalidPDE else pd y) \<and> entries_align pde_range_sz (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (x + p && mask pd_bits >> 2)) ` set [0 , 4 .e. 0x3C] then InvalidPDE else pd y) proof (prove)
goal (1 subgoal):
 1. \<And>s pd. \<lbrakk>is_aligned p 6; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; ako_at (PageDirectory pd) (p && ~~ mask 14) s\<rbrakk> \<Longrightarrow> valid_entries pde_range (\<lambda>y. if y && ~~ mask 4 = UCAST(32 \<rightarrow> 12) (p && mask 14 >> 2) then InvalidPDE else pd y) \<and> entries_align pde_range_sz (\<lambda>y. if y && ~~ mask 4 = UCAST(32 \<rightarrow> 12) (p && mask 14 >> 2) then InvalidPDE else pd y) proof (prove)
goal (2 subgoals):
 1. \<And>s pd. \<lbrakk>is_aligned p 6; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; ako_at (PageDirectory pd) (p && ~~ mask 14) s\<rbrakk> \<Longrightarrow> valid_entries pde_range (\<lambda>y. if y && ~~ mask 4 = UCAST(32 \<rightarrow> 12) (p && mask 14 >> 2) then InvalidPDE else pd y)
 2. \<And>s pd. \<lbrakk>is_aligned p 6; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; ako_at (PageDirectory pd) (p && ~~ mask 14) s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y && ~~ mask 4 = UCAST(32 \<rightarrow> 12) (p && mask 14 >> 2) then InvalidPDE else pd y) proof (prove)
goal (5 subgoals):
 1. \<And>s pd. \<lbrakk>is_aligned p 6; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; ako_at (PageDirectory pd) (p && ~~ mask 14) s\<rbrakk> \<Longrightarrow> valid_entries pde_range pd
 2. \<And>s pd. \<lbrakk>is_aligned p 6; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; ako_at (PageDirectory pd) (p && ~~ mask 14) s\<rbrakk> \<Longrightarrow> valid_entries pde_range (\<lambda>_. InvalidPDE)
 3. \<And>s pd. \<lbrakk>is_aligned p 6; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; ako_at (PageDirectory pd) (p && ~~ mask 14) s\<rbrakk> \<Longrightarrow> \<forall>v y. y && ~~ mask 4 = UCAST(32 \<rightarrow> 12) (p && mask 14 >> 2) \<longrightarrow> pde_range v y \<subseteq> {y. y && ~~ mask 4 = UCAST(32 \<rightarrow> 12) (p && mask 14 >> 2)}
 4. \<And>s pd. \<lbrakk>is_aligned p 6; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; ako_at (PageDirectory pd) (p && ~~ mask 14) s\<rbrakk> \<Longrightarrow> \<forall>v y. y && ~~ mask 4 \<noteq> UCAST(32 \<rightarrow> 12) (p && mask 14 >> 2) \<longrightarrow> pde_range v y \<inter> {y. y && ~~ mask 4 = UCAST(32 \<rightarrow> 12) (p && mask 14 >> 2)} = {}
 5. \<And>s pd. \<lbrakk>is_aligned p 6; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; ako_at (PageDirectory pd) (p && ~~ mask 14) s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y && ~~ mask 4 = UCAST(32 \<rightarrow> 12) (p && mask 14 >> 2) then InvalidPDE else pd y) proof (prove)
goal (4 subgoals):
 1. \<And>s pd. \<lbrakk>is_aligned p 6; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; ako_at (PageDirectory pd) (p && ~~ mask 14) s\<rbrakk> \<Longrightarrow> valid_entries pde_range (\<lambda>_. InvalidPDE)
 2. \<And>s pd. \<lbrakk>is_aligned p 6; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; ako_at (PageDirectory pd) (p && ~~ mask 14) s\<rbrakk> \<Longrightarrow> \<forall>v y. y && ~~ mask 4 = UCAST(32 \<rightarrow> 12) (p && mask 14 >> 2) \<longrightarrow> pde_range v y \<subseteq> {y. y && ~~ mask 4 = UCAST(32 \<rightarrow> 12) (p && mask 14 >> 2)}
 3. \<And>s pd. \<lbrakk>is_aligned p 6; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; ako_at (PageDirectory pd) (p && ~~ mask 14) s\<rbrakk> \<Longrightarrow> \<forall>v y. y && ~~ mask 4 \<noteq> UCAST(32 \<rightarrow> 12) (p && mask 14 >> 2) \<longrightarrow> pde_range v y \<inter> {y. y && ~~ mask 4 = UCAST(32 \<rightarrow> 12) (p && mask 14 >> 2)} = {}
 4. \<And>s pd. \<lbrakk>is_aligned p 6; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; ako_at (PageDirectory pd) (p && ~~ mask 14) s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y && ~~ mask 4 = UCAST(32 \<rightarrow> 12) (p && mask 14 >> 2) then InvalidPDE else pd y) proof (prove)
goal (3 subgoals):
 1. \<And>s pd. \<lbrakk>is_aligned p 6; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; ako_at (PageDirectory pd) (p && ~~ mask 14) s\<rbrakk> \<Longrightarrow> \<forall>v y. y && ~~ mask 4 = UCAST(32 \<rightarrow> 12) (p && mask 14 >> 2) \<longrightarrow> pde_range v y \<subseteq> {y. y && ~~ mask 4 = UCAST(32 \<rightarrow> 12) (p && mask 14 >> 2)}
 2. \<And>s pd. \<lbrakk>is_aligned p 6; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; ako_at (PageDirectory pd) (p && ~~ mask 14) s\<rbrakk> \<Longrightarrow> \<forall>v y. y && ~~ mask 4 \<noteq> UCAST(32 \<rightarrow> 12) (p && mask 14 >> 2) \<longrightarrow> pde_range v y \<inter> {y. y && ~~ mask 4 = UCAST(32 \<rightarrow> 12) (p && mask 14 >> 2)} = {}
 3. \<And>s pd. \<lbrakk>is_aligned p 6; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; ako_at (PageDirectory pd) (p && ~~ mask 14) s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y && ~~ mask 4 = UCAST(32 \<rightarrow> 12) (p && mask 14 >> 2) then InvalidPDE else pd y) proof (prove)
goal (3 subgoals):
 1. \<And>s pd v y x. \<lbrakk>is_aligned p 6; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; ako_at (PageDirectory pd) (p && ~~ mask 14) s; y && ~~ mask 4 = UCAST(32 \<rightarrow> 12) (p && mask 14 >> 2); x \<in> pde_range v y\<rbrakk> \<Longrightarrow> x && ~~ mask 4 = UCAST(32 \<rightarrow> 12) (p && mask 14 >> 2)
 2. \<And>s pd. \<lbrakk>is_aligned p 6; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; ako_at (PageDirectory pd) (p && ~~ mask 14) s\<rbrakk> \<Longrightarrow> \<forall>v y. y && ~~ mask 4 \<noteq> UCAST(32 \<rightarrow> 12) (p && mask 14 >> 2) \<longrightarrow> pde_range v y \<inter> {y. y && ~~ mask 4 = UCAST(32 \<rightarrow> 12) (p && mask 14 >> 2)} = {}
 3. \<And>s pd. \<lbrakk>is_aligned p 6; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; ako_at (PageDirectory pd) (p && ~~ mask 14) s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y && ~~ mask 4 = UCAST(32 \<rightarrow> 12) (p && mask 14 >> 2) then InvalidPDE else pd y) proof (prove)
goal (2 subgoals):
 1. \<And>s pd. \<lbrakk>is_aligned p 6; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; ako_at (PageDirectory pd) (p && ~~ mask 14) s\<rbrakk> \<Longrightarrow> \<forall>v y. y && ~~ mask 4 \<noteq> UCAST(32 \<rightarrow> 12) (p && mask 14 >> 2) \<longrightarrow> pde_range v y \<inter> {y. y && ~~ mask 4 = UCAST(32 \<rightarrow> 12) (p && mask 14 >> 2)} = {}
 2. \<And>s pd. \<lbrakk>is_aligned p 6; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; ako_at (PageDirectory pd) (p && ~~ mask 14) s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y && ~~ mask 4 = UCAST(32 \<rightarrow> 12) (p && mask 14 >> 2) then InvalidPDE else pd y) proof (prove)
goal (2 subgoals):
 1. \<And>s pd v y. \<lbrakk>is_aligned p 6; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; ako_at (PageDirectory pd) (p && ~~ mask 14) s; y && ~~ mask 4 \<noteq> UCAST(32 \<rightarrow> 12) (p && mask 14 >> 2)\<rbrakk> \<Longrightarrow> pde_range v y \<inter> {y. y && ~~ mask 4 = UCAST(32 \<rightarrow> 12) (p && mask 14 >> 2)} = {}
 2. \<And>s pd. \<lbrakk>is_aligned p 6; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; ako_at (PageDirectory pd) (p && ~~ mask 14) s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y && ~~ mask 4 = UCAST(32 \<rightarrow> 12) (p && mask 14 >> 2) then InvalidPDE else pd y) proof (prove)
goal (2 subgoals):
 1. \<And>s pd v y x41 x42 x43. \<lbrakk>is_aligned p 6; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; ako_at (PageDirectory pd) (p && ~~ mask 14) s; y && ~~ mask 4 \<noteq> UCAST(32 \<rightarrow> 12) (p && mask 14 >> 2); v = SuperSectionPDE x41 x42 x43\<rbrakk> \<Longrightarrow> is_aligned y 4 \<longrightarrow> {x. x && ~~ mask 4 = y} \<inter> {y. y && ~~ mask 4 = UCAST(32 \<rightarrow> 12) (p && mask 14 >> 2)} = {}
 2. \<And>s pd. \<lbrakk>is_aligned p 6; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; ako_at (PageDirectory pd) (p && ~~ mask 14) s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y && ~~ mask 4 = UCAST(32 \<rightarrow> 12) (p && mask 14 >> 2) then InvalidPDE else pd y) proof (prove)
goal (2 subgoals):
 1. \<And>s pd v y x41 x42 x43. \<lbrakk>is_aligned p 6; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; ako_at (PageDirectory pd) (p && ~~ mask 14) s; y && ~~ mask 4 \<noteq> UCAST(32 \<rightarrow> 12) (p && mask 14 >> 2); v = SuperSectionPDE x41 x42 x43; is_aligned y 4\<rbrakk> \<Longrightarrow> {x. x && ~~ mask 4 = y} \<inter> {y. y && ~~ mask 4 = UCAST(32 \<rightarrow> 12) (p && mask 14 >> 2)} = {}
 2. \<And>s pd. \<lbrakk>is_aligned p 6; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; ako_at (PageDirectory pd) (p && ~~ mask 14) s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y && ~~ mask 4 = UCAST(32 \<rightarrow> 12) (p && mask 14 >> 2) then InvalidPDE else pd y) proof (prove)
goal (2 subgoals):
 1. \<And>s pd v y x41 x42 x43 x ya. \<lbrakk>is_aligned p 6; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; ako_at (PageDirectory pd) (p && ~~ mask 14) s; y && ~~ mask 4 \<noteq> UCAST(32 \<rightarrow> 12) (p && mask 14 >> 2); v = SuperSectionPDE x41 x42 x43; is_aligned y 4; x \<in> {x. x && ~~ mask 4 = y}; ya \<in> {y. y && ~~ mask 4 = UCAST(32 \<rightarrow> 12) (p && mask 14 >> 2)}\<rbrakk> \<Longrightarrow> x \<noteq> ya
 2. \<And>s pd. \<lbrakk>is_aligned p 6; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; ako_at (PageDirectory pd) (p && ~~ mask 14) s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y && ~~ mask 4 = UCAST(32 \<rightarrow> 12) (p && mask 14 >> 2) then InvalidPDE else pd y) proof (prove)
goal (1 subgoal):
 1. \<And>s pd. \<lbrakk>is_aligned p 6; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; ako_at (PageDirectory pd) (p && ~~ mask 14) s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if y && ~~ mask 4 = UCAST(32 \<rightarrow> 12) (p && mask 14 >> 2) then InvalidPDE else pd y) proof (prove)
goal (2 subgoals):
 1. \<And>s pd. \<lbrakk>is_aligned p 6; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; ako_at (PageDirectory pd) (p && ~~ mask 14) s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz pd
 2. \<And>s pd. \<lbrakk>is_aligned p 6; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; ako_at (PageDirectory pd) (p && ~~ mask 14) s\<rbrakk> \<Longrightarrow> \<forall>y. y && ~~ mask 4 = UCAST(32 \<rightarrow> 12) (p && mask 14 >> 2) \<longrightarrow> is_aligned y (pde_range_sz InvalidPDE) proof (prove)
goal (2 subgoals):
 1. \<And>s pd. \<lbrakk>is_aligned p 6; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; kheap s (p && ~~ mask 14) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> entries_align pde_range_sz pd
 2. \<And>s pd. \<lbrakk>is_aligned p 6; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; ako_at (PageDirectory pd) (p && ~~ mask 14) s\<rbrakk> \<Longrightarrow> \<forall>y. y && ~~ mask 4 = UCAST(32 \<rightarrow> 12) (p && mask 14 >> 2) \<longrightarrow> is_aligned y (pde_range_sz InvalidPDE) proof (prove)
goal (3 subgoals):
 1. \<And>s pd. \<lbrakk>is_aligned p 6; kheap s (p && ~~ mask 14) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> kheap s (?ptr87 s pd) = Some (ArchObj (PageDirectory (?pd87 s pd)))
 2. \<And>s pd. \<lbrakk>is_aligned p 6; kheap s (p && ~~ mask 14) = Some (ArchObj (PageDirectory pd)); valid_entries pde_range (?pd87 s pd) \<and> entries_align pde_range_sz (?pd87 s pd)\<rbrakk> \<Longrightarrow> entries_align pde_range_sz pd
 3. \<And>s pd. \<lbrakk>is_aligned p 6; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; ako_at (PageDirectory pd) (p && ~~ mask 14) s\<rbrakk> \<Longrightarrow> \<forall>y. y && ~~ mask 4 = UCAST(32 \<rightarrow> 12) (p && mask 14 >> 2) \<longrightarrow> is_aligned y (pde_range_sz InvalidPDE) proof (prove)
goal (2 subgoals):
 1. \<And>s pd. \<lbrakk>is_aligned p 6; kheap s (p && ~~ mask 14) = Some (ArchObj (PageDirectory pd)); valid_entries pde_range pd \<and> entries_align pde_range_sz pd\<rbrakk> \<Longrightarrow> entries_align pde_range_sz pd
 2. \<And>s pd. \<lbrakk>is_aligned p 6; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; ako_at (PageDirectory pd) (p && ~~ mask 14) s\<rbrakk> \<Longrightarrow> \<forall>y. y && ~~ mask 4 = UCAST(32 \<rightarrow> 12) (p && mask 14 >> 2) \<longrightarrow> is_aligned y (pde_range_sz InvalidPDE) proof (prove)
goal (1 subgoal):
 1. \<And>s pd. \<lbrakk>is_aligned p 6; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; ako_at (PageDirectory pd) (p && ~~ mask 14) s\<rbrakk> \<Longrightarrow> \<forall>y. y && ~~ mask 4 = UCAST(32 \<rightarrow> 12) (p && mask 14 >> 2) \<longrightarrow> is_aligned y (pde_range_sz InvalidPDE) proof (prove)
goal:
No subgoals!