theory ArchInvariants_AI

lemma vs_lookup1_ko_at_dest:
  "\<lbrakk> ((ref, p) \<rhd>1 (ref', p')) s; ko_at (ArchObj ao) p s; valid_vspace_obj ao s \<rbrakk> \<Longrightarrow>
  \<exists>ao'. ko_at (ArchObj ao') p' s \<and> (\<exists>tp. vs_ref_aatype (hd ref') = Some tp
                                            \<and> aa_type ao = tp)" apply (drule vs_lookup1D) apply (clarsimp simp: obj_at_def vs_refs_def) apply (cases ao, simp_all add: graph_of_def) apply clarsimp apply (drule bspec, fastforce simp: ran_def) apply (clarsimp simp add: aa_type_def obj_at_def) apply (clarsimp split: arch_kernel_obj.split_asm if_split_asm) apply (simp add: pde_ref_def aa_type_def
            split: pde.splits) apply (erule_tac x=a in ballE) apply (clarsimp simp add: obj_at_def) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>((ref, p), ref', p') \<in> vs_lookup1 s; ako_at ao p s; valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> \<exists>ao'. ako_at ao' p' s \<and> (\<exists>tp. vs_ref_aatype (hd ref') = Some tp \<and> aa_type ao = tp) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ako_at ao p s; valid_vspace_obj ao s; \<exists>rs r pa p'a ko. (ref, p) = (rs, pa) \<and> (ref', p') = (r # rs, p'a) \<and> ko_at ko pa s \<and> (r, p'a) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> \<exists>ao'. ako_at ao' p' s \<and> (\<exists>tp. vs_ref_aatype (hd ref') = Some tp \<and> aa_type ao = tp) proof (prove)
goal (1 subgoal):
 1. \<And>r. \<lbrakk>kheap s p = Some (ArchObj ao); valid_vspace_obj ao s; (r, p') \<in> (case ao of ASIDPool pool \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | 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)) | _ \<Rightarrow> {}); ref' = r # ref\<rbrakk> \<Longrightarrow> (\<exists>ao'. kheap s p' = Some (ArchObj ao')) \<and> vs_ref_aatype r = Some (aa_type ao) proof (prove)
goal (2 subgoals):
 1. \<And>r x1. \<lbrakk>kheap s p = Some (ArchObj (ASIDPool x1)); \<forall>x\<in>ran x1. typ_at (AArch APageDirectory) x s; (r, p') \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), x)) ` {(x, y). x1 x = Some y}; ref' = r # ref; ao = ASIDPool x1\<rbrakk> \<Longrightarrow> (\<exists>ao'. kheap s p' = Some (ArchObj ao')) \<and> vs_ref_aatype r = Some (aa_type (ASIDPool x1))
 2. \<And>r x3. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); \<forall>x\<in>- kernel_mapping_slots. valid_pde (x3 x) s; (r, p') \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` {(x, y). (if x \<in> kernel_mapping_slots then None else pde_ref (x3 x)) = Some y}; ref' = r # ref; ao = PageDirectory x3\<rbrakk> \<Longrightarrow> (\<exists>ao'. kheap s p' = Some (ArchObj ao')) \<and> vs_ref_aatype r = Some (aa_type (PageDirectory x3)) proof (prove)
goal (2 subgoals):
 1. \<And>x1 a. \<lbrakk>kheap s p = Some (ArchObj (ASIDPool x1)); \<forall>x\<in>ran x1. typ_at (AArch APageDirectory) x s; ref' = VSRef (UCAST(10 \<rightarrow> 32) a) (Some AASIDPool) # ref; ao = ASIDPool x1; x1 a = Some p'\<rbrakk> \<Longrightarrow> (\<exists>ao'. kheap s p' = Some (ArchObj ao')) \<and> AASIDPool = aa_type (ASIDPool x1)
 2. \<And>r x3. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); \<forall>x\<in>- kernel_mapping_slots. valid_pde (x3 x) s; (r, p') \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` {(x, y). (if x \<in> kernel_mapping_slots then None else pde_ref (x3 x)) = Some y}; ref' = r # ref; ao = PageDirectory x3\<rbrakk> \<Longrightarrow> (\<exists>ao'. kheap s p' = Some (ArchObj ao')) \<and> vs_ref_aatype r = Some (aa_type (PageDirectory x3)) proof (prove)
goal (2 subgoals):
 1. \<And>x1 a. \<lbrakk>kheap s p = Some (ArchObj (ASIDPool x1)); ref' = VSRef (UCAST(10 \<rightarrow> 32) a) (Some AASIDPool) # ref; ao = ASIDPool x1; x1 a = Some p'; typ_at (AArch APageDirectory) p' s\<rbrakk> \<Longrightarrow> (\<exists>ao'. kheap s p' = Some (ArchObj ao')) \<and> AASIDPool = aa_type (ASIDPool x1)
 2. \<And>r x3. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); \<forall>x\<in>- kernel_mapping_slots. valid_pde (x3 x) s; (r, p') \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` {(x, y). (if x \<in> kernel_mapping_slots then None else pde_ref (x3 x)) = Some y}; ref' = r # ref; ao = PageDirectory x3\<rbrakk> \<Longrightarrow> (\<exists>ao'. kheap s p' = Some (ArchObj ao')) \<and> vs_ref_aatype r = Some (aa_type (PageDirectory x3)) proof (prove)
goal (1 subgoal):
 1. \<And>r x3. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); \<forall>x\<in>- kernel_mapping_slots. valid_pde (x3 x) s; (r, p') \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` {(x, y). (if x \<in> kernel_mapping_slots then None else pde_ref (x3 x)) = Some y}; ref' = r # ref; ao = PageDirectory x3\<rbrakk> \<Longrightarrow> (\<exists>ao'. kheap s p' = Some (ArchObj ao')) \<and> vs_ref_aatype r = Some (aa_type (PageDirectory x3)) proof (prove)
goal (1 subgoal):
 1. \<And>x3 a. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); \<forall>x\<in>- kernel_mapping_slots. valid_pde (x3 x) s; ref' = VSRef (UCAST(12 \<rightarrow> 32) a) (Some APageDirectory) # ref; ao = PageDirectory x3; a \<notin> kernel_mapping_slots; pde_ref (x3 a) = Some p'\<rbrakk> \<Longrightarrow> (\<exists>ao'. kheap s p' = Some (ArchObj ao')) \<and> APageDirectory = aa_type (PageDirectory x3) proof (prove)
goal (1 subgoal):
 1. \<And>x3 a x21 x22 x23. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); \<forall>x\<in>- kernel_mapping_slots. valid_pde (x3 x) s; ref' = VSRef (UCAST(12 \<rightarrow> 32) a) (Some APageDirectory) # ref; ao = PageDirectory x3; a \<notin> kernel_mapping_slots; x3 a = PageTablePDE x21 x22 x23; ptrFromPAddr x21 = p'\<rbrakk> \<Longrightarrow> \<exists>ao'. kheap s p' = Some (ArchObj ao') proof (prove)
goal (2 subgoals):
 1. \<And>x3 a x21 x22 x23. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); ref' = VSRef (UCAST(12 \<rightarrow> 32) a) (Some APageDirectory) # ref; ao = PageDirectory x3; a \<notin> kernel_mapping_slots; x3 a = PageTablePDE x21 x22 x23; ptrFromPAddr x21 = p'; valid_pde (x3 a) s\<rbrakk> \<Longrightarrow> \<exists>ao'. kheap s p' = Some (ArchObj ao')
 2. \<And>x3 a x21 x22 x23. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); ref' = VSRef (UCAST(12 \<rightarrow> 32) a) (Some APageDirectory) # ref; ao = PageDirectory x3; a \<notin> kernel_mapping_slots; x3 a = PageTablePDE x21 x22 x23; ptrFromPAddr x21 = p'; a \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<exists>ao'. kheap s p' = Some (ArchObj ao') proof (prove)
goal (1 subgoal):
 1. \<And>x3 a x21 x22 x23. \<lbrakk>kheap s p = Some (ArchObj (PageDirectory x3)); ref' = VSRef (UCAST(12 \<rightarrow> 32) a) (Some APageDirectory) # ref; ao = PageDirectory x3; a \<notin> kernel_mapping_slots; x3 a = PageTablePDE x21 x22 x23; ptrFromPAddr x21 = p'; a \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<exists>ao'. kheap s p' = Some (ArchObj ao') proof (prove)
goal:
No subgoals!