theory ArchAcc_AI

lemma set_asid_pool_vs_lookup_unmap':
  "\<lbrace>valid_vs_lookup and
    obj_at (\<lambda>ko. \<exists>ap'. ko = ArchObj (ASIDPool ap') \<and> graph_of ap \<subseteq> graph_of ap') p\<rbrace>
  set_asid_pool p ap \<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];wp?) apply (simp add: set_asid_pool_def set_object_def) apply (wp get_object_wp) apply (clarsimp simp: obj_at_def simp del: fun_upd_apply del: disjCI
                  split: kernel_object.splits arch_kernel_obj.splits) subgoal for \<dots> pa ref apply (spec pa) apply (spec ref) apply (erule impE) apply (erule vs_lookup_pages_stateI) by (clarsimp simp: obj_at_def vs_refs_pages_def split: if_split_asm)
         fastforce+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vs_lookup and obj_at (\<lambda>ko. \<exists>ap'. ko = ArchObj (ASIDPool ap') \<and> graph_of ap \<subseteq> graph_of ap') p\<rbrace> set_asid_pool p ap \<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. \<exists>ap'. ko = ArchObj (ASIDPool ap') \<and> graph_of ap \<subseteq> graph_of ap') p x\<rbrace> set_asid_pool p ap \<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 (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. \<exists>ap'. ko = ArchObj (ASIDPool ap') \<and> graph_of ap \<subseteq> graph_of ap') p xa\<rbrace> set_asid_pool p ap \<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. \<exists>ap'. ko = ArchObj (ASIDPool ap') \<and> graph_of ap \<subseteq> graph_of ap') p xa\<rbrace> do kobj <- get_object p;
y <- assert (a_type kobj = a_type (ArchObj (ASIDPool ap)));
s <- get;
put (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool ap))\<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. \<exists>ap'. ko = ArchObj (ASIDPool ap') \<and> graph_of ap \<subseteq> graph_of ap') p s \<Longrightarrow> \<forall>ko. ko_at ko p s \<longrightarrow> a_type ko = a_type (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>pa ref. (ref \<unrhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool ap))\<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 ap' 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); graph_of ap \<subseteq> graph_of ap'; kheap s p = Some (ArchObj (ASIDPool ap')); a_type (ArchObj (ASIDPool ap')) = a_type (ArchObj (ASIDPool ap)); (ref \<unrhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool ap))\<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. \<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); graph_of ap \<subseteq> graph_of ap'_; kheap s_ p = Some (ArchObj (ASIDPool ap'_)); a_type (ArchObj (ASIDPool ap'_)) = a_type (ArchObj (ASIDPool ap)); (ref \<unrhd> pa) (s_\<lparr>kheap := (kheap s_)(p \<mapsto> ArchObj (ASIDPool ap))\<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. \<lbrakk>graph_of ap \<subseteq> graph_of ap'_; kheap s_ p = Some (ArchObj (ASIDPool ap'_)); a_type (ArchObj (ASIDPool ap'_)) = a_type (ArchObj (ASIDPool ap)); (ref \<unrhd> pa) (s_\<lparr>kheap := (kheap s_)(p \<mapsto> ArchObj (ASIDPool ap))\<rparr>); \<forall>ref. (ref \<unrhd> pa) s_ \<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)\<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. \<lbrakk>graph_of ap \<subseteq> graph_of ap'_; kheap s_ p = Some (ArchObj (ASIDPool ap'_)); a_type (ArchObj (ASIDPool ap'_)) = a_type (ArchObj (ASIDPool ap)); (ref \<unrhd> pa) (s_\<lparr>kheap := (kheap s_)(p \<mapsto> ArchObj (ASIDPool ap))\<rparr>); (ref \<unrhd> pa) s_ \<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)\<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. \<lbrakk>graph_of ap \<subseteq> graph_of ap'_; kheap s_ p = Some (ArchObj (ASIDPool ap'_)); a_type (ArchObj (ASIDPool ap'_)) = a_type (ArchObj (ASIDPool ap)); (ref \<unrhd> pa) (s_\<lparr>kheap := (kheap s_)(p \<mapsto> ArchObj (ASIDPool ap))\<rparr>)\<rbrakk> \<Longrightarrow> (ref \<unrhd> pa) s_
 2. \<lbrakk>graph_of ap \<subseteq> graph_of ap'_; kheap s_ p = Some (ArchObj (ASIDPool ap'_)); a_type (ArchObj (ASIDPool ap'_)) = a_type (ArchObj (ASIDPool ap)); (ref \<unrhd> pa) (s_\<lparr>kheap := (kheap s_)(p \<mapsto> ArchObj (ASIDPool ap))\<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 (3 subgoals):
 1. \<And>ko pa. \<lbrakk>graph_of ap \<subseteq> graph_of ap'_; kheap s_ p = Some (ArchObj (ASIDPool ap'_)); a_type (ArchObj (ASIDPool ap'_)) = a_type (ArchObj (ASIDPool ap)); ko_at ko pa (s_\<lparr>kheap := (kheap s_)(p \<mapsto> ArchObj (ASIDPool ap))\<rparr>)\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko'. vs_refs_pages ko \<subseteq> vs_refs_pages ko') pa s_
 2. \<lbrakk>graph_of ap \<subseteq> graph_of ap'_; kheap s_ p = Some (ArchObj (ASIDPool ap'_)); a_type (ArchObj (ASIDPool ap'_)) = a_type (ArchObj (ASIDPool ap))\<rbrakk> \<Longrightarrow> graph_of (asid_table (s_\<lparr>kheap := (kheap s_)(p \<mapsto> ArchObj (ASIDPool ap))\<rparr>)) \<subseteq> graph_of (asid_table s_)
 3. \<lbrakk>graph_of ap \<subseteq> graph_of ap'_; kheap s_ p = Some (ArchObj (ASIDPool ap'_)); a_type (ArchObj (ASIDPool ap'_)) = a_type (ArchObj (ASIDPool ap)); (ref \<unrhd> pa) (s_\<lparr>kheap := (kheap s_)(p \<mapsto> ArchObj (ASIDPool ap))\<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!