theory ArchAcc_AI

lemma set_pd_global_objs[wp]:
  "\<lbrace>valid_global_objs and valid_global_refs and
    valid_arch_state and
    (\<lambda>s. (obj_at (empty_table (set (second_level_tables (arch_state s)))) p s
             \<longrightarrow> empty_table (set (second_level_tables (arch_state s)))
                                 (ArchObj (PageDirectory pd)))
        \<or> (\<exists>slot. cte_wp_at (\<lambda>cap. p \<in> obj_refs cap) slot s))\<rbrace>
  set_pd p pd \<lbrace>\<lambda>rv. valid_global_objs\<rbrace>" apply (simp add: set_pd_def second_level_tables_def) apply (wpsimp wp: set_object_wp_strong) apply (clarsimp simp add: valid_global_objs_def valid_vso_at_def
                            cte_wp_at_caps_of_state second_level_tables_def) apply (intro conjI) apply (clarsimp simp: obj_at_def
                simp del: valid_vspace_obj.simps) apply (intro conjI impI) apply (clarsimp simp del: valid_vspace_obj.simps) apply (erule disjE) apply (drule(1) empty_table_is_valid)+ apply (rule valid_vspace_obj_same_type, (simp add: valid_vspace_obj_def)+) apply (clarsimp simp: a_type_def) apply (drule (1) valid_global_refsD2) apply (simp add: cap_range_def global_refs_def) apply (rule valid_vspace_obj_same_type, simp+) apply (simp add: a_type_def) apply (clarsimp simp: obj_at_def) apply (drule (1) valid_global_refsD2) apply (simp add: cap_range_def global_refs_def) apply clarsimp apply (clarsimp simp: obj_at_def
              simp del: valid_vspace_obj.simps) apply (drule(1) bspec, clarsimp simp: a_type_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_objs and valid_global_refs and valid_arch_state and (\<lambda>s. (obj_at (empty_table (set (second_level_tables (arch_state s)))) p s \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd))) \<or> (\<exists>slot. cte_wp_at (\<lambda>cap. p \<in> obj_refs cap) slot s))\<rbrace> set_pd p pd \<lbrace>\<lambda>rv. valid_global_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_objs and valid_global_refs and valid_arch_state and (\<lambda>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) p s \<longrightarrow> empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b. cte_wp_at (\<lambda>cap. p \<in> obj_refs cap) (a, b) s))\<rbrace> set_object p (ArchObj (PageDirectory pd)) \<lbrace>\<lambda>rv. valid_global_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>valid_global_objs s; valid_global_refs s; valid_arch_state s; obj_at (empty_table (set (arm_global_pts (arch_state s)))) p s \<longrightarrow> empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b. cte_wp_at (\<lambda>cap. p \<in> obj_refs cap) (a, b) s); ko_at ko p s; a_type (ArchObj (PageDirectory pd)) = a_type ko\<rbrakk> \<Longrightarrow> valid_global_objs (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s ko ao. \<lbrakk>valid_global_refs s; valid_arch_state s; obj_at (empty_table (set (arm_global_pts (arch_state s)))) p s \<longrightarrow> empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap); ko_at ko p s; a_type (ArchObj (PageDirectory pd)) = a_type ko; obj_at (empty_table (set (arm_global_pts (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 (PageDirectory pd))\<rparr>) \<and> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>)) \<and> obj_at (empty_table (set (arm_global_pts (arch_state s)))) (arm_global_pd (arch_state s)) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<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 (PageDirectory pd))\<rparr>) \<and> (\<forall>x. aligned_pte (pt x))) proof (prove)
goal (3 subgoals):
 1. \<And>s ko ao. \<lbrakk>valid_global_refs s; valid_arch_state s; obj_at (empty_table (set (arm_global_pts (arch_state s)))) p s \<longrightarrow> empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap); ko_at ko p s; a_type (ArchObj (PageDirectory pd)) = a_type ko; obj_at (empty_table (set (arm_global_pts (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 (PageDirectory pd))\<rparr>) \<and> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>)
 2. \<And>s ko ao. \<lbrakk>valid_global_refs s; valid_arch_state s; obj_at (empty_table (set (arm_global_pts (arch_state s)))) p s \<longrightarrow> empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap); ko_at ko p s; a_type (ArchObj (PageDirectory pd)) = a_type ko; obj_at (empty_table (set (arm_global_pts (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 (arm_global_pts (arch_state s)))) (arm_global_pd (arch_state s)) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>)
 3. \<And>s ko ao. \<lbrakk>valid_global_refs s; valid_arch_state s; obj_at (empty_table (set (arm_global_pts (arch_state s)))) p s \<longrightarrow> empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap); ko_at ko p s; a_type (ArchObj (PageDirectory pd)) = a_type ko; obj_at (empty_table (set (arm_global_pts (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 (PageDirectory pd))\<rparr>) \<and> (\<forall>x. aligned_pte (pt x)) proof (prove)
goal (3 subgoals):
 1. \<And>s ko ao. \<lbrakk>valid_global_refs s; valid_arch_state s; empty_table (set (arm_global_pts (arch_state s))) ko \<longrightarrow> empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap); kheap s p = Some ko; a_type (ArchObj (PageDirectory pd)) = a_type ko; empty_table (set (arm_global_pts (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> valid_vspace_obj (PageDirectory pd) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>)) \<and> (arm_global_pd (arch_state s) \<noteq> p \<longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>))
 2. \<And>s ko ao. \<lbrakk>valid_global_refs s; valid_arch_state s; obj_at (empty_table (set (arm_global_pts (arch_state s)))) p s \<longrightarrow> empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap); ko_at ko p s; a_type (ArchObj (PageDirectory pd)) = a_type ko; obj_at (empty_table (set (arm_global_pts (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 (arm_global_pts (arch_state s)))) (arm_global_pd (arch_state s)) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>)
 3. \<And>s ko ao. \<lbrakk>valid_global_refs s; valid_arch_state s; obj_at (empty_table (set (arm_global_pts (arch_state s)))) p s \<longrightarrow> empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap); ko_at ko p s; a_type (ArchObj (PageDirectory pd)) = a_type ko; obj_at (empty_table (set (arm_global_pts (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 (PageDirectory pd))\<rparr>) \<and> (\<forall>x. aligned_pte (pt x)) proof (prove)
goal (4 subgoals):
 1. \<And>s ko ao. \<lbrakk>valid_global_refs s; valid_arch_state s; empty_table (set (arm_global_pts (arch_state s))) ko \<longrightarrow> empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap); kheap s p = Some ko; a_type (ArchObj (PageDirectory pd)) = a_type ko; empty_table (set (arm_global_pts (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) = p\<rbrakk> \<Longrightarrow> valid_vspace_obj (PageDirectory pd) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>)
 2. \<And>s ko ao. \<lbrakk>valid_global_refs s; valid_arch_state s; empty_table (set (arm_global_pts (arch_state s))) ko \<longrightarrow> empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap); kheap s p = Some ko; a_type (ArchObj (PageDirectory pd)) = a_type ko; empty_table (set (arm_global_pts (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 (PageDirectory pd))\<rparr>)
 3. \<And>s ko ao. \<lbrakk>valid_global_refs s; valid_arch_state s; obj_at (empty_table (set (arm_global_pts (arch_state s)))) p s \<longrightarrow> empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap); ko_at ko p s; a_type (ArchObj (PageDirectory pd)) = a_type ko; obj_at (empty_table (set (arm_global_pts (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 (arm_global_pts (arch_state s)))) (arm_global_pd (arch_state s)) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>)
 4. \<And>s ko ao. \<lbrakk>valid_global_refs s; valid_arch_state s; obj_at (empty_table (set (arm_global_pts (arch_state s)))) p s \<longrightarrow> empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap); ko_at ko p s; a_type (ArchObj (PageDirectory pd)) = a_type ko; obj_at (empty_table (set (arm_global_pts (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 (PageDirectory pd))\<rparr>) \<and> (\<forall>x. aligned_pte (pt x)) proof (prove)
goal (4 subgoals):
 1. \<And>s ao. \<lbrakk>valid_global_refs s; valid_arch_state s; empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> arm_global_pd (arch_state s) \<in> obj_refs cap); kheap s (arm_global_pd (arch_state s)) = Some (ArchObj ao); a_type (ArchObj (PageDirectory pd)) = a_type (ArchObj ao); empty_table (set (arm_global_pts (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)); valid_vspace_obj ao s; p = arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> valid_vspace_obj (PageDirectory pd) (s\<lparr>kheap := (kheap s)(arm_global_pd (arch_state s) \<mapsto> ArchObj (PageDirectory pd))\<rparr>)
 2. \<And>s ko ao. \<lbrakk>valid_global_refs s; valid_arch_state s; empty_table (set (arm_global_pts (arch_state s))) ko \<longrightarrow> empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap); kheap s p = Some ko; a_type (ArchObj (PageDirectory pd)) = a_type ko; empty_table (set (arm_global_pts (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 (PageDirectory pd))\<rparr>)
 3. \<And>s ko ao. \<lbrakk>valid_global_refs s; valid_arch_state s; obj_at (empty_table (set (arm_global_pts (arch_state s)))) p s \<longrightarrow> empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap); ko_at ko p s; a_type (ArchObj (PageDirectory pd)) = a_type ko; obj_at (empty_table (set (arm_global_pts (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 (arm_global_pts (arch_state s)))) (arm_global_pd (arch_state s)) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>)
 4. \<And>s ko ao. \<lbrakk>valid_global_refs s; valid_arch_state s; obj_at (empty_table (set (arm_global_pts (arch_state s)))) p s \<longrightarrow> empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap); ko_at ko p s; a_type (ArchObj (PageDirectory pd)) = a_type ko; obj_at (empty_table (set (arm_global_pts (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 (PageDirectory pd))\<rparr>) \<and> (\<forall>x. aligned_pte (pt x)) proof (prove)
goal (5 subgoals):
 1. \<And>s ao. \<lbrakk>valid_global_refs s; valid_arch_state s; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj ao); a_type (ArchObj (PageDirectory pd)) = a_type (ArchObj ao); empty_table (set (arm_global_pts (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)); valid_vspace_obj ao s; p = arm_global_pd (arch_state s); empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> valid_vspace_obj (PageDirectory pd) (s\<lparr>kheap := (kheap s)(arm_global_pd (arch_state s) \<mapsto> ArchObj (PageDirectory pd))\<rparr>)
 2. \<And>s ao. \<lbrakk>valid_global_refs s; valid_arch_state s; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj ao); a_type (ArchObj (PageDirectory pd)) = a_type (ArchObj ao); empty_table (set (arm_global_pts (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)); valid_vspace_obj ao s; p = arm_global_pd (arch_state s); \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> arm_global_pd (arch_state s) \<in> obj_refs cap\<rbrakk> \<Longrightarrow> valid_vspace_obj (PageDirectory pd) (s\<lparr>kheap := (kheap s)(arm_global_pd (arch_state s) \<mapsto> ArchObj (PageDirectory pd))\<rparr>)
 3. \<And>s ko ao. \<lbrakk>valid_global_refs s; valid_arch_state s; empty_table (set (arm_global_pts (arch_state s))) ko \<longrightarrow> empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap); kheap s p = Some ko; a_type (ArchObj (PageDirectory pd)) = a_type ko; empty_table (set (arm_global_pts (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 (PageDirectory pd))\<rparr>)
 4. \<And>s ko ao. \<lbrakk>valid_global_refs s; valid_arch_state s; obj_at (empty_table (set (arm_global_pts (arch_state s)))) p s \<longrightarrow> empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap); ko_at ko p s; a_type (ArchObj (PageDirectory pd)) = a_type ko; obj_at (empty_table (set (arm_global_pts (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 (arm_global_pts (arch_state s)))) (arm_global_pd (arch_state s)) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>)
 5. \<And>s ko ao. \<lbrakk>valid_global_refs s; valid_arch_state s; obj_at (empty_table (set (arm_global_pts (arch_state s)))) p s \<longrightarrow> empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap); ko_at ko p s; a_type (ArchObj (PageDirectory pd)) = a_type ko; obj_at (empty_table (set (arm_global_pts (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 (PageDirectory pd))\<rparr>) \<and> (\<forall>x. aligned_pte (pt x)) proof (prove)
goal (5 subgoals):
 1. \<And>s ao. \<lbrakk>valid_global_refs s; valid_arch_state s; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj ao); a_type (ArchObj (PageDirectory pd)) = a_type (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)); valid_vspace_obj ao s; p = arm_global_pd (arch_state s); valid_vspace_obj ao s; valid_vspace_obj (PageDirectory pd) s\<rbrakk> \<Longrightarrow> valid_vspace_obj (PageDirectory pd) (s\<lparr>kheap := (kheap s)(arm_global_pd (arch_state s) \<mapsto> ArchObj (PageDirectory pd))\<rparr>)
 2. \<And>s ao. \<lbrakk>valid_global_refs s; valid_arch_state s; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj ao); a_type (ArchObj (PageDirectory pd)) = a_type (ArchObj ao); empty_table (set (arm_global_pts (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)); valid_vspace_obj ao s; p = arm_global_pd (arch_state s); \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> arm_global_pd (arch_state s) \<in> obj_refs cap\<rbrakk> \<Longrightarrow> valid_vspace_obj (PageDirectory pd) (s\<lparr>kheap := (kheap s)(arm_global_pd (arch_state s) \<mapsto> ArchObj (PageDirectory pd))\<rparr>)
 3. \<And>s ko ao. \<lbrakk>valid_global_refs s; valid_arch_state s; empty_table (set (arm_global_pts (arch_state s))) ko \<longrightarrow> empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap); kheap s p = Some ko; a_type (ArchObj (PageDirectory pd)) = a_type ko; empty_table (set (arm_global_pts (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 (PageDirectory pd))\<rparr>)
 4. \<And>s ko ao. \<lbrakk>valid_global_refs s; valid_arch_state s; obj_at (empty_table (set (arm_global_pts (arch_state s)))) p s \<longrightarrow> empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap); ko_at ko p s; a_type (ArchObj (PageDirectory pd)) = a_type ko; obj_at (empty_table (set (arm_global_pts (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 (arm_global_pts (arch_state s)))) (arm_global_pd (arch_state s)) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>)
 5. \<And>s ko ao. \<lbrakk>valid_global_refs s; valid_arch_state s; obj_at (empty_table (set (arm_global_pts (arch_state s)))) p s \<longrightarrow> empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap); ko_at ko p s; a_type (ArchObj (PageDirectory pd)) = a_type ko; obj_at (empty_table (set (arm_global_pts (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 (PageDirectory pd))\<rparr>) \<and> (\<forall>x. aligned_pte (pt x)) proof (prove)
goal (4 subgoals):
 1. \<And>s ao. \<lbrakk>valid_global_refs s; valid_arch_state s; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj ao); a_type (ArchObj (PageDirectory pd)) = a_type (ArchObj ao); empty_table (set (arm_global_pts (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)); rec_arch_kernel_obj (\<lambda>pool s. \<forall>x\<in>ran pool. typ_at (AArch APageDirectory) x s) (\<lambda>pt s. \<forall>x. valid_pte (pt x) s) (\<lambda>pd s. \<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s) (\<lambda>dev sz _. True) ao s; p = arm_global_pd (arch_state s); \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> arm_global_pd (arch_state s) \<in> obj_refs cap\<rbrakk> \<Longrightarrow> \<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) (s\<lparr>kheap := (kheap s)(arm_global_pd (arch_state s) \<mapsto> ArchObj (PageDirectory pd))\<rparr>)
 2. \<And>s ko ao. \<lbrakk>valid_global_refs s; valid_arch_state s; empty_table (set (arm_global_pts (arch_state s))) ko \<longrightarrow> empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap); kheap s p = Some ko; a_type (ArchObj (PageDirectory pd)) = a_type ko; empty_table (set (arm_global_pts (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 (PageDirectory pd))\<rparr>)
 3. \<And>s ko ao. \<lbrakk>valid_global_refs s; valid_arch_state s; obj_at (empty_table (set (arm_global_pts (arch_state s)))) p s \<longrightarrow> empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap); ko_at ko p s; a_type (ArchObj (PageDirectory pd)) = a_type ko; obj_at (empty_table (set (arm_global_pts (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 (arm_global_pts (arch_state s)))) (arm_global_pd (arch_state s)) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>)
 4. \<And>s ko ao. \<lbrakk>valid_global_refs s; valid_arch_state s; obj_at (empty_table (set (arm_global_pts (arch_state s)))) p s \<longrightarrow> empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap); ko_at ko p s; a_type (ArchObj (PageDirectory pd)) = a_type ko; obj_at (empty_table (set (arm_global_pts (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 (PageDirectory pd))\<rparr>) \<and> (\<forall>x. aligned_pte (pt x)) proof (prove)
goal (4 subgoals):
 1. \<And>s ao x a b cap. \<lbrakk>valid_global_refs s; valid_arch_state s; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj ao); APageDirectory = (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); empty_table (set (arm_global_pts (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)); rec_arch_kernel_obj (\<lambda>pool s. \<forall>x\<in>ran pool. obj_at (\<lambda>ob. (case ob 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 APageDirectory) x s) (\<lambda>pt s. \<forall>x. valid_pte (pt x) s) (\<lambda>pd s. \<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s) (\<lambda>dev sz _. True) ao s; p = arm_global_pd (arch_state s); x \<notin> kernel_mapping_slots; caps_of_state s (a, b) = Some cap; arm_global_pd (arch_state s) \<in> obj_refs cap\<rbrakk> \<Longrightarrow> valid_pde (pd x) (s\<lparr>kheap := (kheap s)(arm_global_pd (arch_state s) \<mapsto> ArchObj (PageDirectory pd))\<rparr>)
 2. \<And>s ko ao. \<lbrakk>valid_global_refs s; valid_arch_state s; empty_table (set (arm_global_pts (arch_state s))) ko \<longrightarrow> empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap); kheap s p = Some ko; a_type (ArchObj (PageDirectory pd)) = a_type ko; empty_table (set (arm_global_pts (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 (PageDirectory pd))\<rparr>)
 3. \<And>s ko ao. \<lbrakk>valid_global_refs s; valid_arch_state s; obj_at (empty_table (set (arm_global_pts (arch_state s)))) p s \<longrightarrow> empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap); ko_at ko p s; a_type (ArchObj (PageDirectory pd)) = a_type ko; obj_at (empty_table (set (arm_global_pts (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 (arm_global_pts (arch_state s)))) (arm_global_pd (arch_state s)) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>)
 4. \<And>s ko ao. \<lbrakk>valid_global_refs s; valid_arch_state s; obj_at (empty_table (set (arm_global_pts (arch_state s)))) p s \<longrightarrow> empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap); ko_at ko p s; a_type (ArchObj (PageDirectory pd)) = a_type ko; obj_at (empty_table (set (arm_global_pts (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 (PageDirectory pd))\<rparr>) \<and> (\<forall>x. aligned_pte (pt x)) proof (prove)
goal (4 subgoals):
 1. \<And>s ao x a b cap. \<lbrakk>valid_global_refs s; valid_arch_state s; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj ao); APageDirectory = (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); empty_table (set (arm_global_pts (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)); rec_arch_kernel_obj (\<lambda>pool s. \<forall>x\<in>ran pool. obj_at (\<lambda>ob. (case ob 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 APageDirectory) x s) (\<lambda>pt s. \<forall>x. valid_pte (pt x) s) (\<lambda>pd s. \<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s) (\<lambda>dev sz _. True) ao s; p = arm_global_pd (arch_state s); x \<notin> kernel_mapping_slots; arm_global_pd (arch_state s) \<in> obj_refs cap; global_refs s \<inter> cap_range cap = {}\<rbrakk> \<Longrightarrow> valid_pde (pd x) (s\<lparr>kheap := (kheap s)(arm_global_pd (arch_state s) \<mapsto> ArchObj (PageDirectory pd))\<rparr>)
 2. \<And>s ko ao. \<lbrakk>valid_global_refs s; valid_arch_state s; empty_table (set (arm_global_pts (arch_state s))) ko \<longrightarrow> empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap); kheap s p = Some ko; a_type (ArchObj (PageDirectory pd)) = a_type ko; empty_table (set (arm_global_pts (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 (PageDirectory pd))\<rparr>)
 3. \<And>s ko ao. \<lbrakk>valid_global_refs s; valid_arch_state s; obj_at (empty_table (set (arm_global_pts (arch_state s)))) p s \<longrightarrow> empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap); ko_at ko p s; a_type (ArchObj (PageDirectory pd)) = a_type ko; obj_at (empty_table (set (arm_global_pts (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 (arm_global_pts (arch_state s)))) (arm_global_pd (arch_state s)) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>)
 4. \<And>s ko ao. \<lbrakk>valid_global_refs s; valid_arch_state s; obj_at (empty_table (set (arm_global_pts (arch_state s)))) p s \<longrightarrow> empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap); ko_at ko p s; a_type (ArchObj (PageDirectory pd)) = a_type ko; obj_at (empty_table (set (arm_global_pts (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 (PageDirectory pd))\<rparr>) \<and> (\<forall>x. aligned_pte (pt x)) proof (prove)
goal (3 subgoals):
 1. \<And>s ko ao. \<lbrakk>valid_global_refs s; valid_arch_state s; empty_table (set (arm_global_pts (arch_state s))) ko \<longrightarrow> empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap); kheap s p = Some ko; a_type (ArchObj (PageDirectory pd)) = a_type ko; empty_table (set (arm_global_pts (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 (PageDirectory pd))\<rparr>)
 2. \<And>s ko ao. \<lbrakk>valid_global_refs s; valid_arch_state s; obj_at (empty_table (set (arm_global_pts (arch_state s)))) p s \<longrightarrow> empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap); ko_at ko p s; a_type (ArchObj (PageDirectory pd)) = a_type ko; obj_at (empty_table (set (arm_global_pts (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 (arm_global_pts (arch_state s)))) (arm_global_pd (arch_state s)) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>)
 3. \<And>s ko ao. \<lbrakk>valid_global_refs s; valid_arch_state s; obj_at (empty_table (set (arm_global_pts (arch_state s)))) p s \<longrightarrow> empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap); ko_at ko p s; a_type (ArchObj (PageDirectory pd)) = a_type ko; obj_at (empty_table (set (arm_global_pts (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 (PageDirectory pd))\<rparr>) \<and> (\<forall>x. aligned_pte (pt x)) proof (prove)
goal (2 subgoals):
 1. \<And>s ko ao. \<lbrakk>valid_global_refs s; valid_arch_state s; obj_at (empty_table (set (arm_global_pts (arch_state s)))) p s \<longrightarrow> empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap); ko_at ko p s; a_type (ArchObj (PageDirectory pd)) = a_type ko; obj_at (empty_table (set (arm_global_pts (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 (arm_global_pts (arch_state s)))) (arm_global_pd (arch_state s)) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>)
 2. \<And>s ko ao. \<lbrakk>valid_global_refs s; valid_arch_state s; obj_at (empty_table (set (arm_global_pts (arch_state s)))) p s \<longrightarrow> empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap); ko_at ko p s; a_type (ArchObj (PageDirectory pd)) = a_type ko; obj_at (empty_table (set (arm_global_pts (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 (PageDirectory pd))\<rparr>) \<and> (\<forall>x. aligned_pte (pt x)) proof (prove)
goal (2 subgoals):
 1. \<And>s ko ao. \<lbrakk>valid_global_refs s; valid_arch_state s; obj_at (empty_table (set (arm_global_pts (arch_state s)))) p s \<longrightarrow> empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap); ko_at ko p s; AArch APageDirectory = (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)); obj_at (empty_table (set (arm_global_pts (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 (arm_global_pts (arch_state s)))) (arm_global_pd (arch_state s)) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>)
 2. \<And>s ko ao. \<lbrakk>valid_global_refs s; valid_arch_state s; obj_at (empty_table (set (arm_global_pts (arch_state s)))) p s \<longrightarrow> empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap); ko_at ko p s; a_type (ArchObj (PageDirectory pd)) = a_type ko; obj_at (empty_table (set (arm_global_pts (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 (PageDirectory pd))\<rparr>) \<and> (\<forall>x. aligned_pte (pt x)) proof (prove)
goal (2 subgoals):
 1. \<And>s ao a b cap. \<lbrakk>valid_global_refs s; valid_arch_state s; APageDirectory = (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); empty_table (set (arm_global_pts (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 = arm_global_pd (arch_state s); caps_of_state s (a, b) = Some cap; arm_global_pd (arch_state s) \<in> obj_refs cap\<rbrakk> \<Longrightarrow> empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory pd))
 2. \<And>s ko ao. \<lbrakk>valid_global_refs s; valid_arch_state s; obj_at (empty_table (set (arm_global_pts (arch_state s)))) p s \<longrightarrow> empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap); ko_at ko p s; a_type (ArchObj (PageDirectory pd)) = a_type ko; obj_at (empty_table (set (arm_global_pts (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 (PageDirectory pd))\<rparr>) \<and> (\<forall>x. aligned_pte (pt x)) proof (prove)
goal (2 subgoals):
 1. \<And>s ao a b cap. \<lbrakk>valid_global_refs s; valid_arch_state s; APageDirectory = (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); empty_table (set (arm_global_pts (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 = arm_global_pd (arch_state s); arm_global_pd (arch_state s) \<in> obj_refs cap; global_refs s \<inter> cap_range cap = {}\<rbrakk> \<Longrightarrow> empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory pd))
 2. \<And>s ko ao. \<lbrakk>valid_global_refs s; valid_arch_state s; obj_at (empty_table (set (arm_global_pts (arch_state s)))) p s \<longrightarrow> empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap); ko_at ko p s; a_type (ArchObj (PageDirectory pd)) = a_type ko; obj_at (empty_table (set (arm_global_pts (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 (PageDirectory pd))\<rparr>) \<and> (\<forall>x. aligned_pte (pt x)) proof (prove)
goal (1 subgoal):
 1. \<And>s ko ao. \<lbrakk>valid_global_refs s; valid_arch_state s; obj_at (empty_table (set (arm_global_pts (arch_state s)))) p s \<longrightarrow> empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap); ko_at ko p s; a_type (ArchObj (PageDirectory pd)) = a_type ko; obj_at (empty_table (set (arm_global_pts (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 (PageDirectory pd))\<rparr>) \<and> (\<forall>x. aligned_pte (pt x)) proof (prove)
goal (1 subgoal):
 1. \<And>s ko ao pa. \<lbrakk>valid_global_refs s; valid_arch_state s; obj_at (empty_table (set (arm_global_pts (arch_state s)))) p s \<longrightarrow> empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap); ko_at ko p s; a_type (ArchObj (PageDirectory pd)) = a_type ko; obj_at (empty_table (set (arm_global_pts (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; pa \<in> set (arm_global_pts (arch_state s))\<rbrakk> \<Longrightarrow> \<exists>pt. ako_at (PageTable pt) pa (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>) \<and> (\<forall>x. aligned_pte (pt x)) proof (prove)
goal (1 subgoal):
 1. \<And>s ko ao. \<lbrakk>valid_global_refs s; valid_arch_state s; empty_table (set (arm_global_pts (arch_state s))) ko \<longrightarrow> empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap); kheap s p = Some ko; a_type (ArchObj (PageDirectory pd)) = a_type ko; empty_table (set (arm_global_pts (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:
No subgoals!