theory Finalise_DR

lemma remain_pt_pd_relation:
  "\<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr\<notin> ys\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>y\<in>ys. pt_page_relation (y && ~~ mask pt_bits) pg_id y S s\<rbrace>
    store_pte ptr sp
   \<lbrace>\<lambda>r s. \<forall>y\<in>ys. pt_page_relation (y && ~~ mask pt_bits) pg_id y S s\<rbrace>" apply (rule hoare_vcg_const_Ball_lift) apply (subgoal_tac "ptr\<noteq> y") apply (simp add: store_pte_def) apply wp apply (rule_tac Q = "ko_at (ArchObj (arch_kernel_obj.PageTable x)) (ptr && ~~ mask pt_bits)
                and  pt_page_relation (y && ~~ mask pt_bits) pg_id y S" in hoare_vcg_precond_imp) apply (clarsimp simp: set_pt_def) apply (rule_tac Q = "ko_at (ArchObj (arch_kernel_obj.PageTable x)) (ptr && ~~ mask pt_bits)
                   and  pt_page_relation (y && ~~ mask pt_bits) pg_id y S" in hoare_vcg_precond_imp) apply (clarsimp simp: valid_def set_object_def get_object_def in_monad) apply (drule_tac x= y in bspec,simp) apply (clarsimp simp: pt_page_relation_def dest!: ucast_inj_mask| rule conjI)+ apply (drule mask_compare_imply) apply ((simp add: word_size 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; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>y\<in>ys. pt_page_relation (y && ~~ mask pt_bits) pg_id y S s\<rbrace> store_pte ptr sp \<lbrace>\<lambda>r s. \<forall>y\<in>ys. pt_page_relation (y && ~~ mask pt_bits) pg_id y S s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys; y \<in> ys\<rbrakk> \<Longrightarrow> \<lbrace>pt_page_relation (y && ~~ mask pt_bits) pg_id y S\<rbrace> store_pte ptr sp \<lbrace>\<lambda>rv. pt_page_relation (y && ~~ mask pt_bits) pg_id y S\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys; y \<in> ys; ptr \<noteq> y\<rbrakk> \<Longrightarrow> \<lbrace>pt_page_relation (y && ~~ mask pt_bits) pg_id y S\<rbrace> store_pte ptr sp \<lbrace>\<lambda>rv. pt_page_relation (y && ~~ mask pt_bits) pg_id y S\<rbrace>
 2. \<And>y. \<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys; y \<in> ys\<rbrakk> \<Longrightarrow> ptr \<noteq> y proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys; y \<in> ys; ptr \<noteq> y\<rbrakk> \<Longrightarrow> \<lbrace>pt_page_relation (y && ~~ mask pt_bits) pg_id y S\<rbrace> do pt <- get_pt (ptr && ~~ mask pt_bits);
set_pt (ptr && ~~ mask pt_bits) (pt(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := sp))
od \<lbrace>\<lambda>rv. pt_page_relation (y && ~~ mask pt_bits) pg_id y S\<rbrace>
 2. \<And>y. \<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys; y \<in> ys\<rbrakk> \<Longrightarrow> ptr \<noteq> y proof (prove)
goal (4 subgoals):
 1. \<And>y x. \<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys; y \<in> ys; ptr \<noteq> y\<rbrakk> \<Longrightarrow> \<lbrace>?B5 y x\<rbrace> set_pt (ptr && ~~ mask pt_bits) (x(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := sp)) \<lbrace>\<lambda>rv. pt_page_relation (y && ~~ mask pt_bits) pg_id y S\<rbrace>
 2. \<And>y. \<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys; y \<in> ys; ptr \<noteq> y\<rbrakk> \<Longrightarrow> \<lbrace>?Q4 y\<rbrace> get_pt (ptr && ~~ mask pt_bits) \<lbrace>?B5 y\<rbrace>
 3. \<And>y s. \<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys; y \<in> ys; ptr \<noteq> y; pt_page_relation (y && ~~ mask pt_bits) pg_id y S s\<rbrakk> \<Longrightarrow> ?Q4 y s
 4. \<And>y. \<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys; y \<in> ys\<rbrakk> \<Longrightarrow> ptr \<noteq> y proof (prove)
goal (5 subgoals):
 1. \<And>y x. \<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys; y \<in> ys; ptr \<noteq> y\<rbrakk> \<Longrightarrow> \<lbrace>ako_at (arch_kernel_obj.PageTable x) (ptr && ~~ mask pt_bits) and pt_page_relation (y && ~~ mask pt_bits) pg_id y S\<rbrace> set_pt (ptr && ~~ mask pt_bits) (x(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := sp)) \<lbrace>\<lambda>rv. pt_page_relation (y && ~~ mask pt_bits) pg_id y S\<rbrace>
 2. \<And>y x s. \<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys; y \<in> ys; ptr \<noteq> y; ?B5 y x s\<rbrakk> \<Longrightarrow> (ako_at (arch_kernel_obj.PageTable x) (ptr && ~~ mask pt_bits) and pt_page_relation (y && ~~ mask pt_bits) pg_id y S) s
 3. \<And>y. \<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys; y \<in> ys; ptr \<noteq> y\<rbrakk> \<Longrightarrow> \<lbrace>?Q4 y\<rbrace> get_pt (ptr && ~~ mask pt_bits) \<lbrace>?B5 y\<rbrace>
 4. \<And>y s. \<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys; y \<in> ys; ptr \<noteq> y; pt_page_relation (y && ~~ mask pt_bits) pg_id y S s\<rbrakk> \<Longrightarrow> ?Q4 y s
 5. \<And>y. \<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys; y \<in> ys\<rbrakk> \<Longrightarrow> ptr \<noteq> y proof (prove)
goal (5 subgoals):
 1. \<And>y x. \<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys; y \<in> ys; ptr \<noteq> y\<rbrakk> \<Longrightarrow> \<lbrace>ako_at (arch_kernel_obj.PageTable x) (ptr && ~~ mask pt_bits) and pt_page_relation (y && ~~ mask pt_bits) pg_id y S\<rbrace> KHeap_A.set_object (ptr && ~~ mask pt_bits) (ArchObj (arch_kernel_obj.PageTable (x(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := sp)))) \<lbrace>\<lambda>rv. pt_page_relation (y && ~~ mask pt_bits) pg_id y S\<rbrace>
 2. \<And>y x s. \<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys; y \<in> ys; ptr \<noteq> y; ?B5 y x s\<rbrakk> \<Longrightarrow> (ako_at (arch_kernel_obj.PageTable x) (ptr && ~~ mask pt_bits) and pt_page_relation (y && ~~ mask pt_bits) pg_id y S) s
 3. \<And>y. \<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys; y \<in> ys; ptr \<noteq> y\<rbrakk> \<Longrightarrow> \<lbrace>?Q4 y\<rbrace> get_pt (ptr && ~~ mask pt_bits) \<lbrace>?B5 y\<rbrace>
 4. \<And>y s. \<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys; y \<in> ys; ptr \<noteq> y; pt_page_relation (y && ~~ mask pt_bits) pg_id y S s\<rbrakk> \<Longrightarrow> ?Q4 y s
 5. \<And>y. \<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys; y \<in> ys\<rbrakk> \<Longrightarrow> ptr \<noteq> y proof (prove)
goal (6 subgoals):
 1. \<And>y x. \<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys; y \<in> ys; ptr \<noteq> y\<rbrakk> \<Longrightarrow> \<lbrace>ako_at (arch_kernel_obj.PageTable x) (ptr && ~~ mask pt_bits) and pt_page_relation (y && ~~ mask pt_bits) pg_id y S\<rbrace> KHeap_A.set_object (ptr && ~~ mask pt_bits) (ArchObj (arch_kernel_obj.PageTable (x(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := sp)))) \<lbrace>\<lambda>rv. pt_page_relation (y && ~~ mask pt_bits) pg_id y S\<rbrace>
 2. \<And>y x s. \<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys; y \<in> ys; ptr \<noteq> y; (ako_at (arch_kernel_obj.PageTable x) (ptr && ~~ mask pt_bits) and pt_page_relation (y && ~~ mask pt_bits) pg_id y S) s\<rbrakk> \<Longrightarrow> (ako_at (arch_kernel_obj.PageTable x) (ptr && ~~ mask pt_bits) and pt_page_relation (y && ~~ mask pt_bits) pg_id y S) s
 3. \<And>y x s. \<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys; y \<in> ys; ptr \<noteq> y; ?B5 y x s\<rbrakk> \<Longrightarrow> (ako_at (arch_kernel_obj.PageTable x) (ptr && ~~ mask pt_bits) and pt_page_relation (y && ~~ mask pt_bits) pg_id y S) s
 4. \<And>y. \<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys; y \<in> ys; ptr \<noteq> y\<rbrakk> \<Longrightarrow> \<lbrace>?Q4 y\<rbrace> get_pt (ptr && ~~ mask pt_bits) \<lbrace>?B5 y\<rbrace>
 5. \<And>y s. \<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys; y \<in> ys; ptr \<noteq> y; pt_page_relation (y && ~~ mask pt_bits) pg_id y S s\<rbrakk> \<Longrightarrow> ?Q4 y s
 6. \<And>y. \<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys; y \<in> ys\<rbrakk> \<Longrightarrow> ptr \<noteq> y proof (prove)
goal (6 subgoals):
 1. \<And>y x s ya. \<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys; y \<in> ys; ptr \<noteq> y; ako_at (arch_kernel_obj.PageTable x) (ptr && ~~ mask pt_bits) s; pt_page_relation (y && ~~ mask pt_bits) pg_id y S s; a_type ya = a_type (ArchObj (arch_kernel_obj.PageTable (x(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := sp)))); kheap s (ptr && ~~ mask pt_bits) = Some ya\<rbrakk> \<Longrightarrow> pt_page_relation (y && ~~ mask pt_bits) pg_id y S (update_kheap ((kheap s)(ptr && ~~ mask pt_bits \<mapsto> ArchObj (arch_kernel_obj.PageTable (x(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := sp))))) s)
 2. \<And>y x s. \<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys; y \<in> ys; ptr \<noteq> y; (ako_at (arch_kernel_obj.PageTable x) (ptr && ~~ mask pt_bits) and pt_page_relation (y && ~~ mask pt_bits) pg_id y S) s\<rbrakk> \<Longrightarrow> (ako_at (arch_kernel_obj.PageTable x) (ptr && ~~ mask pt_bits) and pt_page_relation (y && ~~ mask pt_bits) pg_id y S) s
 3. \<And>y x s. \<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys; y \<in> ys; ptr \<noteq> y; ?B5 y x s\<rbrakk> \<Longrightarrow> (ako_at (arch_kernel_obj.PageTable x) (ptr && ~~ mask pt_bits) and pt_page_relation (y && ~~ mask pt_bits) pg_id y S) s
 4. \<And>y. \<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys; y \<in> ys; ptr \<noteq> y\<rbrakk> \<Longrightarrow> \<lbrace>?Q4 y\<rbrace> get_pt (ptr && ~~ mask pt_bits) \<lbrace>?B5 y\<rbrace>
 5. \<And>y s. \<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys; y \<in> ys; ptr \<noteq> y; pt_page_relation (y && ~~ mask pt_bits) pg_id y S s\<rbrakk> \<Longrightarrow> ?Q4 y s
 6. \<And>y. \<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys; y \<in> ys\<rbrakk> \<Longrightarrow> ptr \<noteq> y proof (prove)
goal (6 subgoals):
 1. \<And>y x s ya. \<lbrakk>is_aligned ptr 2; ptr \<notin> ys; y \<in> ys; ptr \<noteq> y; ako_at (arch_kernel_obj.PageTable x) (ptr && ~~ mask pt_bits) s; pt_page_relation (y && ~~ mask pt_bits) pg_id y S s; a_type ya = a_type (ArchObj (arch_kernel_obj.PageTable (x(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := sp)))); kheap s (ptr && ~~ mask pt_bits) = Some ya; is_aligned y 2\<rbrakk> \<Longrightarrow> pt_page_relation (y && ~~ mask pt_bits) pg_id y S (update_kheap ((kheap s)(ptr && ~~ mask pt_bits \<mapsto> ArchObj (arch_kernel_obj.PageTable (x(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := sp))))) s)
 2. \<And>y x s. \<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys; y \<in> ys; ptr \<noteq> y; (ako_at (arch_kernel_obj.PageTable x) (ptr && ~~ mask pt_bits) and pt_page_relation (y && ~~ mask pt_bits) pg_id y S) s\<rbrakk> \<Longrightarrow> (ako_at (arch_kernel_obj.PageTable x) (ptr && ~~ mask pt_bits) and pt_page_relation (y && ~~ mask pt_bits) pg_id y S) s
 3. \<And>y x s. \<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys; y \<in> ys; ptr \<noteq> y; ?B5 y x s\<rbrakk> \<Longrightarrow> (ako_at (arch_kernel_obj.PageTable x) (ptr && ~~ mask pt_bits) and pt_page_relation (y && ~~ mask pt_bits) pg_id y S) s
 4. \<And>y. \<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys; y \<in> ys; ptr \<noteq> y\<rbrakk> \<Longrightarrow> \<lbrace>?Q4 y\<rbrace> get_pt (ptr && ~~ mask pt_bits) \<lbrace>?B5 y\<rbrace>
 5. \<And>y s. \<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys; y \<in> ys; ptr \<noteq> y; pt_page_relation (y && ~~ mask pt_bits) pg_id y S s\<rbrakk> \<Longrightarrow> ?Q4 y s
 6. \<And>y. \<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys; y \<in> ys\<rbrakk> \<Longrightarrow> ptr \<noteq> y proof (prove)
goal (7 subgoals):
 1. \<And>y x s fun. \<lbrakk>is_aligned ptr 2; ptr \<notin> ys; y \<in> ys; ptr \<noteq> y; ako_at (arch_kernel_obj.PageTable x) (ptr && ~~ mask pt_bits) s; a_type (ArchObj (arch_kernel_obj.PageTable fun)) = a_type (ArchObj (arch_kernel_obj.PageTable (x(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := sp)))); kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); is_aligned y 2; case fun (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> S | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> S; (y && mask pt_bits >> 2) && mask 8 = (ptr && mask pt_bits >> 2) && mask 8; y && ~~ mask pt_bits = ptr && ~~ mask pt_bits\<rbrakk> \<Longrightarrow> case sp of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> S | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> S
 2. \<And>y x s ya fun. \<lbrakk>is_aligned ptr 2; ptr \<notin> ys; y \<in> ys; ptr \<noteq> y; ako_at (arch_kernel_obj.PageTable x) (ptr && ~~ mask pt_bits) s; a_type ya = a_type (ArchObj (arch_kernel_obj.PageTable (x(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := sp)))); kheap s (ptr && ~~ mask pt_bits) = Some ya; is_aligned y 2; kheap s (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> S | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> S\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) \<noteq> UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) \<longrightarrow> y && ~~ mask pt_bits = ptr && ~~ mask pt_bits \<longrightarrow> (case x (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> S | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> S)
 3. \<And>y x s. \<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys; y \<in> ys; ptr \<noteq> y; (ako_at (arch_kernel_obj.PageTable x) (ptr && ~~ mask pt_bits) and pt_page_relation (y && ~~ mask pt_bits) pg_id y S) s\<rbrakk> \<Longrightarrow> (ako_at (arch_kernel_obj.PageTable x) (ptr && ~~ mask pt_bits) and pt_page_relation (y && ~~ mask pt_bits) pg_id y S) s
 4. \<And>y x s. \<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys; y \<in> ys; ptr \<noteq> y; ?B5 y x s\<rbrakk> \<Longrightarrow> (ako_at (arch_kernel_obj.PageTable x) (ptr && ~~ mask pt_bits) and pt_page_relation (y && ~~ mask pt_bits) pg_id y S) s
 5. \<And>y. \<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys; y \<in> ys; ptr \<noteq> y\<rbrakk> \<Longrightarrow> \<lbrace>?Q4 y\<rbrace> get_pt (ptr && ~~ mask pt_bits) \<lbrace>?B5 y\<rbrace>
 6. \<And>y s. \<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys; y \<in> ys; ptr \<noteq> y; pt_page_relation (y && ~~ mask pt_bits) pg_id y S s\<rbrakk> \<Longrightarrow> ?Q4 y s
 7. \<And>y. \<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys; y \<in> ys\<rbrakk> \<Longrightarrow> ptr \<noteq> y proof (prove)
goal (11 subgoals):
 1. \<And>y x s fun. \<lbrakk>is_aligned ptr 2; ptr \<notin> ys; y \<in> ys; ptr \<noteq> y; ako_at (arch_kernel_obj.PageTable x) (ptr && ~~ mask pt_bits) s; a_type (ArchObj (arch_kernel_obj.PageTable fun)) = a_type (ArchObj (arch_kernel_obj.PageTable (x(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := sp)))); kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); is_aligned y 2; case fun (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> S | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> S; y && ~~ mask pt_bits = ptr && ~~ mask pt_bits\<rbrakk> \<Longrightarrow> size y = size ptr
 2. \<And>y x s fun. \<lbrakk>is_aligned ptr 2; ptr \<notin> ys; y \<in> ys; ptr \<noteq> y; ako_at (arch_kernel_obj.PageTable x) (ptr && ~~ mask pt_bits) s; a_type (ArchObj (arch_kernel_obj.PageTable fun)) = a_type (ArchObj (arch_kernel_obj.PageTable (x(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := sp)))); kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); is_aligned y 2; case fun (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> S | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> S; y && ~~ mask pt_bits = ptr && ~~ mask pt_bits\<rbrakk> \<Longrightarrow> pt_bits \<le> size y
 3. \<And>y x s fun. \<lbrakk>is_aligned ptr 2; ptr \<notin> ys; y \<in> ys; ptr \<noteq> y; ako_at (arch_kernel_obj.PageTable x) (ptr && ~~ mask pt_bits) s; a_type (ArchObj (arch_kernel_obj.PageTable fun)) = a_type (ArchObj (arch_kernel_obj.PageTable (x(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := sp)))); kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); is_aligned y 2; case fun (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> S | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> S; y && ~~ mask pt_bits = ptr && ~~ mask pt_bits\<rbrakk> \<Longrightarrow> 2 + 8 \<le> pt_bits
 4. \<And>y x s fun. \<lbrakk>is_aligned ptr 2; ptr \<notin> ys; y \<in> ys; ptr \<noteq> y; ako_at (arch_kernel_obj.PageTable x) (ptr && ~~ mask pt_bits) s; a_type (ArchObj (arch_kernel_obj.PageTable fun)) = a_type (ArchObj (arch_kernel_obj.PageTable (x(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := sp)))); kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); is_aligned y 2; case fun (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> S | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> S; y && ~~ mask pt_bits = ptr && ~~ mask pt_bits\<rbrakk> \<Longrightarrow> y \<noteq> ptr
 5. \<And>y x s fun. \<lbrakk>is_aligned ptr 2; ptr \<notin> ys; y \<in> ys; ptr \<noteq> y; ako_at (arch_kernel_obj.PageTable x) (ptr && ~~ mask pt_bits) s; a_type (ArchObj (arch_kernel_obj.PageTable fun)) = a_type (ArchObj (arch_kernel_obj.PageTable (x(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := sp)))); kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); is_aligned y 2; case fun (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> S | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> S; y && ~~ mask pt_bits = ptr && ~~ mask pt_bits; y && mask 2 \<noteq> ptr && mask 2 \<or> y && ~~ mask (2 + 8) \<noteq> ptr && ~~ mask (2 + 8)\<rbrakk> \<Longrightarrow> case sp of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> S | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> S
 6. \<And>y x s ya fun. \<lbrakk>is_aligned ptr 2; ptr \<notin> ys; y \<in> ys; ptr \<noteq> y; ako_at (arch_kernel_obj.PageTable x) (ptr && ~~ mask pt_bits) s; a_type ya = a_type (ArchObj (arch_kernel_obj.PageTable (x(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := sp)))); kheap s (ptr && ~~ mask pt_bits) = Some ya; is_aligned y 2; kheap s (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> S | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> S\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) \<noteq> UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) \<longrightarrow> y && ~~ mask pt_bits = ptr && ~~ mask pt_bits \<longrightarrow> (case x (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> S | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> S)
 7. \<And>y x s. \<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys; y \<in> ys; ptr \<noteq> y; (ako_at (arch_kernel_obj.PageTable x) (ptr && ~~ mask pt_bits) and pt_page_relation (y && ~~ mask pt_bits) pg_id y S) s\<rbrakk> \<Longrightarrow> (ako_at (arch_kernel_obj.PageTable x) (ptr && ~~ mask pt_bits) and pt_page_relation (y && ~~ mask pt_bits) pg_id y S) s
 8. \<And>y x s. \<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys; y \<in> ys; ptr \<noteq> y; ?B5 y x s\<rbrakk> \<Longrightarrow> (ako_at (arch_kernel_obj.PageTable x) (ptr && ~~ mask pt_bits) and pt_page_relation (y && ~~ mask pt_bits) pg_id y S) s
 9. \<And>y. \<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys; y \<in> ys; ptr \<noteq> y\<rbrakk> \<Longrightarrow> \<lbrace>?Q4 y\<rbrace> get_pt (ptr && ~~ mask pt_bits) \<lbrace>?B5 y\<rbrace>
 10. \<And>y s. \<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys; y \<in> ys; ptr \<noteq> y; pt_page_relation (y && ~~ mask pt_bits) pg_id y S s\<rbrakk> \<Longrightarrow> ?Q4 y s
A total of 11 subgoals... proof (prove)
goal (6 subgoals):
 1. \<And>y x s ya fun. \<lbrakk>ptr && mask 2 = 0; ptr \<notin> ys; y \<in> ys; ptr \<noteq> y; ako_at (arch_kernel_obj.PageTable x) (ptr && ~~ mask 10) s; a_type ya = a_type (ArchObj (arch_kernel_obj.PageTable (x(UCAST(32 \<rightarrow> 8) (ptr && mask 10 >> 2) := sp)))); kheap s (ptr && ~~ mask 10) = Some ya; y && mask 2 = 0; kheap s (y && ~~ mask 10) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (y && mask 10 >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> S | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> S\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 8) (y && mask 10 >> 2) \<noteq> UCAST(32 \<rightarrow> 8) (ptr && mask 10 >> 2) \<longrightarrow> y && ~~ mask 10 = ptr && ~~ mask 10 \<longrightarrow> (case x (UCAST(32 \<rightarrow> 8) (y && mask 10 >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> S | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> S)
 2. \<And>y x s. \<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys; y \<in> ys; ptr \<noteq> y; (ako_at (arch_kernel_obj.PageTable x) (ptr && ~~ mask pt_bits) and pt_page_relation (y && ~~ mask pt_bits) pg_id y S) s\<rbrakk> \<Longrightarrow> (ako_at (arch_kernel_obj.PageTable x) (ptr && ~~ mask pt_bits) and pt_page_relation (y && ~~ mask pt_bits) pg_id y S) s
 3. \<And>y x s. \<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys; y \<in> ys; ptr \<noteq> y; ?B5 y x s\<rbrakk> \<Longrightarrow> (ako_at (arch_kernel_obj.PageTable x) (ptr && ~~ mask pt_bits) and pt_page_relation (y && ~~ mask pt_bits) pg_id y S) s
 4. \<And>y. \<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys; y \<in> ys; ptr \<noteq> y\<rbrakk> \<Longrightarrow> \<lbrace>?Q4 y\<rbrace> get_pt (ptr && ~~ mask pt_bits) \<lbrace>?B5 y\<rbrace>
 5. \<And>y s. \<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys; y \<in> ys; ptr \<noteq> y; pt_page_relation (y && ~~ mask pt_bits) pg_id y S s\<rbrakk> \<Longrightarrow> ?Q4 y s
 6. \<And>y. \<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys; y \<in> ys\<rbrakk> \<Longrightarrow> ptr \<noteq> y proof (prove)
goal (5 subgoals):
 1. \<And>y x s. \<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys; y \<in> ys; ptr \<noteq> y; (ako_at (arch_kernel_obj.PageTable x) (ptr && ~~ mask pt_bits) and pt_page_relation (y && ~~ mask pt_bits) pg_id y S) s\<rbrakk> \<Longrightarrow> (ako_at (arch_kernel_obj.PageTable x) (ptr && ~~ mask pt_bits) and pt_page_relation (y && ~~ mask pt_bits) pg_id y S) s
 2. \<And>y x s. \<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys; y \<in> ys; ptr \<noteq> y; ?B5 y x s\<rbrakk> \<Longrightarrow> (ako_at (arch_kernel_obj.PageTable x) (ptr && ~~ mask pt_bits) and pt_page_relation (y && ~~ mask pt_bits) pg_id y S) s
 3. \<And>y. \<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys; y \<in> ys; ptr \<noteq> y\<rbrakk> \<Longrightarrow> \<lbrace>?Q4 y\<rbrace> get_pt (ptr && ~~ mask pt_bits) \<lbrace>?B5 y\<rbrace>
 4. \<And>y s. \<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys; y \<in> ys; ptr \<noteq> y; pt_page_relation (y && ~~ mask pt_bits) pg_id y S s\<rbrakk> \<Longrightarrow> ?Q4 y s
 5. \<And>y. \<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys; y \<in> ys\<rbrakk> \<Longrightarrow> ptr \<noteq> y proof (prove)
goal (4 subgoals):
 1. \<And>y x s. \<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys; y \<in> ys; ptr \<noteq> y; ?B5 y x s\<rbrakk> \<Longrightarrow> (ako_at (arch_kernel_obj.PageTable x) (ptr && ~~ mask pt_bits) and pt_page_relation (y && ~~ mask pt_bits) pg_id y S) s
 2. \<And>y. \<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys; y \<in> ys; ptr \<noteq> y\<rbrakk> \<Longrightarrow> \<lbrace>?Q4 y\<rbrace> get_pt (ptr && ~~ mask pt_bits) \<lbrace>?B5 y\<rbrace>
 3. \<And>y s. \<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys; y \<in> ys; ptr \<noteq> y; pt_page_relation (y && ~~ mask pt_bits) pg_id y S s\<rbrakk> \<Longrightarrow> ?Q4 y s
 4. \<And>y. \<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys; y \<in> ys\<rbrakk> \<Longrightarrow> ptr \<noteq> y proof (prove)
goal (3 subgoals):
 1. \<And>y. \<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys; y \<in> ys; ptr \<noteq> y\<rbrakk> \<Longrightarrow> \<lbrace>?Q4 y\<rbrace> get_pt (ptr && ~~ mask pt_bits) \<lbrace>\<lambda>x s. ako_at (arch_kernel_obj.PageTable x) (ptr && ~~ mask pt_bits) s \<and> pt_page_relation (y && ~~ mask pt_bits) pg_id y S s\<rbrace>
 2. \<And>y s. \<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys; y \<in> ys; ptr \<noteq> y; pt_page_relation (y && ~~ mask pt_bits) pg_id y S s\<rbrakk> \<Longrightarrow> ?Q4 y s
 3. \<And>y. \<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys; y \<in> ys\<rbrakk> \<Longrightarrow> ptr \<noteq> y proof (prove)
goal (2 subgoals):
 1. \<And>y s. \<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys; y \<in> ys; ptr \<noteq> y; pt_page_relation (y && ~~ mask pt_bits) pg_id y S s\<rbrakk> \<Longrightarrow> \<forall>pt. ako_at (arch_kernel_obj.PageTable pt) (ptr && ~~ mask pt_bits) s \<longrightarrow> ako_at (arch_kernel_obj.PageTable pt) (ptr && ~~ mask pt_bits) s \<and> pt_page_relation (y && ~~ mask pt_bits) pg_id y S s
 2. \<And>y. \<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr \<notin> ys; y \<in> ys\<rbrakk> \<Longrightarrow> ptr \<noteq> y proof (prove)
goal:
No subgoals!