theory Finalise_DR

lemma remain_pd_super_section_relation:
  "\<lbrakk>is_aligned ptr 2; is_aligned y 2; ptr \<noteq> y\<rbrakk>
   \<Longrightarrow> \<lbrace>\<lambda>s. pd_super_section_relation ( y && ~~ mask pd_bits) sid y s\<rbrace> store_pde ptr sp
       \<lbrace>\<lambda>r s. pd_super_section_relation (y && ~~ mask pd_bits) sid y s\<rbrace>" apply (simp add: store_pde_def) apply wp apply (rule_tac Q = "ko_at (ArchObj (arch_kernel_obj.PageDirectory x)) (ptr && ~~ mask pd_bits)
               and pd_super_section_relation (y && ~~ mask pd_bits) sid y " in hoare_vcg_precond_imp) apply (clarsimp simp: set_pd_def) apply (rule_tac Q = "ko_at (ArchObj (arch_kernel_obj.PageDirectory x)) (ptr && ~~ mask pd_bits)
               and pd_super_section_relation (y && ~~ mask pd_bits) sid y " in hoare_vcg_precond_imp) apply (clarsimp simp: valid_def set_object_def get_object_def in_monad) apply (clarsimp simp: pd_super_section_relation_def dest!: ucast_inj_mask | rule conjI)+ apply (drule mask_compare_imply) apply (simp add: word_size pd_bits_def pt_bits_def pageBits_def is_aligned_mask)+ apply (clarsimp simp: pt_page_relation_def obj_at_def) apply (assumption) apply (simp add: get_object_def) apply wp apply (clarsimp simp: obj_at_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 2; is_aligned y 2; ptr \<noteq> y\<rbrakk> \<Longrightarrow> \<lbrace>pd_super_section_relation (y && ~~ mask pd_bits) sid y\<rbrace> store_pde ptr sp \<lbrace>\<lambda>r. pd_super_section_relation (y && ~~ mask pd_bits) sid y\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 2; is_aligned y 2; ptr \<noteq> y\<rbrakk> \<Longrightarrow> \<lbrace>pd_super_section_relation (y && ~~ mask pd_bits) sid y\<rbrace> do pd <- get_pd (ptr && ~~ mask pd_bits);
set_pd (ptr && ~~ mask pd_bits) (pd(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := sp))
od \<lbrace>\<lambda>r. pd_super_section_relation (y && ~~ mask pd_bits) sid y\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>is_aligned ptr 2; is_aligned y 2; ptr \<noteq> y\<rbrakk> \<Longrightarrow> \<lbrace>?B1 x\<rbrace> set_pd (ptr && ~~ mask pd_bits) (x(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := sp)) \<lbrace>\<lambda>r. pd_super_section_relation (y && ~~ mask pd_bits) sid y\<rbrace>
 2. \<lbrakk>is_aligned ptr 2; is_aligned y 2; ptr \<noteq> y\<rbrakk> \<Longrightarrow> \<lbrace>?Q\<rbrace> get_pd (ptr && ~~ mask pd_bits) \<lbrace>?B1\<rbrace>
 3. \<And>s. \<lbrakk>is_aligned ptr 2; is_aligned y 2; ptr \<noteq> y; pd_super_section_relation (y && ~~ mask pd_bits) sid y s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>is_aligned ptr 2; is_aligned y 2; ptr \<noteq> y\<rbrakk> \<Longrightarrow> \<lbrace>ako_at (arch_kernel_obj.PageDirectory x) (ptr && ~~ mask pd_bits) and pd_super_section_relation (y && ~~ mask pd_bits) sid y\<rbrace> set_pd (ptr && ~~ mask pd_bits) (x(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := sp)) \<lbrace>\<lambda>r. pd_super_section_relation (y && ~~ mask pd_bits) sid y\<rbrace>
 2. \<And>x s. \<lbrakk>is_aligned ptr 2; is_aligned y 2; ptr \<noteq> y; ?B1 x s\<rbrakk> \<Longrightarrow> (ako_at (arch_kernel_obj.PageDirectory x) (ptr && ~~ mask pd_bits) and pd_super_section_relation (y && ~~ mask pd_bits) sid y) s
 3. \<lbrakk>is_aligned ptr 2; is_aligned y 2; ptr \<noteq> y\<rbrakk> \<Longrightarrow> \<lbrace>?Q\<rbrace> get_pd (ptr && ~~ mask pd_bits) \<lbrace>?B1\<rbrace>
 4. \<And>s. \<lbrakk>is_aligned ptr 2; is_aligned y 2; ptr \<noteq> y; pd_super_section_relation (y && ~~ mask pd_bits) sid y s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>is_aligned ptr 2; is_aligned y 2; ptr \<noteq> y\<rbrakk> \<Longrightarrow> \<lbrace>ako_at (arch_kernel_obj.PageDirectory x) (ptr && ~~ mask pd_bits) and pd_super_section_relation (y && ~~ mask pd_bits) sid y\<rbrace> KHeap_A.set_object (ptr && ~~ mask pd_bits) (ArchObj (arch_kernel_obj.PageDirectory (x(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := sp)))) \<lbrace>\<lambda>r. pd_super_section_relation (y && ~~ mask pd_bits) sid y\<rbrace>
 2. \<And>x s. \<lbrakk>is_aligned ptr 2; is_aligned y 2; ptr \<noteq> y; ?B1 x s\<rbrakk> \<Longrightarrow> (ako_at (arch_kernel_obj.PageDirectory x) (ptr && ~~ mask pd_bits) and pd_super_section_relation (y && ~~ mask pd_bits) sid y) s
 3. \<lbrakk>is_aligned ptr 2; is_aligned y 2; ptr \<noteq> y\<rbrakk> \<Longrightarrow> \<lbrace>?Q\<rbrace> get_pd (ptr && ~~ mask pd_bits) \<lbrace>?B1\<rbrace>
 4. \<And>s. \<lbrakk>is_aligned ptr 2; is_aligned y 2; ptr \<noteq> y; pd_super_section_relation (y && ~~ mask pd_bits) sid y s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>x. \<lbrakk>is_aligned ptr 2; is_aligned y 2; ptr \<noteq> y\<rbrakk> \<Longrightarrow> \<lbrace>ako_at (arch_kernel_obj.PageDirectory x) (ptr && ~~ mask pd_bits) and pd_super_section_relation (y && ~~ mask pd_bits) sid y\<rbrace> KHeap_A.set_object (ptr && ~~ mask pd_bits) (ArchObj (arch_kernel_obj.PageDirectory (x(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := sp)))) \<lbrace>\<lambda>r. pd_super_section_relation (y && ~~ mask pd_bits) sid y\<rbrace>
 2. \<And>x s. \<lbrakk>is_aligned ptr 2; is_aligned y 2; ptr \<noteq> y; (ako_at (arch_kernel_obj.PageDirectory x) (ptr && ~~ mask pd_bits) and pd_super_section_relation (y && ~~ mask pd_bits) sid y) s\<rbrakk> \<Longrightarrow> (ako_at (arch_kernel_obj.PageDirectory x) (ptr && ~~ mask pd_bits) and pd_super_section_relation (y && ~~ mask pd_bits) sid y) s
 3. \<And>x s. \<lbrakk>is_aligned ptr 2; is_aligned y 2; ptr \<noteq> y; ?B1 x s\<rbrakk> \<Longrightarrow> (ako_at (arch_kernel_obj.PageDirectory x) (ptr && ~~ mask pd_bits) and pd_super_section_relation (y && ~~ mask pd_bits) sid y) s
 4. \<lbrakk>is_aligned ptr 2; is_aligned y 2; ptr \<noteq> y\<rbrakk> \<Longrightarrow> \<lbrace>?Q\<rbrace> get_pd (ptr && ~~ mask pd_bits) \<lbrace>?B1\<rbrace>
 5. \<And>s. \<lbrakk>is_aligned ptr 2; is_aligned y 2; ptr \<noteq> y; pd_super_section_relation (y && ~~ mask pd_bits) sid y s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>x s ya. \<lbrakk>is_aligned ptr 2; is_aligned y 2; ptr \<noteq> y; ako_at (arch_kernel_obj.PageDirectory x) (ptr && ~~ mask pd_bits) s; pd_super_section_relation (y && ~~ mask pd_bits) sid y s; a_type ya = a_type (ArchObj (arch_kernel_obj.PageDirectory (x(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := sp)))); kheap s (ptr && ~~ mask pd_bits) = Some ya\<rbrakk> \<Longrightarrow> pd_super_section_relation (y && ~~ mask pd_bits) sid y (update_kheap ((kheap s)(ptr && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (x(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := sp))))) s)
 2. \<And>x s. \<lbrakk>is_aligned ptr 2; is_aligned y 2; ptr \<noteq> y; (ako_at (arch_kernel_obj.PageDirectory x) (ptr && ~~ mask pd_bits) and pd_super_section_relation (y && ~~ mask pd_bits) sid y) s\<rbrakk> \<Longrightarrow> (ako_at (arch_kernel_obj.PageDirectory x) (ptr && ~~ mask pd_bits) and pd_super_section_relation (y && ~~ mask pd_bits) sid y) s
 3. \<And>x s. \<lbrakk>is_aligned ptr 2; is_aligned y 2; ptr \<noteq> y; ?B1 x s\<rbrakk> \<Longrightarrow> (ako_at (arch_kernel_obj.PageDirectory x) (ptr && ~~ mask pd_bits) and pd_super_section_relation (y && ~~ mask pd_bits) sid y) s
 4. \<lbrakk>is_aligned ptr 2; is_aligned y 2; ptr \<noteq> y\<rbrakk> \<Longrightarrow> \<lbrace>?Q\<rbrace> get_pd (ptr && ~~ mask pd_bits) \<lbrace>?B1\<rbrace>
 5. \<And>s. \<lbrakk>is_aligned ptr 2; is_aligned y 2; ptr \<noteq> y; pd_super_section_relation (y && ~~ mask pd_bits) sid y s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>x s fun u v ref1. \<lbrakk>is_aligned ptr 2; is_aligned y 2; ptr \<noteq> y; ako_at (arch_kernel_obj.PageDirectory x) (ptr && ~~ mask pd_bits) s; a_type (ArchObj (arch_kernel_obj.PageDirectory fun)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := sp)))); kheap s (ptr && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory fun)); fun (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2)) = SuperSectionPDE ref1 u v; sid = ptrFromPAddr ref1; (y && mask pd_bits >> 2) && mask 12 = (ptr && mask pd_bits >> 2) && mask 12; y && ~~ mask pd_bits = ptr && ~~ mask pd_bits\<rbrakk> \<Longrightarrow> \<exists>u v ref1a. sp = SuperSectionPDE ref1a u v \<and> ptrFromPAddr ref1 = ptrFromPAddr ref1a
 2. \<And>x s ya fun u v ref1. \<lbrakk>is_aligned ptr 2; is_aligned y 2; ptr \<noteq> y; ako_at (arch_kernel_obj.PageDirectory x) (ptr && ~~ mask pd_bits) s; a_type ya = a_type (ArchObj (arch_kernel_obj.PageDirectory (x(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := sp)))); kheap s (ptr && ~~ mask pd_bits) = Some ya; kheap s (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory fun)); fun (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2)) = SuperSectionPDE ref1 u v; sid = ptrFromPAddr ref1\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<noteq> UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<longrightarrow> y && ~~ mask pd_bits = ptr && ~~ mask pd_bits \<longrightarrow> (\<exists>u v ref1a. x (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2)) = SuperSectionPDE ref1a u v \<and> ptrFromPAddr ref1 = ptrFromPAddr ref1a)
 3. \<And>x s. \<lbrakk>is_aligned ptr 2; is_aligned y 2; ptr \<noteq> y; (ako_at (arch_kernel_obj.PageDirectory x) (ptr && ~~ mask pd_bits) and pd_super_section_relation (y && ~~ mask pd_bits) sid y) s\<rbrakk> \<Longrightarrow> (ako_at (arch_kernel_obj.PageDirectory x) (ptr && ~~ mask pd_bits) and pd_super_section_relation (y && ~~ mask pd_bits) sid y) s
 4. \<And>x s. \<lbrakk>is_aligned ptr 2; is_aligned y 2; ptr \<noteq> y; ?B1 x s\<rbrakk> \<Longrightarrow> (ako_at (arch_kernel_obj.PageDirectory x) (ptr && ~~ mask pd_bits) and pd_super_section_relation (y && ~~ mask pd_bits) sid y) s
 5. \<lbrakk>is_aligned ptr 2; is_aligned y 2; ptr \<noteq> y\<rbrakk> \<Longrightarrow> \<lbrace>?Q\<rbrace> get_pd (ptr && ~~ mask pd_bits) \<lbrace>?B1\<rbrace>
 6. \<And>s. \<lbrakk>is_aligned ptr 2; is_aligned y 2; ptr \<noteq> y; pd_super_section_relation (y && ~~ mask pd_bits) sid y s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (10 subgoals):
 1. \<And>x s fun u v ref1. \<lbrakk>is_aligned ptr 2; is_aligned y 2; ptr \<noteq> y; ako_at (arch_kernel_obj.PageDirectory x) (ptr && ~~ mask pd_bits) s; a_type (ArchObj (arch_kernel_obj.PageDirectory fun)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := sp)))); kheap s (ptr && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory fun)); fun (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2)) = SuperSectionPDE ref1 u v; sid = ptrFromPAddr ref1; y && ~~ mask pd_bits = ptr && ~~ mask pd_bits\<rbrakk> \<Longrightarrow> size y = size ptr
 2. \<And>x s fun u v ref1. \<lbrakk>is_aligned ptr 2; is_aligned y 2; ptr \<noteq> y; ako_at (arch_kernel_obj.PageDirectory x) (ptr && ~~ mask pd_bits) s; a_type (ArchObj (arch_kernel_obj.PageDirectory fun)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := sp)))); kheap s (ptr && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory fun)); fun (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2)) = SuperSectionPDE ref1 u v; sid = ptrFromPAddr ref1; y && ~~ mask pd_bits = ptr && ~~ mask pd_bits\<rbrakk> \<Longrightarrow> pd_bits \<le> size y
 3. \<And>x s fun u v ref1. \<lbrakk>is_aligned ptr 2; is_aligned y 2; ptr \<noteq> y; ako_at (arch_kernel_obj.PageDirectory x) (ptr && ~~ mask pd_bits) s; a_type (ArchObj (arch_kernel_obj.PageDirectory fun)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := sp)))); kheap s (ptr && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory fun)); fun (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2)) = SuperSectionPDE ref1 u v; sid = ptrFromPAddr ref1; y && ~~ mask pd_bits = ptr && ~~ mask pd_bits\<rbrakk> \<Longrightarrow> 2 + 12 \<le> pd_bits
 4. \<And>x s fun u v ref1. \<lbrakk>is_aligned ptr 2; is_aligned y 2; ptr \<noteq> y; ako_at (arch_kernel_obj.PageDirectory x) (ptr && ~~ mask pd_bits) s; a_type (ArchObj (arch_kernel_obj.PageDirectory fun)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := sp)))); kheap s (ptr && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory fun)); fun (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2)) = SuperSectionPDE ref1 u v; sid = ptrFromPAddr ref1; y && ~~ mask pd_bits = ptr && ~~ mask pd_bits\<rbrakk> \<Longrightarrow> y \<noteq> ptr
 5. \<And>x s fun u v ref1. \<lbrakk>is_aligned ptr 2; is_aligned y 2; ptr \<noteq> y; ako_at (arch_kernel_obj.PageDirectory x) (ptr && ~~ mask pd_bits) s; a_type (ArchObj (arch_kernel_obj.PageDirectory fun)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := sp)))); kheap s (ptr && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory fun)); fun (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2)) = SuperSectionPDE ref1 u v; sid = ptrFromPAddr ref1; y && ~~ mask pd_bits = ptr && ~~ mask pd_bits; y && mask 2 \<noteq> ptr && mask 2 \<or> y && ~~ mask (2 + 12) \<noteq> ptr && ~~ mask (2 + 12)\<rbrakk> \<Longrightarrow> \<exists>u v ref1a. sp = SuperSectionPDE ref1a u v \<and> ptrFromPAddr ref1 = ptrFromPAddr ref1a
 6. \<And>x s ya fun u v ref1. \<lbrakk>is_aligned ptr 2; is_aligned y 2; ptr \<noteq> y; ako_at (arch_kernel_obj.PageDirectory x) (ptr && ~~ mask pd_bits) s; a_type ya = a_type (ArchObj (arch_kernel_obj.PageDirectory (x(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := sp)))); kheap s (ptr && ~~ mask pd_bits) = Some ya; kheap s (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory fun)); fun (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2)) = SuperSectionPDE ref1 u v; sid = ptrFromPAddr ref1\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<noteq> UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<longrightarrow> y && ~~ mask pd_bits = ptr && ~~ mask pd_bits \<longrightarrow> (\<exists>u v ref1a. x (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2)) = SuperSectionPDE ref1a u v \<and> ptrFromPAddr ref1 = ptrFromPAddr ref1a)
 7. \<And>x s. \<lbrakk>is_aligned ptr 2; is_aligned y 2; ptr \<noteq> y; (ako_at (arch_kernel_obj.PageDirectory x) (ptr && ~~ mask pd_bits) and pd_super_section_relation (y && ~~ mask pd_bits) sid y) s\<rbrakk> \<Longrightarrow> (ako_at (arch_kernel_obj.PageDirectory x) (ptr && ~~ mask pd_bits) and pd_super_section_relation (y && ~~ mask pd_bits) sid y) s
 8. \<And>x s. \<lbrakk>is_aligned ptr 2; is_aligned y 2; ptr \<noteq> y; ?B1 x s\<rbrakk> \<Longrightarrow> (ako_at (arch_kernel_obj.PageDirectory x) (ptr && ~~ mask pd_bits) and pd_super_section_relation (y && ~~ mask pd_bits) sid y) s
 9. \<lbrakk>is_aligned ptr 2; is_aligned y 2; ptr \<noteq> y\<rbrakk> \<Longrightarrow> \<lbrace>?Q\<rbrace> get_pd (ptr && ~~ mask pd_bits) \<lbrace>?B1\<rbrace>
 10. \<And>s. \<lbrakk>is_aligned ptr 2; is_aligned y 2; ptr \<noteq> y; pd_super_section_relation (y && ~~ mask pd_bits) sid y s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>x s ya fun u v ref1. \<lbrakk>ptr && mask 2 = 0; y && mask 2 = 0; ptr \<noteq> y; ako_at (arch_kernel_obj.PageDirectory x) (ptr && ~~ mask 14) s; a_type ya = a_type (ArchObj (arch_kernel_obj.PageDirectory (x(UCAST(32 \<rightarrow> 12) (ptr && mask 14 >> 2) := sp)))); kheap s (ptr && ~~ mask 14) = Some ya; kheap s (y && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory fun)); fun (UCAST(32 \<rightarrow> 12) (y && mask 14 >> 2)) = SuperSectionPDE ref1 u v; sid = ptrFromPAddr ref1\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (y && mask 14 >> 2) \<noteq> UCAST(32 \<rightarrow> 12) (ptr && mask 14 >> 2) \<longrightarrow> y && ~~ mask 14 = ptr && ~~ mask 14 \<longrightarrow> (\<exists>u v ref1a. x (UCAST(32 \<rightarrow> 12) (y && mask 14 >> 2)) = SuperSectionPDE ref1a u v \<and> ptrFromPAddr ref1 = ptrFromPAddr ref1a)
 2. \<And>x s. \<lbrakk>is_aligned ptr 2; is_aligned y 2; ptr \<noteq> y; (ako_at (arch_kernel_obj.PageDirectory x) (ptr && ~~ mask pd_bits) and pd_super_section_relation (y && ~~ mask pd_bits) sid y) s\<rbrakk> \<Longrightarrow> (ako_at (arch_kernel_obj.PageDirectory x) (ptr && ~~ mask pd_bits) and pd_super_section_relation (y && ~~ mask pd_bits) sid y) s
 3. \<And>x s. \<lbrakk>is_aligned ptr 2; is_aligned y 2; ptr \<noteq> y; ?B1 x s\<rbrakk> \<Longrightarrow> (ako_at (arch_kernel_obj.PageDirectory x) (ptr && ~~ mask pd_bits) and pd_super_section_relation (y && ~~ mask pd_bits) sid y) s
 4. \<lbrakk>is_aligned ptr 2; is_aligned y 2; ptr \<noteq> y\<rbrakk> \<Longrightarrow> \<lbrace>?Q\<rbrace> get_pd (ptr && ~~ mask pd_bits) \<lbrace>?B1\<rbrace>
 5. \<And>s. \<lbrakk>is_aligned ptr 2; is_aligned y 2; ptr \<noteq> y; pd_super_section_relation (y && ~~ mask pd_bits) sid y s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>x s. \<lbrakk>is_aligned ptr 2; is_aligned y 2; ptr \<noteq> y; (ako_at (arch_kernel_obj.PageDirectory x) (ptr && ~~ mask pd_bits) and pd_super_section_relation (y && ~~ mask pd_bits) sid y) s\<rbrakk> \<Longrightarrow> (ako_at (arch_kernel_obj.PageDirectory x) (ptr && ~~ mask pd_bits) and pd_super_section_relation (y && ~~ mask pd_bits) sid y) s
 2. \<And>x s. \<lbrakk>is_aligned ptr 2; is_aligned y 2; ptr \<noteq> y; ?B1 x s\<rbrakk> \<Longrightarrow> (ako_at (arch_kernel_obj.PageDirectory x) (ptr && ~~ mask pd_bits) and pd_super_section_relation (y && ~~ mask pd_bits) sid y) s
 3. \<lbrakk>is_aligned ptr 2; is_aligned y 2; ptr \<noteq> y\<rbrakk> \<Longrightarrow> \<lbrace>?Q\<rbrace> get_pd (ptr && ~~ mask pd_bits) \<lbrace>?B1\<rbrace>
 4. \<And>s. \<lbrakk>is_aligned ptr 2; is_aligned y 2; ptr \<noteq> y; pd_super_section_relation (y && ~~ mask pd_bits) sid y s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>x s. \<lbrakk>is_aligned ptr 2; is_aligned y 2; ptr \<noteq> y; ?B1 x s\<rbrakk> \<Longrightarrow> (ako_at (arch_kernel_obj.PageDirectory x) (ptr && ~~ mask pd_bits) and pd_super_section_relation (y && ~~ mask pd_bits) sid y) s
 2. \<lbrakk>is_aligned ptr 2; is_aligned y 2; ptr \<noteq> y\<rbrakk> \<Longrightarrow> \<lbrace>?Q\<rbrace> get_pd (ptr && ~~ mask pd_bits) \<lbrace>?B1\<rbrace>
 3. \<And>s. \<lbrakk>is_aligned ptr 2; is_aligned y 2; ptr \<noteq> y; pd_super_section_relation (y && ~~ mask pd_bits) sid y s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 2; is_aligned y 2; ptr \<noteq> y\<rbrakk> \<Longrightarrow> \<lbrace>?Q\<rbrace> get_pd (ptr && ~~ mask pd_bits) \<lbrace>\<lambda>x s. ako_at (arch_kernel_obj.PageDirectory x) (ptr && ~~ mask pd_bits) s \<and> pd_super_section_relation (y && ~~ mask pd_bits) sid y s\<rbrace>
 2. \<And>s. \<lbrakk>is_aligned ptr 2; is_aligned y 2; ptr \<noteq> y; pd_super_section_relation (y && ~~ mask pd_bits) sid y s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_aligned ptr 2; is_aligned y 2; ptr \<noteq> y; pd_super_section_relation (y && ~~ mask pd_bits) sid y s\<rbrakk> \<Longrightarrow> \<forall>pd. ako_at (arch_kernel_obj.PageDirectory pd) (ptr && ~~ mask pd_bits) s \<longrightarrow> ako_at (arch_kernel_obj.PageDirectory pd) (ptr && ~~ mask pd_bits) s \<and> pd_super_section_relation (y && ~~ mask pd_bits) sid y s proof (prove)
goal:
No subgoals!