theory ArchInvariants_AI

lemma vs_lookup_pdI:
  "\<And>a p\<^sub>1 ap b p\<^sub>2 pd c.
     \<lbrakk>arm_asid_table (arch_state s) a = Some p\<^sub>1;
      kheap s p\<^sub>1 = Some (ArchObj (arch_kernel_obj.ASIDPool ap));
      ap b = Some p\<^sub>2;
      kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd));
      c \<notin> kernel_mapping_slots;
      pd c = pde.PageTablePDE p f w\<rbrakk>
     \<Longrightarrow> ([VSRef (ucast c) (Some APageDirectory),
           VSRef (ucast b) (Some AASIDPool), VSRef (ucast a) None]
          \<rhd> ptrFromPAddr p) s" apply (simp add: vs_lookup_def Image_def vs_asid_refs_def graph_of_def) apply (intro exI conjI, assumption) apply (rule rtrancl_into_rtrancl) apply (rule rtrancl_into_rtrancl) apply (rule rtrancl_refl) apply (fastforce simp: vs_lookup1_def obj_at_def
                          vs_refs_def graph_of_def image_def) apply (simp add: vs_lookup1_def obj_at_def vs_refs_def graph_of_def image_def) apply (rule_tac x=c in exI) apply (simp add: pde_ref_def ptrFormPAddr_addFromPPtr) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>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 p f w\<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 p) s proof (prove)
goal (1 subgoal):
 1. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>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 p f w\<rbrakk> \<Longrightarrow> \<exists>aa ba. asid_table s aa = Some ba \<and> (([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba), [VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], ptrFromPAddr p) \<in> (vs_lookup1 s)\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>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 p f w\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) a) None], p\<^sub>1), [VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], ptrFromPAddr p) \<in> (vs_lookup1 s)\<^sup>* proof (prove)
goal (2 subgoals):
 1. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>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 p f w\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) a) None], p\<^sub>1), ?b16 a p\<^sub>1 ap b p\<^sub>2 pd c) \<in> (vs_lookup1 s)\<^sup>*
 2. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>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 p f w\<rbrakk> \<Longrightarrow> (?b16 a p\<^sub>1 ap b p\<^sub>2 pd c, [VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], ptrFromPAddr p) \<in> vs_lookup1 s proof (prove)
goal (3 subgoals):
 1. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>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 p f w\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) a) None], p\<^sub>1), ?b19 a p\<^sub>1 ap b p\<^sub>2 pd c) \<in> (vs_lookup1 s)\<^sup>*
 2. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>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 p f w\<rbrakk> \<Longrightarrow> (?b19 a p\<^sub>1 ap b p\<^sub>2 pd c, ?b16 a p\<^sub>1 ap b p\<^sub>2 pd c) \<in> vs_lookup1 s
 3. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>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 p f w\<rbrakk> \<Longrightarrow> (?b16 a p\<^sub>1 ap b p\<^sub>2 pd c, [VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], ptrFromPAddr p) \<in> vs_lookup1 s proof (prove)
goal (2 subgoals):
 1. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>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 p f w\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) a) None], p\<^sub>1), ?b16 a p\<^sub>1 ap b p\<^sub>2 pd c) \<in> vs_lookup1 s
 2. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>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 p f w\<rbrakk> \<Longrightarrow> (?b16 a p\<^sub>1 ap b p\<^sub>2 pd c, [VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], ptrFromPAddr p) \<in> vs_lookup1 s proof (prove)
goal (1 subgoal):
 1. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>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 p f w\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], p\<^sub>2), [VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], ptrFromPAddr p) \<in> vs_lookup1 s proof (prove)
goal (1 subgoal):
 1. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>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 p f w\<rbrakk> \<Longrightarrow> \<exists>a. a \<notin> kernel_mapping_slots \<and> (a \<notin> kernel_mapping_slots \<longrightarrow> pde_ref (pd a) = Some (ptrFromPAddr p) \<and> UCAST(12 \<rightarrow> 32) c = UCAST(12 \<rightarrow> 32) a) proof (prove)
goal (1 subgoal):
 1. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>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 p f w\<rbrakk> \<Longrightarrow> c \<notin> kernel_mapping_slots \<and> (c \<notin> kernel_mapping_slots \<longrightarrow> pde_ref (pd c) = Some (ptrFromPAddr p) \<and> UCAST(12 \<rightarrow> 32) c = UCAST(12 \<rightarrow> 32) c) proof (prove)
goal:
No subgoals!