theory ArchInvariants_AI

lemma vs_lookupE_alt:
  assumes vl: "(ref \<rhd> p) s"
  assumes va: "valid_vspace_objs s"
  assumes vt: "(\<forall>p\<in>ran (arm_asid_table (arch_state s)). asid_pool_at p s)"
  assumes 0: "\<And>a. arm_asid_table (arch_state s) a = Some p \<Longrightarrow>
                   typ_at (AArch AASIDPool) p s \<Longrightarrow>
                   R [VSRef (ucast a) None] p"
  assumes 1: "\<And>a p\<^sub>1 ap b.
       \<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; page_directory_at p s\<rbrakk>
       \<Longrightarrow> R [VSRef (ucast b) (Some AASIDPool), VSRef (ucast a) None] p"
  assumes 2: "\<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; pde_ref (pd c) = Some p; page_table_at p s\<rbrakk>
       \<Longrightarrow> R [VSRef (ucast c) (Some APageDirectory),
              VSRef (ucast b) (Some AASIDPool), VSRef (ucast a) None] p"
  shows "R ref p" proof - note vao = valid_vspace_objs_alt[THEN iffD1, OF conjI[OF vt va]] note vat = vao[THEN conjunct1, rule_format] note vap = vao[THEN conjunct2, THEN conjunct1, rule_format] note vpd = vao[THEN conjunct2, THEN conjunct2, THEN conjunct1, rule_format] from vl show ?thesis apply (clarsimp simp: vs_lookup_def) apply (clarsimp simp: Image_def vs_asid_refs_def graph_of_def) apply (frule vat) apply (erule converse_rtranclE) apply clarsimp apply (erule (1) 0) apply (clarsimp simp: vs_refs_def graph_of_def obj_at_def
                   dest!: vs_lookup1D) apply (frule (2) vap) apply (erule converse_rtranclE) apply clarsimp apply (erule (3) 1) apply (clarsimp simp: vs_refs_def graph_of_def obj_at_def
                   dest!: vs_lookup1D  split: if_split_asm) apply (frule (4) vpd) apply (erule converse_rtranclE) apply clarsimp apply (erule (5) 2) apply (simp add: valid_pde_def pde_ref_def split: pde.splits) by (clarsimp simp: obj_at_def pde_ref_def vs_refs_def
                split: pde.splits
                dest!: vs_lookup1D) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. R ref p proof (state)
goal (1 subgoal):
 1. R ref p proof (state)
this:
(\<forall>a p. asid_table s a = Some p \<longrightarrow> typ_at (AArch AASIDPool) p s) \<and> (\<forall>a p\<^sub>1 ap b p. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p \<longrightarrow> typ_at (AArch APageDirectory) p s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> valid_pde (pd c) s) \<and> (\<forall>a p\<^sub>1 ap b p\<^sub>2 pd c addr f w pt. asid_table s a = Some p\<^sub>1 \<longrightarrow> kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)) \<longrightarrow> ap b = Some p\<^sub>2 \<longrightarrow> kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow> c \<notin> kernel_mapping_slots \<longrightarrow> pd c = PageTablePDE addr f w \<longrightarrow> kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. valid_pte (pt d) s))

goal (1 subgoal):
 1. R ref p proof (state)
this:
asid_table s ?a = Some ?p \<Longrightarrow> typ_at (AArch AASIDPool) ?p s

goal (1 subgoal):
 1. R ref p proof (state)
this:
\<lbrakk>asid_table s ?a = Some ?p\<^sub>1; kheap s ?p\<^sub>1 = Some (ArchObj (ASIDPool ?ap)); ?ap ?b = Some ?p\<rbrakk> \<Longrightarrow> typ_at (AArch APageDirectory) ?p s

goal (1 subgoal):
 1. R ref p proof (state)
this:
\<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\<rbrakk> \<Longrightarrow> valid_pde (?pd ?c) s

goal (1 subgoal):
 1. R ref p proof (chain)
picking this:
(ref \<rhd> p) s proof (prove)
using this:
(ref \<rhd> p) s

goal (1 subgoal):
 1. R ref p proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>((a, b), ref, p) \<in> (vs_lookup1 s)\<^sup>*; (a, b) \<in> vs_asid_refs (asid_table s)\<rbrakk> \<Longrightarrow> R ref p proof (prove)
goal (1 subgoal):
 1. \<And>aa ba. \<lbrakk>(([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba), ref, p) \<in> (vs_lookup1 s)\<^sup>*; asid_table s aa = Some ba\<rbrakk> \<Longrightarrow> R ref p proof (prove)
goal (1 subgoal):
 1. \<And>aa ba. \<lbrakk>(([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba), ref, p) \<in> (vs_lookup1 s)\<^sup>*; asid_table s aa = Some ba; typ_at (AArch AASIDPool) ba s\<rbrakk> \<Longrightarrow> R ref p proof (prove)
goal (2 subgoals):
 1. \<And>aa ba. \<lbrakk>asid_table s aa = Some ba; typ_at (AArch AASIDPool) ba s; ([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba) = (ref, p)\<rbrakk> \<Longrightarrow> R ref p
 2. \<And>aa ba y. \<lbrakk>asid_table s aa = Some ba; typ_at (AArch AASIDPool) ba s; (([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba), y) \<in> vs_lookup1 s; (y, ref, p) \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> R ref p proof (prove)
goal (2 subgoals):
 1. \<And>aa. \<lbrakk>asid_table s aa = Some p; typ_at (AArch AASIDPool) p s; ref = [VSRef (UCAST(7 \<rightarrow> 32) aa) None]\<rbrakk> \<Longrightarrow> R [VSRef (UCAST(7 \<rightarrow> 32) aa) None] p
 2. \<And>aa ba y. \<lbrakk>asid_table s aa = Some ba; typ_at (AArch AASIDPool) ba s; (([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba), y) \<in> vs_lookup1 s; (y, ref, p) \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> R ref p proof (prove)
goal (1 subgoal):
 1. \<And>aa ba y. \<lbrakk>asid_table s aa = Some ba; typ_at (AArch AASIDPool) ba s; (([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba), y) \<in> vs_lookup1 s; (y, ref, p) \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> R ref p proof (prove)
goal (1 subgoal):
 1. \<And>aa pa ap a b. \<lbrakk>asid_table s aa = Some pa; (([VSRef (UCAST(10 \<rightarrow> 32) a) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) aa) None], b), ref, p) \<in> (vs_lookup1 s)\<^sup>*; kheap s pa = Some (ArchObj (ASIDPool ap)); ap a = Some b\<rbrakk> \<Longrightarrow> R ref p proof (prove)
goal (1 subgoal):
 1. \<And>aa pa ap a b. \<lbrakk>asid_table s aa = Some pa; (([VSRef (UCAST(10 \<rightarrow> 32) a) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) aa) None], b), ref, p) \<in> (vs_lookup1 s)\<^sup>*; kheap s pa = Some (ArchObj (ASIDPool ap)); ap a = Some b; typ_at (AArch APageDirectory) b s\<rbrakk> \<Longrightarrow> R ref p proof (prove)
goal (2 subgoals):
 1. \<And>aa pa ap a b. \<lbrakk>asid_table s aa = Some pa; kheap s pa = Some (ArchObj (ASIDPool ap)); ap a = Some b; typ_at (AArch APageDirectory) b s; ([VSRef (UCAST(10 \<rightarrow> 32) a) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) aa) None], b) = (ref, p)\<rbrakk> \<Longrightarrow> R ref p
 2. \<And>aa pa ap a b y. \<lbrakk>asid_table s aa = Some pa; kheap s pa = Some (ArchObj (ASIDPool ap)); ap a = Some b; typ_at (AArch APageDirectory) b s; (([VSRef (UCAST(10 \<rightarrow> 32) a) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) aa) None], b), y) \<in> vs_lookup1 s; (y, ref, p) \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> R ref p proof (prove)
goal (2 subgoals):
 1. \<And>aa pa ap a. \<lbrakk>asid_table s aa = Some pa; kheap s pa = Some (ArchObj (ASIDPool ap)); ap a = Some p; typ_at (AArch APageDirectory) p s; ref = [VSRef (UCAST(10 \<rightarrow> 32) a) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) aa) None]\<rbrakk> \<Longrightarrow> R [VSRef (UCAST(10 \<rightarrow> 32) a) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) aa) None] p
 2. \<And>aa pa ap a b y. \<lbrakk>asid_table s aa = Some pa; kheap s pa = Some (ArchObj (ASIDPool ap)); ap a = Some b; typ_at (AArch APageDirectory) b s; (([VSRef (UCAST(10 \<rightarrow> 32) a) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) aa) None], b), y) \<in> vs_lookup1 s; (y, ref, p) \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> R ref p proof (prove)
goal (1 subgoal):
 1. \<And>aa pa ap a b y. \<lbrakk>asid_table s aa = Some pa; kheap s pa = Some (ArchObj (ASIDPool ap)); ap a = Some b; typ_at (AArch APageDirectory) b s; (([VSRef (UCAST(10 \<rightarrow> 32) a) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) aa) None], b), y) \<in> vs_lookup1 s; (y, ref, p) \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> R ref p proof (prove)
goal (1 subgoal):
 1. \<And>aa pa ap a paa pd ab b. \<lbrakk>asid_table s aa = Some pa; kheap s pa = Some (ArchObj (ASIDPool ap)); ap a = Some paa; (([VSRef (UCAST(12 \<rightarrow> 32) ab) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) a) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) aa) None], b), ref, p) \<in> (vs_lookup1 s)\<^sup>*; kheap s paa = Some (ArchObj (PageDirectory pd)); ab \<notin> kernel_mapping_slots; pde_ref (pd ab) = Some b\<rbrakk> \<Longrightarrow> R ref p proof (prove)
goal (1 subgoal):
 1. \<And>aa pa ap a paa pd ab b. \<lbrakk>asid_table s aa = Some pa; kheap s pa = Some (ArchObj (ASIDPool ap)); ap a = Some paa; (([VSRef (UCAST(12 \<rightarrow> 32) ab) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) a) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) aa) None], b), ref, p) \<in> (vs_lookup1 s)\<^sup>*; kheap s paa = Some (ArchObj (PageDirectory pd)); ab \<notin> kernel_mapping_slots; pde_ref (pd ab) = Some b; valid_pde (pd ab) s\<rbrakk> \<Longrightarrow> R ref p proof (prove)
goal (2 subgoals):
 1. \<And>aa pa ap a paa pd ab b. \<lbrakk>asid_table s aa = Some pa; kheap s pa = Some (ArchObj (ASIDPool ap)); ap a = Some paa; kheap s paa = Some (ArchObj (PageDirectory pd)); ab \<notin> kernel_mapping_slots; pde_ref (pd ab) = Some b; valid_pde (pd ab) s; ([VSRef (UCAST(12 \<rightarrow> 32) ab) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) a) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) aa) None], b) = (ref, p)\<rbrakk> \<Longrightarrow> R ref p
 2. \<And>aa pa ap a paa pd ab b y. \<lbrakk>asid_table s aa = Some pa; kheap s pa = Some (ArchObj (ASIDPool ap)); ap a = Some paa; kheap s paa = Some (ArchObj (PageDirectory pd)); ab \<notin> kernel_mapping_slots; pde_ref (pd ab) = Some b; valid_pde (pd ab) s; (([VSRef (UCAST(12 \<rightarrow> 32) ab) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) a) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) aa) None], b), y) \<in> vs_lookup1 s; (y, ref, p) \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> R ref p proof (prove)
goal (2 subgoals):
 1. \<And>aa pa ap a paa pd ab. \<lbrakk>asid_table s aa = Some pa; kheap s pa = Some (ArchObj (ASIDPool ap)); ap a = Some paa; kheap s paa = Some (ArchObj (PageDirectory pd)); ab \<notin> kernel_mapping_slots; pde_ref (pd ab) = Some p; valid_pde (pd ab) s; ref = [VSRef (UCAST(12 \<rightarrow> 32) ab) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) a) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) aa) None]\<rbrakk> \<Longrightarrow> R [VSRef (UCAST(12 \<rightarrow> 32) ab) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) a) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) aa) None] p
 2. \<And>aa pa ap a paa pd ab b y. \<lbrakk>asid_table s aa = Some pa; kheap s pa = Some (ArchObj (ASIDPool ap)); ap a = Some paa; kheap s paa = Some (ArchObj (PageDirectory pd)); ab \<notin> kernel_mapping_slots; pde_ref (pd ab) = Some b; valid_pde (pd ab) s; (([VSRef (UCAST(12 \<rightarrow> 32) ab) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) a) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) aa) None], b), y) \<in> vs_lookup1 s; (y, ref, p) \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> R ref p proof (prove)
goal (2 subgoals):
 1. \<And>aa pa ap a paa pd ab. \<lbrakk>kheap s pa = Some (ArchObj (ASIDPool ap)); ap a = Some paa; kheap s paa = Some (ArchObj (PageDirectory pd)); ab \<notin> kernel_mapping_slots; pde_ref (pd ab) = Some p; valid_pde (pd ab) s; ref = [VSRef (UCAST(12 \<rightarrow> 32) ab) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) a) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) aa) None]\<rbrakk> \<Longrightarrow> typ_at (AArch APageTable) p s
 2. \<And>aa pa ap a paa pd ab b y. \<lbrakk>asid_table s aa = Some pa; kheap s pa = Some (ArchObj (ASIDPool ap)); ap a = Some paa; kheap s paa = Some (ArchObj (PageDirectory pd)); ab \<notin> kernel_mapping_slots; pde_ref (pd ab) = Some b; valid_pde (pd ab) s; (([VSRef (UCAST(12 \<rightarrow> 32) ab) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) a) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) aa) None], b), y) \<in> vs_lookup1 s; (y, ref, p) \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> R ref p proof (prove)
goal (1 subgoal):
 1. \<And>aa pa ap a paa pd ab b y. \<lbrakk>asid_table s aa = Some pa; kheap s pa = Some (ArchObj (ASIDPool ap)); ap a = Some paa; kheap s paa = Some (ArchObj (PageDirectory pd)); ab \<notin> kernel_mapping_slots; pde_ref (pd ab) = Some b; valid_pde (pd ab) s; (([VSRef (UCAST(12 \<rightarrow> 32) ab) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) a) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) aa) None], b), y) \<in> vs_lookup1 s; (y, ref, p) \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> R ref p proof (state)
this:
R ref p

goal:
No subgoals!