theory ArchVSpace_AI

lemma store_pte_no_lookup_pages:
  "\<lbrace>\<lambda>s. \<not> (r \<unrhd> q) s\<rbrace>
   store_pte p InvalidPTE
   \<lbrace>\<lambda>_ s. \<not> (r \<unrhd> q) s\<rbrace>" apply (simp add: store_pte_def set_pt_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_pte p InvalidPTE \<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 pt <- get_pt (p && ~~ mask pt_bits);
kobj <- get_object (p && ~~ mask pt_bits);
y <- assert (a_type kobj = a_type (ArchObj (PageTable (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := InvalidPTE)))));
s <- get;
put (s\<lparr>kheap := (kheap s)(p && ~~ mask pt_bits \<mapsto> ArchObj (PageTable (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := InvalidPTE))))\<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>pt. ako_at (PageTable pt) (p && ~~ mask pt_bits) s \<longrightarrow> (\<forall>ko. ko_at ko (p && ~~ mask pt_bits) s \<longrightarrow> a_type ko = a_type (ArchObj (PageTable (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := InvalidPTE)))) \<longrightarrow> (r, q) \<notin> vs_lookup_pages (s\<lparr>kheap := (kheap s)(p && ~~ mask pt_bits \<mapsto> ArchObj (PageTable (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := InvalidPTE))))\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s pt. \<lbrakk>(r, q) \<notin> vs_lookup_pages s; kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); a_type (ArchObj (PageTable pt)) = a_type (ArchObj (PageTable (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := InvalidPTE)))); (r \<unrhd> q) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pt_bits then Some (ArchObj (PageTable (\<lambda>a. if a = UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) then InvalidPTE else pt a))) else kheap s a\<rparr>)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s pt. \<lbrakk>kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); a_type (ArchObj (PageTable pt)) = a_type (ArchObj (PageTable (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := InvalidPTE)))); (r \<unrhd> q) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pt_bits then Some (ArchObj (PageTable (\<lambda>a. if a = UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) then InvalidPTE else pt a))) else kheap s a\<rparr>)\<rbrakk> \<Longrightarrow> (r \<unrhd> q) s proof (prove)
goal (2 subgoals):
 1. \<And>s pt asid pa. \<lbrakk>kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); a_type (ArchObj (PageTable pt)) = a_type (ArchObj (PageTable (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := InvalidPTE)))); asid_table (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pt_bits then Some (ArchObj (PageTable (\<lambda>a. if a = UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) then InvalidPTE else pt a))) else kheap s a\<rparr>) asid = Some pa\<rbrakk> \<Longrightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) asid) None] \<unrhd> pa) s
 2. \<And>s pt ref pa ref' p'. \<lbrakk>kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); a_type (ArchObj (PageTable pt)) = a_type (ArchObj (PageTable (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := InvalidPTE)))); (ref \<unrhd> pa) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pt_bits then Some (ArchObj (PageTable (\<lambda>a. if a = UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) then InvalidPTE else pt a))) else kheap s a\<rparr>); ((ref, pa), ref', p') \<in> vs_lookup_pages1 (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pt_bits then Some (ArchObj (PageTable (\<lambda>a. if a = UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) then InvalidPTE else pt a))) else kheap s a\<rparr>); (ref \<unrhd> pa) s\<rbrakk> \<Longrightarrow> (ref' \<unrhd> p') s proof (prove)
goal (1 subgoal):
 1. \<And>s pt ref pa ref' p'. \<lbrakk>kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); a_type (ArchObj (PageTable pt)) = a_type (ArchObj (PageTable (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := InvalidPTE)))); (ref \<unrhd> pa) (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pt_bits then Some (ArchObj (PageTable (\<lambda>a. if a = UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) then InvalidPTE else pt a))) else kheap s a\<rparr>); ((ref, pa), ref', p') \<in> vs_lookup_pages1 (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pt_bits then Some (ArchObj (PageTable (\<lambda>a. if a = UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) then InvalidPTE else pt a))) else kheap s a\<rparr>); (ref \<unrhd> pa) s\<rbrakk> \<Longrightarrow> (ref' \<unrhd> p') s proof (prove)
goal (1 subgoal):
 1. \<And>s pt ref pa ref' p'. \<lbrakk>kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); a_type (ArchObj (PageTable pt)) = a_type (ArchObj (PageTable (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := InvalidPTE)))); ((ref, pa), ref', p') \<in> vs_lookup_pages1 (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pt_bits then Some (ArchObj (PageTable (\<lambda>a. if a = UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) then InvalidPTE else pt a))) else kheap s a\<rparr>); (ref \<unrhd> pa) s\<rbrakk> \<Longrightarrow> (ref' \<unrhd> p') s proof (prove)
goal (1 subgoal):
 1. \<And>s pt ref pa ref' p'. \<lbrakk>kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); a_type (ArchObj (PageTable pt)) = a_type (ArchObj (PageTable (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := InvalidPTE)))); ((ref, pa), ref', p') \<in> vs_lookup_pages1 (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pt_bits then Some (ArchObj (PageTable (\<lambda>a. if a = UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) then InvalidPTE else pt a))) else kheap s a\<rparr>)\<rbrakk> \<Longrightarrow> ((ref, pa), ref', p') \<in> vs_lookup_pages1 s