theory ArchVSpace_AI

lemma reachable_page_table_not_global:
  "\<lbrakk>(ref \<rhd> p) s; valid_kernel_mappings s; valid_global_pts s;
    valid_vspace_objs s; valid_asid_table (arm_asid_table (arch_state s)) s\<rbrakk>
   \<Longrightarrow> p \<notin> set (arm_global_pts (arch_state s))" apply clarsimp apply (erule (2) vs_lookupE_alt[OF _ _ valid_asid_table_ran]) apply (clarsimp simp: valid_global_pts_def) apply (drule (1) bspec) apply (clarsimp simp: obj_at_def a_type_def) apply (clarsimp simp: valid_global_pts_def) apply (drule (1) bspec) apply (clarsimp simp: obj_at_def a_type_def) apply (clarsimp simp: valid_kernel_mappings_def valid_kernel_mappings_if_pd_def ran_def) apply (drule_tac x="ArchObj (PageDirectory pd)" in spec) apply (drule mp, erule_tac x=p\<^sub>2 in exI) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(ref \<rhd> p) s; valid_kernel_mappings s; valid_global_pts s; valid_vspace_objs s; valid_asid_table (asid_table s) s\<rbrakk> \<Longrightarrow> p \<notin> set (arm_global_pts (arch_state s)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(ref \<rhd> p) s; valid_kernel_mappings s; valid_global_pts s; valid_vspace_objs s; valid_asid_table (asid_table s) s; p \<in> set (arm_global_pts (arch_state s))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>a. \<lbrakk>valid_kernel_mappings s; valid_global_pts s; valid_vspace_objs s; valid_asid_table (asid_table s) s; p \<in> set (arm_global_pts (arch_state s)); asid_table s a = Some p; typ_at (AArch AASIDPool) p s\<rbrakk> \<Longrightarrow> False
 2. \<And>a p\<^sub>1 ap b. \<lbrakk>valid_kernel_mappings s; valid_global_pts s; valid_vspace_objs s; valid_asid_table (asid_table s) s; p \<in> set (arm_global_pts (arch_state s)); asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p; typ_at (AArch APageDirectory) p s\<rbrakk> \<Longrightarrow> False
 3. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>valid_kernel_mappings s; valid_global_pts s; valid_vspace_objs s; valid_asid_table (asid_table s) s; p \<in> set (arm_global_pts (arch_state s)); asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p\<^sub>2; kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)); c \<notin> kernel_mapping_slots; pde_ref (pd c) = Some p; typ_at (AArch APageTable) p s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>a. \<lbrakk>valid_kernel_mappings s; \<forall>p\<in>set (arm_global_pts (arch_state s)). typ_at (AArch APageTable) p s; valid_vspace_objs s; valid_asid_table (asid_table s) s; p \<in> set (arm_global_pts (arch_state s)); asid_table s a = Some p; typ_at (AArch AASIDPool) p s\<rbrakk> \<Longrightarrow> False
 2. \<And>a p\<^sub>1 ap b. \<lbrakk>valid_kernel_mappings s; valid_global_pts s; valid_vspace_objs s; valid_asid_table (asid_table s) s; p \<in> set (arm_global_pts (arch_state s)); asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p; typ_at (AArch APageDirectory) p s\<rbrakk> \<Longrightarrow> False
 3. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>valid_kernel_mappings s; valid_global_pts s; valid_vspace_objs s; valid_asid_table (asid_table s) s; p \<in> set (arm_global_pts (arch_state s)); asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p\<^sub>2; kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)); c \<notin> kernel_mapping_slots; pde_ref (pd c) = Some p; typ_at (AArch APageTable) p s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>a. \<lbrakk>valid_kernel_mappings s; valid_vspace_objs s; valid_asid_table (asid_table s) s; p \<in> set (arm_global_pts (arch_state s)); asid_table s a = Some p; typ_at (AArch AASIDPool) p s; typ_at (AArch APageTable) p s\<rbrakk> \<Longrightarrow> False
 2. \<And>a p\<^sub>1 ap b. \<lbrakk>valid_kernel_mappings s; valid_global_pts s; valid_vspace_objs s; valid_asid_table (asid_table s) s; p \<in> set (arm_global_pts (arch_state s)); asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p; typ_at (AArch APageDirectory) p s\<rbrakk> \<Longrightarrow> False
 3. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>valid_kernel_mappings s; valid_global_pts s; valid_vspace_objs s; valid_asid_table (asid_table s) s; p \<in> set (arm_global_pts (arch_state s)); asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p\<^sub>2; kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)); c \<notin> kernel_mapping_slots; pde_ref (pd c) = Some p; typ_at (AArch APageTable) p s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a p\<^sub>1 ap b. \<lbrakk>valid_kernel_mappings s; valid_global_pts s; valid_vspace_objs s; valid_asid_table (asid_table s) s; p \<in> set (arm_global_pts (arch_state s)); asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p; typ_at (AArch APageDirectory) p s\<rbrakk> \<Longrightarrow> False
 2. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>valid_kernel_mappings s; valid_global_pts s; valid_vspace_objs s; valid_asid_table (asid_table s) s; p \<in> set (arm_global_pts (arch_state s)); asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p\<^sub>2; kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)); c \<notin> kernel_mapping_slots; pde_ref (pd c) = Some p; typ_at (AArch APageTable) p s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a p\<^sub>1 ap b. \<lbrakk>valid_kernel_mappings s; \<forall>p\<in>set (arm_global_pts (arch_state s)). typ_at (AArch APageTable) p s; valid_vspace_objs s; valid_asid_table (asid_table s) s; p \<in> set (arm_global_pts (arch_state s)); asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p; typ_at (AArch APageDirectory) p s\<rbrakk> \<Longrightarrow> False
 2. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>valid_kernel_mappings s; valid_global_pts s; valid_vspace_objs s; valid_asid_table (asid_table s) s; p \<in> set (arm_global_pts (arch_state s)); asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p\<^sub>2; kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)); c \<notin> kernel_mapping_slots; pde_ref (pd c) = Some p; typ_at (AArch APageTable) p s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a p\<^sub>1 ap b. \<lbrakk>valid_kernel_mappings s; valid_vspace_objs s; valid_asid_table (asid_table s) s; p \<in> set (arm_global_pts (arch_state s)); asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p; typ_at (AArch APageDirectory) p s; typ_at (AArch APageTable) p s\<rbrakk> \<Longrightarrow> False
 2. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>valid_kernel_mappings s; valid_global_pts s; valid_vspace_objs s; valid_asid_table (asid_table s) s; p \<in> set (arm_global_pts (arch_state s)); asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p\<^sub>2; kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)); c \<notin> kernel_mapping_slots; pde_ref (pd c) = Some p; typ_at (AArch APageTable) p s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>valid_kernel_mappings s; valid_global_pts s; valid_vspace_objs s; valid_asid_table (asid_table s) s; p \<in> set (arm_global_pts (arch_state s)); asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p\<^sub>2; kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)); c \<notin> kernel_mapping_slots; pde_ref (pd c) = Some p; typ_at (AArch APageTable) p s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>\<forall>x. (\<exists>a. kheap s a = Some x) \<longrightarrow> (case x of ArchObj (PageDirectory pd) \<Rightarrow> \<forall>x r. pde_ref (pd x) = Some r \<longrightarrow> (r \<in> set (arm_global_pts (arch_state s))) = (x \<in> kernel_mapping_slots) | ArchObj _ \<Rightarrow> True | _ \<Rightarrow> True); valid_global_pts s; valid_vspace_objs s; valid_asid_table (asid_table s) s; p \<in> set (arm_global_pts (arch_state s)); asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p\<^sub>2; kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)); c \<notin> kernel_mapping_slots; pde_ref (pd c) = Some p; typ_at (AArch APageTable) p s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>valid_global_pts s; valid_vspace_objs s; valid_asid_table (asid_table s) s; p \<in> set (arm_global_pts (arch_state s)); asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p\<^sub>2; kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)); c \<notin> kernel_mapping_slots; pde_ref (pd c) = Some p; typ_at (AArch APageTable) p s; (\<exists>a. kheap s a = Some (ArchObj (PageDirectory pd))) \<longrightarrow> (case ArchObj (PageDirectory pd) of ArchObj (PageDirectory pd) \<Rightarrow> \<forall>x r. pde_ref (pd x) = Some r \<longrightarrow> (r \<in> set (arm_global_pts (arch_state s))) = (x \<in> kernel_mapping_slots) | ArchObj _ \<Rightarrow> True | _ \<Rightarrow> True)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>valid_global_pts s; valid_vspace_objs s; valid_asid_table (asid_table s) s; p \<in> set (arm_global_pts (arch_state s)); asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p\<^sub>2; kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)); c \<notin> kernel_mapping_slots; pde_ref (pd c) = Some p; typ_at (AArch APageTable) p s; case ArchObj (PageDirectory pd) of ArchObj (PageDirectory pd) \<Rightarrow> \<forall>x r. pde_ref (pd x) = Some r \<longrightarrow> (r \<in> set (arm_global_pts (arch_state s))) = (x \<in> kernel_mapping_slots) | ArchObj _ \<Rightarrow> True | _ \<Rightarrow> True\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!