theory ArchADT_AC

lemma pt_in_pd_page_table_at:
  "\<lbrakk> invs s; get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) pd_ptr x =
     Some (PageTablePDE word1 set1 word2); (\<exists>\<rhd> pd_ptr) s; x \<notin> kernel_mappings \<rbrakk>
     \<Longrightarrow> page_table_at (ptrFromPAddr word1) s" apply (clarsimp simp: get_pd_entry_def get_arch_obj_def
                  split: option.splits kernel_object.splits arch_kernel_obj.splits) apply (rename_tac "fun") apply (subgoal_tac "valid_vspace_obj (PageDirectory fun) s") apply (simp add: kernel_mappings_slots_eq) apply (drule bspec) apply simp+ apply (drule invs_vspace_objs) apply (auto simp: obj_at_def invs_vspace_objs valid_vspace_objs_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) pd_ptr x = Some (PageTablePDE word1 set1 word2); \<exists>ref. (ref \<rhd> pd_ptr) s; x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> typ_at (AArch APageTable) (ptrFromPAddr word1) s proof (prove)
goal (1 subgoal):
 1. \<And>ref x3. \<lbrakk>x \<notin> kernel_mappings; invs s; kheap s pd_ptr = Some (ArchObj (PageDirectory x3)); (ref \<rhd> pd_ptr) s; x3 (UCAST(32 \<rightarrow> 12) (x >> 20)) = PageTablePDE word1 set1 word2\<rbrakk> \<Longrightarrow> typ_at (AArch APageTable) (ptrFromPAddr word1) s proof (prove)
goal (1 subgoal):
 1. \<And>ref fun. \<lbrakk>x \<notin> kernel_mappings; invs s; kheap s pd_ptr = Some (ArchObj (PageDirectory fun)); (ref \<rhd> pd_ptr) s; fun (UCAST(32 \<rightarrow> 12) (x >> 20)) = PageTablePDE word1 set1 word2\<rbrakk> \<Longrightarrow> typ_at (AArch APageTable) (ptrFromPAddr word1) s proof (prove)
goal (2 subgoals):
 1. \<And>ref fun. \<lbrakk>x \<notin> kernel_mappings; invs s; kheap s pd_ptr = Some (ArchObj (PageDirectory fun)); (ref \<rhd> pd_ptr) s; fun (UCAST(32 \<rightarrow> 12) (x >> 20)) = PageTablePDE word1 set1 word2; valid_vspace_obj (PageDirectory fun) s\<rbrakk> \<Longrightarrow> typ_at (AArch APageTable) (ptrFromPAddr word1) s
 2. \<And>ref fun. \<lbrakk>x \<notin> kernel_mappings; invs s; kheap s pd_ptr = Some (ArchObj (PageDirectory fun)); (ref \<rhd> pd_ptr) s; fun (UCAST(32 \<rightarrow> 12) (x >> 20)) = PageTablePDE word1 set1 word2\<rbrakk> \<Longrightarrow> valid_vspace_obj (PageDirectory fun) s proof (prove)
goal (2 subgoals):
 1. \<And>ref fun. \<lbrakk>UCAST(32 \<rightarrow> 12) (x >> 20) \<notin> kernel_mapping_slots; invs s; kheap s pd_ptr = Some (ArchObj (PageDirectory fun)); (ref \<rhd> pd_ptr) s; fun (UCAST(32 \<rightarrow> 12) (x >> 20)) = PageTablePDE word1 set1 word2; \<forall>x\<in>- kernel_mapping_slots. valid_pde (fun x) s\<rbrakk> \<Longrightarrow> typ_at (AArch APageTable) (ptrFromPAddr word1) s
 2. \<And>ref fun. \<lbrakk>x \<notin> kernel_mappings; invs s; kheap s pd_ptr = Some (ArchObj (PageDirectory fun)); (ref \<rhd> pd_ptr) s; fun (UCAST(32 \<rightarrow> 12) (x >> 20)) = PageTablePDE word1 set1 word2\<rbrakk> \<Longrightarrow> valid_vspace_obj (PageDirectory fun) s proof (prove)
goal (3 subgoals):
 1. \<And>ref fun. \<lbrakk>UCAST(32 \<rightarrow> 12) (x >> 20) \<notin> kernel_mapping_slots; invs s; kheap s pd_ptr = Some (ArchObj (PageDirectory fun)); (ref \<rhd> pd_ptr) s; fun (UCAST(32 \<rightarrow> 12) (x >> 20)) = PageTablePDE word1 set1 word2\<rbrakk> \<Longrightarrow> ?x86 ref fun \<in> - kernel_mapping_slots
 2. \<And>ref fun. \<lbrakk>UCAST(32 \<rightarrow> 12) (x >> 20) \<notin> kernel_mapping_slots; invs s; kheap s pd_ptr = Some (ArchObj (PageDirectory fun)); (ref \<rhd> pd_ptr) s; fun (UCAST(32 \<rightarrow> 12) (x >> 20)) = PageTablePDE word1 set1 word2; valid_pde (fun (?x86 ref fun)) s\<rbrakk> \<Longrightarrow> typ_at (AArch APageTable) (ptrFromPAddr word1) s
 3. \<And>ref fun. \<lbrakk>x \<notin> kernel_mappings; invs s; kheap s pd_ptr = Some (ArchObj (PageDirectory fun)); (ref \<rhd> pd_ptr) s; fun (UCAST(32 \<rightarrow> 12) (x >> 20)) = PageTablePDE word1 set1 word2\<rbrakk> \<Longrightarrow> valid_vspace_obj (PageDirectory fun) s proof (prove)
goal (1 subgoal):
 1. \<And>ref fun. \<lbrakk>x \<notin> kernel_mappings; invs s; kheap s pd_ptr = Some (ArchObj (PageDirectory fun)); (ref \<rhd> pd_ptr) s; fun (UCAST(32 \<rightarrow> 12) (x >> 20)) = PageTablePDE word1 set1 word2\<rbrakk> \<Longrightarrow> \<forall>x\<in>- kernel_mapping_slots. valid_pde (fun x) s proof (prove)
goal (1 subgoal):
 1. \<And>ref fun. \<lbrakk>x \<notin> kernel_mappings; kheap s pd_ptr = Some (ArchObj (PageDirectory fun)); (ref \<rhd> pd_ptr) s; fun (UCAST(32 \<rightarrow> 12) (x >> 20)) = PageTablePDE word1 set1 word2; valid_vspace_objs s\<rbrakk> \<Longrightarrow> \<forall>x\<in>- kernel_mapping_slots. valid_pde (fun x) s proof (prove)
goal:
No subgoals!