theory ArchAcc_AI

lemma set_pd_table_caps [wp]:
  "\<lbrace>valid_table_caps and (\<lambda>s.
    (obj_at (empty_table (set (second_level_tables (arch_state s)))) p s \<longrightarrow>
     empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd))) \<or>
    (\<exists>slot cap. caps_of_state s slot = Some cap \<and> is_pd_cap cap \<and> p \<in> obj_refs cap \<and> cap_asid cap \<noteq> None) \<and>
    valid_caps (caps_of_state s) s \<and>
    unique_table_caps (caps_of_state s))\<rbrace>
  set_pd p pd
  \<lbrace>\<lambda>_. valid_table_caps\<rbrace>" unfolding valid_table_caps_def apply (simp add: pred_conj_def
              del: split_paired_All split_paired_Ex imp_disjL) apply (rule hoare_lift_Pf2 [where f=caps_of_state]) prefer 2 apply wp apply (unfold set_pd_def set_object_def) apply (wp get_object_wp) apply (rule allI, intro impI) apply (elim exE conjE) apply (elim allEI) apply (intro impI, simp) apply (clarsimp simp: obj_at_def) apply (erule disjE) apply (erule(6) unique_table_caps_pdE) apply (clarsimp simp: is_arch_cap_simps) apply (simp add: valid_caps_def) apply (erule_tac x=a in allE, erule allE, erule allE, erule (1) impE) apply (clarsimp simp: is_arch_cap_simps valid_cap_def) apply (clarsimp simp: obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_table_caps and (\<lambda>s. (obj_at (empty_table (set (second_level_tables (arch_state s)))) p s \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd))) \<or> (\<exists>slot cap. caps_of_state s slot = Some cap \<and> is_pd_cap cap \<and> p \<in> obj_refs cap \<and> cap_asid cap \<noteq> None) \<and> valid_caps (caps_of_state s) s \<and> unique_table_caps (caps_of_state s))\<rbrace> set_pd p pd \<lbrace>\<lambda>_. 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. (obj_at (empty_table (set (second_level_tables (arch_state s)))) p s \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd))) \<or> (\<exists>slot cap. caps_of_state s slot = Some cap \<and> is_pd_cap cap \<and> p \<in> obj_refs cap \<and> cap_asid cap \<noteq> None) \<and> valid_caps (caps_of_state s) s \<and> unique_table_caps (caps_of_state s))\<rbrace> set_pd p pd \<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\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>x. (\<forall>r p cap. caps_of_state x 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 x)))) r x) \<and> (obj_at (empty_table (set (second_level_tables (arch_state x)))) p x \<longrightarrow> empty_table (set (second_level_tables (arch_state x))) (ArchObj (PageDirectory pd)) \<or> (\<exists>slot cap. caps_of_state x slot = Some cap \<and> is_pd_cap cap \<and> p \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<and> valid_caps (caps_of_state x) x \<and> unique_table_caps (caps_of_state x))\<rbrace> set_pd p pd \<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\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>\<lambda>xa. (\<forall>r p cap. x 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 xa)))) r xa) \<and> (obj_at (empty_table (set (second_level_tables (arch_state xa)))) p xa \<longrightarrow> empty_table (set (second_level_tables (arch_state xa))) (ArchObj (PageDirectory pd)) \<or> (\<exists>slot cap. x slot = Some cap \<and> is_pd_cap cap \<and> p \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<and> valid_caps x xa \<and> unique_table_caps x)\<rbrace> set_pd p pd \<lbrace>\<lambda>_ a. \<forall>r p cap. x 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 a)))) r a\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>x. P (caps_of_state x)\<rbrace> set_pd p pd \<lbrace>\<lambda>_ x. P (caps_of_state x)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>P. \<lbrace>\<lambda>x. P (caps_of_state x)\<rbrace> set_pd p pd \<lbrace>\<lambda>_ x. P (caps_of_state x)\<rbrace>
 2. \<And>x. \<lbrace>\<lambda>xa. (\<forall>r p cap. x 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 xa)))) r xa) \<and> (obj_at (empty_table (set (second_level_tables (arch_state xa)))) p xa \<longrightarrow> empty_table (set (second_level_tables (arch_state xa))) (ArchObj (PageDirectory pd)) \<or> (\<exists>slot cap. x slot = Some cap \<and> is_pd_cap cap \<and> p \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<and> valid_caps x xa \<and> unique_table_caps x)\<rbrace> set_pd p pd \<lbrace>\<lambda>_ a. \<forall>r p cap. x 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 a)))) r a\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrace>\<lambda>xa. (\<forall>r p cap. x 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 xa)))) r xa) \<and> (obj_at (empty_table (set (second_level_tables (arch_state xa)))) p xa \<longrightarrow> empty_table (set (second_level_tables (arch_state xa))) (ArchObj (PageDirectory pd)) \<or> (\<exists>slot cap. x slot = Some cap \<and> is_pd_cap cap \<and> p \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<and> valid_caps x xa \<and> unique_table_caps x)\<rbrace> set_pd p pd \<lbrace>\<lambda>_ a. \<forall>r p cap. x 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 a)))) r a\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrace>\<lambda>xa. (\<forall>r p cap. x 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 xa)))) r xa) \<and> (obj_at (empty_table (set (second_level_tables (arch_state xa)))) p xa \<longrightarrow> empty_table (set (second_level_tables (arch_state xa))) (ArchObj (PageDirectory pd)) \<or> (\<exists>slot cap. x slot = Some cap \<and> is_pd_cap cap \<and> p \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<and> valid_caps x xa \<and> unique_table_caps x)\<rbrace> do kobj <- get_object p;
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>_ a. \<forall>r p cap. x 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 a)))) r a\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x s. (\<forall>r p cap. x 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> (obj_at (empty_table (set (second_level_tables (arch_state s)))) p s \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>slot cap. x slot = Some cap \<and> is_pd_cap cap \<and> p \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<and> valid_caps x s \<and> unique_table_caps x) \<Longrightarrow> \<forall>ko. ko_at ko p s \<longrightarrow> a_type ko = a_type (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>r pa cap. x 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 (PageDirectory pd))\<rparr>))))) r (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>x s ko. \<lbrakk>(\<forall>r p cap. x 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> (obj_at (empty_table (set (second_level_tables (arch_state s)))) p s \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>slot cap. x slot = Some cap \<and> is_pd_cap cap \<and> p \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<and> valid_caps x s \<and> unique_table_caps x); ko_at ko p s; a_type ko = a_type (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> \<forall>r pa cap. x 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 (PageDirectory pd))\<rparr>))))) r (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>x s ko. \<lbrakk>ko_at ko p s; a_type ko = a_type (ArchObj (PageDirectory pd)); \<forall>r p cap. x 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; obj_at (empty_table (set (second_level_tables (arch_state s)))) p s \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>slot cap. x slot = Some cap \<and> is_pd_cap cap \<and> p \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<and> valid_caps x s \<and> unique_table_caps x\<rbrakk> \<Longrightarrow> \<forall>r pa cap. x 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 (PageDirectory pd))\<rparr>))))) r (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>x s ko r pa cap. \<lbrakk>ko_at ko p s; a_type ko = a_type (ArchObj (PageDirectory pd)); obj_at (empty_table (set (second_level_tables (arch_state s)))) p s \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>slot cap. x slot = Some cap \<and> is_pd_cap cap \<and> p \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<and> valid_caps x s \<and> unique_table_caps x; x 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)))) r s\<rbrakk> \<Longrightarrow> x 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 (PageDirectory pd))\<rparr>))))) r (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>x s ko r pa cap. \<lbrakk>ko_at ko p s; a_type ko = a_type (ArchObj (PageDirectory pd)); obj_at (empty_table (set (second_level_tables (arch_state s)))) p s \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. x (a, b) = Some cap \<and> is_pd_cap cap \<and> p \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<and> valid_caps x s \<and> unique_table_caps x; obj_at (empty_table (set (second_level_tables (arch_state s)))) r s; x 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 (empty_table (set (second_level_tables (arch_state s)))) r (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageDirectory pd)) else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>x s ko a b cap aa ba capa y. \<lbrakk>a_type ko = a_type (ArchObj (PageDirectory pd)); x (a, b) = Some cap; is_pd_cap cap \<or> is_pt_cap cap; cap_asid cap = None; p \<in> obj_refs cap; kheap s p = Some ko; empty_table (set (second_level_tables (arch_state s))) ko; valid_caps x s; unique_table_caps x; x (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>x s ko a b cap aa ba capa y. \<lbrakk>a_type ko = a_type (ArchObj (PageDirectory pd)); x (a, b) = Some cap; cap_asid cap = None; p \<in> obj_refs cap; kheap s p = Some ko; empty_table (set (second_level_tables (arch_state s))) ko; valid_caps x s; unique_table_caps x; x (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>x s ko a b cap aa ba capa y. \<lbrakk>a_type ko = a_type (ArchObj (PageDirectory pd)); x (a, b) = Some cap; cap_asid cap = None; p \<in> obj_refs cap; kheap s p = Some ko; empty_table (set (second_level_tables (arch_state s))) ko; valid_caps x s; unique_table_caps x; x (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>x s ko a b cap aa ba capa y. \<lbrakk>a_type ko = a_type (ArchObj (PageDirectory pd)); x (a, b) = Some cap; cap_asid cap = None; p \<in> obj_refs cap; kheap s p = Some ko; empty_table (set (second_level_tables (arch_state s))) ko; valid_caps x s; x (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
 2. \<And>x s ko a b cap aa ba capa y. \<lbrakk>a_type ko = a_type (ArchObj (PageDirectory pd)); x (a, b) = Some cap; cap_asid cap = None; p \<in> obj_refs cap; kheap s p = Some ko; empty_table (set (second_level_tables (arch_state s))) ko; valid_caps x s; unique_table_caps x; x (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 (1 subgoal):
 1. \<And>x s ko a b cap aa ba capa y. \<lbrakk>a_type ko = a_type (ArchObj (PageDirectory pd)); x (a, b) = Some cap; cap_asid cap = None; p \<in> obj_refs cap; kheap s p = Some ko; empty_table (set (second_level_tables (arch_state s))) ko; valid_caps x s; unique_table_caps x; x (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 (1 subgoal):
 1. \<And>x s ko a b cap aa ba capa y. \<lbrakk>a_type ko = a_type (ArchObj (PageDirectory pd)); x (a, b) = Some cap; cap_asid cap = None; p \<in> obj_refs cap; kheap s p = Some ko; empty_table (set (second_level_tables (arch_state s))) ko; \<forall>a b cap. x (a, b) = Some cap \<longrightarrow> s \<turnstile> cap; unique_table_caps x; x (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 (1 subgoal):
 1. \<And>x s ko a b cap aa ba capa y. \<lbrakk>a_type ko = a_type (ArchObj (PageDirectory pd)); x (a, b) = Some cap; cap_asid cap = None; p \<in> obj_refs cap; kheap s p = Some ko; empty_table (set (second_level_tables (arch_state s))) ko; unique_table_caps x; x (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)) proof (prove)
goal (1 subgoal):
 1. \<And>x s ko a b aa ba y asid asida. \<lbrakk>a_type ko = a_type (ArchObj (PageDirectory pd)); x (a, b) = Some (ArchObjectCap (PageTableCap p asida)); cap_asid (ArchObjectCap (PageTableCap p asida)) = None; kheap s p = Some ko; empty_table (set (second_level_tables (arch_state s))) ko; unique_table_caps x; x (aa, ba) = Some (ArchObjectCap (PageDirectoryCap p asid)); cap_asid (ArchObjectCap (PageDirectoryCap p asid)) = Some y; cap_aligned (ArchObjectCap (PageTableCap p asida)); typ_at (AArch APageTable) p s; case asida of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection)\<rbrakk> \<Longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)) proof (prove)
goal:
No subgoals!