theory ArchAcc_AI

lemma set_pd_vs_lookup_unmap:
  "\<lbrace>valid_vs_lookup and
    obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory pd)) \<subseteq> vs_refs_pages ko) p\<rbrace>
  set_pd p pd
  \<lbrace>\<lambda>_. valid_vs_lookup\<rbrace>" apply (simp add: valid_vs_lookup_def pred_conj_def) apply (rule hoare_lift_Pf2 [where f=caps_of_state]) prefer 2 apply wp apply (simp add: set_pd_def set_object_def) apply (wp get_object_wp) apply (clarsimp simp del: fun_upd_apply del: disjCI
                  split: kernel_object.splits arch_kernel_obj.splits) apply (erule allE)+ apply (erule impE) apply (erule vs_lookup_pages_stateI) apply (clarsimp simp: obj_at_def split: if_split_asm) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vs_lookup and obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory pd)) \<subseteq> vs_refs_pages ko) p\<rbrace> set_pd p pd \<lbrace>\<lambda>_. valid_vs_lookup\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>x. (\<forall>p ref. (ref \<unrhd> p) x \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. caps_of_state x (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref)) \<and> obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory pd)) \<subseteq> vs_refs_pages ko) p x\<rbrace> set_pd p pd \<lbrace>\<lambda>_ s. \<forall>p ref. (ref \<unrhd> p) s \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>\<lambda>xa. (\<forall>p ref. (ref \<unrhd> p) xa \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. x (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref)) \<and> obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory pd)) \<subseteq> vs_refs_pages ko) p xa\<rbrace> set_pd p pd \<lbrace>\<lambda>_ a. \<forall>p ref. (ref \<unrhd> p) a \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. x (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref)\<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>p ref. (ref \<unrhd> p) xa \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. x (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref)) \<and> obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory pd)) \<subseteq> vs_refs_pages ko) p xa\<rbrace> set_pd p pd \<lbrace>\<lambda>_ a. \<forall>p ref. (ref \<unrhd> p) a \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. x (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrace>\<lambda>xa. (\<forall>p ref. (ref \<unrhd> p) xa \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. x (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref)) \<and> obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory pd)) \<subseteq> vs_refs_pages ko) p xa\<rbrace> set_pd p pd \<lbrace>\<lambda>_ a. \<forall>p ref. (ref \<unrhd> p) a \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. x (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrace>\<lambda>xa. (\<forall>p ref. (ref \<unrhd> p) xa \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. x (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref)) \<and> obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory pd)) \<subseteq> vs_refs_pages ko) p xa\<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>_ a. \<forall>p ref. (ref \<unrhd> p) a \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. x (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x s. (\<forall>p ref. (ref \<unrhd> p) s \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. x (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref)) \<and> obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory pd)) \<subseteq> vs_refs_pages ko) p s \<Longrightarrow> \<forall>ko. ko_at ko p s \<longrightarrow> a_type ko = a_type (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>pa ref. (ref \<unrhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>) \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. x (a, b) = Some cap \<and> pa \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref)) proof (prove)
goal (1 subgoal):
 1. \<And>x s ko pa ref. \<lbrakk>\<forall>p ref. (ref \<unrhd> p) s \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. x (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref); obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory pd)) \<subseteq> vs_refs_pages ko) p s; ko_at ko p s; a_type ko = a_type (ArchObj (PageDirectory pd)); (ref \<unrhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>)\<rbrakk> \<Longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. x (a, b) = Some cap \<and> pa \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref) proof (prove)
goal (1 subgoal):
 1. \<And>x s ko pa ref. \<lbrakk>obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory pd)) \<subseteq> vs_refs_pages ko) p s; ko_at ko p s; a_type ko = a_type (ArchObj (PageDirectory pd)); (ref \<unrhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>); (?ref32 x s ko pa ref \<unrhd> ?p30 x s ko pa ref) s \<longrightarrow> ?ref32 x s ko pa ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. x (a, b) = Some cap \<and> ?p30 x s ko pa ref \<in> obj_refs cap \<and> vs_cap_ref cap = Some (?ref32 x s ko pa ref))\<rbrakk> \<Longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. x (a, b) = Some cap \<and> pa \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref) proof (prove)
goal (2 subgoals):
 1. \<And>x s ko pa ref. \<lbrakk>obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory pd)) \<subseteq> vs_refs_pages ko) p s; ko_at ko p s; a_type ko = a_type (ArchObj (PageDirectory pd)); (ref \<unrhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>)\<rbrakk> \<Longrightarrow> (?ref32 x s ko pa ref \<unrhd> ?p30 x s ko pa ref) s
 2. \<And>x s ko pa ref. \<lbrakk>obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory pd)) \<subseteq> vs_refs_pages ko) p s; ko_at ko p s; a_type ko = a_type (ArchObj (PageDirectory pd)); (ref \<unrhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>); ?ref32 x s ko pa ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. x (a, b) = Some cap \<and> ?p30 x s ko pa ref \<in> obj_refs cap \<and> vs_cap_ref cap = Some (?ref32 x s ko pa ref))\<rbrakk> \<Longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. x (a, b) = Some cap \<and> pa \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref) proof (prove)
goal (3 subgoals):
 1. \<And>x s ko pa ref koa paa. \<lbrakk>obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory pd)) \<subseteq> vs_refs_pages ko) p s; ko_at ko p s; a_type ko = a_type (ArchObj (PageDirectory pd)); ko_at koa paa (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>)\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko'. vs_refs_pages koa \<subseteq> vs_refs_pages ko') paa s
 2. \<And>x s ko pa ref. \<lbrakk>obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory pd)) \<subseteq> vs_refs_pages ko) p s; ko_at ko p s; a_type ko = a_type (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> graph_of (asid_table (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>)) \<subseteq> graph_of (asid_table s)
 3. \<And>x s ko pa ref. \<lbrakk>obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory pd)) \<subseteq> vs_refs_pages ko) p s; ko_at ko p s; a_type ko = a_type (ArchObj (PageDirectory pd)); (ref \<unrhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>); ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. x (a, b) = Some cap \<and> pa \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref)\<rbrakk> \<Longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. x (a, b) = Some cap \<and> pa \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref) proof (prove)
goal (2 subgoals):
 1. \<And>x s ko pa ref. \<lbrakk>obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory pd)) \<subseteq> vs_refs_pages ko) p s; ko_at ko p s; a_type ko = a_type (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> graph_of (asid_table (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>)) \<subseteq> graph_of (asid_table s)
 2. \<And>x s ko pa ref. \<lbrakk>obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory pd)) \<subseteq> vs_refs_pages ko) p s; ko_at ko p s; a_type ko = a_type (ArchObj (PageDirectory pd)); (ref \<unrhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>); ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. x (a, b) = Some cap \<and> pa \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref)\<rbrakk> \<Longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. x (a, b) = Some cap \<and> pa \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref) proof (prove)
goal (1 subgoal):
 1. \<And>x s ko pa ref. \<lbrakk>obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory pd)) \<subseteq> vs_refs_pages ko) p s; ko_at ko p s; a_type ko = a_type (ArchObj (PageDirectory pd)); (ref \<unrhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>); ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. x (a, b) = Some cap \<and> pa \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref)\<rbrakk> \<Longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. x (a, b) = Some cap \<and> pa \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref) proof (prove)
goal:
No subgoals!