theory ArchVSpace_AI

lemma set_pd_valid_arch_caps:
  "\<lbrace>valid_arch_caps and valid_arch_state and valid_vspace_objs and
    valid_objs and
    obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory pd)) =
                 vs_refs ko - T \<union> S) p and
    obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory pd)) =
                 vs_refs_pages ko - T' \<union> S') p and
    (\<lambda>s. \<forall>x\<in>S. page_table_at (snd x) s) and
    (\<lambda>s. \<forall>p. (VSRef 0 (Some AASIDPool), p) \<notin> S) and
    (\<lambda>s. \<forall>(r, p')\<in>S. \<forall>ao. (\<exists>\<rhd> p) s \<longrightarrow>
                           ko_at (ArchObj ao) p' s \<longrightarrow> valid_vspace_obj ao s) and
    (\<lambda>s. (\<exists>\<rhd> p) s \<longrightarrow> valid_vspace_obj (PageDirectory pd) s) and
    (\<lambda>s. (\<exists>p' cap. caps_of_state s p' = Some cap \<and> is_pd_cap cap \<and>
                   p \<in> obj_refs cap \<and> cap_asid cap \<noteq> None)
       \<or> (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)))) and
    (\<lambda>s. \<forall>r. (r \<unrhd> p) s \<longrightarrow>
             (\<forall>c\<in>- kernel_mapping_slots. \<forall>q.
                 pde_ref_pages (pd c) = Some q \<longrightarrow>
                    (\<exists>p' cap. caps_of_state s p' = Some cap \<and>
                         q \<in> obj_refs cap \<and> vs_cap_ref cap =
         Some (VSRef (ucast c) (Some APageDirectory) # r)))) and
    (\<lambda>s. \<forall>r. (r \<unrhd> p) s \<longrightarrow>
             (\<forall>c\<in>- kernel_mapping_slots. \<forall>q.
                 pde_ref (pd c) = Some q \<longrightarrow>
                    (\<forall>q' pt d. ko_at (ArchObj (PageTable pt)) q s \<longrightarrow>
                        pte_ref_pages (pt d) = Some q' \<longrightarrow>
                        (\<exists>p' cap. caps_of_state s p' = Some cap \<and>
                                  q' \<in> obj_refs cap \<and> vs_cap_ref cap =
         Some (VSRef (ucast d) (Some APageTable) #
               VSRef (ucast c) (Some APageDirectory) # r)))))\<rbrace>
   set_pd p pd
   \<lbrace>\<lambda>rv. valid_arch_caps\<rbrace>" apply (simp add: set_pd_def set_object_def) apply (wp get_object_wp) apply (clarsimp simp: obj_at_def a_type_simps  simp del: fun_upd_apply
                 split: Structures_A.kernel_object.splits arch_kernel_obj.splits) apply (clarsimp simp: valid_arch_caps_def) apply (subst caps_of_state_after_update[folded fun_upd_def],
         simp add: obj_at_def)+ apply simp apply (rule conjI) using set_pd_valid_vs_lookup_map[where p=p and pd=pd and T=T and S=S
      and T'=T' and S'=S'] apply (clarsimp simp add: valid_def) apply (drule_tac x=s in spec) apply (simp add: simpler_set_pd_def obj_at_def) apply (simp add: valid_table_caps_def obj_at_def
                   caps_of_state_after_update[folded fun_upd_def]
              del: imp_disjL) apply (drule_tac x=p in spec, elim allEI, intro impI) apply clarsimp apply (erule_tac P="is_pd_cap cap" in disjE) prefer 2 apply (frule_tac p="(a,b)" in caps_of_state_valid_cap, simp) apply (clarsimp simp add: is_pt_cap_def valid_cap_def obj_at_def
                             valid_arch_cap_def
                             a_type_def) apply (frule_tac cap=cap and cap'=capa and cs="caps_of_state s" in unique_table_caps_pdD) apply (simp add: is_pd_cap_def)+ apply (clarsimp simp: is_pd_cap_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_caps and valid_arch_state and valid_vspace_objs and valid_objs and obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory pd)) = vs_refs ko - T \<union> S) p and obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages ko - T' \<union> S') p and (\<lambda>s. \<forall>x\<in>S. typ_at (AArch APageTable) (snd x) s) and (\<lambda>s. \<forall>p. (VSRef 0 (Some AASIDPool), p) \<notin> S) and (\<lambda>s. \<forall>(r, p')\<in>S. \<forall>ao. (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> ako_at ao p' s \<longrightarrow> valid_vspace_obj ao s) and (\<lambda>s. (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> valid_vspace_obj (PageDirectory pd) s) and (\<lambda>s. (\<exists>p' cap. caps_of_state s p' = Some cap \<and> is_pd_cap cap \<and> p \<in> obj_refs cap \<and> cap_asid cap \<noteq> None) \<or> (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)))) and (\<lambda>s. \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref_pages (pd c) = Some q \<longrightarrow> (\<exists>p' cap. caps_of_state s p' = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)))) and (\<lambda>s. \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt d. ako_at (PageTable pt) q s \<longrightarrow> pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>p' cap. caps_of_state s p' = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)))))\<rbrace> set_pd p pd \<lbrace>\<lambda>rv. valid_arch_caps\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_caps and valid_arch_state and valid_vspace_objs and valid_objs and obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory pd)) = vs_refs ko - T \<union> S) p and obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages ko - T' \<union> S') p and (\<lambda>s. \<forall>x\<in>S. typ_at (AArch APageTable) (snd x) s) and (\<lambda>s. \<forall>p. (VSRef 0 (Some AASIDPool), p) \<notin> S) and (\<lambda>s. \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p' s \<longrightarrow> valid_vspace_obj ao s)) and (\<lambda>s. (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s)) and (\<lambda>s. obj_at (empty_table (set (second_level_tables (arch_state s)))) p s \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pd_cap cap \<and> p \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<or> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd))) and (\<lambda>s. \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref_pages (pd c) = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)))) and (\<lambda>s. \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. ako_at (PageTable pt) q s \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))))))\<rbrace> do kobj <- get_object p;
y <- assert (a_type kobj = a_type (ArchObj (PageDirectory pd)));
s <- get;
put (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>)
od \<lbrace>\<lambda>rv. valid_arch_caps\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_arch_caps and valid_arch_state and valid_vspace_objs and valid_objs and obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory pd)) = vs_refs ko - T \<union> S) p and obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages ko - T' \<union> S') p and (\<lambda>s. \<forall>x\<in>S. typ_at (AArch APageTable) (snd x) s) and (\<lambda>s. \<forall>p. (VSRef 0 (Some AASIDPool), p) \<notin> S) and (\<lambda>s. \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p' s \<longrightarrow> valid_vspace_obj ao s)) and (\<lambda>s. (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s)) and (\<lambda>s. obj_at (empty_table (set (second_level_tables (arch_state s)))) p s \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pd_cap cap \<and> p \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<or> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd))) and (\<lambda>s. \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref_pages (pd c) = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)))) and (\<lambda>s. \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. ako_at (PageTable pt) q s \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))))))) s \<Longrightarrow> \<forall>ko. ko_at ko p s \<longrightarrow> a_type ko = a_type (ArchObj (PageDirectory pd)) \<longrightarrow> valid_arch_caps (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s pda. \<lbrakk>valid_arch_caps s; valid_arch_state s; valid_vspace_objs s; valid_objs s; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pda)) - T' \<union> S'; \<forall>p. (VSRef 0 (Some AASIDPool), p) \<notin> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pd_cap cap \<and> p \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<or> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref_pages (pd c) = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))))); kheap s p = Some (ArchObj (PageDirectory pda))\<rbrakk> \<Longrightarrow> valid_arch_caps (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s pda. \<lbrakk>valid_arch_state s; valid_vspace_objs s; valid_objs s; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pda)) - T' \<union> S'; \<forall>p. (VSRef 0 (Some AASIDPool), p) \<notin> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pd_cap cap \<and> p \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<or> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref_pages (pd c) = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))))); kheap s p = Some (ArchObj (PageDirectory pda)); valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s)\<rbrakk> \<Longrightarrow> valid_vs_lookup (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>) \<and> valid_table_caps (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>) \<and> unique_table_caps (caps_of_state (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>)) \<and> unique_table_refs (caps_of_state (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s pda. \<lbrakk>valid_arch_state s; valid_vspace_objs s; valid_objs s; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pda)) - T' \<union> S'; \<forall>p. (VSRef 0 (Some AASIDPool), p) \<notin> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pd_cap cap \<and> p \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<or> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref_pages (pd c) = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))))); kheap s p = Some (ArchObj (PageDirectory pda)); valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s)\<rbrakk> \<Longrightarrow> valid_vs_lookup (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>) \<and> valid_table_caps (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>) \<and> unique_table_caps (caps_of_state s) \<and> unique_table_refs (caps_of_state s) proof (prove)
goal (1 subgoal):
 1. \<And>s pda. \<lbrakk>valid_arch_state s; valid_vspace_objs s; valid_objs s; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pda)) - T' \<union> S'; \<forall>p. (VSRef 0 (Some AASIDPool), p) \<notin> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pd_cap cap \<and> p \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<or> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref_pages (pd c) = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))))); kheap s p = Some (ArchObj (PageDirectory pda)); valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s)\<rbrakk> \<Longrightarrow> valid_vs_lookup (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>) \<and> valid_table_caps (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s pda. \<lbrakk>valid_arch_state s; valid_vspace_objs s; valid_objs s; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pda)) - T' \<union> S'; \<forall>p. (VSRef 0 (Some AASIDPool), p) \<notin> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pd_cap cap \<and> p \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<or> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref_pages (pd c) = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))))); kheap s p = Some (ArchObj (PageDirectory pda)); valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s)\<rbrakk> \<Longrightarrow> valid_vs_lookup (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>)
 2. \<And>s pda. \<lbrakk>valid_arch_state s; valid_vspace_objs s; valid_objs s; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pda)) - T' \<union> S'; \<forall>p. (VSRef 0 (Some AASIDPool), p) \<notin> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pd_cap cap \<and> p \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<or> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref_pages (pd c) = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))))); kheap s p = Some (ArchObj (PageDirectory pda)); valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s)\<rbrakk> \<Longrightarrow> valid_table_caps (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>) proof (prove)
using this:
\<lbrace>valid_vs_lookup and valid_arch_state and valid_vspace_objs and obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory pd)) = vs_refs ko - T \<union> S) p and (\<lambda>s. \<forall>x\<in>S. typ_at (AArch APageTable) (snd x) s) and obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages ko - T' \<union> S') p and (\<lambda>s. \<forall>(r, p')\<in>S. \<forall>ao. (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> ako_at ao p' s \<longrightarrow> valid_vspace_obj ao s) and (\<lambda>s. (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> valid_vspace_obj (PageDirectory pd) s) and (\<lambda>s. \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref_pages (pd c) = Some q \<longrightarrow> (\<exists>p' cap. caps_of_state s p' = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)))) and (\<lambda>s. \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt d. ako_at (PageTable pt) q s \<longrightarrow> pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>p' cap. caps_of_state s p' = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)))))\<rbrace> set_pd p pd \<lbrace>\<lambda>rv. valid_vs_lookup\<rbrace>

goal (2 subgoals):
 1. \<And>s pda. \<lbrakk>valid_arch_state s; valid_vspace_objs s; valid_objs s; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pda)) - T' \<union> S'; \<forall>p. (VSRef 0 (Some AASIDPool), p) \<notin> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pd_cap cap \<and> p \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<or> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref_pages (pd c) = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))))); kheap s p = Some (ArchObj (PageDirectory pda)); valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s)\<rbrakk> \<Longrightarrow> valid_vs_lookup (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>)
 2. \<And>s pda. \<lbrakk>valid_arch_state s; valid_vspace_objs s; valid_objs s; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pda)) - T' \<union> S'; \<forall>p. (VSRef 0 (Some AASIDPool), p) \<notin> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pd_cap cap \<and> p \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<or> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref_pages (pd c) = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))))); kheap s p = Some (ArchObj (PageDirectory pda)); valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s)\<rbrakk> \<Longrightarrow> valid_table_caps (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s pda. \<lbrakk>valid_arch_state s; valid_vspace_objs s; valid_objs s; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pda)) - T' \<union> S'; \<forall>p. (VSRef 0 (Some AASIDPool), p) \<notin> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pd_cap cap \<and> p \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<or> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref_pages (pd c) = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))))); kheap s p = Some (ArchObj (PageDirectory pda)); valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); \<forall>s. valid_vs_lookup s \<and> valid_arch_state s \<and> valid_vspace_objs s \<and> obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory pda)) - T \<union> S = vs_refs ko - T \<union> S) p s \<and> (\<forall>x\<in>S. typ_at (AArch APageTable) (snd x) s) \<and> obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory pda)) - T' \<union> S' = vs_refs_pages ko - T' \<union> S') p s \<and> (\<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p' s \<longrightarrow> valid_vspace_obj ao s)) \<and> ((\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s)) \<and> (\<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref_pages (pd c) = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)))) \<and> (\<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. ako_at (PageTable pt) q s \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)))))) \<longrightarrow> (\<forall>x\<in>fst (set_pd p pd s). case x of (r, s') \<Rightarrow> valid_vs_lookup s')\<rbrakk> \<Longrightarrow> valid_vs_lookup (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>)
 2. \<And>s pda. \<lbrakk>valid_arch_state s; valid_vspace_objs s; valid_objs s; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pda)) - T' \<union> S'; \<forall>p. (VSRef 0 (Some AASIDPool), p) \<notin> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pd_cap cap \<and> p \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<or> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref_pages (pd c) = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))))); kheap s p = Some (ArchObj (PageDirectory pda)); valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s)\<rbrakk> \<Longrightarrow> valid_table_caps (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s pda. \<lbrakk>valid_arch_state s; valid_vspace_objs s; valid_objs s; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pda)) - T' \<union> S'; \<forall>p. (VSRef 0 (Some AASIDPool), p) \<notin> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pd_cap cap \<and> p \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<or> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref_pages (pd c) = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))))); kheap s p = Some (ArchObj (PageDirectory pda)); valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_vs_lookup s \<and> valid_arch_state s \<and> valid_vspace_objs s \<and> obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory pda)) - T \<union> S = vs_refs ko - T \<union> S) p s \<and> (\<forall>x\<in>S. typ_at (AArch APageTable) (snd x) s) \<and> obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory pda)) - T' \<union> S' = vs_refs_pages ko - T' \<union> S') p s \<and> (\<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p' s \<longrightarrow> valid_vspace_obj ao s)) \<and> ((\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s)) \<and> (\<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref_pages (pd c) = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)))) \<and> (\<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. ako_at (PageTable pt) q s \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)))))) \<longrightarrow> (\<forall>x\<in>fst (set_pd p pd s). case x of (r, s') \<Rightarrow> valid_vs_lookup s')\<rbrakk> \<Longrightarrow> valid_vs_lookup (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>)
 2. \<And>s pda. \<lbrakk>valid_arch_state s; valid_vspace_objs s; valid_objs s; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pda)) - T' \<union> S'; \<forall>p. (VSRef 0 (Some AASIDPool), p) \<notin> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pd_cap cap \<and> p \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<or> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref_pages (pd c) = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))))); kheap s p = Some (ArchObj (PageDirectory pda)); valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s)\<rbrakk> \<Longrightarrow> valid_table_caps (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s pda. \<lbrakk>valid_arch_state s; valid_vspace_objs s; valid_objs s; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pda)) - T' \<union> S'; \<forall>p. (VSRef 0 (Some AASIDPool), p) \<notin> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pd_cap cap \<and> p \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<or> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref_pages (pd c) = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))))); kheap s p = Some (ArchObj (PageDirectory pda)); valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s)\<rbrakk> \<Longrightarrow> valid_table_caps (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s pda. \<lbrakk>valid_arch_state s; valid_vspace_objs s; valid_objs s; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pda)) - T' \<union> S'; \<forall>p. (VSRef 0 (Some AASIDPool), p) \<notin> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pd_cap cap \<and> p \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<or> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref_pages (pd c) = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))))); kheap s p = Some (ArchObj (PageDirectory pda)); valid_vs_lookup s; \<forall>r a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> is_pd_cap cap \<or> is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> (\<exists>ko. kheap s r = Some ko \<and> empty_table (set (second_level_tables (arch_state s))) ko); unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s)\<rbrakk> \<Longrightarrow> \<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> is_pd_cap cap \<or> is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> p \<in> obj_refs cap \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)) proof (prove)
goal (1 subgoal):
 1. \<And>s pda a b cap. \<lbrakk>valid_arch_state s; valid_vspace_objs s; valid_objs s; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pda)) - T' \<union> S'; \<forall>p. (VSRef 0 (Some AASIDPool), p) \<notin> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pd_cap cap \<and> p \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<or> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref_pages (pd c) = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))))); kheap s p = Some (ArchObj (PageDirectory pda)); valid_vs_lookup s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); caps_of_state s (a, b) = Some cap \<longrightarrow> is_pd_cap cap \<or> is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> p \<in> obj_refs cap \<longrightarrow> (\<exists>ko. kheap s p = Some ko \<and> empty_table (set (second_level_tables (arch_state s))) ko); caps_of_state s (a, b) = Some cap; is_pd_cap cap \<or> is_pt_cap cap; cap_asid cap = None; p \<in> obj_refs cap\<rbrakk> \<Longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)) proof (prove)
goal (1 subgoal):
 1. \<And>s pda a b cap aa ba capa y. \<lbrakk>valid_arch_state s; valid_vspace_objs s; valid_objs s; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pda)) - T' \<union> S'; \<forall>p. (VSRef 0 (Some AASIDPool), p) \<notin> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref_pages (pd c) = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))))); kheap s p = Some (ArchObj (PageDirectory pda)); valid_vs_lookup s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); caps_of_state s (a, b) = Some cap; is_pd_cap cap \<or> is_pt_cap cap; cap_asid cap = None; p \<in> obj_refs cap; caps_of_state s (aa, ba) = Some capa; is_pd_cap capa; p \<in> obj_refs capa; cap_asid capa = Some y\<rbrakk> \<Longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)) proof (prove)
goal (2 subgoals):
 1. \<And>s pda a b cap aa ba capa y. \<lbrakk>valid_arch_state s; valid_vspace_objs s; valid_objs s; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pda)) - T' \<union> S'; \<forall>p. (VSRef 0 (Some AASIDPool), p) \<notin> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref_pages (pd c) = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))))); kheap s p = Some (ArchObj (PageDirectory pda)); valid_vs_lookup s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); caps_of_state s (a, b) = Some cap; cap_asid cap = None; p \<in> obj_refs cap; caps_of_state s (aa, ba) = Some capa; is_pd_cap capa; p \<in> obj_refs capa; cap_asid capa = Some y; is_pd_cap cap\<rbrakk> \<Longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd))
 2. \<And>s pda a b cap aa ba capa y. \<lbrakk>valid_arch_state s; valid_vspace_objs s; valid_objs s; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pda)) - T' \<union> S'; \<forall>p. (VSRef 0 (Some AASIDPool), p) \<notin> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref_pages (pd c) = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))))); kheap s p = Some (ArchObj (PageDirectory pda)); valid_vs_lookup s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); caps_of_state s (a, b) = Some cap; cap_asid cap = None; p \<in> obj_refs cap; caps_of_state s (aa, ba) = Some capa; is_pd_cap capa; p \<in> obj_refs capa; cap_asid capa = Some y; is_pt_cap cap\<rbrakk> \<Longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)) proof (prove)
goal (2 subgoals):
 1. \<And>s pda a b cap aa ba capa y. \<lbrakk>valid_arch_state s; valid_vspace_objs s; valid_objs s; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pda)) - T' \<union> S'; \<forall>p. (VSRef 0 (Some AASIDPool), p) \<notin> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref_pages (pd c) = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))))); kheap s p = Some (ArchObj (PageDirectory pda)); valid_vs_lookup s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); caps_of_state s (a, b) = Some cap; cap_asid cap = None; p \<in> obj_refs cap; caps_of_state s (aa, ba) = Some capa; is_pd_cap capa; p \<in> obj_refs capa; cap_asid capa = Some y; is_pt_cap cap\<rbrakk> \<Longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd))
 2. \<And>s pda a b cap aa ba capa y. \<lbrakk>valid_arch_state s; valid_vspace_objs s; valid_objs s; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pda)) - T' \<union> S'; \<forall>p. (VSRef 0 (Some AASIDPool), p) \<notin> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref_pages (pd c) = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))))); kheap s p = Some (ArchObj (PageDirectory pda)); valid_vs_lookup s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); caps_of_state s (a, b) = Some cap; cap_asid cap = None; p \<in> obj_refs cap; caps_of_state s (aa, ba) = Some capa; is_pd_cap capa; p \<in> obj_refs capa; cap_asid capa = Some y; is_pd_cap cap\<rbrakk> \<Longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)) proof (prove)
goal (2 subgoals):
 1. \<And>s pda a b cap aa ba capa y. \<lbrakk>valid_arch_state s; valid_vspace_objs s; valid_objs s; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pda)) - T' \<union> S'; \<forall>p. (VSRef 0 (Some AASIDPool), p) \<notin> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref_pages (pd c) = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))))); kheap s p = Some (ArchObj (PageDirectory pda)); valid_vs_lookup s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); caps_of_state s (a, b) = Some cap; cap_asid cap = None; p \<in> obj_refs cap; caps_of_state s (aa, ba) = Some capa; is_pd_cap capa; p \<in> obj_refs capa; cap_asid capa = Some y; is_pt_cap cap; s \<turnstile> cap\<rbrakk> \<Longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd))
 2. \<And>s pda a b cap aa ba capa y. \<lbrakk>valid_arch_state s; valid_vspace_objs s; valid_objs s; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pda)) - T' \<union> S'; \<forall>p. (VSRef 0 (Some AASIDPool), p) \<notin> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref_pages (pd c) = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))))); kheap s p = Some (ArchObj (PageDirectory pda)); valid_vs_lookup s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); caps_of_state s (a, b) = Some cap; cap_asid cap = None; p \<in> obj_refs cap; caps_of_state s (aa, ba) = Some capa; is_pd_cap capa; p \<in> obj_refs capa; cap_asid capa = Some y; is_pd_cap cap\<rbrakk> \<Longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)) proof (prove)
goal (1 subgoal):
 1. \<And>s pda a b cap aa ba capa y. \<lbrakk>valid_arch_state s; valid_vspace_objs s; valid_objs s; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pda)) - T' \<union> S'; \<forall>p. (VSRef 0 (Some AASIDPool), p) \<notin> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref_pages (pd c) = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))))); kheap s p = Some (ArchObj (PageDirectory pda)); valid_vs_lookup s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); caps_of_state s (a, b) = Some cap; cap_asid cap = None; p \<in> obj_refs cap; caps_of_state s (aa, ba) = Some capa; is_pd_cap capa; p \<in> obj_refs capa; cap_asid capa = Some y; is_pd_cap cap\<rbrakk> \<Longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)) proof (prove)
goal (7 subgoals):
 1. \<And>s pda a b cap aa ba capa y. \<lbrakk>valid_arch_state s; valid_vspace_objs s; valid_objs s; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pda)) - T' \<union> S'; \<forall>p. (VSRef 0 (Some AASIDPool), p) \<notin> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref_pages (pd c) = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))))); kheap s p = Some (ArchObj (PageDirectory pda)); valid_vs_lookup s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); caps_of_state s (a, b) = Some cap; cap_asid cap = None; p \<in> obj_refs cap; caps_of_state s (aa, ba) = Some capa; is_pd_cap capa; p \<in> obj_refs capa; cap_asid capa = Some y; is_pd_cap cap\<rbrakk> \<Longrightarrow> cap_asid cap = None
 2. \<And>s pda a b cap aa ba capa y. \<lbrakk>valid_arch_state s; valid_vspace_objs s; valid_objs s; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pda)) - T' \<union> S'; \<forall>p. (VSRef 0 (Some AASIDPool), p) \<notin> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref_pages (pd c) = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))))); kheap s p = Some (ArchObj (PageDirectory pda)); valid_vs_lookup s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); caps_of_state s (a, b) = Some cap; cap_asid cap = None; p \<in> obj_refs cap; caps_of_state s (aa, ba) = Some capa; is_pd_cap capa; p \<in> obj_refs capa; cap_asid capa = Some y; is_pd_cap cap\<rbrakk> \<Longrightarrow> caps_of_state s (?p'111 s pda a b cap aa ba capa y) = Some capa
 3. \<And>s pda a b cap aa ba capa y. \<lbrakk>valid_arch_state s; valid_vspace_objs s; valid_objs s; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pda)) - T' \<union> S'; \<forall>p. (VSRef 0 (Some AASIDPool), p) \<notin> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref_pages (pd c) = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))))); kheap s p = Some (ArchObj (PageDirectory pda)); valid_vs_lookup s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); caps_of_state s (a, b) = Some cap; cap_asid cap = None; p \<in> obj_refs cap; caps_of_state s (aa, ba) = Some capa; is_pd_cap capa; p \<in> obj_refs capa; cap_asid capa = Some y; is_pd_cap cap\<rbrakk> \<Longrightarrow> is_pd_cap cap
 4. \<And>s pda a b cap aa ba capa y. \<lbrakk>valid_arch_state s; valid_vspace_objs s; valid_objs s; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pda)) - T' \<union> S'; \<forall>p. (VSRef 0 (Some AASIDPool), p) \<notin> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref_pages (pd c) = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))))); kheap s p = Some (ArchObj (PageDirectory pda)); valid_vs_lookup s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); caps_of_state s (a, b) = Some cap; cap_asid cap = None; p \<in> obj_refs cap; caps_of_state s (aa, ba) = Some capa; is_pd_cap capa; p \<in> obj_refs capa; cap_asid capa = Some y; is_pd_cap cap\<rbrakk> \<Longrightarrow> is_pd_cap capa
 5. \<And>s pda a b cap aa ba capa y. \<lbrakk>valid_arch_state s; valid_vspace_objs s; valid_objs s; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pda)) - T' \<union> S'; \<forall>p. (VSRef 0 (Some AASIDPool), p) \<notin> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref_pages (pd c) = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))))); kheap s p = Some (ArchObj (PageDirectory pda)); valid_vs_lookup s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); caps_of_state s (a, b) = Some cap; cap_asid cap = None; p \<in> obj_refs cap; caps_of_state s (aa, ba) = Some capa; is_pd_cap capa; p \<in> obj_refs capa; cap_asid capa = Some y; is_pd_cap cap\<rbrakk> \<Longrightarrow> obj_refs capa = obj_refs cap
 6. \<And>s pda a b cap aa ba capa y. \<lbrakk>valid_arch_state s; valid_vspace_objs s; valid_objs s; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pda)) - T' \<union> S'; \<forall>p. (VSRef 0 (Some AASIDPool), p) \<notin> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref_pages (pd c) = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))))); kheap s p = Some (ArchObj (PageDirectory pda)); valid_vs_lookup s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); caps_of_state s (a, b) = Some cap; cap_asid cap = None; p \<in> obj_refs cap; caps_of_state s (aa, ba) = Some capa; is_pd_cap capa; p \<in> obj_refs capa; cap_asid capa = Some y; is_pd_cap cap\<rbrakk> \<Longrightarrow> unique_table_caps (caps_of_state s)
 7. \<And>s pda a b cap aa ba capa y. \<lbrakk>valid_arch_state s; valid_vspace_objs s; valid_objs s; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pda)) - T' \<union> S'; \<forall>p. (VSRef 0 (Some AASIDPool), p) \<notin> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref_pages (pd c) = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))))); kheap s p = Some (ArchObj (PageDirectory pda)); valid_vs_lookup s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); caps_of_state s (a, b) = Some cap; cap_asid cap = None; p \<in> obj_refs cap; caps_of_state s (aa, ba) = Some capa; is_pd_cap capa; p \<in> obj_refs capa; cap_asid capa = Some y; is_pd_cap cap; (a, b) = ?p'111 s pda a b cap aa ba capa y\<rbrakk> \<Longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)) proof (prove)
goal (3 subgoals):
 1. \<And>s pda a b cap aa ba capa y. \<lbrakk>valid_arch_state s; valid_vspace_objs s; valid_objs s; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pda)) - T' \<union> S'; \<forall>p. (VSRef 0 (Some AASIDPool), p) \<notin> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref_pages (pd c) = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))))); kheap s p = Some (ArchObj (PageDirectory pda)); valid_vs_lookup s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); caps_of_state s (a, b) = Some cap; cap_asid cap = None; p \<in> obj_refs cap; caps_of_state s (aa, ba) = Some capa; \<exists>p asid. capa = ArchObjectCap (PageDirectoryCap p asid); p \<in> obj_refs capa; cap_asid capa = Some y; \<exists>p asid. cap = ArchObjectCap (PageDirectoryCap p asid)\<rbrakk> \<Longrightarrow> obj_refs capa = obj_refs cap
 2. \<And>s pda a b cap aa ba capa y. \<lbrakk>valid_arch_state s; valid_vspace_objs s; valid_objs s; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pda)) - T' \<union> S'; \<forall>p. (VSRef 0 (Some AASIDPool), p) \<notin> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref_pages (pd c) = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))))); kheap s p = Some (ArchObj (PageDirectory pda)); valid_vs_lookup s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); caps_of_state s (a, b) = Some cap; cap_asid cap = None; p \<in> obj_refs cap; caps_of_state s (aa, ba) = Some capa; is_pd_cap capa; p \<in> obj_refs capa; cap_asid capa = Some y; is_pd_cap cap\<rbrakk> \<Longrightarrow> unique_table_caps (caps_of_state s)
 3. \<And>s pda a b cap aa ba capa y. \<lbrakk>valid_arch_state s; valid_vspace_objs s; valid_objs s; vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pda)) - T \<union> S; \<forall>x\<in>S. \<exists>ko. kheap s (snd x) = Some ko \<and> a_type ko = AArch APageTable; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pda)) - T' \<union> S'; \<forall>p. (VSRef 0 (Some AASIDPool), p) \<notin> S; \<forall>x\<in>S. case x of (r, p') \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p' = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref_pages (pd c) = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))); \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r))))); kheap s p = Some (ArchObj (PageDirectory pda)); valid_vs_lookup s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); caps_of_state s (a, b) = Some cap; cap_asid cap = None; p \<in> obj_refs cap; caps_of_state s (aa, ba) = Some capa; is_pd_cap capa; p \<in> obj_refs capa; cap_asid capa = Some y; is_pd_cap cap; (a, b) = (aa, ba)\<rbrakk> \<Longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)) proof (prove)
goal:
No subgoals!