theory ArchAcc_AI

lemma set_pt_table_caps [wp]:
  "\<lbrace>valid_table_caps and (\<lambda>s. valid_caps (caps_of_state s) s) and
    (\<lambda>s. ((\<exists>slot. caps_of_state s slot =
                 Some (ArchObjectCap (PageTableCap p None))) \<longrightarrow>
          pt = (\<lambda>x. InvalidPTE)) \<or>
         (\<forall>slot. \<exists>asid. caps_of_state s slot =
             Some (ArchObjectCap (PageTableCap p (Some asid)))))\<rbrace>
   set_pt p pt
   \<lbrace>\<lambda>rv. valid_table_caps\<rbrace>" unfolding valid_table_caps_def apply (rule valid_set_ptI) apply (intro allI impI, simp add: obj_at_def del: HOL.imp_disjL) apply (cut_tac s=s and val= "ArchObj (PageTable pt)" and p=p
              in caps_of_state_after_update[folded fun_upd_def]) apply (simp add: obj_at_def) apply (clarsimp simp del: HOL.imp_disjL) apply (thin_tac "ALL x. P x" for P) apply (case_tac cap, simp_all add: is_pd_cap_def is_pt_cap_def) apply (erule disjE) apply (simp add: valid_caps_def) apply ((drule spec)+, erule impE, assumption) apply (rename_tac arch_cap) apply (case_tac arch_cap,
          simp_all add: valid_cap_def obj_at_def aa_type_simps) apply clarsimp apply (erule impE, fastforce simp: cap_asid_def split: option.splits) apply (erule disjE, simp add: empty_table_def) apply (drule_tac x=a in spec, drule_tac x=b in spec) apply (clarsimp simp add: cap_asid_def split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_table_caps and (\<lambda>s. valid_caps (caps_of_state s) s) and (\<lambda>s. ((\<exists>slot. caps_of_state s slot = Some (ArchObjectCap (PageTableCap p None))) \<longrightarrow> pt = (\<lambda>x. InvalidPTE)) \<or> (\<forall>slot. \<exists>asid. caps_of_state s slot = Some (ArchObjectCap (PageTableCap p (Some asid)))))\<rbrace> set_pt p pt \<lbrace>\<lambda>rv. valid_table_caps\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<forall>r p cap. caps_of_state s p = Some cap \<longrightarrow> is_pd_cap cap \<or> is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) r s) and (\<lambda>s. valid_caps (caps_of_state s) s) and (\<lambda>s. ((\<exists>slot. caps_of_state s slot = Some (ArchObjectCap (PageTableCap p None))) \<longrightarrow> pt = (\<lambda>x. InvalidPTE)) \<or> (\<forall>slot. \<exists>asid. caps_of_state s slot = Some (ArchObjectCap (PageTableCap p (Some asid)))))\<rbrace> set_pt p pt \<lbrace>\<lambda>rv s. \<forall>r p cap. caps_of_state s p = Some cap \<longrightarrow> is_pd_cap cap \<or> is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) r s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s opt. \<lbrakk>((\<lambda>s. \<forall>r p cap. caps_of_state s p = Some cap \<longrightarrow> is_pd_cap cap \<or> is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) r s) and (\<lambda>s. valid_caps (caps_of_state s) s) and (\<lambda>s. ((\<exists>slot. caps_of_state s slot = Some (ArchObjectCap (PageTableCap p None))) \<longrightarrow> pt = (\<lambda>x. InvalidPTE)) \<or> (\<forall>slot. \<exists>asid. caps_of_state s slot = Some (ArchObjectCap (PageTableCap p (Some asid)))))) s; kheap s p = Some (ArchObj (PageTable opt))\<rbrakk> \<Longrightarrow> \<forall>r pa cap. caps_of_state (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) pa = Some cap \<longrightarrow> is_pd_cap cap \<or> is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>))))) r (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s opt r pa cap. \<lbrakk>(\<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)) \<and> valid_caps (caps_of_state s) s \<and> ((\<exists>a b. caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap p None))) \<longrightarrow> pt = (\<lambda>x. InvalidPTE) \<or> (\<forall>a b. \<exists>aa ba. caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap p (Some (aa, ba)))))); kheap s p = Some (ArchObj (PageTable opt)); caps_of_state (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) pa = Some cap; is_pd_cap cap \<or> is_pt_cap cap; cap_asid cap = None; r \<in> obj_refs cap\<rbrakk> \<Longrightarrow> (r = p \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageTable pt))) \<and> (r \<noteq> p \<longrightarrow> (\<exists>ko. kheap s r = Some ko \<and> empty_table (set (second_level_tables (arch_state s))) ko)) proof (prove)
goal (2 subgoals):
 1. \<And>s opt r pa cap. \<lbrakk>(\<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)) \<and> valid_caps (caps_of_state s) s \<and> ((\<exists>a b. caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap p None))) \<longrightarrow> pt = (\<lambda>x. InvalidPTE) \<or> (\<forall>a b. \<exists>aa ba. caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap p (Some (aa, ba)))))); kheap s p = Some (ArchObj (PageTable opt)); caps_of_state (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) pa = Some cap; is_pd_cap cap \<or> is_pt_cap cap; cap_asid cap = None; r \<in> obj_refs cap\<rbrakk> \<Longrightarrow> obj_at (same_caps (ArchObj (PageTable pt))) p s
 2. \<And>s opt r pa cap. \<lbrakk>(\<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)) \<and> valid_caps (caps_of_state s) s \<and> ((\<exists>a b. caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap p None))) \<longrightarrow> pt = (\<lambda>x. InvalidPTE) \<or> (\<forall>a b. \<exists>aa ba. caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap p (Some (aa, ba)))))); kheap s p = Some (ArchObj (PageTable opt)); caps_of_state (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) pa = Some cap; is_pd_cap cap \<or> is_pt_cap cap; cap_asid cap = None; r \<in> obj_refs cap; caps_of_state (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) = caps_of_state s\<rbrakk> \<Longrightarrow> (r = p \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageTable pt))) \<and> (r \<noteq> p \<longrightarrow> (\<exists>ko. kheap s r = Some ko \<and> empty_table (set (second_level_tables (arch_state s))) ko)) proof (prove)
goal (1 subgoal):
 1. \<And>s opt r pa cap. \<lbrakk>(\<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)) \<and> valid_caps (caps_of_state s) s \<and> ((\<exists>a b. caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap p None))) \<longrightarrow> pt = (\<lambda>x. InvalidPTE) \<or> (\<forall>a b. \<exists>aa ba. caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap p (Some (aa, ba)))))); kheap s p = Some (ArchObj (PageTable opt)); caps_of_state (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) pa = Some cap; is_pd_cap cap \<or> is_pt_cap cap; cap_asid cap = None; r \<in> obj_refs cap; caps_of_state (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) = caps_of_state s\<rbrakk> \<Longrightarrow> (r = p \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageTable pt))) \<and> (r \<noteq> p \<longrightarrow> (\<exists>ko. kheap s r = Some ko \<and> empty_table (set (second_level_tables (arch_state s))) ko)) proof (prove)
goal (1 subgoal):
 1. \<And>s opt a b cap. \<lbrakk>kheap s p = Some (ArchObj (PageTable opt)); 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\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) = caps_of_state 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); valid_caps (caps_of_state s) s; (\<exists>a b. caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap p None))) \<longrightarrow> pt = (\<lambda>x. InvalidPTE) \<or> (\<forall>a b. \<exists>aa ba. caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap p (Some (aa, ba)))))\<rbrakk> \<Longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageTable pt)) proof (prove)
goal (1 subgoal):
 1. \<And>s opt a b cap. \<lbrakk>kheap s p = Some (ArchObj (PageTable opt)); 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\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) = caps_of_state s; valid_caps (caps_of_state s) s; (\<exists>a b. caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap p None))) \<longrightarrow> pt = (\<lambda>x. InvalidPTE) \<or> (\<forall>a b. \<exists>aa ba. caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap p (Some (aa, ba)))))\<rbrakk> \<Longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageTable pt)) proof (prove)
goal (1 subgoal):
 1. \<And>s opt a b cap x12. \<lbrakk>kheap s p = Some (ArchObj (PageTable opt)); caps_of_state s (a, b) = Some (ArchObjectCap x12); (\<exists>p asid. x12 = PageDirectoryCap p asid) \<or> (\<exists>p asid. x12 = PageTableCap p asid); cap_asid (ArchObjectCap x12) = None; aobj_ref x12 = Some p; caps_of_state (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) = caps_of_state s; valid_caps (caps_of_state s) s; (\<exists>a b. caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap p None))) \<longrightarrow> pt = (\<lambda>x. InvalidPTE) \<or> (\<forall>a b. \<exists>aa ba. caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap p (Some (aa, ba))))); cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageTable pt)) proof (prove)
goal (2 subgoals):
 1. \<And>s opt a b cap x12. \<lbrakk>kheap s p = Some (ArchObj (PageTable opt)); caps_of_state s (a, b) = Some (ArchObjectCap x12); cap_asid (ArchObjectCap x12) = None; aobj_ref x12 = Some p; caps_of_state (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) = caps_of_state s; valid_caps (caps_of_state s) s; (\<exists>a b. caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap p None))) \<longrightarrow> pt = (\<lambda>x. InvalidPTE) \<or> (\<forall>a b. \<exists>aa ba. caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap p (Some (aa, ba))))); cap = ArchObjectCap x12; \<exists>p asid. x12 = PageDirectoryCap p asid\<rbrakk> \<Longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageTable pt))
 2. \<And>s opt a b cap x12. \<lbrakk>kheap s p = Some (ArchObj (PageTable opt)); caps_of_state s (a, b) = Some (ArchObjectCap x12); cap_asid (ArchObjectCap x12) = None; aobj_ref x12 = Some p; caps_of_state (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) = caps_of_state s; valid_caps (caps_of_state s) s; (\<exists>a b. caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap p None))) \<longrightarrow> pt = (\<lambda>x. InvalidPTE) \<or> (\<forall>a b. \<exists>aa ba. caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap p (Some (aa, ba))))); cap = ArchObjectCap x12; \<exists>p asid. x12 = PageTableCap p asid\<rbrakk> \<Longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageTable pt)) proof (prove)
goal (2 subgoals):
 1. \<And>s opt a b cap x12. \<lbrakk>kheap s p = Some (ArchObj (PageTable opt)); caps_of_state s (a, b) = Some (ArchObjectCap x12); cap_asid (ArchObjectCap x12) = None; aobj_ref x12 = Some p; caps_of_state (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) = caps_of_state s; \<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> s \<turnstile> cap; (\<exists>a b. caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap p None))) \<longrightarrow> pt = (\<lambda>x. InvalidPTE) \<or> (\<forall>a b. \<exists>aa ba. caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap p (Some (aa, ba))))); cap = ArchObjectCap x12; \<exists>p asid. x12 = PageDirectoryCap p asid\<rbrakk> \<Longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageTable pt))
 2. \<And>s opt a b cap x12. \<lbrakk>kheap s p = Some (ArchObj (PageTable opt)); caps_of_state s (a, b) = Some (ArchObjectCap x12); cap_asid (ArchObjectCap x12) = None; aobj_ref x12 = Some p; caps_of_state (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) = caps_of_state s; valid_caps (caps_of_state s) s; (\<exists>a b. caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap p None))) \<longrightarrow> pt = (\<lambda>x. InvalidPTE) \<or> (\<forall>a b. \<exists>aa ba. caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap p (Some (aa, ba))))); cap = ArchObjectCap x12; \<exists>p asid. x12 = PageTableCap p asid\<rbrakk> \<Longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageTable pt)) proof (prove)
goal (2 subgoals):
 1. \<And>s opt a b cap x12. \<lbrakk>kheap s p = Some (ArchObj (PageTable opt)); caps_of_state s (a, b) = Some (ArchObjectCap x12); cap_asid (ArchObjectCap x12) = None; aobj_ref x12 = Some p; caps_of_state (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) = caps_of_state s; (\<exists>a b. caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap p None))) \<longrightarrow> pt = (\<lambda>x. InvalidPTE) \<or> (\<forall>a b. \<exists>aa ba. caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap p (Some (aa, ba))))); cap = ArchObjectCap x12; \<exists>p asid. x12 = PageDirectoryCap p asid; s \<turnstile> ArchObjectCap x12\<rbrakk> \<Longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageTable pt))
 2. \<And>s opt a b cap x12. \<lbrakk>kheap s p = Some (ArchObj (PageTable opt)); caps_of_state s (a, b) = Some (ArchObjectCap x12); cap_asid (ArchObjectCap x12) = None; aobj_ref x12 = Some p; caps_of_state (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) = caps_of_state s; valid_caps (caps_of_state s) s; (\<exists>a b. caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap p None))) \<longrightarrow> pt = (\<lambda>x. InvalidPTE) \<or> (\<forall>a b. \<exists>aa ba. caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap p (Some (aa, ba))))); cap = ArchObjectCap x12; \<exists>p asid. x12 = PageTableCap p asid\<rbrakk> \<Longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageTable pt)) proof (prove)
goal (2 subgoals):
 1. \<And>s opt a b cap arch_cap. \<lbrakk>kheap s p = Some (ArchObj (PageTable opt)); caps_of_state s (a, b) = Some (ArchObjectCap arch_cap); cap_asid (ArchObjectCap arch_cap) = None; aobj_ref arch_cap = Some p; caps_of_state (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) = caps_of_state s; (\<exists>a b. caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap p None))) \<longrightarrow> pt = (\<lambda>x. InvalidPTE) \<or> (\<forall>a b. \<exists>aa ba. caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap p (Some (aa, ba))))); cap = ArchObjectCap arch_cap; \<exists>p asid. arch_cap = PageDirectoryCap p asid; s \<turnstile> ArchObjectCap arch_cap\<rbrakk> \<Longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageTable pt))
 2. \<And>s opt a b cap x12. \<lbrakk>kheap s p = Some (ArchObj (PageTable opt)); caps_of_state s (a, b) = Some (ArchObjectCap x12); cap_asid (ArchObjectCap x12) = None; aobj_ref x12 = Some p; caps_of_state (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) = caps_of_state s; valid_caps (caps_of_state s) s; (\<exists>a b. caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap p None))) \<longrightarrow> pt = (\<lambda>x. InvalidPTE) \<or> (\<forall>a b. \<exists>aa ba. caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap p (Some (aa, ba))))); cap = ArchObjectCap x12; \<exists>p asid. x12 = PageTableCap p asid\<rbrakk> \<Longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageTable pt)) proof (prove)
goal (2 subgoals):
 1. \<And>s opt a b cap arch_cap x51 x52. \<lbrakk>kheap s p = Some (ArchObj (PageTable opt)); caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap p x52)); cap_asid (ArchObjectCap (PageDirectoryCap p x52)) = None; x51 = p; caps_of_state (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) = caps_of_state s; (\<exists>a b. caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap p None))) \<longrightarrow> pt = (\<lambda>x. InvalidPTE) \<or> (\<forall>a b. \<exists>aa ba. caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap p (Some (aa, ba))))); cap = ArchObjectCap (PageDirectoryCap p x52); cap_aligned (ArchObjectCap (PageDirectoryCap p x52)) \<and> a_type (ArchObj (PageTable opt)) = AArch APageDirectory \<and> (case x52 of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1); arch_cap = PageDirectoryCap p x52\<rbrakk> \<Longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageTable pt))
 2. \<And>s opt a b cap x12. \<lbrakk>kheap s p = Some (ArchObj (PageTable opt)); caps_of_state s (a, b) = Some (ArchObjectCap x12); cap_asid (ArchObjectCap x12) = None; aobj_ref x12 = Some p; caps_of_state (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) = caps_of_state s; valid_caps (caps_of_state s) s; (\<exists>a b. caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap p None))) \<longrightarrow> pt = (\<lambda>x. InvalidPTE) \<or> (\<forall>a b. \<exists>aa ba. caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap p (Some (aa, ba))))); cap = ArchObjectCap x12; \<exists>p asid. x12 = PageTableCap p asid\<rbrakk> \<Longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageTable pt)) proof (prove)
goal (1 subgoal):
 1. \<And>s opt a b cap x12. \<lbrakk>kheap s p = Some (ArchObj (PageTable opt)); caps_of_state s (a, b) = Some (ArchObjectCap x12); cap_asid (ArchObjectCap x12) = None; aobj_ref x12 = Some p; caps_of_state (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) = caps_of_state s; valid_caps (caps_of_state s) s; (\<exists>a b. caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap p None))) \<longrightarrow> pt = (\<lambda>x. InvalidPTE) \<or> (\<forall>a b. \<exists>aa ba. caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap p (Some (aa, ba))))); cap = ArchObjectCap x12; \<exists>p asid. x12 = PageTableCap p asid\<rbrakk> \<Longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageTable pt)) proof (prove)
goal (1 subgoal):
 1. \<And>s opt a b cap x12. \<lbrakk>kheap s p = Some (ArchObj (PageTable opt)); caps_of_state s (a, b) = Some (ArchObjectCap x12); cap_asid (ArchObjectCap x12) = None; aobj_ref x12 = Some p; caps_of_state (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) = caps_of_state s; valid_caps (caps_of_state s) s; cap = ArchObjectCap x12; \<exists>p asid. x12 = PageTableCap p asid; pt = (\<lambda>x. InvalidPTE) \<or> (\<forall>a b. \<exists>aa ba. caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap p (Some (aa, ba)))))\<rbrakk> \<Longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageTable pt)) proof (prove)
goal (1 subgoal):
 1. \<And>s opt a b cap x12. \<lbrakk>kheap s p = Some (ArchObj (PageTable opt)); caps_of_state s (a, b) = Some (ArchObjectCap x12); cap_asid (ArchObjectCap x12) = None; aobj_ref x12 = Some p; caps_of_state (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) = caps_of_state s; valid_caps (caps_of_state s) s; cap = ArchObjectCap x12; \<exists>p asid. x12 = PageTableCap p asid; \<forall>a b. \<exists>aa ba. caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap p (Some (aa, ba))))\<rbrakk> \<Longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageTable pt)) proof (prove)
goal (1 subgoal):
 1. \<And>s opt a b cap x12. \<lbrakk>kheap s p = Some (ArchObj (PageTable opt)); caps_of_state s (a, b) = Some (ArchObjectCap x12); cap_asid (ArchObjectCap x12) = None; aobj_ref x12 = Some p; caps_of_state (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) = caps_of_state s; valid_caps (caps_of_state s) s; cap = ArchObjectCap x12; \<exists>p asid. x12 = PageTableCap p asid; \<exists>aa ba. caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap p (Some (aa, ba))))\<rbrakk> \<Longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageTable pt)) proof (prove)
goal:
No subgoals!