theory ArchVSpace_AI

lemma vs_lookup_vs_lookup_pagesI':
  "\<lbrakk>(r \<unrhd> p) s; page_table_at p s \<or> page_directory_at p s \<or> asid_pool_at p s;
    valid_vspace_objs s; valid_asid_table (arm_asid_table (arch_state s)) s\<rbrakk>
   \<Longrightarrow> (r \<rhd> p) s" apply (erule (1) vs_lookup_pagesE_alt) apply (clarsimp simp:ran_def) apply (drule (2) valid_asid_tableD) apply (rule vs_lookupI) apply (fastforce simp: vs_asid_refs_def graph_of_def) apply simp apply (rule vs_lookupI) apply (fastforce simp: vs_asid_refs_def graph_of_def) apply (rule rtrancl_into_rtrancl[OF rtrancl.intros(1)]) apply (fastforce simp: vs_lookup1_def obj_at_def vs_refs_def graph_of_def) apply (rule vs_lookupI) apply (fastforce simp: vs_asid_refs_def graph_of_def) apply (rule_tac y="([VSRef (ucast b) (Some AASIDPool), VSRef (ucast a) None], p\<^sub>2)" in rtrancl_trans) apply (rule rtrancl_into_rtrancl[OF rtrancl.intros(1)]) apply (fastforce simp: vs_lookup1_def obj_at_def vs_refs_def graph_of_def) apply (rule rtrancl_into_rtrancl[OF rtrancl.intros(1)]) apply (clarsimp simp: vs_lookup1_def obj_at_def vs_refs_def graph_of_def) apply (rule_tac x="(c, p)" in image_eqI) apply simp apply (fastforce simp: pde_ref_def pde_ref_pages_def valid_pde_def obj_at_def
                          a_type_def data_at_def
                   split: pde.splits if_splits arch_kernel_obj.splits) apply (rule vs_lookupI) apply (fastforce simp: vs_asid_refs_def graph_of_def) apply (rule_tac y="([VSRef (ucast b) (Some AASIDPool), VSRef (ucast a) None], p\<^sub>2)" in rtrancl_trans) apply (rule rtrancl_into_rtrancl[OF rtrancl.intros(1)]) apply (fastforce simp: vs_lookup1_def obj_at_def vs_refs_def graph_of_def) apply (rule_tac y="([VSRef (ucast c) (Some APageDirectory), VSRef (ucast b) (Some AASIDPool),
           VSRef (ucast a) None], (ptrFromPAddr addr))" in rtrancl_trans) apply (rule rtrancl_into_rtrancl[OF rtrancl.intros(1)]) apply (clarsimp simp: vs_lookup1_def obj_at_def vs_refs_def graph_of_def) apply (rule_tac x="(c,(ptrFromPAddr addr))" in image_eqI) apply simp apply (clarsimp simp: pde_ref_def) apply (rule rtrancl_into_rtrancl[OF rtrancl.intros(1)]) apply (auto simp: data_at_def vs_lookup1_def obj_at_def vs_refs_def graph_of_def
                    pte_ref_pages_def a_type_def
             split: pte.splits if_splits arch_kernel_obj.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(r \<unrhd> p) s; typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) s\<rbrakk> \<Longrightarrow> (r \<rhd> p) s proof (prove)
goal (5 subgoals):
 1. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) s\<rbrakk> \<Longrightarrow> \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s
 2. \<And>a. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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
 3. \<And>a p\<^sub>1 ap b. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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
 4. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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
 5. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c addr x y pt d. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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 (5 subgoals):
 1. \<And>pa a. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) s; asid_table s a = Some pa\<rbrakk> \<Longrightarrow> typ_at (AArch AASIDPool) pa s
 2. \<And>a. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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
 3. \<And>a p\<^sub>1 ap b. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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
 4. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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
 5. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c addr x y pt d. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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 (5 subgoals):
 1. \<And>a. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) s; asid_table s a = Some p; typ_at (AArch AASIDPool) p s\<rbrakk> \<Longrightarrow> ?ref'16 a \<in> vs_asid_refs (asid_table s)
 2. \<And>a. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) s; asid_table s a = Some p; typ_at (AArch AASIDPool) p s\<rbrakk> \<Longrightarrow> (?ref'16 a, [VSRef (UCAST(7 \<rightarrow> 32) a) None], p) \<in> (vs_lookup1 s)\<^sup>*
 3. \<And>a p\<^sub>1 ap b. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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
 4. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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
 5. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c addr x y pt d. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) s; asid_table s a = Some p; typ_at (AArch AASIDPool) p s\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) a) None], p), [VSRef (UCAST(7 \<rightarrow> 32) a) None], p) \<in> (vs_lookup1 s)\<^sup>*
 2. \<And>a p\<^sub>1 ap b. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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
 2. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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
 3. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c addr x y pt d. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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> ?ref'30 a p\<^sub>1 ap b \<in> vs_asid_refs (asid_table s)
 2. \<And>a p\<^sub>1 ap b. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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> (?ref'30 a p\<^sub>1 ap b, [VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], p) \<in> (vs_lookup1 s)\<^sup>*
 3. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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(7 \<rightarrow> 32) a) None], p\<^sub>1), [VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], p) \<in> (vs_lookup1 s)\<^sup>*
 2. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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
 3. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c addr x y pt d. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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(7 \<rightarrow> 32) a) None], p\<^sub>1), [VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], p) \<in> vs_lookup1 s
 2. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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
 3. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c addr x y pt d. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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
 2. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c addr x y pt d. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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> ?ref'73 a p\<^sub>1 ap b p\<^sub>2 pd c \<in> vs_asid_refs (asid_table s)
 2. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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> (?ref'73 a p\<^sub>1 ap b p\<^sub>2 pd c, [VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], p) \<in> (vs_lookup1 s)\<^sup>*
 3. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c addr x y pt d. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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(7 \<rightarrow> 32) a) None], p\<^sub>1), [VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], p) \<in> (vs_lookup1 s)\<^sup>*
 2. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c addr x y pt d. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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(7 \<rightarrow> 32) a) None], p\<^sub>1), [VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], p\<^sub>2) \<in> (vs_lookup1 s)\<^sup>*
 2. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], p\<^sub>2), [VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], p) \<in> (vs_lookup1 s)\<^sup>*
 3. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c addr x y pt d. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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(7 \<rightarrow> 32) a) None], p\<^sub>1), [VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], p\<^sub>2) \<in> vs_lookup1 s
 2. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], p\<^sub>2), [VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], p) \<in> (vs_lookup1 s)\<^sup>*
 3. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c addr x y pt d. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], p\<^sub>2), [VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], p) \<in> (vs_lookup1 s)\<^sup>*
 2. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c addr x y pt d. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], p\<^sub>2), [VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], p) \<in> vs_lookup1 s
 2. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c addr x y pt d. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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. \<lbrakk>(\<exists>ko. kheap s p = Some ko \<and> a_type ko = AArch APageTable) \<or> (\<exists>ko. kheap s p = Some ko \<and> a_type ko = AArch APageDirectory) \<or> (\<exists>ko. kheap s p = Some ko \<and> a_type ko = AArch AASIDPool); valid_vspace_objs s; valid_asid_table (asid_table s) 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), p) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` {(x, y). (if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) = Some y}
 2. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c addr x y pt d. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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. \<lbrakk>(\<exists>ko. kheap s p = Some ko \<and> a_type ko = AArch APageTable) \<or> (\<exists>ko. kheap s p = Some ko \<and> a_type ko = AArch APageDirectory) \<or> (\<exists>ko. kheap s p = Some ko \<and> a_type ko = AArch AASIDPool); valid_vspace_objs s; valid_asid_table (asid_table s) 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), p) = (case (c, p) of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x))
 2. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>(\<exists>ko. kheap s p = Some ko \<and> a_type ko = AArch APageTable) \<or> (\<exists>ko. kheap s p = Some ko \<and> a_type ko = AArch APageDirectory) \<or> (\<exists>ko. kheap s p = Some ko \<and> a_type ko = AArch AASIDPool); valid_vspace_objs s; valid_asid_table (asid_table s) 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> (c, p) \<in> {(x, y). (if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) = Some y}
 3. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c addr x y pt d. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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. \<lbrakk>(\<exists>ko. kheap s p = Some ko \<and> a_type ko = AArch APageTable) \<or> (\<exists>ko. kheap s p = Some ko \<and> a_type ko = AArch APageDirectory) \<or> (\<exists>ko. kheap s p = Some ko \<and> a_type ko = AArch AASIDPool); valid_vspace_objs s; valid_asid_table (asid_table s) 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> (c, p) \<in> {(x, y). (if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) = Some y}
 2. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c addr x y pt d. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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 (1 subgoal):
 1. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c addr x y pt d. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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 addr x y pt d. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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> ?ref'229 a p\<^sub>1 ap b p\<^sub>2 pd c addr x y pt d \<in> vs_asid_refs (asid_table s)
 2. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c addr x y pt d. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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> (?ref'229 a p\<^sub>1 ap b p\<^sub>2 pd c addr x y pt d, [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], p) \<in> (vs_lookup1 s)\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c addr x y pt d. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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(7 \<rightarrow> 32) a) None], p\<^sub>1), [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], p) \<in> (vs_lookup1 s)\<^sup>* proof (prove)
goal (2 subgoals):
 1. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c addr x y pt d. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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(7 \<rightarrow> 32) a) None], p\<^sub>1), [VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], p\<^sub>2) \<in> (vs_lookup1 s)\<^sup>*
 2. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c addr x y pt d. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], p\<^sub>2), [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], p) \<in> (vs_lookup1 s)\<^sup>* proof (prove)
goal (2 subgoals):
 1. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c addr x y pt d. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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(7 \<rightarrow> 32) a) None], p\<^sub>1), [VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], p\<^sub>2) \<in> vs_lookup1 s
 2. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c addr x y pt d. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], p\<^sub>2), [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], p) \<in> (vs_lookup1 s)\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c addr x y pt d. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], p\<^sub>2), [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], p) \<in> (vs_lookup1 s)\<^sup>* proof (prove)
goal (2 subgoals):
 1. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c addr x y pt d. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], p\<^sub>2), [VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], ptrFromPAddr addr) \<in> (vs_lookup1 s)\<^sup>*
 2. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c addr x y pt d. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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(12 \<rightarrow> 32) c) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], ptrFromPAddr addr), [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], p) \<in> (vs_lookup1 s)\<^sup>* proof (prove)
goal (2 subgoals):
 1. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c addr x y pt d. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], p\<^sub>2), [VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], ptrFromPAddr addr) \<in> vs_lookup1 s
 2. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c addr x y pt d. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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(12 \<rightarrow> 32) c) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], ptrFromPAddr addr), [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], p) \<in> (vs_lookup1 s)\<^sup>* proof (prove)
goal (2 subgoals):
 1. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c addr x y pt d. \<lbrakk>(\<exists>ko. kheap s p = Some ko \<and> a_type ko = AArch APageTable) \<or> (\<exists>ko. kheap s p = Some ko \<and> a_type ko = AArch APageDirectory) \<or> (\<exists>ko. kheap s p = Some ko \<and> a_type ko = AArch AASIDPool); valid_vspace_objs s; valid_asid_table (asid_table s) 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(12 \<rightarrow> 32) c) (Some APageDirectory), ptrFromPAddr addr) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` {(x, y). (if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) = Some y}
 2. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c addr x y pt d. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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(12 \<rightarrow> 32) c) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], ptrFromPAddr addr), [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], p) \<in> (vs_lookup1 s)\<^sup>* proof (prove)
goal (3 subgoals):
 1. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c addr x y pt d. \<lbrakk>(\<exists>ko. kheap s p = Some ko \<and> a_type ko = AArch APageTable) \<or> (\<exists>ko. kheap s p = Some ko \<and> a_type ko = AArch APageDirectory) \<or> (\<exists>ko. kheap s p = Some ko \<and> a_type ko = AArch AASIDPool); valid_vspace_objs s; valid_asid_table (asid_table s) 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(12 \<rightarrow> 32) c) (Some APageDirectory), ptrFromPAddr addr) = (case (c, ptrFromPAddr addr) of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x))
 2. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c addr x y pt d. \<lbrakk>(\<exists>ko. kheap s p = Some ko \<and> a_type ko = AArch APageTable) \<or> (\<exists>ko. kheap s p = Some ko \<and> a_type ko = AArch APageDirectory) \<or> (\<exists>ko. kheap s p = Some ko \<and> a_type ko = AArch AASIDPool); valid_vspace_objs s; valid_asid_table (asid_table s) 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> (c, ptrFromPAddr addr) \<in> {(x, y). (if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) = Some y}
 3. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c addr x y pt d. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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(12 \<rightarrow> 32) c) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], ptrFromPAddr addr), [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], p) \<in> (vs_lookup1 s)\<^sup>* proof (prove)
goal (2 subgoals):
 1. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c addr x y pt d. \<lbrakk>(\<exists>ko. kheap s p = Some ko \<and> a_type ko = AArch APageTable) \<or> (\<exists>ko. kheap s p = Some ko \<and> a_type ko = AArch APageDirectory) \<or> (\<exists>ko. kheap s p = Some ko \<and> a_type ko = AArch AASIDPool); valid_vspace_objs s; valid_asid_table (asid_table s) 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> (c, ptrFromPAddr addr) \<in> {(x, y). (if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) = Some y}
 2. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c addr x y pt d. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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(12 \<rightarrow> 32) c) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], ptrFromPAddr addr), [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], p) \<in> (vs_lookup1 s)\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c addr x y pt d. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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(12 \<rightarrow> 32) c) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], ptrFromPAddr addr), [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], p) \<in> (vs_lookup1 s)\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c addr x y pt d. \<lbrakk>typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s; valid_vspace_objs s; valid_asid_table (asid_table s) 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(12 \<rightarrow> 32) c) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], ptrFromPAddr addr), [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], p) \<in> vs_lookup1 s proof (prove)
goal:
No subgoals!