theory ArchInvariants_AI

lemma valid_vspace_objs_alt:
  "(\<forall>p\<in>ran (arm_asid_table (arch_state s)). asid_pool_at p s) \<and>
   valid_vspace_objs s \<longleftrightarrow>
   (\<forall>a p. arm_asid_table (arch_state s) a = Some p \<longrightarrow>
          typ_at (AArch AASIDPool) p s) \<and>
   (\<forall>a p\<^sub>1 ap b p.
          arm_asid_table (arch_state s) a = Some p\<^sub>1 \<longrightarrow>
          kheap s p\<^sub>1 = Some (ArchObj (arch_kernel_obj.ASIDPool ap)) \<longrightarrow>
          ap b = Some p \<longrightarrow> page_directory_at p s) \<and>
   (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c.
          arm_asid_table (arch_state s) a = Some p\<^sub>1 \<longrightarrow>
          kheap s p\<^sub>1 = Some (ArchObj (arch_kernel_obj.ASIDPool ap)) \<longrightarrow>
          ap b = Some p\<^sub>2 \<longrightarrow>
          kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow>
          c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s) \<and>
   (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt.
          arm_asid_table (arch_state s) a = Some p\<^sub>1 \<longrightarrow>
          kheap s p\<^sub>1 = Some (ArchObj (arch_kernel_obj.ASIDPool ap)) \<longrightarrow>
          ap b = Some p\<^sub>2 \<longrightarrow>
          kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow>
          c \<notin> kernel_mapping_slots \<longrightarrow>
          pd c = pde.PageTablePDE addr f w \<longrightarrow>
          kheap s (ptrFromPAddr addr) =
            Some (ArchObj (PageTable pt)) \<longrightarrow>
          (\<forall>d. valid_pte (pt d) s))" apply (intro iffI conjI) apply fastforce apply (clarsimp simp: obj_at_def) apply (thin_tac "Ball S P" for S P) apply (frule vs_lookup_atI) apply (drule valid_vspace_objsD) apply (simp add: obj_at_def) apply assumption apply (clarsimp simp: valid_vspace_obj_def obj_at_def ranI) apply (clarsimp simp: obj_at_def) apply (thin_tac "Ball S P" for S P) apply (frule (2) vs_lookup_apI) apply (drule valid_vspace_objsD) apply (simp add: obj_at_def valid_vspace_obj_def) apply assumption apply (fastforce simp: valid_vspace_obj_def) apply (clarsimp simp: obj_at_def) apply (thin_tac "Ball S P" for S P) apply (frule (5) vs_lookup_pdI) apply (drule valid_vspace_objsD) apply (simp add: obj_at_def) apply assumption apply (fastforce simp: valid_vspace_obj_def) apply (clarsimp simp: ran_def) apply (clarsimp simp: valid_vspace_objs_def vs_lookup_def) apply (erule converse_rtranclE) apply (clarsimp simp: vs_asid_refs_def graph_of_def) apply (drule spec, drule spec, erule impE, assumption) apply (clarsimp simp: obj_at_def ran_def) apply (erule converse_rtranclE) apply (drule vs_lookup1D) apply (clarsimp simp: vs_asid_refs_def graph_of_def) apply (drule spec, drule spec, erule impE, assumption) apply (drule spec, drule spec, erule impE, assumption) apply (drule spec, drule spec, erule impE, assumption) apply (clarsimp simp: obj_at_def) apply (clarsimp simp: vs_refs_def graph_of_def image_def) apply (drule spec, drule spec, erule impE, assumption) apply (drule spec, drule spec, erule impE, assumption) apply fastforce apply (erule converse_rtranclE) apply (clarsimp dest!: vs_lookup1D) apply (clarsimp simp: vs_asid_refs_def graph_of_def) apply (drule spec, drule spec, erule impE, assumption) apply (drule spec, drule spec, erule impE, assumption) apply (drule spec, drule spec, erule impE, assumption) apply (drule spec, drule spec, erule impE, assumption) apply (clarsimp simp: obj_at_def) apply (clarsimp simp: vs_refs_def graph_of_def image_def) apply (drule spec, drule spec, erule impE, assumption) apply (drule spec, drule spec, erule impE, assumption) apply (drule spec, drule spec, erule impE, assumption) apply (clarsimp simp: graph_of_def  split: if_split_asm) apply (drule_tac x=ab in spec) apply (clarsimp simp: pde_ref_def obj_at_def
                  split: pde.splits) apply (clarsimp dest!: vs_lookup1D) apply (clarsimp simp: vs_asid_refs_def graph_of_def) apply (drule spec, drule spec, erule impE, assumption) apply (drule spec, drule spec, erule impE, assumption) apply (drule spec, drule spec, erule impE, assumption) apply (drule spec, drule spec, erule impE, assumption) apply (clarsimp simp: obj_at_def) apply (clarsimp simp: vs_refs_def graph_of_def image_def) apply (drule spec, drule spec, erule impE, assumption) apply (drule spec, drule spec, erule impE, assumption) apply (drule spec, drule spec, erule impE, assumption) apply (clarsimp simp: graph_of_def  split: if_split_asm) apply (drule_tac x=ab in spec) apply (clarsimp simp: pde_ref_def obj_at_def
                 split: pde.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((\<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s) \<and> valid_vspace_objs s) = ((\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s) \<and> (\<forall>a p\<^sub>1 ap b p. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))) proof (prove)
goal (6 subgoals):
 1. (\<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s) \<and> valid_vspace_objs s \<Longrightarrow> \<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s
 2. (\<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s) \<and> valid_vspace_objs s \<Longrightarrow> \<forall>a p\<^sub>1 ap b p. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s
 3. (\<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s) \<and> valid_vspace_objs s \<Longrightarrow> \<forall>a p\<^sub>1 ap b p\<^sub>2 pd c. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s
 4. (\<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s) \<and> valid_vspace_objs s \<Longrightarrow> \<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)
 5. (\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s) \<and> (\<forall>a p\<^sub>1 ap b p. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)) \<Longrightarrow> \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s
 6. (\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s) \<and> (\<forall>a p\<^sub>1 ap b p. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)) \<Longrightarrow> valid_vspace_objs s proof (prove)
goal (5 subgoals):
 1. (\<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s) \<and> valid_vspace_objs s \<Longrightarrow> \<forall>a p\<^sub>1 ap b p. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s
 2. (\<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s) \<and> valid_vspace_objs s \<Longrightarrow> \<forall>a p\<^sub>1 ap b p\<^sub>2 pd c. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s
 3. (\<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s) \<and> valid_vspace_objs s \<Longrightarrow> \<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)
 4. (\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s) \<and> (\<forall>a p\<^sub>1 ap b p. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)) \<Longrightarrow> \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s
 5. (\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s) \<and> (\<forall>a p\<^sub>1 ap b p. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)) \<Longrightarrow> valid_vspace_objs s proof (prove)
goal (5 subgoals):
 1. \<And>a p\<^sub>1 ap b p. \<lbrakk>\<forall>p\<in>ran (asid_table s). \<exists>ko. kheap s p = Some ko \<and> a_type ko = AArch AASIDPool; 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\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s p = Some ko \<and> a_type ko = AArch APageDirectory
 2. (\<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s) \<and> valid_vspace_objs s \<Longrightarrow> \<forall>a p\<^sub>1 ap b p\<^sub>2 pd c. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s
 3. (\<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s) \<and> valid_vspace_objs s \<Longrightarrow> \<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)
 4. (\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s) \<and> (\<forall>a p\<^sub>1 ap b p. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)) \<Longrightarrow> \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s
 5. (\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s) \<and> (\<forall>a p\<^sub>1 ap b p. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)) \<Longrightarrow> valid_vspace_objs s proof (prove)
goal (5 subgoals):
 1. \<And>a p\<^sub>1 ap b p. \<lbrakk>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\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s p = Some ko \<and> a_type ko = AArch APageDirectory
 2. (\<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s) \<and> valid_vspace_objs s \<Longrightarrow> \<forall>a p\<^sub>1 ap b p\<^sub>2 pd c. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s
 3. (\<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s) \<and> valid_vspace_objs s \<Longrightarrow> \<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)
 4. (\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s) \<and> (\<forall>a p\<^sub>1 ap b p. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)) \<Longrightarrow> \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s
 5. (\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s) \<and> (\<forall>a p\<^sub>1 ap b p. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)) \<Longrightarrow> valid_vspace_objs s proof (prove)
goal (5 subgoals):
 1. \<And>a p\<^sub>1 ap b p. \<lbrakk>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; ([VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> p\<^sub>1) s\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s p = Some ko \<and> a_type ko = AArch APageDirectory
 2. (\<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s) \<and> valid_vspace_objs s \<Longrightarrow> \<forall>a p\<^sub>1 ap b p\<^sub>2 pd c. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s
 3. (\<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s) \<and> valid_vspace_objs s \<Longrightarrow> \<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)
 4. (\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s) \<and> (\<forall>a p\<^sub>1 ap b p. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)) \<Longrightarrow> \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s
 5. (\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s) \<and> (\<forall>a p\<^sub>1 ap b p. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)) \<Longrightarrow> valid_vspace_objs s proof (prove)
goal (7 subgoals):
 1. \<And>a p\<^sub>1 ap b p. \<lbrakk>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\<rbrakk> \<Longrightarrow> ako_at (?ao32 a p\<^sub>1 ap b p) p\<^sub>1 s
 2. \<And>a p\<^sub>1 ap b p. \<lbrakk>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\<rbrakk> \<Longrightarrow> valid_vspace_objs s
 3. \<And>a p\<^sub>1 ap b p. \<lbrakk>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; valid_vspace_obj (?ao32 a p\<^sub>1 ap b p) s\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s p = Some ko \<and> a_type ko = AArch APageDirectory
 4. (\<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s) \<and> valid_vspace_objs s \<Longrightarrow> \<forall>a p\<^sub>1 ap b p\<^sub>2 pd c. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s
 5. (\<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s) \<and> valid_vspace_objs s \<Longrightarrow> \<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)
 6. (\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s) \<and> (\<forall>a p\<^sub>1 ap b p. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)) \<Longrightarrow> \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s
 7. (\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s) \<and> (\<forall>a p\<^sub>1 ap b p. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)) \<Longrightarrow> valid_vspace_objs s proof (prove)
goal (6 subgoals):
 1. \<And>a p\<^sub>1 ap b p. \<lbrakk>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\<rbrakk> \<Longrightarrow> valid_vspace_objs s
 2. \<And>a p\<^sub>1 ap b p. \<lbrakk>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; valid_vspace_obj (ASIDPool ap) s\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s p = Some ko \<and> a_type ko = AArch APageDirectory
 3. (\<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s) \<and> valid_vspace_objs s \<Longrightarrow> \<forall>a p\<^sub>1 ap b p\<^sub>2 pd c. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s
 4. (\<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s) \<and> valid_vspace_objs s \<Longrightarrow> \<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)
 5. (\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s) \<and> (\<forall>a p\<^sub>1 ap b p. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)) \<Longrightarrow> \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s
 6. (\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s) \<and> (\<forall>a p\<^sub>1 ap b p. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)) \<Longrightarrow> valid_vspace_objs s proof (prove)
goal (5 subgoals):
 1. \<And>a p\<^sub>1 ap b p. \<lbrakk>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; valid_vspace_obj (ASIDPool ap) s\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s p = Some ko \<and> a_type ko = AArch APageDirectory
 2. (\<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s) \<and> valid_vspace_objs s \<Longrightarrow> \<forall>a p\<^sub>1 ap b p\<^sub>2 pd c. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s
 3. (\<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s) \<and> valid_vspace_objs s \<Longrightarrow> \<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)
 4. (\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s) \<and> (\<forall>a p\<^sub>1 ap b p. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)) \<Longrightarrow> \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s
 5. (\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s) \<and> (\<forall>a p\<^sub>1 ap b p. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)) \<Longrightarrow> valid_vspace_objs s proof (prove)
goal (4 subgoals):
 1. (\<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s) \<and> valid_vspace_objs s \<Longrightarrow> \<forall>a p\<^sub>1 ap b p\<^sub>2 pd c. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s
 2. (\<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s) \<and> valid_vspace_objs s \<Longrightarrow> \<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)
 3. (\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s) \<and> (\<forall>a p\<^sub>1 ap b p. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)) \<Longrightarrow> \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s
 4. (\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s) \<and> (\<forall>a p\<^sub>1 ap b p. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)) \<Longrightarrow> valid_vspace_objs s proof (prove)
goal (4 subgoals):
 1. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>\<forall>p\<in>ran (asid_table s). \<exists>ko. kheap s p = Some ko \<and> a_type ko = AArch AASIDPool; 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\<rbrakk> \<Longrightarrow> valid_pde (pd c) s
 2. (\<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s) \<and> valid_vspace_objs s \<Longrightarrow> \<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)
 3. (\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s) \<and> (\<forall>a p\<^sub>1 ap b p. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)) \<Longrightarrow> \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s
 4. (\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s) \<and> (\<forall>a p\<^sub>1 ap b p. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)) \<Longrightarrow> valid_vspace_objs s proof (prove)
goal (4 subgoals):
 1. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>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\<rbrakk> \<Longrightarrow> valid_pde (pd c) s
 2. (\<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s) \<and> valid_vspace_objs s \<Longrightarrow> \<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)
 3. (\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s) \<and> (\<forall>a p\<^sub>1 ap b p. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)) \<Longrightarrow> \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s
 4. (\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s) \<and> (\<forall>a p\<^sub>1 ap b p. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)) \<Longrightarrow> valid_vspace_objs s proof (prove)
goal (4 subgoals):
 1. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>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; ([VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> p\<^sub>2) s\<rbrakk> \<Longrightarrow> valid_pde (pd c) s
 2. (\<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s) \<and> valid_vspace_objs s \<Longrightarrow> \<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)
 3. (\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s) \<and> (\<forall>a p\<^sub>1 ap b p. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)) \<Longrightarrow> \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s
 4. (\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s) \<and> (\<forall>a p\<^sub>1 ap b p. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)) \<Longrightarrow> valid_vspace_objs s proof (prove)
goal (6 subgoals):
 1. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>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\<rbrakk> \<Longrightarrow> ako_at (?ao61 a p\<^sub>1 ap b p\<^sub>2 pd c) p\<^sub>2 s
 2. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>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\<rbrakk> \<Longrightarrow> valid_vspace_objs s
 3. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>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; valid_vspace_obj (?ao61 a p\<^sub>1 ap b p\<^sub>2 pd c) s\<rbrakk> \<Longrightarrow> valid_pde (pd c) s
 4. (\<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s) \<and> valid_vspace_objs s \<Longrightarrow> \<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)
 5. (\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s) \<and> (\<forall>a p\<^sub>1 ap b p. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)) \<Longrightarrow> \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s
 6. (\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s) \<and> (\<forall>a p\<^sub>1 ap b p. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)) \<Longrightarrow> valid_vspace_objs s proof (prove)
goal (5 subgoals):
 1. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>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\<rbrakk> \<Longrightarrow> valid_vspace_objs s
 2. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>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; valid_vspace_obj (PageDirectory pd) s\<rbrakk> \<Longrightarrow> valid_pde (pd c) s
 3. (\<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s) \<and> valid_vspace_objs s \<Longrightarrow> \<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)
 4. (\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s) \<and> (\<forall>a p\<^sub>1 ap b p. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)) \<Longrightarrow> \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s
 5. (\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s) \<and> (\<forall>a p\<^sub>1 ap b p. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)) \<Longrightarrow> valid_vspace_objs s proof (prove)
goal (4 subgoals):
 1. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>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; valid_vspace_obj (PageDirectory pd) s\<rbrakk> \<Longrightarrow> valid_pde (pd c) s
 2. (\<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s) \<and> valid_vspace_objs s \<Longrightarrow> \<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)
 3. (\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s) \<and> (\<forall>a p\<^sub>1 ap b p. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)) \<Longrightarrow> \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s
 4. (\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s) \<and> (\<forall>a p\<^sub>1 ap b p. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)) \<Longrightarrow> valid_vspace_objs s proof (prove)
goal (3 subgoals):
 1. (\<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s) \<and> valid_vspace_objs s \<Longrightarrow> \<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)
 2. (\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s) \<and> (\<forall>a p\<^sub>1 ap b p. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)) \<Longrightarrow> \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s
 3. (\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s) \<and> (\<forall>a p\<^sub>1 ap b p. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)) \<Longrightarrow> valid_vspace_objs s proof (prove)
goal (3 subgoals):
 1. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt d. \<lbrakk>\<forall>p\<in>ran (asid_table s). \<exists>ko. kheap s p = Some ko \<and> a_type ko = AArch AASIDPool; 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 f w; kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt))\<rbrakk> \<Longrightarrow> valid_pte (pt d) s
 2. (\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s) \<and> (\<forall>a p\<^sub>1 ap b p. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)) \<Longrightarrow> \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s
 3. (\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s) \<and> (\<forall>a p\<^sub>1 ap b p. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)) \<Longrightarrow> valid_vspace_objs s proof (prove)
goal (3 subgoals):
 1. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt d. \<lbrakk>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 f w; kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt))\<rbrakk> \<Longrightarrow> valid_pte (pt d) s
 2. (\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s) \<and> (\<forall>a p\<^sub>1 ap b p. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)) \<Longrightarrow> \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s
 3. (\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s) \<and> (\<forall>a p\<^sub>1 ap b p. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)) \<Longrightarrow> valid_vspace_objs s proof (prove)
goal (3 subgoals):
 1. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt d. \<lbrakk>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 f w; kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)); ([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 addr) s\<rbrakk> \<Longrightarrow> valid_pte (pt d) s
 2. (\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s) \<and> (\<forall>a p\<^sub>1 ap b p. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)) \<Longrightarrow> \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s
 3. (\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s) \<and> (\<forall>a p\<^sub>1 ap b p. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)) \<Longrightarrow> valid_vspace_objs s proof (prove)
goal (5 subgoals):
 1. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt d. \<lbrakk>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 f w; kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt))\<rbrakk> \<Longrightarrow> ako_at (?ao102 a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt d) (ptrFromPAddr addr) s
 2. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt d. \<lbrakk>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 f w; kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt))\<rbrakk> \<Longrightarrow> valid_vspace_objs s
 3. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt d. \<lbrakk>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 f w; kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)); valid_vspace_obj (?ao102 a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt d) s\<rbrakk> \<Longrightarrow> valid_pte (pt d) s
 4. (\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s) \<and> (\<forall>a p\<^sub>1 ap b p. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)) \<Longrightarrow> \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s
 5. (\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s) \<and> (\<forall>a p\<^sub>1 ap b p. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)) \<Longrightarrow> valid_vspace_objs s proof (prove)
goal (4 subgoals):
 1. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt d. \<lbrakk>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 f w; kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt))\<rbrakk> \<Longrightarrow> valid_vspace_objs s
 2. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt d. \<lbrakk>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 f w; kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)); valid_vspace_obj (PageTable pt) s\<rbrakk> \<Longrightarrow> valid_pte (pt d) s
 3. (\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s) \<and> (\<forall>a p\<^sub>1 ap b p. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)) \<Longrightarrow> \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s
 4. (\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s) \<and> (\<forall>a p\<^sub>1 ap b p. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)) \<Longrightarrow> valid_vspace_objs s proof (prove)
goal (3 subgoals):
 1. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt d. \<lbrakk>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 f w; kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)); valid_vspace_obj (PageTable pt) s\<rbrakk> \<Longrightarrow> valid_pte (pt d) s
 2. (\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s) \<and> (\<forall>a p\<^sub>1 ap b p. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)) \<Longrightarrow> \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s
 3. (\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s) \<and> (\<forall>a p\<^sub>1 ap b p. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)) \<Longrightarrow> valid_vspace_objs s proof (prove)
goal (2 subgoals):
 1. (\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s) \<and> (\<forall>a p\<^sub>1 ap b p. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)) \<Longrightarrow> \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s
 2. (\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s) \<and> (\<forall>a p\<^sub>1 ap b p. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)) \<Longrightarrow> valid_vspace_objs s proof (prove)
goal (1 subgoal):
 1. (\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s) \<and> (\<forall>a p\<^sub>1 ap b p. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)) \<Longrightarrow> valid_vspace_objs s proof (prove)
goal (1 subgoal):
 1. \<And>p rs a b ao. \<lbrakk>\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s; \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p. ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s)); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s)))); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))))))); ((a, b), rs, p) \<in> (vs_lookup1 s)\<^sup>*; (a, b) \<in> vs_asid_refs (asid_table s); ako_at ao p s\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s proof (prove)
goal (2 subgoals):
 1. \<And>p rs a b ao. \<lbrakk>\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s; \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p. ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s)); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s)))); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))))))); (a, b) \<in> vs_asid_refs (asid_table s); ako_at ao p s; (a, b) = (rs, p)\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s
 2. \<And>p rs a b ao y. \<lbrakk>\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s; \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p. ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s)); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s)))); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))))))); (a, b) \<in> vs_asid_refs (asid_table s); ako_at ao p s; ((a, b), y) \<in> vs_lookup1 s; (y, rs, p) \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s proof (prove)
goal (2 subgoals):
 1. \<And>ao aa b. \<lbrakk>\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s; \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p. ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s)); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s)))); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))))))); ako_at ao b s; asid_table s aa = Some b\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s
 2. \<And>p rs a b ao y. \<lbrakk>\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s; \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p. ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s)); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s)))); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))))))); (a, b) \<in> vs_asid_refs (asid_table s); ako_at ao p s; ((a, b), y) \<in> vs_lookup1 s; (y, rs, p) \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s proof (prove)
goal (2 subgoals):
 1. \<And>ao aa b. \<lbrakk>\<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p. ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s)); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s)))); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))))))); ako_at ao b s; asid_table s aa = Some b; typ_at (AArch AASIDPool) b s\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s
 2. \<And>p rs a b ao y. \<lbrakk>\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s; \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p. ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s)); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s)))); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))))))); (a, b) \<in> vs_asid_refs (asid_table s); ako_at ao p s; ((a, b), y) \<in> vs_lookup1 s; (y, rs, p) \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s proof (prove)
goal (1 subgoal):
 1. \<And>p rs a b ao y. \<lbrakk>\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s; \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p. ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s)); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s)))); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))))))); (a, b) \<in> vs_asid_refs (asid_table s); ako_at ao p s; ((a, b), y) \<in> vs_lookup1 s; (y, rs, p) \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s proof (prove)
goal (2 subgoals):
 1. \<And>p rs a b ao y. \<lbrakk>\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s; \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p. ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s)); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s)))); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))))))); (a, b) \<in> vs_asid_refs (asid_table s); ako_at ao p s; ((a, b), y) \<in> vs_lookup1 s; y = (rs, p)\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s
 2. \<And>p rs a b ao y ya. \<lbrakk>\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s; \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p. ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s)); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s)))); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))))))); (a, b) \<in> vs_asid_refs (asid_table s); ako_at ao p s; ((a, b), y) \<in> vs_lookup1 s; (y, ya) \<in> vs_lookup1 s; (ya, rs, p) \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s proof (prove)
goal (2 subgoals):
 1. \<And>p rs a b ao y. \<lbrakk>\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s; \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p. ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s)); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s)))); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))))))); (a, b) \<in> vs_asid_refs (asid_table s); ako_at ao p s; y = (rs, p); \<exists>rs r p p' ko. (a, b) = (rs, p) \<and> y = (r # rs, p') \<and> ko_at ko p s \<and> (r, p') \<in> vs_refs ko\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s
 2. \<And>p rs a b ao y ya. \<lbrakk>\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s; \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p. ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s)); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s)))); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))))))); (a, b) \<in> vs_asid_refs (asid_table s); ako_at ao p s; ((a, b), y) \<in> vs_lookup1 s; (y, ya) \<in> vs_lookup1 s; (ya, rs, p) \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s proof (prove)
goal (2 subgoals):
 1. \<And>p ao ab bb r ko. \<lbrakk>\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s; \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p. ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s)); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s)))); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))))))); ako_at ao p s; asid_table s ab = Some bb; ko_at ko bb s; (r, p) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s
 2. \<And>p rs a b ao y ya. \<lbrakk>\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s; \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p. ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s)); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s)))); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))))))); (a, b) \<in> vs_asid_refs (asid_table s); ako_at ao p s; ((a, b), y) \<in> vs_lookup1 s; (y, ya) \<in> vs_lookup1 s; (ya, rs, p) \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s proof (prove)
goal (2 subgoals):
 1. \<And>p ao ab bb r ko. \<lbrakk>\<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p. ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s)); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s)))); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))))))); ako_at ao p s; asid_table s ab = Some bb; ko_at ko bb s; (r, p) \<in> vs_refs ko; typ_at (AArch AASIDPool) bb s\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s
 2. \<And>p rs a b ao y ya. \<lbrakk>\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s; \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p. ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s)); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s)))); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))))))); (a, b) \<in> vs_asid_refs (asid_table s); ako_at ao p s; ((a, b), y) \<in> vs_lookup1 s; (y, ya) \<in> vs_lookup1 s; (ya, rs, p) \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s proof (prove)
goal (2 subgoals):
 1. \<And>p ao ab bb r ko. \<lbrakk>\<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s)))); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))))))); ako_at ao p s; asid_table s ab = Some bb; ko_at ko bb s; (r, p) \<in> vs_refs ko; typ_at (AArch AASIDPool) bb s; \<forall>ap. kheap s bb = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p. ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s)\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s
 2. \<And>p rs a b ao y ya. \<lbrakk>\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s; \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p. ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s)); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s)))); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))))))); (a, b) \<in> vs_asid_refs (asid_table s); ako_at ao p s; ((a, b), y) \<in> vs_lookup1 s; (y, ya) \<in> vs_lookup1 s; (ya, rs, p) \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s proof (prove)
goal (2 subgoals):
 1. \<And>p ao ab bb r ko. \<lbrakk>\<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))))))); ako_at ao p s; asid_table s ab = Some bb; ko_at ko bb s; (r, p) \<in> vs_refs ko; typ_at (AArch AASIDPool) bb s; \<forall>ap. kheap s bb = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p. ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s); \<forall>ap. kheap s bb = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s)))\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s
 2. \<And>p rs a b ao y ya. \<lbrakk>\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s; \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p. ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s)); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s)))); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))))))); (a, b) \<in> vs_asid_refs (asid_table s); ako_at ao p s; ((a, b), y) \<in> vs_lookup1 s; (y, ya) \<in> vs_lookup1 s; (ya, rs, p) \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s proof (prove)
goal (2 subgoals):
 1. \<And>p ao ab bb r ap. \<lbrakk>\<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))))))); kheap s p = Some (ArchObj ao); asid_table s ab = Some bb; kheap s bb = Some (ArchObj (ASIDPool ap)); (r, p) \<in> vs_refs (ArchObj (ASIDPool ap)); \<forall>b p. ap b = Some p \<longrightarrow> (\<exists>ko. kheap s p = Some ko \<and> a_type ko = AArch APageDirectory); \<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s))\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s
 2. \<And>p rs a b ao y ya. \<lbrakk>\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s; \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p. ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s)); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s)))); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))))))); (a, b) \<in> vs_asid_refs (asid_table s); ako_at ao p s; ((a, b), y) \<in> vs_lookup1 s; (y, ya) \<in> vs_lookup1 s; (ya, rs, p) \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s proof (prove)
goal (2 subgoals):
 1. \<And>p ao ab bb ap a. \<lbrakk>\<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))))))); kheap s p = Some (ArchObj ao); asid_table s ab = Some bb; kheap s bb = Some (ArchObj (ASIDPool ap)); \<forall>b p. ap b = Some p \<longrightarrow> (\<exists>ko. kheap s p = Some ko \<and> a_type ko = AArch APageDirectory); \<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s)); ap a = Some p\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s
 2. \<And>p rs a b ao y ya. \<lbrakk>\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s; \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p. ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s)); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s)))); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))))))); (a, b) \<in> vs_asid_refs (asid_table s); ako_at ao p s; ((a, b), y) \<in> vs_lookup1 s; (y, ya) \<in> vs_lookup1 s; (ya, rs, p) \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s proof (prove)
goal (2 subgoals):
 1. \<And>p ao ab bb ap a. \<lbrakk>kheap s p = Some (ArchObj ao); asid_table s ab = Some bb; kheap s bb = Some (ArchObj (ASIDPool ap)); \<forall>b p. ap b = Some p \<longrightarrow> (\<exists>ko. kheap s p = Some ko \<and> a_type ko = AArch APageDirectory); \<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s)); ap a = Some p; \<forall>ap. kheap s bb = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))))))\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s
 2. \<And>p rs a b ao y ya. \<lbrakk>\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s; \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p. ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s)); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s)))); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))))))); (a, b) \<in> vs_asid_refs (asid_table s); ako_at ao p s; ((a, b), y) \<in> vs_lookup1 s; (y, ya) \<in> vs_lookup1 s; (ya, rs, p) \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s proof (prove)
goal (2 subgoals):
 1. \<And>p ao ab bb ap a. \<lbrakk>kheap s p = Some (ArchObj ao); asid_table s ab = Some bb; kheap s bb = Some (ArchObj (ASIDPool ap)); \<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s)); ap a = Some p; \<forall>pa. ap (?b212 p ao ab bb ap a) = Some pa \<longrightarrow> (\<exists>ko. kheap s pa = Some ko \<and> a_type ko = AArch APageDirectory); \<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)))))\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s
 2. \<And>p rs a b ao y ya. \<lbrakk>\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s; \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p. ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s)); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s)))); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))))))); (a, b) \<in> vs_asid_refs (asid_table s); ako_at ao p s; ((a, b), y) \<in> vs_lookup1 s; (y, ya) \<in> vs_lookup1 s; (ya, rs, p) \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s proof (prove)
goal (1 subgoal):
 1. \<And>p rs a b ao y ya. \<lbrakk>\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s; \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p. ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s)); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s)))); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))))))); (a, b) \<in> vs_asid_refs (asid_table s); ako_at ao p s; ((a, b), y) \<in> vs_lookup1 s; (y, ya) \<in> vs_lookup1 s; (ya, rs, p) \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s proof (prove)
goal (2 subgoals):
 1. \<And>p rs a b ao y ya. \<lbrakk>\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s; \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p. ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s)); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s)))); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))))))); (a, b) \<in> vs_asid_refs (asid_table s); ako_at ao p s; ((a, b), y) \<in> vs_lookup1 s; (y, ya) \<in> vs_lookup1 s; ya = (rs, p)\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s
 2. \<And>p rs a b ao y ya yb. \<lbrakk>\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s; \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p. ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s)); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s)))); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))))))); (a, b) \<in> vs_asid_refs (asid_table s); ako_at ao p s; ((a, b), y) \<in> vs_lookup1 s; (y, ya) \<in> vs_lookup1 s; (ya, yb) \<in> vs_lookup1 s; (yb, rs, p) \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s proof (prove)
goal (2 subgoals):
 1. \<And>ao rsa r ra pa p' p'a ko koa. \<lbrakk>\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s; \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p. ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s)); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s)))); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))))))); (rsa, pa) \<in> vs_asid_refs (asid_table s); ako_at ao p'a s; ko_at ko pa s; (r, p') \<in> vs_refs ko; ko_at koa p' s; (ra, p'a) \<in> vs_refs koa\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s
 2. \<And>p rs a b ao y ya yb. \<lbrakk>\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s; \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p. ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s)); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s)))); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))))))); (a, b) \<in> vs_asid_refs (asid_table s); ako_at ao p s; ((a, b), y) \<in> vs_lookup1 s; (y, ya) \<in> vs_lookup1 s; (ya, yb) \<in> vs_lookup1 s; (yb, rs, p) \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s proof (prove)
goal (2 subgoals):
 1. \<And>ao r ra p' p'a ko koa a b. \<lbrakk>\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s; \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p. ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s)); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s)))); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))))))); ako_at ao p'a s; ko_at ko b s; (r, p') \<in> vs_refs ko; ko_at koa p' s; (ra, p'a) \<in> vs_refs koa; asid_table s a = Some b\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s
 2. \<And>p rs a b ao y ya yb. \<lbrakk>\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s; \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p. ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s)); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s)))); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))))))); (a, b) \<in> vs_asid_refs (asid_table s); ako_at ao p s; ((a, b), y) \<in> vs_lookup1 s; (y, ya) \<in> vs_lookup1 s; (ya, yb) \<in> vs_lookup1 s; (yb, rs, p) \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s proof (prove)
goal (2 subgoals):
 1. \<And>ao r ra p' p'a ko koa a b. \<lbrakk>\<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p. ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s)); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s)))); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))))))); ako_at ao p'a s; ko_at ko b s; (r, p') \<in> vs_refs ko; ko_at koa p' s; (ra, p'a) \<in> vs_refs koa; asid_table s a = Some b; typ_at (AArch AASIDPool) b s\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s
 2. \<And>p rs a b ao y ya yb. \<lbrakk>\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s; \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p. ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s)); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s)))); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))))))); (a, b) \<in> vs_asid_refs (asid_table s); ako_at ao p s; ((a, b), y) \<in> vs_lookup1 s; (y, ya) \<in> vs_lookup1 s; (ya, yb) \<in> vs_lookup1 s; (yb, rs, p) \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s proof (prove)
goal (2 subgoals):
 1. \<And>ao r ra p' p'a ko koa a b. \<lbrakk>\<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s)))); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))))))); ako_at ao p'a s; ko_at ko b s; (r, p') \<in> vs_refs ko; ko_at koa p' s; (ra, p'a) \<in> vs_refs koa; asid_table s a = Some b; typ_at (AArch AASIDPool) b s; \<forall>ap. kheap s b = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p. ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s)\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s
 2. \<And>p rs a b ao y ya yb. \<lbrakk>\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s; \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p. ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s)); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s)))); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))))))); (a, b) \<in> vs_asid_refs (asid_table s); ako_at ao p s; ((a, b), y) \<in> vs_lookup1 s; (y, ya) \<in> vs_lookup1 s; (ya, yb) \<in> vs_lookup1 s; (yb, rs, p) \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s proof (prove)
goal (2 subgoals):
 1. \<And>ao r ra p' p'a ko koa a b. \<lbrakk>\<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))))))); ako_at ao p'a s; ko_at ko b s; (r, p') \<in> vs_refs ko; ko_at koa p' s; (ra, p'a) \<in> vs_refs koa; asid_table s a = Some b; typ_at (AArch AASIDPool) b s; \<forall>ap. kheap s b = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p. ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s); \<forall>ap. kheap s b = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s)))\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s
 2. \<And>p rs a b ao y ya yb. \<lbrakk>\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s; \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p. ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s)); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s)))); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))))))); (a, b) \<in> vs_asid_refs (asid_table s); ako_at ao p s; ((a, b), y) \<in> vs_lookup1 s; (y, ya) \<in> vs_lookup1 s; (ya, yb) \<in> vs_lookup1 s; (yb, rs, p) \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s proof (prove)
goal (2 subgoals):
 1. \<And>ao r ra p' p'a ko koa a b. \<lbrakk>ako_at ao p'a s; ko_at ko b s; (r, p') \<in> vs_refs ko; ko_at koa p' s; (ra, p'a) \<in> vs_refs koa; asid_table s a = Some b; typ_at (AArch AASIDPool) b s; \<forall>ap. kheap s b = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p. ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s); \<forall>ap. kheap s b = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s))); \<forall>ap. kheap s b = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))))))\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s
 2. \<And>p rs a b ao y ya yb. \<lbrakk>\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s; \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p. ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s)); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s)))); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))))))); (a, b) \<in> vs_asid_refs (asid_table s); ako_at ao p s; ((a, b), y) \<in> vs_lookup1 s; (y, ya) \<in> vs_lookup1 s; (ya, yb) \<in> vs_lookup1 s; (yb, rs, p) \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s proof (prove)
goal (2 subgoals):
 1. \<And>ao r ra p' p'a koa a b ap. \<lbrakk>kheap s p'a = Some (ArchObj ao); kheap s b = Some (ArchObj (ASIDPool ap)); (r, p') \<in> vs_refs (ArchObj (ASIDPool ap)); kheap s p' = Some koa; (ra, p'a) \<in> vs_refs koa; asid_table s a = Some b; \<forall>b p. ap b = Some p \<longrightarrow> (\<exists>ko. kheap s p = Some ko \<and> a_type ko = AArch APageDirectory); \<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s)); \<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)))))\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s
 2. \<And>p rs a b ao y ya yb. \<lbrakk>\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s; \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p. ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s)); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s)))); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))))))); (a, b) \<in> vs_asid_refs (asid_table s); ako_at ao p s; ((a, b), y) \<in> vs_lookup1 s; (y, ya) \<in> vs_lookup1 s; (ya, yb) \<in> vs_lookup1 s; (yb, rs, p) \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s proof (prove)
goal (2 subgoals):
 1. \<And>ao ra p' p'a koa a b ap aa. \<lbrakk>kheap s p'a = Some (ArchObj ao); kheap s b = Some (ArchObj (ASIDPool ap)); kheap s p' = Some koa; (ra, p'a) \<in> (case koa of ArchObj (ASIDPool pool) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | ArchObj (PageDirectory pd) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), y)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) | ArchObj _ \<Rightarrow> {} | _ \<Rightarrow> {}); asid_table s a = Some b; \<forall>b p. ap b = Some p \<longrightarrow> (\<exists>ko. kheap s p = Some ko \<and> a_type ko = AArch APageDirectory); \<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s)); \<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))))); ap aa = Some p'\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s
 2. \<And>p rs a b ao y ya yb. \<lbrakk>\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s; \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p. ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s)); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s)))); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))))))); (a, b) \<in> vs_asid_refs (asid_table s); ako_at ao p s; ((a, b), y) \<in> vs_lookup1 s; (y, ya) \<in> vs_lookup1 s; (ya, yb) \<in> vs_lookup1 s; (yb, rs, p) \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s proof (prove)
goal (2 subgoals):
 1. \<And>ao ra p' p'a koa a b ap aa. \<lbrakk>kheap s p'a = Some (ArchObj ao); kheap s b = Some (ArchObj (ASIDPool ap)); kheap s p' = Some koa; (ra, p'a) \<in> (case koa of ArchObj (ASIDPool pool) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | ArchObj (PageDirectory pd) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), y)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) | ArchObj _ \<Rightarrow> {} | _ \<Rightarrow> {}); asid_table s a = Some b; \<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s)); \<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))))); ap aa = Some p'; \<exists>ko. kheap s p' = Some ko \<and> a_type ko = AArch APageDirectory\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s
 2. \<And>p rs a b ao y ya yb. \<lbrakk>\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s; \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p. ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s)); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s)))); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))))))); (a, b) \<in> vs_asid_refs (asid_table s); ako_at ao p s; ((a, b), y) \<in> vs_lookup1 s; (y, ya) \<in> vs_lookup1 s; (ya, yb) \<in> vs_lookup1 s; (yb, rs, p) \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s proof (prove)
goal (2 subgoals):
 1. \<And>ao ra p' p'a koa a b ap aa. \<lbrakk>kheap s p'a = Some (ArchObj ao); kheap s b = Some (ArchObj (ASIDPool ap)); kheap s p' = Some koa; (ra, p'a) \<in> (case koa of ArchObj (ASIDPool pool) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | ArchObj (PageDirectory pd) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), y)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) | ArchObj _ \<Rightarrow> {} | _ \<Rightarrow> {}); asid_table s a = Some b; \<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))))); ap aa = Some p'; \<exists>ko. kheap s p' = Some ko \<and> a_type ko = AArch APageDirectory; \<forall>pd. kheap s p' = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s)\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s
 2. \<And>p rs a b ao y ya yb. \<lbrakk>\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s; \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p. ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s)); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s)))); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))))))); (a, b) \<in> vs_asid_refs (asid_table s); ako_at ao p s; ((a, b), y) \<in> vs_lookup1 s; (y, ya) \<in> vs_lookup1 s; (ya, yb) \<in> vs_lookup1 s; (yb, rs, p) \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s proof (prove)
goal (2 subgoals):
 1. \<And>ao ra p' p'a koa a b ap aa. \<lbrakk>kheap s p'a = Some (ArchObj ao); kheap s b = Some (ArchObj (ASIDPool ap)); kheap s p' = Some koa; (ra, p'a) \<in> (case koa of ArchObj (ASIDPool pool) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | ArchObj (PageDirectory pd) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), y)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) | ArchObj _ \<Rightarrow> {} | _ \<Rightarrow> {}); asid_table s a = Some b; ap aa = Some p'; \<exists>ko. kheap s p' = Some ko \<and> a_type ko = AArch APageDirectory; \<forall>pd. kheap s p' = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s); \<forall>pd. kheap s p' = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))))\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s
 2. \<And>p rs a b ao y ya yb. \<lbrakk>\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s; \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p. ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s)); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s)))); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))))))); (a, b) \<in> vs_asid_refs (asid_table s); ako_at ao p s; ((a, b), y) \<in> vs_lookup1 s; (y, ya) \<in> vs_lookup1 s; (ya, yb) \<in> vs_lookup1 s; (yb, rs, p) \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s proof (prove)
goal (2 subgoals):
 1. \<And>ao p' a b ap aa pd ab ba. \<lbrakk>kheap s ba = Some (ArchObj ao); kheap s b = Some (ArchObj (ASIDPool ap)); kheap s p' = Some (ArchObj (PageDirectory pd)); asid_table s a = Some b; ap aa = Some p'; \<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s; \<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))); ab \<notin> kernel_mapping_slots; pde_ref (pd ab) = Some ba\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s
 2. \<And>p rs a b ao y ya yb. \<lbrakk>\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s; \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p. ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s)); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s)))); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))))))); (a, b) \<in> vs_asid_refs (asid_table s); ako_at ao p s; ((a, b), y) \<in> vs_lookup1 s; (y, ya) \<in> vs_lookup1 s; (ya, yb) \<in> vs_lookup1 s; (yb, rs, p) \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s proof (prove)
goal (2 subgoals):
 1. \<And>ao p' a b ap aa pd ab ba. \<lbrakk>kheap s ba = Some (ArchObj ao); kheap s b = Some (ArchObj (ASIDPool ap)); kheap s p' = Some (ArchObj (PageDirectory pd)); asid_table s a = Some b; ap aa = Some p'; \<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))); ab \<notin> kernel_mapping_slots; pde_ref (pd ab) = Some ba; ab \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd ab) s\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s
 2. \<And>p rs a b ao y ya yb. \<lbrakk>\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s; \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p. ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s)); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s)))); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))))))); (a, b) \<in> vs_asid_refs (asid_table s); ako_at ao p s; ((a, b), y) \<in> vs_lookup1 s; (y, ya) \<in> vs_lookup1 s; (ya, yb) \<in> vs_lookup1 s; (yb, rs, p) \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s proof (prove)
goal (1 subgoal):
 1. \<And>p rs a b ao y ya yb. \<lbrakk>\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s; \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p. ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s)); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s)))); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))))))); (a, b) \<in> vs_asid_refs (asid_table s); ako_at ao p s; ((a, b), y) \<in> vs_lookup1 s; (y, ya) \<in> vs_lookup1 s; (ya, yb) \<in> vs_lookup1 s; (yb, rs, p) \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s proof (prove)
goal (1 subgoal):
 1. \<And>p rs ao rsa r ra rb pa p' p'a p'b ko koa kob. \<lbrakk>\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s; \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p. ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s)); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s)))); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))))))); (rsa, pa) \<in> vs_asid_refs (asid_table s); ako_at ao p s; ((rb # ra # r # rsa, p'b), rs, p) \<in> (vs_lookup1 s)\<^sup>*; ko_at ko pa s; (r, p') \<in> vs_refs ko; ko_at koa p' s; (ra, p'a) \<in> vs_refs koa; ko_at kob p'a s; (rb, p'b) \<in> vs_refs kob\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s proof (prove)
goal (1 subgoal):
 1. \<And>p rs ao r ra rb p' p'a p'b ko koa kob a b. \<lbrakk>\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s; \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p. ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s)); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s)))); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))))))); ako_at ao p s; (([rb, ra, r, VSRef (UCAST(7 \<rightarrow> 32) a) None], p'b), rs, p) \<in> (vs_lookup1 s)\<^sup>*; ko_at ko b s; (r, p') \<in> vs_refs ko; ko_at koa p' s; (ra, p'a) \<in> vs_refs koa; ko_at kob p'a s; (rb, p'b) \<in> vs_refs kob; asid_table s a = Some b\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s proof (prove)
goal (1 subgoal):
 1. \<And>p rs ao r ra rb p' p'a p'b ko koa kob a b. \<lbrakk>\<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p. ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s)); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s)))); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))))))); ako_at ao p s; (([rb, ra, r, VSRef (UCAST(7 \<rightarrow> 32) a) None], p'b), rs, p) \<in> (vs_lookup1 s)\<^sup>*; ko_at ko b s; (r, p') \<in> vs_refs ko; ko_at koa p' s; (ra, p'a) \<in> vs_refs koa; ko_at kob p'a s; (rb, p'b) \<in> vs_refs kob; asid_table s a = Some b; typ_at (AArch AASIDPool) b s\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s proof (prove)
goal (1 subgoal):
 1. \<And>p rs ao r ra rb p' p'a p'b ko koa kob a b. \<lbrakk>\<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s)))); \<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))))))); ako_at ao p s; (([rb, ra, r, VSRef (UCAST(7 \<rightarrow> 32) a) None], p'b), rs, p) \<in> (vs_lookup1 s)\<^sup>*; ko_at ko b s; (r, p') \<in> vs_refs ko; ko_at koa p' s; (ra, p'a) \<in> vs_refs koa; ko_at kob p'a s; (rb, p'b) \<in> vs_refs kob; asid_table s a = Some b; typ_at (AArch AASIDPool) b s; \<forall>ap. kheap s b = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p. ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s)\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s proof (prove)
goal (1 subgoal):
 1. \<And>p rs ao r ra rb p' p'a p'b ko koa kob a b. \<lbrakk>\<forall>a p\<^sub>1. asid_table s a = Some p\<^sub>1 \<longrightarrow> (\<forall>ap. kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))))))); ako_at ao p s; (([rb, ra, r, VSRef (UCAST(7 \<rightarrow> 32) a) None], p'b), rs, p) \<in> (vs_lookup1 s)\<^sup>*; ko_at ko b s; (r, p') \<in> vs_refs ko; ko_at koa p' s; (ra, p'a) \<in> vs_refs koa; ko_at kob p'a s; (rb, p'b) \<in> vs_refs kob; asid_table s a = Some b; typ_at (AArch AASIDPool) b s; \<forall>ap. kheap s b = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p. ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s); \<forall>ap. kheap s b = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s)))\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s proof (prove)
goal (1 subgoal):
 1. \<And>p rs ao r ra rb p' p'a p'b ko koa kob a b. \<lbrakk>ako_at ao p s; (([rb, ra, r, VSRef (UCAST(7 \<rightarrow> 32) a) None], p'b), rs, p) \<in> (vs_lookup1 s)\<^sup>*; ko_at ko b s; (r, p') \<in> vs_refs ko; ko_at koa p' s; (ra, p'a) \<in> vs_refs koa; ko_at kob p'a s; (rb, p'b) \<in> vs_refs kob; asid_table s a = Some b; typ_at (AArch AASIDPool) b s; \<forall>ap. kheap s b = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p. ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s); \<forall>ap. kheap s b = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s))); \<forall>ap. kheap s b = Some (ArchObj (ASIDPool ap)) \<longrightarrow> (\<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))))))\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s proof (prove)
goal (1 subgoal):
 1. \<And>p rs ao r ra rb p' p'a p'b koa kob a b ap. \<lbrakk>kheap s p = Some (ArchObj ao); (([rb, ra, r, VSRef (UCAST(7 \<rightarrow> 32) a) None], p'b), rs, p) \<in> (vs_lookup1 s)\<^sup>*; kheap s b = Some (ArchObj (ASIDPool ap)); (r, p') \<in> vs_refs (ArchObj (ASIDPool ap)); kheap s p' = Some koa; (ra, p'a) \<in> vs_refs koa; kheap s p'a = Some kob; (rb, p'b) \<in> vs_refs kob; asid_table s a = Some b; \<forall>b p. ap b = Some p \<longrightarrow> (\<exists>ko. kheap s p = Some ko \<and> a_type ko = AArch APageDirectory); \<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s)); \<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s)))))\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s proof (prove)
goal (1 subgoal):
 1. \<And>p rs ao ra rb p' p'a p'b koa kob a b ap aa. \<lbrakk>kheap s p = Some (ArchObj ao); (([rb, ra, VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], p'b), rs, p) \<in> (vs_lookup1 s)\<^sup>*; kheap s b = Some (ArchObj (ASIDPool ap)); kheap s p' = Some koa; (ra, p'a) \<in> (case koa of ArchObj (ASIDPool pool) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | ArchObj (PageDirectory pd) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), y)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) | ArchObj _ \<Rightarrow> {} | _ \<Rightarrow> {}); kheap s p'a = Some kob; (rb, p'b) \<in> (case kob of ArchObj (ASIDPool pool) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | ArchObj (PageDirectory pd) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), y)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) | ArchObj _ \<Rightarrow> {} | _ \<Rightarrow> {}); asid_table s a = Some b; \<forall>b p. ap b = Some p \<longrightarrow> (\<exists>ko. kheap s p = Some ko \<and> a_type ko = AArch APageDirectory); \<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s)); \<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))))); ap aa = Some p'\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s proof (prove)
goal (1 subgoal):
 1. \<And>p rs ao ra rb p' p'a p'b koa kob a b ap aa. \<lbrakk>kheap s p = Some (ArchObj ao); (([rb, ra, VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], p'b), rs, p) \<in> (vs_lookup1 s)\<^sup>*; kheap s b = Some (ArchObj (ASIDPool ap)); kheap s p' = Some koa; (ra, p'a) \<in> (case koa of ArchObj (ASIDPool pool) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | ArchObj (PageDirectory pd) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), y)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) | ArchObj _ \<Rightarrow> {} | _ \<Rightarrow> {}); kheap s p'a = Some kob; (rb, p'b) \<in> (case kob of ArchObj (ASIDPool pool) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | ArchObj (PageDirectory pd) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), y)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) | ArchObj _ \<Rightarrow> {} | _ \<Rightarrow> {}); asid_table s a = Some b; \<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s)); \<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))))); ap aa = Some p'; \<exists>ko. kheap s p' = Some ko \<and> a_type ko = AArch APageDirectory\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s proof (prove)
goal (1 subgoal):
 1. \<And>p rs ao ra rb p' p'a p'b koa kob a b ap aa. \<lbrakk>kheap s p = Some (ArchObj ao); (([rb, ra, VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], p'b), rs, p) \<in> (vs_lookup1 s)\<^sup>*; kheap s b = Some (ArchObj (ASIDPool ap)); kheap s p' = Some koa; (ra, p'a) \<in> (case koa of ArchObj (ASIDPool pool) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | ArchObj (PageDirectory pd) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), y)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) | ArchObj _ \<Rightarrow> {} | _ \<Rightarrow> {}); kheap s p'a = Some kob; (rb, p'b) \<in> (case kob of ArchObj (ASIDPool pool) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | ArchObj (PageDirectory pd) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), y)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) | ArchObj _ \<Rightarrow> {} | _ \<Rightarrow> {}); asid_table s a = Some b; \<forall>b p\<^sub>2. ap b = Some p\<^sub>2 \<longrightarrow> (\<forall>pd. kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))))); ap aa = Some p'; \<exists>ko. kheap s p' = Some ko \<and> a_type ko = AArch APageDirectory; \<forall>pd. kheap s p' = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s)\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s proof (prove)
goal (1 subgoal):
 1. \<And>p rs ao ra rb p' p'a p'b koa kob a b ap aa. \<lbrakk>kheap s p = Some (ArchObj ao); (([rb, ra, VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], p'b), rs, p) \<in> (vs_lookup1 s)\<^sup>*; kheap s b = Some (ArchObj (ASIDPool ap)); kheap s p' = Some koa; (ra, p'a) \<in> (case koa of ArchObj (ASIDPool pool) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | ArchObj (PageDirectory pd) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), y)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) | ArchObj _ \<Rightarrow> {} | _ \<Rightarrow> {}); kheap s p'a = Some kob; (rb, p'b) \<in> (case kob of ArchObj (ASIDPool pool) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | ArchObj (PageDirectory pd) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), y)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) | ArchObj _ \<Rightarrow> {} | _ \<Rightarrow> {}); asid_table s a = Some b; ap aa = Some p'; \<exists>ko. kheap s p' = Some ko \<and> a_type ko = AArch APageDirectory; \<forall>pd. kheap s p' = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s); \<forall>pd. kheap s p' = Some (ArchObj (PageDirectory pd)) \<longrightarrow> (\<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))))\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s proof (prove)
goal (1 subgoal):
 1. \<And>p rs ao rb p' p'b kob a b ap aa pd ab ba. \<lbrakk>(rb, p'b) \<in> (case kob of ArchObj (ASIDPool pool) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | ArchObj (PageDirectory pd) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), y)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) | ArchObj _ \<Rightarrow> {} | _ \<Rightarrow> {}); asid_table s a = Some b; ap aa = Some p'; \<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s; \<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))); kheap s p = Some (ArchObj ao); (([rb, VSRef (UCAST(12 \<rightarrow> 32) ab) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], p'b), rs, p) \<in> (vs_lookup1 s)\<^sup>*; kheap s b = Some (ArchObj (ASIDPool ap)); kheap s p' = Some (ArchObj (PageDirectory pd)); kheap s ba = Some kob; ab \<notin> kernel_mapping_slots; pde_ref (pd ab) = Some ba\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s proof (prove)
goal (1 subgoal):
 1. \<And>p rs ao rb p' p'b kob a b ap aa pd ab ba. \<lbrakk>(rb, p'b) \<in> (case kob of ArchObj (ASIDPool pool) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | ArchObj (PageDirectory pd) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), y)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) | ArchObj _ \<Rightarrow> {} | _ \<Rightarrow> {}); asid_table s a = Some b; ap aa = Some p'; \<forall>c. c \<notin> kernel_mapping_slots \<longrightarrow> (\<forall>addr. (\<exists>f w. pd c = PageTablePDE addr f w) \<longrightarrow> (\<forall>pt. kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))); kheap s p = Some (ArchObj ao); (([rb, VSRef (UCAST(12 \<rightarrow> 32) ab) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], p'b), rs, p) \<in> (vs_lookup1 s)\<^sup>*; kheap s b = Some (ArchObj (ASIDPool ap)); kheap s p' = Some (ArchObj (PageDirectory pd)); kheap s ba = Some kob; ab \<notin> kernel_mapping_slots; pde_ref (pd ab) = Some ba; ab \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd ab) s\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s proof (prove)
goal:
No subgoals!