theory ArchVSpace_AI

lemma update_self_reachable:
  "\<lbrakk>(ref \<rhd> p) s; valid_asid_table (arm_asid_table (arch_state s)) s;
    valid_vspace_objs s\<rbrakk>
   \<Longrightarrow> (ref \<rhd> p) (s \<lparr>kheap := \<lambda>a. if a = p then Some y else kheap s a\<rparr>)" apply (erule (2) vs_lookupE_alt[OF _ _ valid_asid_table_ran]) apply (rule vs_lookup_atI, clarsimp) apply (rule_tac ap=ap in vs_lookup_apI, auto simp: obj_at_def)[1] apply (clarsimp simp: pde_ref_def split: pde.splits) apply (rule_tac ap=ap and pd=pd in vs_lookup_pdI, auto simp: obj_at_def)[1] done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(ref \<rhd> p) s; valid_asid_table (asid_table s) s; valid_vspace_objs s\<rbrakk> \<Longrightarrow> (ref \<rhd> p) (s\<lparr>kheap := \<lambda>a. if a = p then Some y else kheap s a\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>a. \<lbrakk>valid_asid_table (asid_table s) s; valid_vspace_objs s; asid_table s a = Some p; typ_at (AArch AASIDPool) p s\<rbrakk> \<Longrightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> p) (s\<lparr>kheap := \<lambda>a. if a = p then Some y else kheap s a\<rparr>)
 2. \<And>a p\<^sub>1 ap b. \<lbrakk>valid_asid_table (asid_table s) s; 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; typ_at (AArch APageDirectory) p s\<rbrakk> \<Longrightarrow> ([VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> p) (s\<lparr>kheap := \<lambda>a. if a = p then Some y else kheap s a\<rparr>)
 3. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>valid_asid_table (asid_table s) s; 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; 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] \<rhd> p) (s\<lparr>kheap := \<lambda>a. if a = p then Some y else kheap s a\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>a p\<^sub>1 ap b. \<lbrakk>valid_asid_table (asid_table s) s; 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; typ_at (AArch APageDirectory) p s\<rbrakk> \<Longrightarrow> ([VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> p) (s\<lparr>kheap := \<lambda>a. if a = p then Some y else kheap s a\<rparr>)
 2. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>valid_asid_table (asid_table s) s; 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; 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] \<rhd> p) (s\<lparr>kheap := \<lambda>a. if a = p then Some y else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>valid_asid_table (asid_table s) s; 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; 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] \<rhd> p) (s\<lparr>kheap := \<lambda>a. if a = p then Some y else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c x21 x22 x23. \<lbrakk>typ_at (AArch APageTable) (ptrFromPAddr x21) s; valid_asid_table (asid_table s) s; 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 x21 x22 x23; p = ptrFromPAddr x21\<rbrakk> \<Longrightarrow> ([VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> ptrFromPAddr x21) (s\<lparr>kheap := \<lambda>a. if a = ptrFromPAddr x21 then Some y else kheap s a\<rparr>) proof (prove)
goal:
No subgoals!