theory ArchVSpace_AI

lemma update_self_reachable_pages:
  "\<lbrakk>(ref \<unrhd> p) s; valid_asid_table (arm_asid_table (arch_state s)) s;
    valid_vspace_objs s\<rbrakk>
   \<Longrightarrow> (ref \<unrhd> p) (s \<lparr>kheap := \<lambda>a. if a = p then Some y else kheap s a\<rparr>)" apply (erule (2) vs_lookup_pagesE_alt[OF _ _ valid_asid_table_ran]) apply (rule vs_lookup_pages_atI, clarsimp) apply (rule_tac ap=ap in vs_lookup_pages_apI, auto simp: obj_at_def)[1] apply (rule_tac ap=ap and pd=pd in vs_lookup_pages_pdI,
          auto simp: obj_at_def pde_ref_pages_def data_at_def
              split: pde.splits)[1] apply (rule_tac ap=ap and pd=pd in vs_lookup_pages_ptI,
          auto simp: obj_at_def pde_ref_pages_def pte_ref_pages_def data_at_def
              split: pde.splits pte.splits)[1] done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(ref \<unrhd> p) s; valid_asid_table (asid_table s) s; valid_vspace_objs s\<rbrakk> \<Longrightarrow> (ref \<unrhd> p) (s\<lparr>kheap := \<lambda>a. if a = p then Some y else kheap s a\<rparr>) proof (prove)
goal (4 subgoals):
 1. \<And>a. \<lbrakk>valid_asid_table (asid_table s) s; valid_vspace_objs s; asid_table s a = Some p; typ_at (AArch AASIDPool) p s\<rbrakk> \<Longrightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) a) None] \<unrhd> p) (s\<lparr>kheap := \<lambda>a. if a = p then Some y else kheap s a\<rparr>)
 2. \<And>a p\<^sub>1 ap b. \<lbrakk>valid_asid_table (asid_table s) s; valid_vspace_objs s; asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p; typ_at (AArch APageDirectory) p s\<rbrakk> \<Longrightarrow> ([VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] \<unrhd> p) (s\<lparr>kheap := \<lambda>a. if a = p then Some y else kheap s a\<rparr>)
 3. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>valid_asid_table (asid_table s) s; valid_vspace_objs s; asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p\<^sub>2; kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)); c \<notin> kernel_mapping_slots; pde_ref_pages (pd c) = Some p; valid_pde (pd c) s\<rbrakk> \<Longrightarrow> ([VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] \<unrhd> p) (s\<lparr>kheap := \<lambda>a. if a = p then Some y else kheap s a\<rparr>)
 4. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c addr x ya pt d. \<lbrakk>valid_asid_table (asid_table s) s; valid_vspace_objs s; asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p\<^sub>2; kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)); c \<notin> kernel_mapping_slots; pd c = PageTablePDE addr x ya; kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)); pte_ref_pages (pt d) = Some p; valid_pte (pt d) s\<rbrakk> \<Longrightarrow> ([VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable), VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] \<unrhd> p) (s\<lparr>kheap := \<lambda>a. if a = p then Some y else kheap s a\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>a p\<^sub>1 ap b. \<lbrakk>valid_asid_table (asid_table s) s; valid_vspace_objs s; asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p; typ_at (AArch APageDirectory) p s\<rbrakk> \<Longrightarrow> ([VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] \<unrhd> p) (s\<lparr>kheap := \<lambda>a. if a = p then Some y else kheap s a\<rparr>)
 2. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>valid_asid_table (asid_table s) s; valid_vspace_objs s; asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p\<^sub>2; kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)); c \<notin> kernel_mapping_slots; pde_ref_pages (pd c) = Some p; valid_pde (pd c) s\<rbrakk> \<Longrightarrow> ([VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] \<unrhd> p) (s\<lparr>kheap := \<lambda>a. if a = p then Some y else kheap s a\<rparr>)
 3. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c addr x ya pt d. \<lbrakk>valid_asid_table (asid_table s) s; valid_vspace_objs s; asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p\<^sub>2; kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)); c \<notin> kernel_mapping_slots; pd c = PageTablePDE addr x ya; kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)); pte_ref_pages (pt d) = Some p; valid_pte (pt d) s\<rbrakk> \<Longrightarrow> ([VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable), VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] \<unrhd> p) (s\<lparr>kheap := \<lambda>a. if a = p then Some y else kheap s a\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>valid_asid_table (asid_table s) s; valid_vspace_objs s; asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p\<^sub>2; kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)); c \<notin> kernel_mapping_slots; pde_ref_pages (pd c) = Some p; valid_pde (pd c) s\<rbrakk> \<Longrightarrow> ([VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] \<unrhd> p) (s\<lparr>kheap := \<lambda>a. if a = p then Some y else kheap s a\<rparr>)
 2. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c addr x ya pt d. \<lbrakk>valid_asid_table (asid_table s) s; valid_vspace_objs s; asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p\<^sub>2; kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)); c \<notin> kernel_mapping_slots; pd c = PageTablePDE addr x ya; kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)); pte_ref_pages (pt d) = Some p; valid_pte (pt d) s\<rbrakk> \<Longrightarrow> ([VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable), VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] \<unrhd> p) (s\<lparr>kheap := \<lambda>a. if a = p then Some y else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c addr x ya pt d. \<lbrakk>valid_asid_table (asid_table s) s; valid_vspace_objs s; asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p\<^sub>2; kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)); c \<notin> kernel_mapping_slots; pd c = PageTablePDE addr x ya; kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)); pte_ref_pages (pt d) = Some p; valid_pte (pt d) s\<rbrakk> \<Longrightarrow> ([VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable), VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] \<unrhd> p) (s\<lparr>kheap := \<lambda>a. if a = p then Some y else kheap s a\<rparr>) proof (prove)
goal:
No subgoals!