theory ArchVSpace_AI

lemma store_pde_no_lookup_pages:
  "\<lbrace>\<lambda>s. \<not> (r \<unrhd> q) s\<rbrace> store_pde p InvalidPDE \<lbrace>\<lambda>_ s. \<not> (r \<unrhd> q) s\<rbrace>" apply (simp add: store_pde_def set_pd_def set_object_def) apply (wp get_object_wp) apply (clarsimp simp: obj_at_def) apply (erule swap, simp) apply (erule vs_lookup_pages_induct) apply (simp add: vs_lookup_pages_atI) apply (thin_tac "(ref \<unrhd> p) (kheap_update f s)" for ref p f) apply (erule vs_lookup_pages_step) by (fastforce simp: vs_lookup_pages1_def obj_at_def vs_refs_pages_def
                     graph_of_def image_def
              split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (r, q) \<notin> vs_lookup_pages s\<rbrace> store_pde p InvalidPDE \<lbrace>\<lambda>_ s. (r, q) \<notin> vs_lookup_pages s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (r, q) \<notin> vs_lookup_pages s\<rbrace> do pd <- get_pd (p && ~~ mask pd_bits);
kobj <- get_object (p && ~~ mask pd_bits);
y <- assert (a_type kobj = a_type (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := InvalidPDE)))));
s <- get;
put (s\<lparr>kheap := (kheap s)(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := InvalidPDE))))\<rparr>)
od \<lbrace>\<lambda>_ s. (r, q) \<notin> vs_lookup_pages s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (r, q) \<notin> vs_lookup_pages s \<Longrightarrow> \<forall>pd. ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s \<longrightarrow> (\<forall>ko. ko_at ko (p && ~~ mask pd_bits) s \<longrightarrow> a_type ko = a_type (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := InvalidPDE)))) \<longrightarrow> (r, q) \<notin> vs_lookup_pages (s\<lparr>kheap := (kheap s)(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := InvalidPDE))))\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s pd. \<lbrakk>(r, q) \<notin> vs_lookup_pages s; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); a_type (ArchObj (PageDirectory pd)) = a_type (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := InvalidPDE)))); (r \<unrhd> q) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then InvalidPDE else pd a))) else kheap s a\<rparr>)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s pd. \<lbrakk>kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); a_type (ArchObj (PageDirectory pd)) = a_type (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := InvalidPDE)))); (r \<unrhd> q) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then InvalidPDE else pd a))) else kheap s a\<rparr>)\<rbrakk> \<Longrightarrow> (r \<unrhd> q) s proof (prove)
goal (2 subgoals):
 1. \<And>s pd asid pa. \<lbrakk>kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); a_type (ArchObj (PageDirectory pd)) = a_type (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := InvalidPDE)))); asid_table (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then InvalidPDE else pd a))) else kheap s a\<rparr>) asid = Some pa\<rbrakk> \<Longrightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) asid) None] \<unrhd> pa) s
 2. \<And>s pd ref pa ref' p'. \<lbrakk>kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); a_type (ArchObj (PageDirectory pd)) = a_type (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := InvalidPDE)))); (ref \<unrhd> pa) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then InvalidPDE else pd a))) else kheap s a\<rparr>); ((ref, pa), ref', p') \<in> vs_lookup_pages1 (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then InvalidPDE else pd a))) else kheap s a\<rparr>); (ref \<unrhd> pa) s\<rbrakk> \<Longrightarrow> (ref' \<unrhd> p') s proof (prove)
goal (1 subgoal):
 1. \<And>s pd ref pa ref' p'. \<lbrakk>kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); a_type (ArchObj (PageDirectory pd)) = a_type (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := InvalidPDE)))); (ref \<unrhd> pa) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then InvalidPDE else pd a))) else kheap s a\<rparr>); ((ref, pa), ref', p') \<in> vs_lookup_pages1 (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then InvalidPDE else pd a))) else kheap s a\<rparr>); (ref \<unrhd> pa) s\<rbrakk> \<Longrightarrow> (ref' \<unrhd> p') s proof (prove)
goal (1 subgoal):
 1. \<And>s pd ref pa ref' p'. \<lbrakk>kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); a_type (ArchObj (PageDirectory pd)) = a_type (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := InvalidPDE)))); ((ref, pa), ref', p') \<in> vs_lookup_pages1 (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then InvalidPDE else pd a))) else kheap s a\<rparr>); (ref \<unrhd> pa) s\<rbrakk> \<Longrightarrow> (ref' \<unrhd> p') s proof (prove)
goal (1 subgoal):
 1. \<And>s pd ref pa ref' p'. \<lbrakk>kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); a_type (ArchObj (PageDirectory pd)) = a_type (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := InvalidPDE)))); ((ref, pa), ref', p') \<in> vs_lookup_pages1 (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then InvalidPDE else pd a))) else kheap s a\<rparr>)\<rbrakk> \<Longrightarrow> ((ref, pa), ref', p') \<in> vs_lookup_pages1 s