theory ArchADT_AI

lemma get_page_info_section:
  "is_aligned pd_ref pd_bits \<Longrightarrow>
   get_pde (lookup_pd_slot pd_ref vptr) s =
     ({(SectionPDE base attrs X rights, s)},False) \<Longrightarrow>
   get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) pd_ref vptr =
     Some (base, 20, attrs, rights)" apply (simp add: lookup_pd_slot_def get_page_info_def split: option.splits) apply (intro conjI impI allI) apply (drule get_pd_entry_None_iff_get_pde_fail[where s=s and vptr=vptr]) apply (simp split: option.splits) apply (drule_tac x=x2 in get_pd_entry_Some_eq_get_pde[where s=s and vptr=vptr]) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned pd_ref pd_bits; get_pde (lookup_pd_slot pd_ref vptr) s = ({(SectionPDE base attrs X rights, s)}, False)\<rbrakk> \<Longrightarrow> get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) pd_ref vptr = Some (base, 20, attrs, rights) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned pd_ref pd_bits; get_pde (pd_ref + (vptr >> 20 << 2)) s = ({(SectionPDE base attrs X rights, s)}, False)\<rbrakk> \<Longrightarrow> (\<exists>y. get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) pd_ref vptr = Some y) \<and> (\<forall>x2. get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) pd_ref vptr = Some x2 \<longrightarrow> (case x2 of InvalidPDE \<Rightarrow> None | PageTablePDE p x xa \<Rightarrow> get_pt_info (\<lambda>obj. get_arch_obj (kheap s obj)) (ptrFromPAddr p) vptr | SectionPDE base attrs x rights \<Rightarrow> Some (base, 20, attrs, rights) | SuperSectionPDE base attrs rights \<Rightarrow> Some (base, 24, attrs, rights)) = Some (base, 20, attrs, rights)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned pd_ref pd_bits; get_pde (pd_ref + (vptr >> 20 << 2)) s = ({(SectionPDE base attrs X rights, s)}, False)\<rbrakk> \<Longrightarrow> \<exists>y. get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) pd_ref vptr = Some y
 2. \<And>x2. \<lbrakk>is_aligned pd_ref pd_bits; get_pde (pd_ref + (vptr >> 20 << 2)) s = ({(SectionPDE base attrs X rights, s)}, False); get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) pd_ref vptr = Some x2\<rbrakk> \<Longrightarrow> (case x2 of InvalidPDE \<Rightarrow> None | PageTablePDE p x xa \<Rightarrow> get_pt_info (\<lambda>obj. get_arch_obj (kheap s obj)) (ptrFromPAddr p) vptr | SectionPDE base attrs x rights \<Rightarrow> Some (base, 20, attrs, rights) | SuperSectionPDE base attrs rights \<Rightarrow> Some (base, 24, attrs, rights)) = Some (base, 20, attrs, rights) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>get_pde (pd_ref + (vptr >> 20 << 2)) s = ({(SectionPDE base attrs X rights, s)}, False); (get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) pd_ref vptr = None) = (get_pde (pd_ref + (vptr >> 20 << 2)) s = ({}, True))\<rbrakk> \<Longrightarrow> \<exists>y. get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) pd_ref vptr = Some y
 2. \<And>x2. \<lbrakk>is_aligned pd_ref pd_bits; get_pde (pd_ref + (vptr >> 20 << 2)) s = ({(SectionPDE base attrs X rights, s)}, False); get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) pd_ref vptr = Some x2\<rbrakk> \<Longrightarrow> (case x2 of InvalidPDE \<Rightarrow> None | PageTablePDE p x xa \<Rightarrow> get_pt_info (\<lambda>obj. get_arch_obj (kheap s obj)) (ptrFromPAddr p) vptr | SectionPDE base attrs x rights \<Rightarrow> Some (base, 20, attrs, rights) | SuperSectionPDE base attrs rights \<Rightarrow> Some (base, 24, attrs, rights)) = Some (base, 20, attrs, rights) proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>is_aligned pd_ref pd_bits; get_pde (pd_ref + (vptr >> 20 << 2)) s = ({(SectionPDE base attrs X rights, s)}, False); get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) pd_ref vptr = Some x2\<rbrakk> \<Longrightarrow> (case x2 of InvalidPDE \<Rightarrow> None | PageTablePDE p x xa \<Rightarrow> get_pt_info (\<lambda>obj. get_arch_obj (kheap s obj)) (ptrFromPAddr p) vptr | SectionPDE base attrs x rights \<Rightarrow> Some (base, 20, attrs, rights) | SuperSectionPDE base attrs rights \<Rightarrow> Some (base, 24, attrs, rights)) = Some (base, 20, attrs, rights) proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>get_pde (pd_ref + (vptr >> 20 << 2)) s = ({(SectionPDE base attrs X rights, s)}, False); get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) pd_ref vptr = Some x2; (get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) pd_ref vptr = Some x2) = (get_pde (pd_ref + (vptr >> 20 << 2)) s = ({(x2, s)}, False))\<rbrakk> \<Longrightarrow> (case x2 of InvalidPDE \<Rightarrow> None | PageTablePDE p x xa \<Rightarrow> get_pt_info (\<lambda>obj. get_arch_obj (kheap s obj)) (ptrFromPAddr p) vptr | SectionPDE base attrs x rights \<Rightarrow> Some (base, 20, attrs, rights) | SuperSectionPDE base attrs rights \<Rightarrow> Some (base, 24, attrs, rights)) = Some (base, 20, attrs, rights) proof (prove)
goal:
No subgoals!