theory ArchAcc_AI

lemma set_asid_pool_global_objs [wp]:
  "\<lbrace>valid_global_objs and valid_arch_state\<rbrace>
   set_asid_pool p ap
   \<lbrace>\<lambda>_. valid_global_objs\<rbrace>" apply (simp add: set_asid_pool_def set_object_def a_type_def) apply (wp get_object_wp) apply (clarsimp simp del: fun_upd_apply
                  split: kernel_object.splits arch_kernel_obj.splits) apply (clarsimp simp: valid_global_objs_def valid_vso_at_def) apply (rule conjI) apply (clarsimp simp: obj_at_def) apply (rule conjI) subgoal by (clarsimp simp: valid_arch_state_def obj_at_def a_type_def) apply clarsimp apply (erule (1) valid_vspace_obj_same_type) subgoal by (simp add: a_type_def) apply (rule conjI) subgoal by (clarsimp simp: obj_at_def valid_arch_state_def a_type_def) apply (clarsimp simp: obj_at_def) apply (drule (1) bspec) by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_objs and valid_arch_state\<rbrace> set_asid_pool p ap \<lbrace>\<lambda>_. valid_global_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_objs and valid_arch_state\<rbrace> do kobj <- get_object p;
y <- assert ((case kobj of CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | Endpoint endpoint \<Rightarrow> AEndpoint | Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | PageTable pt \<Rightarrow> APageTable | PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = AArch AASIDPool);
s <- get;
put (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool ap))\<rparr>)
od \<lbrace>\<lambda>_. valid_global_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_global_objs and valid_arch_state) s \<Longrightarrow> \<forall>ko. ko_at ko p s \<longrightarrow> (case ko of CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | Endpoint endpoint \<Rightarrow> AEndpoint | Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | PageTable pt \<Rightarrow> APageTable | PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = AArch AASIDPool \<longrightarrow> valid_global_objs (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool ap))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s x1. \<lbrakk>valid_global_objs s; valid_arch_state s; ako_at (ASIDPool x1) p s\<rbrakk> \<Longrightarrow> valid_global_objs (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool ap))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s x1 ao. \<lbrakk>valid_arch_state s; ako_at (ASIDPool x1) p s; obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)); ako_at ao (arm_global_pd (arch_state s)) s; valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> (\<exists>ao. ako_at ao (arm_global_pd (arch_state s)) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool ap))\<rparr>) \<and> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool ap))\<rparr>)) \<and> obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool ap))\<rparr>) \<and> (\<forall>pa\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) pa (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool ap))\<rparr>) \<and> (\<forall>x. aligned_pte (pt x))) proof (prove)
goal (2 subgoals):
 1. \<And>s x1 ao. \<lbrakk>valid_arch_state s; ako_at (ASIDPool x1) p s; obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)); ako_at ao (arm_global_pd (arch_state s)) s; valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> \<exists>ao. ako_at ao (arm_global_pd (arch_state s)) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool ap))\<rparr>) \<and> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool ap))\<rparr>)
 2. \<And>s x1 ao. \<lbrakk>valid_arch_state s; ako_at (ASIDPool x1) p s; obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)); ako_at ao (arm_global_pd (arch_state s)) s; valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool ap))\<rparr>) \<and> (\<forall>pa\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) pa (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool ap))\<rparr>) \<and> (\<forall>x. aligned_pte (pt x))) proof (prove)
goal (2 subgoals):
 1. \<And>s x1 ao. \<lbrakk>valid_arch_state s; kheap s p = Some (ArchObj (ASIDPool x1)); empty_table (set (second_level_tables (arch_state s))) (ArchObj ao); \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. kheap s p = Some (ArchObj (PageTable pt)) \<and> (\<forall>x. aligned_pte (pt x)); kheap s (arm_global_pd (arch_state s)) = Some (ArchObj ao); valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> (arm_global_pd (arch_state s) = p \<longrightarrow> (\<forall>x\<in>ran ap. (x = p \<longrightarrow> a_type (ArchObj (ASIDPool ap)) = AArch APageDirectory) \<and> (x \<noteq> p \<longrightarrow> (\<exists>ko. kheap s x = Some ko \<and> a_type ko = AArch APageDirectory)))) \<and> (arm_global_pd (arch_state s) \<noteq> p \<longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool ap))\<rparr>))
 2. \<And>s x1 ao. \<lbrakk>valid_arch_state s; ako_at (ASIDPool x1) p s; obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)); ako_at ao (arm_global_pd (arch_state s)) s; valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool ap))\<rparr>) \<and> (\<forall>pa\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) pa (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool ap))\<rparr>) \<and> (\<forall>x. aligned_pte (pt x))) proof (prove)
goal (3 subgoals):
 1. \<And>s x1 ao. \<lbrakk>valid_arch_state s; kheap s p = Some (ArchObj (ASIDPool x1)); empty_table (set (second_level_tables (arch_state s))) (ArchObj ao); \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. kheap s p = Some (ArchObj (PageTable pt)) \<and> (\<forall>x. aligned_pte (pt x)); kheap s (arm_global_pd (arch_state s)) = Some (ArchObj ao); valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> arm_global_pd (arch_state s) = p \<longrightarrow> (\<forall>x\<in>ran ap. (x = p \<longrightarrow> a_type (ArchObj (ASIDPool ap)) = AArch APageDirectory) \<and> (x \<noteq> p \<longrightarrow> (\<exists>ko. kheap s x = Some ko \<and> a_type ko = AArch APageDirectory)))
 2. \<And>s x1 ao. \<lbrakk>valid_arch_state s; kheap s p = Some (ArchObj (ASIDPool x1)); empty_table (set (second_level_tables (arch_state s))) (ArchObj ao); \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. kheap s p = Some (ArchObj (PageTable pt)) \<and> (\<forall>x. aligned_pte (pt x)); kheap s (arm_global_pd (arch_state s)) = Some (ArchObj ao); valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> arm_global_pd (arch_state s) \<noteq> p \<longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool ap))\<rparr>)
 3. \<And>s x1 ao. \<lbrakk>valid_arch_state s; ako_at (ASIDPool x1) p s; obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)); ako_at ao (arm_global_pd (arch_state s)) s; valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool ap))\<rparr>) \<and> (\<forall>pa\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) pa (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool ap))\<rparr>) \<and> (\<forall>x. aligned_pte (pt x))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_arch_state s_; kheap s_ p = Some (ArchObj (ASIDPool x1_)); empty_table (set (second_level_tables (arch_state s_))) (ArchObj ao_); \<forall>p\<in>set (arm_global_pts (arch_state s_)). \<exists>pt. kheap s_ p = Some (ArchObj (PageTable pt)) \<and> (\<forall>x. aligned_pte (pt x)); kheap s_ (arm_global_pd (arch_state s_)) = Some (ArchObj ao_); valid_vspace_obj ao_ s_\<rbrakk> \<Longrightarrow> arm_global_pd (arch_state s_) = p \<longrightarrow> (\<forall>x\<in>ran ap. (x = p \<longrightarrow> a_type (ArchObj (ASIDPool ap)) = AArch APageDirectory) \<and> (x \<noteq> p \<longrightarrow> (\<exists>ko. kheap s_ x = Some ko \<and> a_type ko = AArch APageDirectory))) proof (prove)
goal (2 subgoals):
 1. \<And>s x1 ao. \<lbrakk>valid_arch_state s; kheap s p = Some (ArchObj (ASIDPool x1)); empty_table (set (second_level_tables (arch_state s))) (ArchObj ao); \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. kheap s p = Some (ArchObj (PageTable pt)) \<and> (\<forall>x. aligned_pte (pt x)); kheap s (arm_global_pd (arch_state s)) = Some (ArchObj ao); valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> arm_global_pd (arch_state s) \<noteq> p \<longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool ap))\<rparr>)
 2. \<And>s x1 ao. \<lbrakk>valid_arch_state s; ako_at (ASIDPool x1) p s; obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)); ako_at ao (arm_global_pd (arch_state s)) s; valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool ap))\<rparr>) \<and> (\<forall>pa\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) pa (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool ap))\<rparr>) \<and> (\<forall>x. aligned_pte (pt x))) proof (prove)
goal (2 subgoals):
 1. \<And>s x1 ao. \<lbrakk>valid_arch_state s; kheap s p = Some (ArchObj (ASIDPool x1)); empty_table (set (second_level_tables (arch_state s))) (ArchObj ao); \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. kheap s p = Some (ArchObj (PageTable pt)) \<and> (\<forall>x. aligned_pte (pt x)); kheap s (arm_global_pd (arch_state s)) = Some (ArchObj ao); valid_vspace_obj ao s; arm_global_pd (arch_state s) \<noteq> p\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool ap))\<rparr>)
 2. \<And>s x1 ao. \<lbrakk>valid_arch_state s; ako_at (ASIDPool x1) p s; obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)); ako_at ao (arm_global_pd (arch_state s)) s; valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool ap))\<rparr>) \<and> (\<forall>pa\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) pa (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool ap))\<rparr>) \<and> (\<forall>x. aligned_pte (pt x))) proof (prove)
goal (2 subgoals):
 1. \<And>s x1 ao. \<lbrakk>valid_arch_state s; kheap s p = Some (ArchObj (ASIDPool x1)); empty_table (set (second_level_tables (arch_state s))) (ArchObj ao); \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. kheap s p = Some (ArchObj (PageTable pt)) \<and> (\<forall>x. aligned_pte (pt x)); kheap s (arm_global_pd (arch_state s)) = Some (ArchObj ao); arm_global_pd (arch_state s) \<noteq> p\<rbrakk> \<Longrightarrow> a_type (ArchObj (ASIDPool ap)) = a_type (ArchObj (ASIDPool x1))
 2. \<And>s x1 ao. \<lbrakk>valid_arch_state s; ako_at (ASIDPool x1) p s; obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)); ako_at ao (arm_global_pd (arch_state s)) s; valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool ap))\<rparr>) \<and> (\<forall>pa\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) pa (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool ap))\<rparr>) \<and> (\<forall>x. aligned_pte (pt x))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_arch_state s_; kheap s_ p = Some (ArchObj (ASIDPool x1_)); empty_table (set (second_level_tables (arch_state s_))) (ArchObj ao_); \<forall>p\<in>set (arm_global_pts (arch_state s_)). \<exists>pt. kheap s_ p = Some (ArchObj (PageTable pt)) \<and> (\<forall>x. aligned_pte (pt x)); kheap s_ (arm_global_pd (arch_state s_)) = Some (ArchObj ao_); arm_global_pd (arch_state s_) \<noteq> p\<rbrakk> \<Longrightarrow> a_type (ArchObj (ASIDPool ap)) = a_type (ArchObj (ASIDPool x1_)) proof (prove)
goal (1 subgoal):
 1. \<And>s x1 ao. \<lbrakk>valid_arch_state s; ako_at (ASIDPool x1) p s; obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)); ako_at ao (arm_global_pd (arch_state s)) s; valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool ap))\<rparr>) \<and> (\<forall>pa\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) pa (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool ap))\<rparr>) \<and> (\<forall>x. aligned_pte (pt x))) proof (prove)
goal (2 subgoals):
 1. \<And>s x1 ao. \<lbrakk>valid_arch_state s; ako_at (ASIDPool x1) p s; obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)); ako_at ao (arm_global_pd (arch_state s)) s; valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool ap))\<rparr>)
 2. \<And>s x1 ao. \<lbrakk>valid_arch_state s; ako_at (ASIDPool x1) p s; obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)); ako_at ao (arm_global_pd (arch_state s)) s; valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> \<forall>pa\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) pa (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool ap))\<rparr>) \<and> (\<forall>x. aligned_pte (pt x)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_arch_state s_; ako_at (ASIDPool x1_) p s_; obj_at (empty_table (set (second_level_tables (arch_state s_)))) (arm_global_pd (arch_state s_)) s_; \<forall>p\<in>set (arm_global_pts (arch_state s_)). \<exists>pt. ako_at (PageTable pt) p s_ \<and> (\<forall>x. aligned_pte (pt x)); ako_at ao_ (arm_global_pd (arch_state s_)) s_; valid_vspace_obj ao_ s_\<rbrakk> \<Longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s_)))) (arm_global_pd (arch_state s_)) (s_\<lparr>kheap := (kheap s_)(p \<mapsto> ArchObj (ASIDPool ap))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s x1 ao. \<lbrakk>valid_arch_state s; ako_at (ASIDPool x1) p s; obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)); ako_at ao (arm_global_pd (arch_state s)) s; valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> \<forall>pa\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) pa (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool ap))\<rparr>) \<and> (\<forall>x. aligned_pte (pt x)) proof (prove)
goal (1 subgoal):
 1. \<And>s x1 ao. \<lbrakk>valid_arch_state s; kheap s p = Some (ArchObj (ASIDPool x1)); empty_table (set (second_level_tables (arch_state s))) (ArchObj ao); \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. kheap s p = Some (ArchObj (PageTable pt)) \<and> (\<forall>x. aligned_pte (pt x)); kheap s (arm_global_pd (arch_state s)) = Some (ArchObj ao); valid_vspace_obj ao s; p \<in> set (arm_global_pts (arch_state s))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s x1 ao. \<lbrakk>valid_arch_state s; kheap s p = Some (ArchObj (ASIDPool x1)); empty_table (set (second_level_tables (arch_state s))) (ArchObj ao); kheap s (arm_global_pd (arch_state s)) = Some (ArchObj ao); valid_vspace_obj ao s; p \<in> set (arm_global_pts (arch_state s)); \<exists>pt. kheap s p = Some (ArchObj (PageTable pt)) \<and> (\<forall>x. aligned_pte (pt x))\<rbrakk> \<Longrightarrow> False