theory ArchInvariants_AI

lemma vs_lookup_pagesE_alt:
  assumes vl: "(ref \<unrhd> 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_pages (pd c) = Some p; valid_pde (pd c) s\<rbrakk>
       \<Longrightarrow> R [VSRef (ucast c) (Some APageDirectory),
              VSRef (ucast b) (Some AASIDPool), VSRef (ucast a) None] p"
  assumes 3: "\<And>a p\<^sub>1 ap b p\<^sub>2 pd c addr x y pt d.
       \<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 = PageTablePDE addr x y;
        kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt));
        pte_ref_pages (pt d) = Some p; valid_pte (pt d) s\<rbrakk>
       \<Longrightarrow> R [VSRef (ucast d) (Some APageTable),
              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] note vpt = vao[THEN conjunct2, THEN conjunct2, THEN conjunct2, rule_format] from vl show ?thesis apply (clarsimp simp: vs_lookup_pages_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_pages_def graph_of_def obj_at_def
                   dest!: vs_lookup_pages1D) apply (frule (2) vap) apply (erule converse_rtranclE) apply clarsimp apply (erule (3) 1) apply (clarsimp simp: vs_refs_pages_def graph_of_def obj_at_def
                   dest!: vs_lookup_pages1D  split: if_split_asm) apply (frule (4) vpd) apply (erule converse_rtranclE) apply clarsimp apply (erule (6) 2) apply (clarsimp simp: vs_refs_pages_def graph_of_def obj_at_def
                          pde_ref_pages_def data_at_def
                   dest!: vs_lookup_pages1D
                   split: if_split_asm pde.splits) apply (frule_tac d=ac in vpt, assumption+) apply (erule converse_rtranclE) apply clarsimp apply (erule (8) 3) apply (auto simp: vs_refs_pages_def graph_of_def obj_at_def
                          pte_ref_pages_def data_at_def
                   dest!: vs_lookup_pages1D
                   split: pte.splits) done 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 (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; ?pd ?c = PageTablePDE ?addr ?f ?w; kheap s (ptrFromPAddr ?addr) = Some (ArchObj (PageTable ?pt))\<rbrakk> \<Longrightarrow> valid_pte (?pt ?d) s

goal (1 subgoal):
 1. R ref p proof (chain)
picking this:
(ref \<unrhd> p) s proof (prove)
using this:
(ref \<unrhd> 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_lookup_pages1 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_lookup_pages1 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_lookup_pages1 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_lookup_pages1 s; (y, ref, p) \<in> (vs_lookup_pages1 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_lookup_pages1 s; (y, ref, p) \<in> (vs_lookup_pages1 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_lookup_pages1 s; (y, ref, p) \<in> (vs_lookup_pages1 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_lookup_pages1 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_lookup_pages1 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_lookup_pages1 s; (y, ref, p) \<in> (vs_lookup_pages1 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_lookup_pages1 s; (y, ref, p) \<in> (vs_lookup_pages1 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_lookup_pages1 s; (y, ref, p) \<in> (vs_lookup_pages1 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_lookup_pages1 s)\<^sup>*; kheap s paa = Some (ArchObj (PageDirectory pd)); ab \<notin> kernel_mapping_slots; pde_ref_pages (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_lookup_pages1 s)\<^sup>*; kheap s paa = Some (ArchObj (PageDirectory pd)); ab \<notin> kernel_mapping_slots; pde_ref_pages (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_pages (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_pages (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_lookup_pages1 s; (y, ref, p) \<in> (vs_lookup_pages1 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_pages (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_pages (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_lookup_pages1 s; (y, ref, p) \<in> (vs_lookup_pages1 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_pages (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_lookup_pages1 s; (y, ref, p) \<in> (vs_lookup_pages1 s)\<^sup>*\<rbrakk> \<Longrightarrow> R ref p proof (prove)
goal (3 subgoals):
 1. \<And>aa pa ap a paa pd ab x21 x22 x23 pt ac b. \<lbrakk>(([VSRef (UCAST(8 \<rightarrow> 32) ac) (Some APageTable), 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_lookup_pages1 s)\<^sup>*; 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; pd ab = PageTablePDE x21 x22 x23; kheap s (ptrFromPAddr x21) = Some (ArchObj (PageTable pt)); pte_ref_pages (pt ac) = Some b\<rbrakk> \<Longrightarrow> R ref p
 2. \<And>aa pa ap a paa pd ab x31 x32 x33 x34 r p' ko. \<lbrakk>a_type ko = AArch (AUserData ARMSection) \<or> a_type ko = AArch (ADeviceData ARMSection); (([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'), ref, p) \<in> (vs_lookup_pages1 s)\<^sup>*; 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; pd ab = SectionPDE x31 x32 x33 x34; kheap s (ptrFromPAddr x31) = Some ko; (r, p') \<in> (case ko of ArchObj (ASIDPool pool) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | ArchObj (PageTable pt) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(8 \<rightarrow> 32) r) (Some APageTable), y)) ` graph_of (pte_ref_pages \<circ> pt) | ArchObj (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_pages (pd x)) | ArchObj (DataPage dev s) \<Rightarrow> {} | _ \<Rightarrow> {})\<rbrakk> \<Longrightarrow> R ref p
 3. \<And>aa pa ap a paa pd ab x41 x42 x43 r p' ko. \<lbrakk>a_type ko = AArch (AUserData ARMSuperSection) \<or> a_type ko = AArch (ADeviceData ARMSuperSection); (([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'), ref, p) \<in> (vs_lookup_pages1 s)\<^sup>*; 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; pd ab = SuperSectionPDE x41 x42 x43; kheap s (ptrFromPAddr x41) = Some ko; (r, p') \<in> (case ko of ArchObj (ASIDPool pool) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | ArchObj (PageTable pt) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(8 \<rightarrow> 32) r) (Some APageTable), y)) ` graph_of (pte_ref_pages \<circ> pt) | ArchObj (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_pages (pd x)) | ArchObj (DataPage dev s) \<Rightarrow> {} | _ \<Rightarrow> {})\<rbrakk> \<Longrightarrow> R ref p proof (prove)
goal (3 subgoals):
 1. \<And>aa pa ap a paa pd ab x21 x22 x23 pt ac b. \<lbrakk>(([VSRef (UCAST(8 \<rightarrow> 32) ac) (Some APageTable), 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_lookup_pages1 s)\<^sup>*; 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; pd ab = PageTablePDE x21 x22 x23; kheap s (ptrFromPAddr x21) = Some (ArchObj (PageTable pt)); pte_ref_pages (pt ac) = Some b; valid_pte (pt ac) s\<rbrakk> \<Longrightarrow> R ref p
 2. \<And>aa pa ap a paa pd ab x31 x32 x33 x34 r p' ko. \<lbrakk>a_type ko = AArch (AUserData ARMSection) \<or> a_type ko = AArch (ADeviceData ARMSection); (([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'), ref, p) \<in> (vs_lookup_pages1 s)\<^sup>*; 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; pd ab = SectionPDE x31 x32 x33 x34; kheap s (ptrFromPAddr x31) = Some ko; (r, p') \<in> (case ko of ArchObj (ASIDPool pool) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | ArchObj (PageTable pt) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(8 \<rightarrow> 32) r) (Some APageTable), y)) ` graph_of (pte_ref_pages \<circ> pt) | ArchObj (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_pages (pd x)) | ArchObj (DataPage dev s) \<Rightarrow> {} | _ \<Rightarrow> {})\<rbrakk> \<Longrightarrow> R ref p
 3. \<And>aa pa ap a paa pd ab x41 x42 x43 r p' ko. \<lbrakk>a_type ko = AArch (AUserData ARMSuperSection) \<or> a_type ko = AArch (ADeviceData ARMSuperSection); (([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'), ref, p) \<in> (vs_lookup_pages1 s)\<^sup>*; 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; pd ab = SuperSectionPDE x41 x42 x43; kheap s (ptrFromPAddr x41) = Some ko; (r, p') \<in> (case ko of ArchObj (ASIDPool pool) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | ArchObj (PageTable pt) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(8 \<rightarrow> 32) r) (Some APageTable), y)) ` graph_of (pte_ref_pages \<circ> pt) | ArchObj (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_pages (pd x)) | ArchObj (DataPage dev s) \<Rightarrow> {} | _ \<Rightarrow> {})\<rbrakk> \<Longrightarrow> R ref p proof (prove)
goal (4 subgoals):
 1. \<And>aa pa ap a paa pd ab x21 x22 x23 pt ac 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; pd ab = PageTablePDE x21 x22 x23; kheap s (ptrFromPAddr x21) = Some (ArchObj (PageTable pt)); pte_ref_pages (pt ac) = Some b; valid_pte (pt ac) s; ([VSRef (UCAST(8 \<rightarrow> 32) ac) (Some APageTable), 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 x21 x22 x23 pt ac 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; pd ab = PageTablePDE x21 x22 x23; kheap s (ptrFromPAddr x21) = Some (ArchObj (PageTable pt)); pte_ref_pages (pt ac) = Some b; valid_pte (pt ac) s; (([VSRef (UCAST(8 \<rightarrow> 32) ac) (Some APageTable), 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_lookup_pages1 s; (y, ref, p) \<in> (vs_lookup_pages1 s)\<^sup>*\<rbrakk> \<Longrightarrow> R ref p
 3. \<And>aa pa ap a paa pd ab x31 x32 x33 x34 r p' ko. \<lbrakk>a_type ko = AArch (AUserData ARMSection) \<or> a_type ko = AArch (ADeviceData ARMSection); (([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'), ref, p) \<in> (vs_lookup_pages1 s)\<^sup>*; 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; pd ab = SectionPDE x31 x32 x33 x34; kheap s (ptrFromPAddr x31) = Some ko; (r, p') \<in> (case ko of ArchObj (ASIDPool pool) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | ArchObj (PageTable pt) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(8 \<rightarrow> 32) r) (Some APageTable), y)) ` graph_of (pte_ref_pages \<circ> pt) | ArchObj (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_pages (pd x)) | ArchObj (DataPage dev s) \<Rightarrow> {} | _ \<Rightarrow> {})\<rbrakk> \<Longrightarrow> R ref p
 4. \<And>aa pa ap a paa pd ab x41 x42 x43 r p' ko. \<lbrakk>a_type ko = AArch (AUserData ARMSuperSection) \<or> a_type ko = AArch (ADeviceData ARMSuperSection); (([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'), ref, p) \<in> (vs_lookup_pages1 s)\<^sup>*; 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; pd ab = SuperSectionPDE x41 x42 x43; kheap s (ptrFromPAddr x41) = Some ko; (r, p') \<in> (case ko of ArchObj (ASIDPool pool) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | ArchObj (PageTable pt) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(8 \<rightarrow> 32) r) (Some APageTable), y)) ` graph_of (pte_ref_pages \<circ> pt) | ArchObj (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_pages (pd x)) | ArchObj (DataPage dev s) \<Rightarrow> {} | _ \<Rightarrow> {})\<rbrakk> \<Longrightarrow> R ref p proof (prove)
goal (4 subgoals):
 1. \<And>aa pa ap a paa pd ab x21 x22 x23 pt ac. \<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; pd ab = PageTablePDE x21 x22 x23; kheap s (ptrFromPAddr x21) = Some (ArchObj (PageTable pt)); pte_ref_pages (pt ac) = Some p; valid_pte (pt ac) s; ref = [VSRef (UCAST(8 \<rightarrow> 32) ac) (Some APageTable), 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(8 \<rightarrow> 32) ac) (Some APageTable), 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 x21 x22 x23 pt ac 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; pd ab = PageTablePDE x21 x22 x23; kheap s (ptrFromPAddr x21) = Some (ArchObj (PageTable pt)); pte_ref_pages (pt ac) = Some b; valid_pte (pt ac) s; (([VSRef (UCAST(8 \<rightarrow> 32) ac) (Some APageTable), 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_lookup_pages1 s; (y, ref, p) \<in> (vs_lookup_pages1 s)\<^sup>*\<rbrakk> \<Longrightarrow> R ref p
 3. \<And>aa pa ap a paa pd ab x31 x32 x33 x34 r p' ko. \<lbrakk>a_type ko = AArch (AUserData ARMSection) \<or> a_type ko = AArch (ADeviceData ARMSection); (([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'), ref, p) \<in> (vs_lookup_pages1 s)\<^sup>*; 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; pd ab = SectionPDE x31 x32 x33 x34; kheap s (ptrFromPAddr x31) = Some ko; (r, p') \<in> (case ko of ArchObj (ASIDPool pool) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | ArchObj (PageTable pt) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(8 \<rightarrow> 32) r) (Some APageTable), y)) ` graph_of (pte_ref_pages \<circ> pt) | ArchObj (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_pages (pd x)) | ArchObj (DataPage dev s) \<Rightarrow> {} | _ \<Rightarrow> {})\<rbrakk> \<Longrightarrow> R ref p
 4. \<And>aa pa ap a paa pd ab x41 x42 x43 r p' ko. \<lbrakk>a_type ko = AArch (AUserData ARMSuperSection) \<or> a_type ko = AArch (ADeviceData ARMSuperSection); (([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'), ref, p) \<in> (vs_lookup_pages1 s)\<^sup>*; 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; pd ab = SuperSectionPDE x41 x42 x43; kheap s (ptrFromPAddr x41) = Some ko; (r, p') \<in> (case ko of ArchObj (ASIDPool pool) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | ArchObj (PageTable pt) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(8 \<rightarrow> 32) r) (Some APageTable), y)) ` graph_of (pte_ref_pages \<circ> pt) | ArchObj (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_pages (pd x)) | ArchObj (DataPage dev s) \<Rightarrow> {} | _ \<Rightarrow> {})\<rbrakk> \<Longrightarrow> R ref p proof (prove)
goal (3 subgoals):
 1. \<And>aa pa ap a paa pd ab x21 x22 x23 pt ac 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; pd ab = PageTablePDE x21 x22 x23; kheap s (ptrFromPAddr x21) = Some (ArchObj (PageTable pt)); pte_ref_pages (pt ac) = Some b; valid_pte (pt ac) s; (([VSRef (UCAST(8 \<rightarrow> 32) ac) (Some APageTable), 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_lookup_pages1 s; (y, ref, p) \<in> (vs_lookup_pages1 s)\<^sup>*\<rbrakk> \<Longrightarrow> R ref p
 2. \<And>aa pa ap a paa pd ab x31 x32 x33 x34 r p' ko. \<lbrakk>a_type ko = AArch (AUserData ARMSection) \<or> a_type ko = AArch (ADeviceData ARMSection); (([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'), ref, p) \<in> (vs_lookup_pages1 s)\<^sup>*; 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; pd ab = SectionPDE x31 x32 x33 x34; kheap s (ptrFromPAddr x31) = Some ko; (r, p') \<in> (case ko of ArchObj (ASIDPool pool) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | ArchObj (PageTable pt) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(8 \<rightarrow> 32) r) (Some APageTable), y)) ` graph_of (pte_ref_pages \<circ> pt) | ArchObj (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_pages (pd x)) | ArchObj (DataPage dev s) \<Rightarrow> {} | _ \<Rightarrow> {})\<rbrakk> \<Longrightarrow> R ref p
 3. \<And>aa pa ap a paa pd ab x41 x42 x43 r p' ko. \<lbrakk>a_type ko = AArch (AUserData ARMSuperSection) \<or> a_type ko = AArch (ADeviceData ARMSuperSection); (([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'), ref, p) \<in> (vs_lookup_pages1 s)\<^sup>*; 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; pd ab = SuperSectionPDE x41 x42 x43; kheap s (ptrFromPAddr x41) = Some ko; (r, p') \<in> (case ko of ArchObj (ASIDPool pool) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | ArchObj (PageTable pt) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(8 \<rightarrow> 32) r) (Some APageTable), y)) ` graph_of (pte_ref_pages \<circ> pt) | ArchObj (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_pages (pd x)) | ArchObj (DataPage dev s) \<Rightarrow> {} | _ \<Rightarrow> {})\<rbrakk> \<Longrightarrow> R ref p proof (prove)
goal:
No subgoals! proof (state)
this:
R ref p

goal:
No subgoals!