theory ArchVSpace_AI

lemma ref_is_unique:
  "\<lbrakk>(ref \<rhd> p) s; (ref' \<rhd> p) s; p \<notin> set (arm_global_pts (arch_state s));
    valid_vs_lookup s; unique_table_refs (caps_of_state s);
    valid_vspace_objs s; valid_asid_table (arm_asid_table (arch_state s)) s;
    valid_caps (caps_of_state s) s\<rbrakk>
   \<Longrightarrow> ref = ref'" apply (erule (1) vs_lookupE_alt[OF _ _ valid_asid_table_ran], clarsimp) apply (erule (1) vs_lookupE_alt[OF _ _ valid_asid_table_ran], clarsimp) apply (clarsimp simp: valid_asid_table_def up_ucast_inj_eq) apply (erule (2) inj_on_domD) apply ((clarsimp simp: obj_at_def)+)[2] apply (erule (1) vs_lookupE_alt[OF _ _ valid_asid_table_ran], clarsimp) apply (clarsimp simp: obj_at_def) apply (drule (2) vs_lookup_apI)+ apply (clarsimp dest!: valid_vs_lookupD[OF vs_lookup_pages_vs_lookupI]
                           obj_ref_elemD
                     simp: table_cap_ref_ap_eq[symmetric]) apply (drule_tac cap=cap and cap'=capa in unique_table_refsD, simp+)[1] apply (clarsimp simp: obj_at_def) apply (erule (1) vs_lookupE_alt[OF _ _ valid_asid_table_ran], clarsimp) apply ((clarsimp simp: obj_at_def)+)[2] apply (simp add: pde_ref_def split: pde.splits) apply (drule (5) vs_lookup_pdI)+ apply (clarsimp dest!: valid_vs_lookupD[OF vs_lookup_pages_vs_lookupI]
                         obj_ref_elemD) apply (drule_tac cap=cap and cap'=capa in unique_table_refsD, simp+)[1] apply (drule (3) valid_capsD[THEN valid_cap_to_pt_cap])+ apply (clarsimp simp: is_pt_cap_def table_cap_ref_simps vs_cap_ref_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(ref \<rhd> p) s; (ref' \<rhd> p) s; p \<notin> set (arm_global_pts (arch_state s)); valid_vs_lookup s; unique_table_refs (caps_of_state s); valid_vspace_objs s; valid_asid_table (asid_table s) s; valid_caps (caps_of_state s) s\<rbrakk> \<Longrightarrow> ref = ref' proof (prove)
goal (3 subgoals):
 1. \<And>a. \<lbrakk>(ref' \<rhd> p) s; p \<notin> set (arm_global_pts (arch_state s)); valid_vs_lookup s; unique_table_refs (caps_of_state s); valid_vspace_objs s; valid_asid_table (asid_table s) s; valid_caps (caps_of_state s) s; asid_table s a = Some p; typ_at (AArch AASIDPool) p s\<rbrakk> \<Longrightarrow> [VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref'
 2. \<And>a p\<^sub>1 ap b. \<lbrakk>(ref' \<rhd> p) s; p \<notin> set (arm_global_pts (arch_state s)); valid_vs_lookup s; unique_table_refs (caps_of_state s); valid_vspace_objs s; valid_asid_table (asid_table s) s; valid_caps (caps_of_state s) s; asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p; typ_at (AArch APageDirectory) p s\<rbrakk> \<Longrightarrow> [VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref'
 3. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>(ref' \<rhd> p) s; p \<notin> set (arm_global_pts (arch_state s)); valid_vs_lookup s; unique_table_refs (caps_of_state s); valid_vspace_objs s; valid_asid_table (asid_table s) s; valid_caps (caps_of_state s) s; asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p\<^sub>2; kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)); c \<notin> kernel_mapping_slots; pde_ref (pd c) = Some p; typ_at (AArch APageTable) p s\<rbrakk> \<Longrightarrow> [VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref' proof (prove)
goal (5 subgoals):
 1. \<And>a aa. \<lbrakk>p \<notin> set (arm_global_pts (arch_state s)); valid_vs_lookup s; unique_table_refs (caps_of_state s); valid_vspace_objs s; valid_asid_table (asid_table s) s; valid_caps (caps_of_state s) s; asid_table s a = Some p; typ_at (AArch AASIDPool) p s; asid_table s aa = Some p; typ_at (AArch AASIDPool) p s\<rbrakk> \<Longrightarrow> [VSRef (UCAST(7 \<rightarrow> 32) a) None] = [VSRef (UCAST(7 \<rightarrow> 32) aa) None]
 2. \<And>a aa p\<^sub>1 ap b. \<lbrakk>p \<notin> set (arm_global_pts (arch_state s)); valid_vs_lookup s; unique_table_refs (caps_of_state s); valid_vspace_objs s; valid_asid_table (asid_table s) s; valid_caps (caps_of_state s) s; asid_table s a = Some p; typ_at (AArch AASIDPool) p s; asid_table s aa = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p; typ_at (AArch APageDirectory) p s\<rbrakk> \<Longrightarrow> [VSRef (UCAST(7 \<rightarrow> 32) a) None] = [VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) aa) None]
 3. \<And>a aa p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>p \<notin> set (arm_global_pts (arch_state s)); valid_vs_lookup s; unique_table_refs (caps_of_state s); valid_vspace_objs s; valid_asid_table (asid_table s) s; valid_caps (caps_of_state s) s; asid_table s a = Some p; typ_at (AArch AASIDPool) p s; asid_table s aa = 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> [VSRef (UCAST(7 \<rightarrow> 32) a) None] = [VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) aa) None]
 4. \<And>a p\<^sub>1 ap b. \<lbrakk>(ref' \<rhd> p) s; p \<notin> set (arm_global_pts (arch_state s)); valid_vs_lookup s; unique_table_refs (caps_of_state s); valid_vspace_objs s; valid_asid_table (asid_table s) s; valid_caps (caps_of_state s) s; asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p; typ_at (AArch APageDirectory) p s\<rbrakk> \<Longrightarrow> [VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref'
 5. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>(ref' \<rhd> p) s; p \<notin> set (arm_global_pts (arch_state s)); valid_vs_lookup s; unique_table_refs (caps_of_state s); valid_vspace_objs s; valid_asid_table (asid_table s) s; valid_caps (caps_of_state s) s; asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p\<^sub>2; kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)); c \<notin> kernel_mapping_slots; pde_ref (pd c) = Some p; typ_at (AArch APageTable) p s\<rbrakk> \<Longrightarrow> [VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref' proof (prove)
goal (5 subgoals):
 1. \<And>a aa. \<lbrakk>p \<notin> set (arm_global_pts (arch_state s)); valid_vs_lookup s; unique_table_refs (caps_of_state s); valid_vspace_objs s; valid_caps (caps_of_state s) s; asid_table s a = Some p; asid_table s aa = Some p; typ_at (AArch AASIDPool) p s; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s; inj_on (asid_table s) (dom (asid_table s))\<rbrakk> \<Longrightarrow> a = aa
 2. \<And>a aa p\<^sub>1 ap b. \<lbrakk>p \<notin> set (arm_global_pts (arch_state s)); valid_vs_lookup s; unique_table_refs (caps_of_state s); valid_vspace_objs s; valid_asid_table (asid_table s) s; valid_caps (caps_of_state s) s; asid_table s a = Some p; typ_at (AArch AASIDPool) p s; asid_table s aa = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p; typ_at (AArch APageDirectory) p s\<rbrakk> \<Longrightarrow> [VSRef (UCAST(7 \<rightarrow> 32) a) None] = [VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) aa) None]
 3. \<And>a aa p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>p \<notin> set (arm_global_pts (arch_state s)); valid_vs_lookup s; unique_table_refs (caps_of_state s); valid_vspace_objs s; valid_asid_table (asid_table s) s; valid_caps (caps_of_state s) s; asid_table s a = Some p; typ_at (AArch AASIDPool) p s; asid_table s aa = 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> [VSRef (UCAST(7 \<rightarrow> 32) a) None] = [VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) aa) None]
 4. \<And>a p\<^sub>1 ap b. \<lbrakk>(ref' \<rhd> p) s; p \<notin> set (arm_global_pts (arch_state s)); valid_vs_lookup s; unique_table_refs (caps_of_state s); valid_vspace_objs s; valid_asid_table (asid_table s) s; valid_caps (caps_of_state s) s; asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p; typ_at (AArch APageDirectory) p s\<rbrakk> \<Longrightarrow> [VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref'
 5. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>(ref' \<rhd> p) s; p \<notin> set (arm_global_pts (arch_state s)); valid_vs_lookup s; unique_table_refs (caps_of_state s); valid_vspace_objs s; valid_asid_table (asid_table s) s; valid_caps (caps_of_state s) s; asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p\<^sub>2; kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)); c \<notin> kernel_mapping_slots; pde_ref (pd c) = Some p; typ_at (AArch APageTable) p s\<rbrakk> \<Longrightarrow> [VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref' proof (prove)
goal (4 subgoals):
 1. \<And>a aa p\<^sub>1 ap b. \<lbrakk>p \<notin> set (arm_global_pts (arch_state s)); valid_vs_lookup s; unique_table_refs (caps_of_state s); valid_vspace_objs s; valid_asid_table (asid_table s) s; valid_caps (caps_of_state s) s; asid_table s a = Some p; typ_at (AArch AASIDPool) p s; asid_table s aa = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p; typ_at (AArch APageDirectory) p s\<rbrakk> \<Longrightarrow> [VSRef (UCAST(7 \<rightarrow> 32) a) None] = [VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) aa) None]
 2. \<And>a aa p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>p \<notin> set (arm_global_pts (arch_state s)); valid_vs_lookup s; unique_table_refs (caps_of_state s); valid_vspace_objs s; valid_asid_table (asid_table s) s; valid_caps (caps_of_state s) s; asid_table s a = Some p; typ_at (AArch AASIDPool) p s; asid_table s aa = 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> [VSRef (UCAST(7 \<rightarrow> 32) a) None] = [VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) aa) None]
 3. \<And>a p\<^sub>1 ap b. \<lbrakk>(ref' \<rhd> p) s; p \<notin> set (arm_global_pts (arch_state s)); valid_vs_lookup s; unique_table_refs (caps_of_state s); valid_vspace_objs s; valid_asid_table (asid_table s) s; valid_caps (caps_of_state s) s; asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p; typ_at (AArch APageDirectory) p s\<rbrakk> \<Longrightarrow> [VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref'
 4. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>(ref' \<rhd> p) s; p \<notin> set (arm_global_pts (arch_state s)); valid_vs_lookup s; unique_table_refs (caps_of_state s); valid_vspace_objs s; valid_asid_table (asid_table s) s; valid_caps (caps_of_state s) s; asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p\<^sub>2; kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)); c \<notin> kernel_mapping_slots; pde_ref (pd c) = Some p; typ_at (AArch APageTable) p s\<rbrakk> \<Longrightarrow> [VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref' proof (prove)
goal (2 subgoals):
 1. \<And>a p\<^sub>1 ap b. \<lbrakk>(ref' \<rhd> p) s; p \<notin> set (arm_global_pts (arch_state s)); valid_vs_lookup s; unique_table_refs (caps_of_state s); valid_vspace_objs s; valid_asid_table (asid_table s) s; valid_caps (caps_of_state s) s; asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p; typ_at (AArch APageDirectory) p s\<rbrakk> \<Longrightarrow> [VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref'
 2. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>(ref' \<rhd> p) s; p \<notin> set (arm_global_pts (arch_state s)); valid_vs_lookup s; unique_table_refs (caps_of_state s); valid_vspace_objs s; valid_asid_table (asid_table s) s; valid_caps (caps_of_state s) s; asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p\<^sub>2; kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)); c \<notin> kernel_mapping_slots; pde_ref (pd c) = Some p; typ_at (AArch APageTable) p s\<rbrakk> \<Longrightarrow> [VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref' proof (prove)
goal (4 subgoals):
 1. \<And>a p\<^sub>1 ap b aa. \<lbrakk>p \<notin> set (arm_global_pts (arch_state s)); valid_vs_lookup s; unique_table_refs (caps_of_state s); valid_vspace_objs s; valid_asid_table (asid_table s) s; valid_caps (caps_of_state s) s; asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p; typ_at (AArch APageDirectory) p s; asid_table s aa = Some p; typ_at (AArch AASIDPool) p s\<rbrakk> \<Longrightarrow> [VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = [VSRef (UCAST(7 \<rightarrow> 32) aa) None]
 2. \<And>a p\<^sub>1 ap b aa p\<^sub>1' apa ba. \<lbrakk>p \<notin> set (arm_global_pts (arch_state s)); valid_vs_lookup s; unique_table_refs (caps_of_state s); valid_vspace_objs s; valid_asid_table (asid_table s) s; valid_caps (caps_of_state s) s; asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p; typ_at (AArch APageDirectory) p s; asid_table s aa = Some p\<^sub>1'; kheap s p\<^sub>1' = Some (ArchObj (ASIDPool apa)); apa ba = Some p; typ_at (AArch APageDirectory) p s\<rbrakk> \<Longrightarrow> [VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = [VSRef (UCAST(10 \<rightarrow> 32) ba) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) aa) None]
 3. \<And>a p\<^sub>1 ap b aa p\<^sub>1' apa ba p\<^sub>2 pd c. \<lbrakk>p \<notin> set (arm_global_pts (arch_state s)); valid_vs_lookup s; unique_table_refs (caps_of_state s); valid_vspace_objs s; valid_asid_table (asid_table s) s; valid_caps (caps_of_state s) s; asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p; typ_at (AArch APageDirectory) p s; asid_table s aa = Some p\<^sub>1'; kheap s p\<^sub>1' = Some (ArchObj (ASIDPool apa)); apa ba = 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> [VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = [VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) ba) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) aa) None]
 4. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>(ref' \<rhd> p) s; p \<notin> set (arm_global_pts (arch_state s)); valid_vs_lookup s; unique_table_refs (caps_of_state s); valid_vspace_objs s; valid_asid_table (asid_table s) s; valid_caps (caps_of_state s) s; asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p\<^sub>2; kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)); c \<notin> kernel_mapping_slots; pde_ref (pd c) = Some p; typ_at (AArch APageTable) p s\<rbrakk> \<Longrightarrow> [VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref' proof (prove)
goal (3 subgoals):
 1. \<And>a p\<^sub>1 ap b aa p\<^sub>1' apa ba. \<lbrakk>p \<notin> set (arm_global_pts (arch_state s)); valid_vs_lookup s; unique_table_refs (caps_of_state s); valid_vspace_objs s; valid_asid_table (asid_table s) s; valid_caps (caps_of_state s) s; asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p; typ_at (AArch APageDirectory) p s; asid_table s aa = Some p\<^sub>1'; kheap s p\<^sub>1' = Some (ArchObj (ASIDPool apa)); apa ba = Some p; typ_at (AArch APageDirectory) p s\<rbrakk> \<Longrightarrow> [VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = [VSRef (UCAST(10 \<rightarrow> 32) ba) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) aa) None]
 2. \<And>a p\<^sub>1 ap b aa p\<^sub>1' apa ba p\<^sub>2 pd c. \<lbrakk>p \<notin> set (arm_global_pts (arch_state s)); valid_vs_lookup s; unique_table_refs (caps_of_state s); valid_vspace_objs s; valid_asid_table (asid_table s) s; valid_caps (caps_of_state s) s; asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p; typ_at (AArch APageDirectory) p s; asid_table s aa = Some p\<^sub>1'; kheap s p\<^sub>1' = Some (ArchObj (ASIDPool apa)); apa ba = 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> [VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = [VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) ba) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) aa) None]
 3. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>(ref' \<rhd> p) s; p \<notin> set (arm_global_pts (arch_state s)); valid_vs_lookup s; unique_table_refs (caps_of_state s); valid_vspace_objs s; valid_asid_table (asid_table s) s; valid_caps (caps_of_state s) s; asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p\<^sub>2; kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)); c \<notin> kernel_mapping_slots; pde_ref (pd c) = Some p; typ_at (AArch APageTable) p s\<rbrakk> \<Longrightarrow> [VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref' proof (prove)
goal (3 subgoals):
 1. \<And>a p\<^sub>1 ap b aa p\<^sub>1' apa ba. \<lbrakk>p \<notin> set (arm_global_pts (arch_state s)); valid_vs_lookup s; unique_table_refs (caps_of_state s); valid_vspace_objs s; valid_asid_table (asid_table s) s; valid_caps (caps_of_state s) s; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p; typ_at (AArch APageDirectory) p s; kheap s p\<^sub>1' = Some (ArchObj (ASIDPool apa)); apa ba = Some p; typ_at (AArch APageDirectory) p s; ([VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> p) s; ([VSRef (UCAST(10 \<rightarrow> 32) ba) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) aa) None] \<rhd> p) s\<rbrakk> \<Longrightarrow> [VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = [VSRef (UCAST(10 \<rightarrow> 32) ba) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) aa) None]
 2. \<And>a p\<^sub>1 ap b aa p\<^sub>1' apa ba p\<^sub>2 pd c. \<lbrakk>p \<notin> set (arm_global_pts (arch_state s)); valid_vs_lookup s; unique_table_refs (caps_of_state s); valid_vspace_objs s; valid_asid_table (asid_table s) s; valid_caps (caps_of_state s) s; asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p; typ_at (AArch APageDirectory) p s; asid_table s aa = Some p\<^sub>1'; kheap s p\<^sub>1' = Some (ArchObj (ASIDPool apa)); apa ba = 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> [VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = [VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) ba) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) aa) None]
 3. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>(ref' \<rhd> p) s; p \<notin> set (arm_global_pts (arch_state s)); valid_vs_lookup s; unique_table_refs (caps_of_state s); valid_vspace_objs s; valid_asid_table (asid_table s) s; valid_caps (caps_of_state s) s; asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p\<^sub>2; kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)); c \<notin> kernel_mapping_slots; pde_ref (pd c) = Some p; typ_at (AArch APageTable) p s\<rbrakk> \<Longrightarrow> [VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref' proof (prove)
goal (3 subgoals):
 1. \<And>a p\<^sub>1 ap b aa p\<^sub>1' apa ba ab bb cap ac bc capa. \<lbrakk>p \<notin> set (arm_global_pts (arch_state s)); valid_vs_lookup s; unique_table_refs (caps_of_state s); valid_vspace_objs s; valid_asid_table (asid_table s) s; valid_caps (caps_of_state s) s; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p; kheap s p\<^sub>1' = Some (ArchObj (ASIDPool apa)); apa ba = Some p; typ_at (AArch APageDirectory) p s; caps_of_state s (ab, bb) = Some cap; table_cap_ref cap = Some [VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None]; obj_refs cap = {p}; caps_of_state s (ac, bc) = Some capa; table_cap_ref capa = Some [VSRef (UCAST(10 \<rightarrow> 32) ba) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) aa) None]; obj_refs capa = {p}\<rbrakk> \<Longrightarrow> UCAST(10 \<rightarrow> 32) b = UCAST(10 \<rightarrow> 32) ba \<and> UCAST(7 \<rightarrow> 32) a = UCAST(7 \<rightarrow> 32) aa
 2. \<And>a p\<^sub>1 ap b aa p\<^sub>1' apa ba p\<^sub>2 pd c. \<lbrakk>p \<notin> set (arm_global_pts (arch_state s)); valid_vs_lookup s; unique_table_refs (caps_of_state s); valid_vspace_objs s; valid_asid_table (asid_table s) s; valid_caps (caps_of_state s) s; asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p; typ_at (AArch APageDirectory) p s; asid_table s aa = Some p\<^sub>1'; kheap s p\<^sub>1' = Some (ArchObj (ASIDPool apa)); apa ba = 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> [VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = [VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) ba) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) aa) None]
 3. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>(ref' \<rhd> p) s; p \<notin> set (arm_global_pts (arch_state s)); valid_vs_lookup s; unique_table_refs (caps_of_state s); valid_vspace_objs s; valid_asid_table (asid_table s) s; valid_caps (caps_of_state s) s; asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p\<^sub>2; kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)); c \<notin> kernel_mapping_slots; pde_ref (pd c) = Some p; typ_at (AArch APageTable) p s\<rbrakk> \<Longrightarrow> [VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref' proof (prove)
goal (2 subgoals):
 1. \<And>a p\<^sub>1 ap b aa p\<^sub>1' apa ba p\<^sub>2 pd c. \<lbrakk>p \<notin> set (arm_global_pts (arch_state s)); valid_vs_lookup s; unique_table_refs (caps_of_state s); valid_vspace_objs s; valid_asid_table (asid_table s) s; valid_caps (caps_of_state s) s; asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p; typ_at (AArch APageDirectory) p s; asid_table s aa = Some p\<^sub>1'; kheap s p\<^sub>1' = Some (ArchObj (ASIDPool apa)); apa ba = 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> [VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = [VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) ba) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) aa) None]
 2. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>(ref' \<rhd> p) s; p \<notin> set (arm_global_pts (arch_state s)); valid_vs_lookup s; unique_table_refs (caps_of_state s); valid_vspace_objs s; valid_asid_table (asid_table s) s; valid_caps (caps_of_state s) s; asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p\<^sub>2; kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)); c \<notin> kernel_mapping_slots; pde_ref (pd c) = Some p; typ_at (AArch APageTable) p s\<rbrakk> \<Longrightarrow> [VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref' proof (prove)
goal (1 subgoal):
 1. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>(ref' \<rhd> p) s; p \<notin> set (arm_global_pts (arch_state s)); valid_vs_lookup s; unique_table_refs (caps_of_state s); valid_vspace_objs s; valid_asid_table (asid_table s) s; valid_caps (caps_of_state s) s; asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p\<^sub>2; kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)); c \<notin> kernel_mapping_slots; pde_ref (pd c) = Some p; typ_at (AArch APageTable) p s\<rbrakk> \<Longrightarrow> [VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = ref' proof (prove)
goal (3 subgoals):
 1. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c aa. \<lbrakk>p \<notin> set (arm_global_pts (arch_state s)); valid_vs_lookup s; unique_table_refs (caps_of_state s); valid_vspace_objs s; valid_asid_table (asid_table s) s; valid_caps (caps_of_state s) s; asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p\<^sub>2; kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)); c \<notin> kernel_mapping_slots; pde_ref (pd c) = Some p; typ_at (AArch APageTable) p s; asid_table s aa = Some p; typ_at (AArch AASIDPool) p s\<rbrakk> \<Longrightarrow> [VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = [VSRef (UCAST(7 \<rightarrow> 32) aa) None]
 2. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c aa p\<^sub>1' apa ba. \<lbrakk>p \<notin> set (arm_global_pts (arch_state s)); valid_vs_lookup s; unique_table_refs (caps_of_state s); valid_vspace_objs s; valid_asid_table (asid_table s) s; valid_caps (caps_of_state s) s; asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p\<^sub>2; kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)); c \<notin> kernel_mapping_slots; pde_ref (pd c) = Some p; typ_at (AArch APageTable) p s; asid_table s aa = Some p\<^sub>1'; kheap s p\<^sub>1' = Some (ArchObj (ASIDPool apa)); apa ba = Some p; typ_at (AArch APageDirectory) p s\<rbrakk> \<Longrightarrow> [VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = [VSRef (UCAST(10 \<rightarrow> 32) ba) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) aa) None]
 3. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c aa p\<^sub>1' apa ba p\<^sub>2' pda ca. \<lbrakk>p \<notin> set (arm_global_pts (arch_state s)); valid_vs_lookup s; unique_table_refs (caps_of_state s); valid_vspace_objs s; valid_asid_table (asid_table s) s; valid_caps (caps_of_state s) s; asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p\<^sub>2; kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)); c \<notin> kernel_mapping_slots; pde_ref (pd c) = Some p; typ_at (AArch APageTable) p s; asid_table s aa = Some p\<^sub>1'; kheap s p\<^sub>1' = Some (ArchObj (ASIDPool apa)); apa ba = Some p\<^sub>2'; kheap s p\<^sub>2' = Some (ArchObj (PageDirectory pda)); ca \<notin> kernel_mapping_slots; pde_ref (pda ca) = Some p; typ_at (AArch APageTable) p s\<rbrakk> \<Longrightarrow> [VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = [VSRef (UCAST(12 \<rightarrow> 32) ca) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) ba) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) aa) None] proof (prove)
goal (1 subgoal):
 1. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c aa p\<^sub>1' apa ba p\<^sub>2' pda ca. \<lbrakk>p \<notin> set (arm_global_pts (arch_state s)); valid_vs_lookup s; unique_table_refs (caps_of_state s); valid_vspace_objs s; valid_asid_table (asid_table s) s; valid_caps (caps_of_state s) s; asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p\<^sub>2; kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)); c \<notin> kernel_mapping_slots; pde_ref (pd c) = Some p; typ_at (AArch APageTable) p s; asid_table s aa = Some p\<^sub>1'; kheap s p\<^sub>1' = Some (ArchObj (ASIDPool apa)); apa ba = Some p\<^sub>2'; kheap s p\<^sub>2' = Some (ArchObj (PageDirectory pda)); ca \<notin> kernel_mapping_slots; pde_ref (pda ca) = Some p; typ_at (AArch APageTable) p s\<rbrakk> \<Longrightarrow> [VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] = [VSRef (UCAST(12 \<rightarrow> 32) ca) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) ba) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) aa) None] proof (prove)
goal (1 subgoal):
 1. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c aa p\<^sub>1' apa ba p\<^sub>2' pda ca x21 x22 x23 x21a x22a x23a. \<lbrakk>typ_at (AArch APageTable) p s; p \<notin> set (arm_global_pts (arch_state s)); valid_vs_lookup s; unique_table_refs (caps_of_state s); valid_vspace_objs s; valid_asid_table (asid_table s) s; valid_caps (caps_of_state s) s; asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p\<^sub>2; kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)); c \<notin> kernel_mapping_slots; pd c = PageTablePDE x21 x22 x23; ptrFromPAddr x21 = p; asid_table s aa = Some p\<^sub>1'; kheap s p\<^sub>1' = Some (ArchObj (ASIDPool apa)); apa ba = Some p\<^sub>2'; kheap s p\<^sub>2' = Some (ArchObj (PageDirectory pda)); ca \<notin> kernel_mapping_slots; pda ca = PageTablePDE x21a x22a x23a; ptrFromPAddr x21a = p\<rbrakk> \<Longrightarrow> c = ca \<and> UCAST(10 \<rightarrow> 32) b = UCAST(10 \<rightarrow> 32) ba \<and> UCAST(7 \<rightarrow> 32) a = UCAST(7 \<rightarrow> 32) aa proof (prove)
goal (1 subgoal):
 1. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c aa p\<^sub>1' apa ba p\<^sub>2' pda ca x21 x22 x23 x21a x22a x23a. \<lbrakk>typ_at (AArch APageTable) p s; p \<notin> set (arm_global_pts (arch_state s)); valid_vs_lookup s; unique_table_refs (caps_of_state s); valid_vspace_objs s; valid_asid_table (asid_table s) s; valid_caps (caps_of_state s) s; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p\<^sub>2; kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)); c \<notin> kernel_mapping_slots; pd c = PageTablePDE x21 x22 x23; ptrFromPAddr x21 = p; kheap s p\<^sub>1' = Some (ArchObj (ASIDPool apa)); apa ba = Some p\<^sub>2'; kheap s p\<^sub>2' = Some (ArchObj (PageDirectory pda)); ca \<notin> kernel_mapping_slots; pda ca = PageTablePDE x21a x22a x23a; ptrFromPAddr x21a = p; ([VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> ptrFromPAddr x21) s; ([VSRef (UCAST(12 \<rightarrow> 32) ca) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) ba) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) aa) None] \<rhd> ptrFromPAddr x21a) s\<rbrakk> \<Longrightarrow> c = ca \<and> UCAST(10 \<rightarrow> 32) b = UCAST(10 \<rightarrow> 32) ba \<and> UCAST(7 \<rightarrow> 32) a = UCAST(7 \<rightarrow> 32) aa proof (prove)
goal (1 subgoal):
 1. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c aa p\<^sub>1' apa ba p\<^sub>2' pda ca x21 x22 x23 x21a x22a x23a ab bb cap ac bc capa. \<lbrakk>typ_at (AArch APageTable) (ptrFromPAddr x21) s; ptrFromPAddr x21 \<notin> set (arm_global_pts (arch_state s)); valid_vs_lookup s; unique_table_refs (caps_of_state s); valid_vspace_objs s; valid_asid_table (asid_table s) s; valid_caps (caps_of_state s) s; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p\<^sub>2; kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)); c \<notin> kernel_mapping_slots; pd c = PageTablePDE x21 x22 x23; kheap s p\<^sub>1' = Some (ArchObj (ASIDPool apa)); apa ba = Some p\<^sub>2'; kheap s p\<^sub>2' = Some (ArchObj (PageDirectory pda)); ca \<notin> kernel_mapping_slots; pda ca = PageTablePDE x21a x22a x23a; ptrFromPAddr x21a = ptrFromPAddr x21; p = ptrFromPAddr x21; caps_of_state s (ab, bb) = Some cap; vs_cap_ref cap = Some [VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None]; obj_refs cap = {ptrFromPAddr x21}; caps_of_state s (ac, bc) = Some capa; vs_cap_ref capa = Some [VSRef (UCAST(12 \<rightarrow> 32) ca) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) ba) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) aa) None]; obj_refs capa = {ptrFromPAddr x21}\<rbrakk> \<Longrightarrow> c = ca \<and> UCAST(10 \<rightarrow> 32) b = UCAST(10 \<rightarrow> 32) ba \<and> UCAST(7 \<rightarrow> 32) a = UCAST(7 \<rightarrow> 32) aa proof (prove)
goal (1 subgoal):
 1. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c aa p\<^sub>1' apa ba p\<^sub>2' pda ca x21 x22 x23 x21a x22a x23a ab bb cap ac bc capa. \<lbrakk>typ_at (AArch APageTable) (ptrFromPAddr x21) s; ptrFromPAddr x21 \<notin> set (arm_global_pts (arch_state s)); valid_vs_lookup s; valid_vspace_objs s; valid_asid_table (asid_table s) s; valid_caps (caps_of_state s) s; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p\<^sub>2; kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)); c \<notin> kernel_mapping_slots; pd c = PageTablePDE x21 x22 x23; kheap s p\<^sub>1' = Some (ArchObj (ASIDPool apa)); apa ba = Some p\<^sub>2'; kheap s p\<^sub>2' = Some (ArchObj (PageDirectory pda)); ca \<notin> kernel_mapping_slots; pda ca = PageTablePDE x21a x22a x23a; ptrFromPAddr x21a = ptrFromPAddr x21; p = ptrFromPAddr x21; caps_of_state s (ab, bb) = Some cap; vs_cap_ref cap = Some [VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None]; obj_refs cap = {ptrFromPAddr x21}; caps_of_state s (ac, bc) = Some capa; vs_cap_ref capa = Some [VSRef (UCAST(12 \<rightarrow> 32) ca) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) ba) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) aa) None]; obj_refs capa = {ptrFromPAddr x21}; table_cap_ref cap = table_cap_ref capa\<rbrakk> \<Longrightarrow> c = ca \<and> UCAST(10 \<rightarrow> 32) b = UCAST(10 \<rightarrow> 32) ba \<and> UCAST(7 \<rightarrow> 32) a = UCAST(7 \<rightarrow> 32) aa proof (prove)
goal (1 subgoal):
 1. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c aa p\<^sub>1' apa ba p\<^sub>2' pda ca x21 x22 x23 x21a x22a x23a ab bb cap ac bc capa. \<lbrakk>typ_at (AArch APageTable) (ptrFromPAddr x21) s; ptrFromPAddr x21 \<notin> set (arm_global_pts (arch_state s)); valid_vs_lookup s; valid_vspace_objs s; valid_asid_table (asid_table s) s; valid_caps (caps_of_state s) s; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p\<^sub>2; kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)); c \<notin> kernel_mapping_slots; pd c = PageTablePDE x21 x22 x23; kheap s p\<^sub>1' = Some (ArchObj (ASIDPool apa)); apa ba = Some p\<^sub>2'; kheap s p\<^sub>2' = Some (ArchObj (PageDirectory pda)); ca \<notin> kernel_mapping_slots; pda ca = PageTablePDE x21a x22a x23a; ptrFromPAddr x21a = ptrFromPAddr x21; p = ptrFromPAddr x21; vs_cap_ref cap = Some [VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None]; obj_refs cap = {ptrFromPAddr x21}; vs_cap_ref capa = Some [VSRef (UCAST(12 \<rightarrow> 32) ca) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) ba) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) aa) None]; obj_refs capa = {ptrFromPAddr x21}; table_cap_ref cap = table_cap_ref capa; is_pt_cap cap; is_pt_cap capa\<rbrakk> \<Longrightarrow> c = ca \<and> UCAST(10 \<rightarrow> 32) b = UCAST(10 \<rightarrow> 32) ba \<and> UCAST(7 \<rightarrow> 32) a = UCAST(7 \<rightarrow> 32) aa proof (prove)
goal:
No subgoals!