theory ArchAcc_AI

lemma vs_lookup_pages_pt_eq:
  "\<lbrakk>valid_vspace_objs s;
    \<forall>p\<in>ran (arm_asid_table (arch_state s)). asid_pool_at p s;
    page_table_at p s\<rbrakk>
   \<Longrightarrow> (ref \<unrhd> p) s = (ref \<rhd> p) s" apply (rule iffI[rotated]) apply (erule vs_lookup_pages_vs_lookupI) apply (erule (2) vs_lookup_pagesE_alt) apply (clarsimp simp: obj_at_def)+ apply (clarsimp simp: obj_at_def pde_ref_pages_def
                  split: pde.splits) apply (erule (5) vs_lookup_pdI) apply (auto simp: obj_at_def pte_ref_pages_def data_at_def
                 split: pte.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_vspace_objs s; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s; typ_at (AArch APageTable) p s\<rbrakk> \<Longrightarrow> (ref \<unrhd> p) s = (ref \<rhd> p) s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_vspace_objs s; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s; typ_at (AArch APageTable) p s; (ref \<rhd> p) s\<rbrakk> \<Longrightarrow> (ref \<unrhd> p) s
 2. \<lbrakk>valid_vspace_objs s; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s; typ_at (AArch APageTable) p s; (ref \<unrhd> p) s\<rbrakk> \<Longrightarrow> (ref \<rhd> p) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_vspace_objs s; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s; typ_at (AArch APageTable) p s; (ref \<unrhd> p) s\<rbrakk> \<Longrightarrow> (ref \<rhd> p) s proof (prove)
goal (4 subgoals):
 1. \<And>a. \<lbrakk>valid_vspace_objs s; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s; typ_at (AArch APageTable) p s; asid_table s a = Some p; typ_at (AArch AASIDPool) p s\<rbrakk> \<Longrightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> p) s
 2. \<And>a p\<^sub>1 ap b. \<lbrakk>valid_vspace_objs s; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s; typ_at (AArch APageTable) p 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] \<rhd> p) s
 3. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>valid_vspace_objs s; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s; typ_at (AArch APageTable) p 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] \<rhd> p) s
 4. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c addr x y pt d. \<lbrakk>valid_vspace_objs s; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s; typ_at (AArch APageTable) p 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 y; 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] \<rhd> p) s proof (prove)
goal (2 subgoals):
 1. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c pt. \<lbrakk>valid_vspace_objs s; \<forall>p\<in>ran (asid_table s). \<exists>ko. kheap s p = Some ko \<and> a_type ko = AArch AASIDPool; 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; kheap s p = Some (ArchObj (PageTable pt))\<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] \<rhd> p) s
 2. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c addr x y pt d. \<lbrakk>valid_vspace_objs s; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s; typ_at (AArch APageTable) p 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 y; 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] \<rhd> p) s proof (prove)
goal (4 subgoals):
 1. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c x21 x22 x23 pta. \<lbrakk>kheap s (ptrFromPAddr x21) = Some (ArchObj (PageTable pta)); valid_vspace_objs s; \<forall>p\<in>ran (asid_table s). \<exists>ko. kheap s p = Some ko \<and> a_type ko = AArch AASIDPool; 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 x21 x22 x23; p = ptrFromPAddr x21\<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] \<rhd> ptrFromPAddr x21) s
 2. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c pt x31 x32 x33 x34. \<lbrakk>data_at ARMSection (ptrFromPAddr x31) s; kheap s (ptrFromPAddr x31) = Some (ArchObj (PageTable pt)); valid_vspace_objs s; \<forall>p\<in>ran (asid_table s). \<exists>ko. kheap s p = Some ko \<and> a_type ko = AArch AASIDPool; 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 = SectionPDE x31 x32 x33 x34; p = ptrFromPAddr x31\<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] \<rhd> ptrFromPAddr x31) s
 3. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c pt x41 x42 x43. \<lbrakk>data_at ARMSuperSection (ptrFromPAddr x41) s; kheap s (ptrFromPAddr x41) = Some (ArchObj (PageTable pt)); valid_vspace_objs s; \<forall>p\<in>ran (asid_table s). \<exists>ko. kheap s p = Some ko \<and> a_type ko = AArch AASIDPool; 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 = SuperSectionPDE x41 x42 x43; p = ptrFromPAddr x41\<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] \<rhd> ptrFromPAddr x41) s
 4. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c addr x y pt d. \<lbrakk>valid_vspace_objs s; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s; typ_at (AArch APageTable) p 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 y; 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] \<rhd> p) s proof (prove)
goal (3 subgoals):
 1. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c pt x31 x32 x33 x34. \<lbrakk>data_at ARMSection (ptrFromPAddr x31) s; kheap s (ptrFromPAddr x31) = Some (ArchObj (PageTable pt)); valid_vspace_objs s; \<forall>p\<in>ran (asid_table s). \<exists>ko. kheap s p = Some ko \<and> a_type ko = AArch AASIDPool; 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 = SectionPDE x31 x32 x33 x34; p = ptrFromPAddr x31\<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] \<rhd> ptrFromPAddr x31) s
 2. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c pt x41 x42 x43. \<lbrakk>data_at ARMSuperSection (ptrFromPAddr x41) s; kheap s (ptrFromPAddr x41) = Some (ArchObj (PageTable pt)); valid_vspace_objs s; \<forall>p\<in>ran (asid_table s). \<exists>ko. kheap s p = Some ko \<and> a_type ko = AArch AASIDPool; 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 = SuperSectionPDE x41 x42 x43; p = ptrFromPAddr x41\<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] \<rhd> ptrFromPAddr x41) s
 3. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c addr x y pt d. \<lbrakk>valid_vspace_objs s; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s; typ_at (AArch APageTable) p 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 y; 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] \<rhd> p) s proof (prove)
goal:
No subgoals!