kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchInvariants_AI

lemma vs_lookup_step:
  "\<lbrakk> (ref \<rhd> p) s; ((ref, p) \<rhd>1 (ref', p')) s \<rbrakk> \<Longrightarrow> (ref' \<rhd> p') s" unfolding vs_lookup_def apply clarsimp apply (drule rtrancl_trans) apply (erule r_into_rtrancl) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(ref \<rhd> p) s; ((ref, p), ref', p') \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> (ref' \<rhd> p') s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(ref, p) \<in> (vs_lookup1 s)\<^sup>* `` vs_asid_refs (asid_table s); ((ref, p), ref', p') \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> (ref', p') \<in> (vs_lookup1 s)\<^sup>* `` vs_asid_refs (asid_table s) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>((ref, p), ref', p') \<in> vs_lookup1 s; ((a, b), ref, p) \<in> (vs_lookup1 s)\<^sup>*; (a, b) \<in> vs_asid_refs (asid_table s)\<rbrakk> \<Longrightarrow> (ref', p') \<in> (vs_lookup1 s)\<^sup>* `` vs_asid_refs (asid_table s) proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>((ref, p), ref', p') \<in> vs_lookup1 s; (a, b) \<in> vs_asid_refs (asid_table s)\<rbrakk> \<Longrightarrow> ((ref, p), ?z1 a b) \<in> (vs_lookup1 s)\<^sup>*
 2. \<And>a b. \<lbrakk>((ref, p), ref', p') \<in> vs_lookup1 s; (a, b) \<in> vs_asid_refs (asid_table s); ((a, b), ?z1 a b) \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> (ref', p') \<in> (vs_lookup1 s)\<^sup>* `` vs_asid_refs (asid_table s) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>((ref, p), ref', p') \<in> vs_lookup1 s; (a, b) \<in> vs_asid_refs (asid_table s); ((a, b), ref', p') \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> (ref', p') \<in> (vs_lookup1 s)\<^sup>* `` vs_asid_refs (asid_table s) proof (prove)
goal:
No subgoals!
theory ArchInvariants_AI

lemma vs_lookup_pages_step:
  "\<lbrakk> (ref \<unrhd> p) s; ((ref, p) \<unrhd>1 (ref', p')) s \<rbrakk> \<Longrightarrow> (ref' \<unrhd> p') s" unfolding vs_lookup_pages_def apply clarsimp apply (drule rtrancl_trans) apply (erule r_into_rtrancl) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(ref \<unrhd> p) s; ((ref, p), ref', p') \<in> vs_lookup_pages1 s\<rbrakk> \<Longrightarrow> (ref' \<unrhd> p') s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(ref, p) \<in> (vs_lookup_pages1 s)\<^sup>* `` vs_asid_refs (asid_table s); ((ref, p), ref', p') \<in> vs_lookup_pages1 s\<rbrakk> \<Longrightarrow> (ref', p') \<in> (vs_lookup_pages1 s)\<^sup>* `` vs_asid_refs (asid_table s) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>((ref, p), ref', p') \<in> vs_lookup_pages1 s; ((a, b), ref, p) \<in> (vs_lookup_pages1 s)\<^sup>*; (a, b) \<in> vs_asid_refs (asid_table s)\<rbrakk> \<Longrightarrow> (ref', p') \<in> (vs_lookup_pages1 s)\<^sup>* `` vs_asid_refs (asid_table s) proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>((ref, p), ref', p') \<in> vs_lookup_pages1 s; (a, b) \<in> vs_asid_refs (asid_table s)\<rbrakk> \<Longrightarrow> ((ref, p), ?z1 a b) \<in> (vs_lookup_pages1 s)\<^sup>*
 2. \<And>a b. \<lbrakk>((ref, p), ref', p') \<in> vs_lookup_pages1 s; (a, b) \<in> vs_asid_refs (asid_table s); ((a, b), ?z1 a b) \<in> (vs_lookup_pages1 s)\<^sup>*\<rbrakk> \<Longrightarrow> (ref', p') \<in> (vs_lookup_pages1 s)\<^sup>* `` vs_asid_refs (asid_table s) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>((ref, p), ref', p') \<in> vs_lookup_pages1 s; (a, b) \<in> vs_asid_refs (asid_table s); ((a, b), ref', p') \<in> (vs_lookup_pages1 s)\<^sup>*\<rbrakk> \<Longrightarrow> (ref', p') \<in> (vs_lookup_pages1 s)\<^sup>* `` vs_asid_refs (asid_table s) proof (prove)
goal:
No subgoals!
theory ArchInvariants_AI

lemma vs_asid_refsI:
  "table asid = Some p \<Longrightarrow>
  ([VSRef (ucast asid) None],p) \<in> vs_asid_refs table" by (fastforce simp: vs_asid_refs_def graph_of_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. table asid = Some p \<Longrightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) asid) None], p) \<in> vs_asid_refs table
theory ArchInvariants_AI

lemma vs_lookup_atI:
  "arm_asid_table (arch_state s) a = Some p \<Longrightarrow> ([VSRef (ucast a) None] \<rhd> p) s" unfolding vs_lookup_def by (drule vs_asid_refsI) fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. asid_table s a = Some p \<Longrightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> p) s proof (prove)
goal (1 subgoal):
 1. asid_table s a = Some p \<Longrightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) a) None], p) \<in> (vs_lookup1 s)\<^sup>* `` vs_asid_refs (asid_table s)
theory ArchInvariants_AI

lemma vs_lookup_apI:
  "\<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\<rbrakk>
     \<Longrightarrow> ([VSRef (ucast b) (Some AASIDPool), VSRef (ucast a) None] \<rhd> 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_refl) apply (fastforce simp: vs_lookup1_def obj_at_def vs_refs_def graph_of_def image_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>a p\<^sub>1 ap b. \<lbrakk>asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p\<rbrakk> \<Longrightarrow> ([VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> p) s proof (prove)
goal (1 subgoal):
 1. \<And>a p\<^sub>1 ap b. \<lbrakk>asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p\<rbrakk> \<Longrightarrow> \<exists>aa ba. asid_table s aa = Some ba \<and> (([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba), [VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], p) \<in> (vs_lookup1 s)\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>a p\<^sub>1 ap b. \<lbrakk>asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) a) None], p\<^sub>1), [VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], p) \<in> (vs_lookup1 s)\<^sup>* proof (prove)
goal (2 subgoals):
 1. \<And>a p\<^sub>1 ap b. \<lbrakk>asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) a) None], p\<^sub>1), ?b16 a p\<^sub>1 ap b) \<in> (vs_lookup1 s)\<^sup>*
 2. \<And>a p\<^sub>1 ap b. \<lbrakk>asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p\<rbrakk> \<Longrightarrow> (?b16 a p\<^sub>1 ap b, [VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], p) \<in> vs_lookup1 s proof (prove)
goal (1 subgoal):
 1. \<And>a p\<^sub>1 ap b. \<lbrakk>asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) a) None], p\<^sub>1), [VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], p) \<in> vs_lookup1 s proof (prove)
goal:
No subgoals!
theory ArchInvariants_AI

lemma vs_lookup_pages_pdI:
  "\<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\<rbrakk>
   \<Longrightarrow> ([VSRef (ucast c) (Some APageDirectory),
         VSRef (ucast b) (Some AASIDPool), VSRef (ucast a) None] \<unrhd> p) s" apply (frule (2) vs_lookup_pages_apI) apply (erule vs_lookup_pages_step) by (fastforce simp: vs_lookup_pages1_def obj_at_def
                      vs_refs_pages_def graph_of_def image_def
               split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<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; pde_ref_pages (pd c) = Some p\<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] \<unrhd> p) s proof (prove)
goal (1 subgoal):
 1. \<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; pde_ref_pages (pd c) = Some p; ([VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] \<unrhd> p\<^sub>2) 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] \<unrhd> p) s proof (prove)
goal (1 subgoal):
 1. \<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; pde_ref_pages (pd c) = Some p\<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], p) \<in> vs_lookup_pages1 s
theory ArchInvariants_AI

lemma vs_lookup_pages_ptI:
  "\<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\<rbrakk>
   \<Longrightarrow> ([VSRef (ucast d) (Some APageTable),
         VSRef (ucast c) (Some APageDirectory),
         VSRef (ucast b) (Some AASIDPool), VSRef (ucast a) None] \<unrhd> p) s" apply (frule (5) vs_lookup_pdI[THEN vs_lookup_pages_vs_lookupI]) apply (erule vs_lookup_pages_step) by (fastforce simp: vs_lookup_pages1_def obj_at_def
                      vs_refs_pages_def graph_of_def image_def
               split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<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 x y; kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)); pte_ref_pages (pt d) = Some p\<rbrakk> \<Longrightarrow> ([VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable), VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] \<unrhd> p) s proof (prove)
goal (1 subgoal):
 1. \<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 x y; kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)); pte_ref_pages (pt d) = Some p; ([VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] \<unrhd> ptrFromPAddr addr) s\<rbrakk> \<Longrightarrow> ([VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable), VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None] \<unrhd> p) s proof (prove)
goal (1 subgoal):
 1. \<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 x y; kheap s (ptrFromPAddr addr) = Some (ArchObj (PageTable pt)); pte_ref_pages (pt d) = Some p\<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], ptrFromPAddr addr), [VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable), VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) b) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) a) None], p) \<in> vs_lookup_pages1 s
theory ArchInvariants_AI

lemma vs_lookupE:
  "\<lbrakk> (ref \<rhd> p) s;
    \<And>ref' p'. \<lbrakk> (ref',p') \<in> vs_asid_refs (arm_asid_table (arch_state s));
                ((ref',p') \<rhd>* (ref,p)) s \<rbrakk> \<Longrightarrow> P \<rbrakk>
  \<Longrightarrow> P" by (auto simp: vs_lookup_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(ref \<rhd> p) s; \<And>ref' p'. \<lbrakk>(ref', p') \<in> vs_asid_refs (asid_table s); ((ref', p'), ref, p) \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
theory ArchInvariants_AI

lemma valid_asid_tableD:
  "\<lbrakk> T x = Some p; valid_asid_table T s \<rbrakk> \<Longrightarrow> asid_pool_at p s" by (auto simp: valid_asid_table_def ran_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>T x = Some p; valid_asid_table T s\<rbrakk> \<Longrightarrow> typ_at (AArch AASIDPool) p s
theory ArchInvariants_AI

lemma pde_graph_ofI:
  "\<lbrakk>pd x = pde; x \<notin> kernel_mapping_slots; pde_ref pde = Some v\<rbrakk>
   \<Longrightarrow> (x, v) \<in> graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None
                              else pde_ref (pd x))" by (rule graph_ofI, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pd x = pde; x \<notin> kernel_mapping_slots; pde_ref pde = Some v\<rbrakk> \<Longrightarrow> (x, v) \<in> graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x))
theory ArchInvariants_AI

lemma aa_type_pdD:
  "aa_type ko = APageDirectory \<Longrightarrow> \<exists>pd. ko = PageDirectory pd" by (clarsimp simp: aa_type_def
               split: arch_kernel_obj.splits if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. aa_type ko = APageDirectory \<Longrightarrow> \<exists>pd. ko = PageDirectory pd
theory ArchInvariants_AI

lemma empty_table_is_valid:
  "\<lbrakk>empty_table (set (arm_global_pts (arch_state s))) (ArchObj ao);
    valid_arch_state s\<rbrakk>
   \<Longrightarrow> valid_vspace_obj ao s" by (cases ao, simp_all add: empty_table_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>empty_table (set (arm_global_pts (arch_state s))) (ArchObj ao); valid_arch_state s\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s
theory ArchInvariants_AI

lemma empty_table_pde_refD:
  "\<lbrakk> pde_ref (pd x) = Some r; empty_table S (ArchObj (PageDirectory pd)) \<rbrakk> \<Longrightarrow>
  r \<in> S" by (simp add: empty_table_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pde_ref (pd x) = Some r; empty_table S (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> r \<in> S
theory ArchInvariants_AI

lemma valid_global_ptsD:
  "\<lbrakk>r \<in> set (arm_global_pts (arch_state s)); valid_global_objs s\<rbrakk>
   \<Longrightarrow> \<exists>pt. ko_at (ArchObj (PageTable pt)) r s \<and> (\<forall>x. aligned_pte (pt x))" by (clarsimp simp: valid_global_objs_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>r \<in> set (arm_global_pts (arch_state s)); valid_global_objs s\<rbrakk> \<Longrightarrow> \<exists>pt. ako_at (PageTable pt) r s \<and> (\<forall>x. aligned_pte (pt x))
theory ArchInvariants_AI

lemma valid_table_caps_pdD:
  "\<lbrakk> caps_of_state s p = Some (ArchObjectCap (PageDirectoryCap pd None));
     valid_table_caps s \<rbrakk> \<Longrightarrow>
    obj_at (empty_table (set (second_level_tables (arch_state s)))) pd s" apply (clarsimp simp: valid_table_caps_def simp del: split_paired_All) apply (erule allE)+ apply (erule (1) impE) apply (fastforce simp add: is_pd_cap_def cap_asid_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s p = Some (ArchObjectCap (PageDirectoryCap pd None)); valid_table_caps s\<rbrakk> \<Longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) pd s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s p = Some (ArchObjectCap (PageDirectoryCap pd None)); \<forall>r p cap. caps_of_state s p = Some cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) r s) \<and> (is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)\<rbrakk> \<Longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) pd s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s p = Some (ArchObjectCap (PageDirectoryCap pd None)); caps_of_state s ?p5 = Some ?cap7 \<longrightarrow> (is_pd_cap ?cap7 \<longrightarrow> cap_asid ?cap7 = None \<longrightarrow> ?r3 \<in> obj_refs ?cap7 \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) ?r3 s) \<and> (is_pt_cap ?cap7 \<longrightarrow> cap_asid ?cap7 = None \<longrightarrow> ?r3 \<in> obj_refs ?cap7 \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) ?r3 s)\<rbrakk> \<Longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) pd s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s p = Some (ArchObjectCap (PageDirectoryCap pd None)); (is_pd_cap (ArchObjectCap (PageDirectoryCap pd None)) \<longrightarrow> cap_asid (ArchObjectCap (PageDirectoryCap pd None)) = None \<longrightarrow> ?r3 \<in> obj_refs (ArchObjectCap (PageDirectoryCap pd None)) \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) ?r3 s) \<and> (is_pt_cap (ArchObjectCap (PageDirectoryCap pd None)) \<longrightarrow> cap_asid (ArchObjectCap (PageDirectoryCap pd None)) = None \<longrightarrow> ?r3 \<in> obj_refs (ArchObjectCap (PageDirectoryCap pd None)) \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) ?r3 s)\<rbrakk> \<Longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) pd s proof (prove)
goal:
No subgoals!
theory ArchInvariants_AI

lemma valid_vs_lookupD:
  "\<lbrakk> (ref \<unrhd> p) s; valid_vs_lookup s \<rbrakk> \<Longrightarrow>
  (\<exists>slot cap. caps_of_state s slot = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref)" by (simp add: valid_vs_lookup_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(ref \<unrhd> p) s; valid_vs_lookup s\<rbrakk> \<Longrightarrow> \<exists>slot cap. caps_of_state s slot = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref
theory ArchInvariants_AI

lemma addrFromPPtr_ptrFromPAddr_id[simp]:
  "addrFromPPtr (ptrFromPAddr x) = x" by (simp add: addrFromPPtr_def ptrFromPAddr_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. addrFromPPtr (ptrFromPAddr x) = x
theory ArchInvariants_AI

lemma valid_pte_lift2:
  assumes x: "\<And>T p. \<lbrace>Q and typ_at (AArch T) p\<rbrace> f \<lbrace>\<lambda>rv. typ_at (AArch T) p\<rbrace>"
  shows "\<lbrace>\<lambda>s. Q s \<and> valid_pte pte s\<rbrace> f \<lbrace>\<lambda>rv s. valid_pte pte s\<rbrace>" by (cases pte) (simp add: data_at_def | wp hoare_vcg_disj_lift x)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. Q s \<and> valid_pte pte s\<rbrace> f \<lbrace>\<lambda>rv. valid_pte pte\<rbrace>
theory ArchInvariants_AI

lemma valid_pde_lift2:
  assumes x: "\<And>T p. \<lbrace>Q and typ_at (AArch T) p\<rbrace> f \<lbrace>\<lambda>rv. typ_at (AArch T) p\<rbrace>"
  shows "\<lbrace>\<lambda>s. Q s \<and> valid_pde pde s\<rbrace> f \<lbrace>\<lambda>rv s. valid_pde pde s\<rbrace>" by (cases pde) (simp add: data_at_def | wp hoare_vcg_disj_lift x)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. Q s \<and> valid_pde pde s\<rbrace> f \<lbrace>\<lambda>rv. valid_pde pde\<rbrace>
theory ArchInvariants_AI

lemma valid_vspace_obj_typ2:
  assumes P: "\<And>P p T. \<lbrace>\<lambda>s. Q s \<and> P (typ_at (AArch T) p s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at (AArch T) p s)\<rbrace>"
  shows      "\<lbrace>\<lambda>s. Q s \<and> valid_vspace_obj ob s\<rbrace> f \<lbrace>\<lambda>rv s. valid_vspace_obj ob s\<rbrace>" by (cases ob; (wpsimp wp: hoare_vcg_all_lift hoare_vcg_const_Ball_lift
        valid_pte_lift2[where Q=Q] valid_pde_lift2[where Q=Q] P))

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. Q s \<and> valid_vspace_obj ob s\<rbrace> f \<lbrace>\<lambda>rv. valid_vspace_obj ob\<rbrace>
theory ArchInvariants_AI

lemma valid_vspace_objsI [intro?]:
  "(\<And>p ao. \<lbrakk> (\<exists>\<rhd> p) s; ko_at (ArchObj ao) p s \<rbrakk> \<Longrightarrow> valid_vspace_obj ao s) \<Longrightarrow> valid_vspace_objs s" by (simp add: valid_vspace_objs_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>p ao. \<lbrakk>\<exists>ref. (ref \<rhd> p) s; ako_at ao p s\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s) \<Longrightarrow> valid_vspace_objs s
theory ArchInvariants_AI

lemma vs_lookup1_stateI2:
  assumes 1: "(r \<rhd>1 r') s"
  assumes ko: "\<And>ko. \<lbrakk> ko_at ko (snd r) s; vs_refs ko \<noteq> {} \<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko'. vs_refs ko \<subseteq> vs_refs ko') (snd r) s'"
  shows "(r \<rhd>1 r') s'" using 1 ko by (fastforce simp: obj_at_def vs_lookup1_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (r, r') \<in> vs_lookup1 s' proof (prove)
using this:
(r, r') \<in> vs_lookup1 s
\<lbrakk>ko_at ?ko (snd r) s; vs_refs ?ko \<noteq> {}\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko'. vs_refs ?ko \<subseteq> vs_refs ko') (snd r) s'

goal (1 subgoal):
 1. (r, r') \<in> vs_lookup1 s'
theory ArchInvariants_AI

lemma vs_lookupI:
  "\<lbrakk> ref' \<in> vs_asid_refs (arm_asid_table (arch_state s));
     (ref',(ref,p)) \<in> (vs_lookup1 s)^*  \<rbrakk> \<Longrightarrow>
  (ref \<rhd> p) s" by (simp add: vs_lookup_def) blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ref' \<in> vs_asid_refs (asid_table s); (ref', ref, p) \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> (ref \<rhd> p) s
theory ArchInvariants_AI

lemma vs_lookup1_trans_is_append':
  "(a, b) \<in> (vs_lookup1 s)\<^sup>* \<Longrightarrow> \<exists>zs. fst b = zs @ fst a" by (erule rtrancl_induct) (auto dest!: vs_lookup1D)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (a, b) \<in> (vs_lookup1 s)\<^sup>* \<Longrightarrow> \<exists>zs. fst b = zs @ fst a
theory ArchInvariants_AI

lemma vs_lookup1_trans_is_append:
  "((xs, a), (ys, b)) \<in> (vs_lookup1 s)\<^sup>* \<Longrightarrow> \<exists>zs. ys = zs @ xs" by (drule vs_lookup1_trans_is_append') auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((xs, a), ys, b) \<in> (vs_lookup1 s)\<^sup>* \<Longrightarrow> \<exists>zs. ys = zs @ xs