theory ArchADT_AI

lemma get_page_info_pte:
  "is_aligned pd_ref pd_bits \<Longrightarrow>
   lookup_pt_slot pd_ref vptr s = ({(Inr x,s)},False) \<Longrightarrow>
   is_aligned (x - ((vptr >> 12) && 0xFF << 2)) pt_bits \<Longrightarrow>
   get_pte x s = ({(pte,s)},False) \<Longrightarrow>
   get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) pd_ref vptr =
   (case pte of
     SmallPagePTE base attrs rights \<Rightarrow> Some (base, 12, attrs, rights)
   | LargePagePTE base attrs rights \<Rightarrow> Some (base, 16, attrs, rights)
   | _ \<Rightarrow> None)" apply (clarsimp simp add: get_page_info_def get_pd_entry_def
                split: option.splits) apply (intro conjI impI allI) apply (frule lookup_pt_slot_fail[of _ vptr s],
         clarsimp simp add: get_arch_obj_def) apply (frule lookup_pt_slot_fail[of _ vptr s],
        clarsimp simp add: get_arch_obj_def) apply (frule lookup_pt_slot_fail[of _ vptr s],
       clarsimp simp add: get_arch_obj_def) apply (frule (1) lookup_pt_slot_no_fail[where vptr=vptr]) apply (clarsimp split: pde.splits option.splits) apply (clarsimp simp add: get_pt_info_def split: option.splits) apply (intro conjI impI) apply (drule get_pt_entry_None_iff_get_pte_fail[where s=s and vptr=vptr]) apply (simp add: pt_bits_def pageBits_def mask_def) apply clarsimp apply (drule_tac x=x2 in get_pt_entry_Some_eq_get_pte[where s=s and vptr=vptr]) apply (simp add: pt_bits_def pageBits_def mask_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned pd_ref pd_bits; lookup_pt_slot pd_ref vptr s = ({(Inr x, s)}, False); is_aligned (x - ((vptr >> 12) && 0xFF << 2)) pt_bits; get_pte x s = ({(pte, s)}, False)\<rbrakk> \<Longrightarrow> get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) pd_ref vptr = (case pte of InvalidPTE \<Rightarrow> None | LargePagePTE base attrs rights \<Rightarrow> Some (base, 16, attrs, rights) | SmallPagePTE base attrs rights \<Rightarrow> Some (base, 12, attrs, rights)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned pd_ref pd_bits; lookup_pt_slot pd_ref vptr s = ({(Inr x, s)}, False); is_aligned (x - ((vptr >> 12) && 0xFF << 2)) pt_bits; get_pte x s = ({(pte, s)}, False)\<rbrakk> \<Longrightarrow> (get_arch_obj (kheap s pd_ref) = None \<longrightarrow> None = (case pte of InvalidPTE \<Rightarrow> None | LargePagePTE base attrs rights \<Rightarrow> Some (base, 16, attrs, rights) | SmallPagePTE base attrs rights \<Rightarrow> Some (base, 12, attrs, rights))) \<and> (\<forall>x2. get_arch_obj (kheap s pd_ref) = Some x2 \<longrightarrow> ((case x2 of PageDirectory pd \<Rightarrow> Some (pd (UCAST(32 \<rightarrow> 12) (vptr >> 20))) | _ \<Rightarrow> None) = None \<longrightarrow> None = (case pte of InvalidPTE \<Rightarrow> None | LargePagePTE base attrs rights \<Rightarrow> Some (base, 16, attrs, rights) | SmallPagePTE base attrs rights \<Rightarrow> Some (base, 12, attrs, rights))) \<and> (\<forall>x2a. (case x2 of PageDirectory pd \<Rightarrow> Some (pd (UCAST(32 \<rightarrow> 12) (vptr >> 20))) | _ \<Rightarrow> None) = Some x2a \<longrightarrow> (case x2a 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)) = (case pte of InvalidPTE \<Rightarrow> None | LargePagePTE base attrs rights \<Rightarrow> Some (base, 16, attrs, rights) | SmallPagePTE base attrs rights \<Rightarrow> Some (base, 12, attrs, rights)))) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned pd_ref pd_bits; lookup_pt_slot pd_ref vptr s = ({(Inr x, s)}, False); is_aligned (x - ((vptr >> 12) && 0xFF << 2)) pt_bits; get_pte x s = ({(pte, s)}, False); get_arch_obj (kheap s pd_ref) = None\<rbrakk> \<Longrightarrow> None = (case pte of InvalidPTE \<Rightarrow> None | LargePagePTE base attrs rights \<Rightarrow> Some (base, 16, attrs, rights) | SmallPagePTE base attrs rights \<Rightarrow> Some (base, 12, attrs, rights))
 2. \<And>x2. \<lbrakk>is_aligned pd_ref pd_bits; lookup_pt_slot pd_ref vptr s = ({(Inr x, s)}, False); is_aligned (x - ((vptr >> 12) && 0xFF << 2)) pt_bits; get_pte x s = ({(pte, s)}, False); get_arch_obj (kheap s pd_ref) = Some x2; (case x2 of PageDirectory pd \<Rightarrow> Some (pd (UCAST(32 \<rightarrow> 12) (vptr >> 20))) | _ \<Rightarrow> None) = None\<rbrakk> \<Longrightarrow> None = (case pte of InvalidPTE \<Rightarrow> None | LargePagePTE base attrs rights \<Rightarrow> Some (base, 16, attrs, rights) | SmallPagePTE base attrs rights \<Rightarrow> Some (base, 12, attrs, rights))
 3. \<And>x2 x2a. \<lbrakk>is_aligned pd_ref pd_bits; lookup_pt_slot pd_ref vptr s = ({(Inr x, s)}, False); is_aligned (x - ((vptr >> 12) && 0xFF << 2)) pt_bits; get_pte x s = ({(pte, s)}, False); get_arch_obj (kheap s pd_ref) = Some x2; (case x2 of PageDirectory pd \<Rightarrow> Some (pd (UCAST(32 \<rightarrow> 12) (vptr >> 20))) | _ \<Rightarrow> None) = Some x2a\<rbrakk> \<Longrightarrow> (case x2a 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)) = (case pte of InvalidPTE \<Rightarrow> None | LargePagePTE base attrs rights \<Rightarrow> Some (base, 16, attrs, rights) | SmallPagePTE base attrs rights \<Rightarrow> Some (base, 12, attrs, rights)) proof (prove)
goal (2 subgoals):
 1. \<And>x2. \<lbrakk>is_aligned pd_ref pd_bits; lookup_pt_slot pd_ref vptr s = ({(Inr x, s)}, False); is_aligned (x - ((vptr >> 12) && 0xFF << 2)) pt_bits; get_pte x s = ({(pte, s)}, False); get_arch_obj (kheap s pd_ref) = Some x2; (case x2 of PageDirectory pd \<Rightarrow> Some (pd (UCAST(32 \<rightarrow> 12) (vptr >> 20))) | _ \<Rightarrow> None) = None\<rbrakk> \<Longrightarrow> None = (case pte of InvalidPTE \<Rightarrow> None | LargePagePTE base attrs rights \<Rightarrow> Some (base, 16, attrs, rights) | SmallPagePTE base attrs rights \<Rightarrow> Some (base, 12, attrs, rights))
 2. \<And>x2 x2a. \<lbrakk>is_aligned pd_ref pd_bits; lookup_pt_slot pd_ref vptr s = ({(Inr x, s)}, False); is_aligned (x - ((vptr >> 12) && 0xFF << 2)) pt_bits; get_pte x s = ({(pte, s)}, False); get_arch_obj (kheap s pd_ref) = Some x2; (case x2 of PageDirectory pd \<Rightarrow> Some (pd (UCAST(32 \<rightarrow> 12) (vptr >> 20))) | _ \<Rightarrow> None) = Some x2a\<rbrakk> \<Longrightarrow> (case x2a 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)) = (case pte of InvalidPTE \<Rightarrow> None | LargePagePTE base attrs rights \<Rightarrow> Some (base, 16, attrs, rights) | SmallPagePTE base attrs rights \<Rightarrow> Some (base, 12, attrs, rights)) proof (prove)
goal (1 subgoal):
 1. \<And>x2 x2a. \<lbrakk>is_aligned pd_ref pd_bits; lookup_pt_slot pd_ref vptr s = ({(Inr x, s)}, False); is_aligned (x - ((vptr >> 12) && 0xFF << 2)) pt_bits; get_pte x s = ({(pte, s)}, False); get_arch_obj (kheap s pd_ref) = Some x2; (case x2 of PageDirectory pd \<Rightarrow> Some (pd (UCAST(32 \<rightarrow> 12) (vptr >> 20))) | _ \<Rightarrow> None) = Some x2a\<rbrakk> \<Longrightarrow> (case x2a 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)) = (case pte of InvalidPTE \<Rightarrow> None | LargePagePTE base attrs rights \<Rightarrow> Some (base, 16, attrs, rights) | SmallPagePTE base attrs rights \<Rightarrow> Some (base, 12, attrs, rights)) proof (prove)
goal (1 subgoal):
 1. \<And>pdo. \<lbrakk>is_aligned pd_ref pd_bits; lookup_pt_slot pd_ref vptr s = ({(Inr x, s)}, False); is_aligned (x - ((vptr >> 12) && 0xFF << 2)) pt_bits; get_pte x s = ({(pte, s)}, False); kheap s pd_ref = Some (ArchObj (PageDirectory pdo))\<rbrakk> \<Longrightarrow> (case pdo (UCAST(32 \<rightarrow> 12) (vptr >> 20)) 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)) = (case pte of InvalidPTE \<Rightarrow> None | LargePagePTE base attrs rights \<Rightarrow> Some (base, 16, attrs, rights) | SmallPagePTE base attrs rights \<Rightarrow> Some (base, 12, attrs, rights)) proof (prove)
goal (1 subgoal):
 1. \<And>pdo. \<lbrakk>is_aligned pd_ref pd_bits; lookup_pt_slot pd_ref vptr s = ({(Inr x, s)}, False); is_aligned (x - ((vptr >> 12) && 0xFF << 2)) pt_bits; get_pte x s = ({(pte, s)}, False); kheap s pd_ref = Some (ArchObj (PageDirectory pdo)); lookup_pt_slot pd_ref vptr s = (case pdo (UCAST(32 \<rightarrow> 12) (vptr >> 20)) of PageTablePDE p x xa \<Rightarrow> ({(Inr (ptrFromPAddr p + ((vptr >> 12) && 0xFF << 2)), s)}, False) | _ \<Rightarrow> ({(Inl (MissingCapability 20), s)}, False))\<rbrakk> \<Longrightarrow> (case pdo (UCAST(32 \<rightarrow> 12) (vptr >> 20)) 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)) = (case pte of InvalidPTE \<Rightarrow> None | LargePagePTE base attrs rights \<Rightarrow> Some (base, 16, attrs, rights) | SmallPagePTE base attrs rights \<Rightarrow> Some (base, 12, attrs, rights)) proof (prove)
goal (1 subgoal):
 1. \<And>pdo x21 x22 x23. \<lbrakk>is_aligned (ptrFromPAddr x21) pt_bits; get_pte (ptrFromPAddr x21 + ((vptr >> 12) && 0xFF << 2)) s = ({(pte, s)}, False); kheap s pd_ref = Some (ArchObj (PageDirectory pdo)); lookup_pt_slot pd_ref vptr s = ({(Inr (ptrFromPAddr x21 + ((vptr >> 12) && 0xFF << 2)), s)}, False); is_aligned pd_ref pd_bits; pdo (UCAST(32 \<rightarrow> 12) (vptr >> 20)) = PageTablePDE x21 x22 x23; x = ptrFromPAddr x21 + ((vptr >> 12) && 0xFF << 2)\<rbrakk> \<Longrightarrow> get_pt_info (\<lambda>obj. get_arch_obj (kheap s obj)) (ptrFromPAddr x21) vptr = (case pte of InvalidPTE \<Rightarrow> None | LargePagePTE base attrs rights \<Rightarrow> Some (base, 16, attrs, rights) | SmallPagePTE base attrs rights \<Rightarrow> Some (base, 12, attrs, rights)) proof (prove)
goal (1 subgoal):
 1. \<And>pdo x21 x22 x23. \<lbrakk>is_aligned (ptrFromPAddr x21) pt_bits; get_pte (ptrFromPAddr x21 + ((vptr >> 12) && 0xFF << 2)) s = ({(pte, s)}, False); kheap s pd_ref = Some (ArchObj (PageDirectory pdo)); lookup_pt_slot pd_ref vptr s = ({(Inr (ptrFromPAddr x21 + ((vptr >> 12) && 0xFF << 2)), s)}, False); is_aligned pd_ref pd_bits; pdo (UCAST(32 \<rightarrow> 12) (vptr >> 20)) = PageTablePDE x21 x22 x23; x = ptrFromPAddr x21 + ((vptr >> 12) && 0xFF << 2)\<rbrakk> \<Longrightarrow> (get_pt_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (ptrFromPAddr x21) vptr = None \<longrightarrow> None = (case pte of InvalidPTE \<Rightarrow> None | LargePagePTE base attrs rights \<Rightarrow> Some (base, 16, attrs, rights) | SmallPagePTE base attrs rights \<Rightarrow> Some (base, 12, attrs, rights))) \<and> (\<forall>x2. get_pt_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (ptrFromPAddr x21) vptr = Some x2 \<longrightarrow> (case x2 of InvalidPTE \<Rightarrow> None | LargePagePTE base attrs rights \<Rightarrow> Some (base, 16, attrs, rights) | SmallPagePTE base attrs rights \<Rightarrow> Some (base, 12, attrs, rights)) = (case pte of InvalidPTE \<Rightarrow> None | LargePagePTE base attrs rights \<Rightarrow> Some (base, 16, attrs, rights) | SmallPagePTE base attrs rights \<Rightarrow> Some (base, 12, attrs, rights))) proof (prove)
goal (2 subgoals):
 1. \<And>pdo x21 x22 x23. \<lbrakk>is_aligned (ptrFromPAddr x21) pt_bits; get_pte (ptrFromPAddr x21 + ((vptr >> 12) && 0xFF << 2)) s = ({(pte, s)}, False); kheap s pd_ref = Some (ArchObj (PageDirectory pdo)); lookup_pt_slot pd_ref vptr s = ({(Inr (ptrFromPAddr x21 + ((vptr >> 12) && 0xFF << 2)), s)}, False); is_aligned pd_ref pd_bits; pdo (UCAST(32 \<rightarrow> 12) (vptr >> 20)) = PageTablePDE x21 x22 x23; x = ptrFromPAddr x21 + ((vptr >> 12) && 0xFF << 2); get_pt_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (ptrFromPAddr x21) vptr = None\<rbrakk> \<Longrightarrow> None = (case pte of InvalidPTE \<Rightarrow> None | LargePagePTE base attrs rights \<Rightarrow> Some (base, 16, attrs, rights) | SmallPagePTE base attrs rights \<Rightarrow> Some (base, 12, attrs, rights))
 2. \<And>pdo x21 x22 x23. \<lbrakk>is_aligned (ptrFromPAddr x21) pt_bits; get_pte (ptrFromPAddr x21 + ((vptr >> 12) && 0xFF << 2)) s = ({(pte, s)}, False); kheap s pd_ref = Some (ArchObj (PageDirectory pdo)); lookup_pt_slot pd_ref vptr s = ({(Inr (ptrFromPAddr x21 + ((vptr >> 12) && 0xFF << 2)), s)}, False); is_aligned pd_ref pd_bits; pdo (UCAST(32 \<rightarrow> 12) (vptr >> 20)) = PageTablePDE x21 x22 x23; x = ptrFromPAddr x21 + ((vptr >> 12) && 0xFF << 2)\<rbrakk> \<Longrightarrow> \<forall>x2. get_pt_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (ptrFromPAddr x21) vptr = Some x2 \<longrightarrow> (case x2 of InvalidPTE \<Rightarrow> None | LargePagePTE base attrs rights \<Rightarrow> Some (base, 16, attrs, rights) | SmallPagePTE base attrs rights \<Rightarrow> Some (base, 12, attrs, rights)) = (case pte of InvalidPTE \<Rightarrow> None | LargePagePTE base attrs rights \<Rightarrow> Some (base, 16, attrs, rights) | SmallPagePTE base attrs rights \<Rightarrow> Some (base, 12, attrs, rights)) proof (prove)
goal (2 subgoals):
 1. \<And>pdo x21 x22 x23. \<lbrakk>get_pte (ptrFromPAddr x21 + ((vptr >> 12) && 0xFF << 2)) s = ({(pte, s)}, False); kheap s pd_ref = Some (ArchObj (PageDirectory pdo)); lookup_pt_slot pd_ref vptr s = ({(Inr (ptrFromPAddr x21 + ((vptr >> 12) && 0xFF << 2)), s)}, False); is_aligned pd_ref pd_bits; pdo (UCAST(32 \<rightarrow> 12) (vptr >> 20)) = PageTablePDE x21 x22 x23; x = ptrFromPAddr x21 + ((vptr >> 12) && 0xFF << 2); get_pt_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (ptrFromPAddr x21) vptr = None; (get_pt_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (ptrFromPAddr x21) vptr = None) = (get_pte (ptrFromPAddr x21 + ((vptr >> 12) && 0xFF << 2)) s = ({}, True))\<rbrakk> \<Longrightarrow> None = (case pte of InvalidPTE \<Rightarrow> None | LargePagePTE base attrs rights \<Rightarrow> Some (base, 16, attrs, rights) | SmallPagePTE base attrs rights \<Rightarrow> Some (base, 12, attrs, rights))
 2. \<And>pdo x21 x22 x23. \<lbrakk>is_aligned (ptrFromPAddr x21) pt_bits; get_pte (ptrFromPAddr x21 + ((vptr >> 12) && 0xFF << 2)) s = ({(pte, s)}, False); kheap s pd_ref = Some (ArchObj (PageDirectory pdo)); lookup_pt_slot pd_ref vptr s = ({(Inr (ptrFromPAddr x21 + ((vptr >> 12) && 0xFF << 2)), s)}, False); is_aligned pd_ref pd_bits; pdo (UCAST(32 \<rightarrow> 12) (vptr >> 20)) = PageTablePDE x21 x22 x23; x = ptrFromPAddr x21 + ((vptr >> 12) && 0xFF << 2)\<rbrakk> \<Longrightarrow> \<forall>x2. get_pt_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (ptrFromPAddr x21) vptr = Some x2 \<longrightarrow> (case x2 of InvalidPTE \<Rightarrow> None | LargePagePTE base attrs rights \<Rightarrow> Some (base, 16, attrs, rights) | SmallPagePTE base attrs rights \<Rightarrow> Some (base, 12, attrs, rights)) = (case pte of InvalidPTE \<Rightarrow> None | LargePagePTE base attrs rights \<Rightarrow> Some (base, 16, attrs, rights) | SmallPagePTE base attrs rights \<Rightarrow> Some (base, 12, attrs, rights)) proof (prove)
goal (1 subgoal):
 1. \<And>pdo x21 x22 x23. \<lbrakk>is_aligned (ptrFromPAddr x21) pt_bits; get_pte (ptrFromPAddr x21 + ((vptr >> 12) && 0xFF << 2)) s = ({(pte, s)}, False); kheap s pd_ref = Some (ArchObj (PageDirectory pdo)); lookup_pt_slot pd_ref vptr s = ({(Inr (ptrFromPAddr x21 + ((vptr >> 12) && 0xFF << 2)), s)}, False); is_aligned pd_ref pd_bits; pdo (UCAST(32 \<rightarrow> 12) (vptr >> 20)) = PageTablePDE x21 x22 x23; x = ptrFromPAddr x21 + ((vptr >> 12) && 0xFF << 2)\<rbrakk> \<Longrightarrow> \<forall>x2. get_pt_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (ptrFromPAddr x21) vptr = Some x2 \<longrightarrow> (case x2 of InvalidPTE \<Rightarrow> None | LargePagePTE base attrs rights \<Rightarrow> Some (base, 16, attrs, rights) | SmallPagePTE base attrs rights \<Rightarrow> Some (base, 12, attrs, rights)) = (case pte of InvalidPTE \<Rightarrow> None | LargePagePTE base attrs rights \<Rightarrow> Some (base, 16, attrs, rights) | SmallPagePTE base attrs rights \<Rightarrow> Some (base, 12, attrs, rights)) proof (prove)
goal (1 subgoal):
 1. \<And>pdo x21 x22 x23 x2. \<lbrakk>is_aligned (ptrFromPAddr x21) pt_bits; get_pte (ptrFromPAddr x21 + ((vptr >> 12) && 0xFF << 2)) s = ({(pte, s)}, False); kheap s pd_ref = Some (ArchObj (PageDirectory pdo)); lookup_pt_slot pd_ref vptr s = ({(Inr (ptrFromPAddr x21 + ((vptr >> 12) && 0xFF << 2)), s)}, False); is_aligned pd_ref pd_bits; pdo (UCAST(32 \<rightarrow> 12) (vptr >> 20)) = PageTablePDE x21 x22 x23; x = ptrFromPAddr x21 + ((vptr >> 12) && 0xFF << 2); get_pt_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (ptrFromPAddr x21) vptr = Some x2\<rbrakk> \<Longrightarrow> (case x2 of InvalidPTE \<Rightarrow> None | LargePagePTE base attrs rights \<Rightarrow> Some (base, 16, attrs, rights) | SmallPagePTE base attrs rights \<Rightarrow> Some (base, 12, attrs, rights)) = (case pte of InvalidPTE \<Rightarrow> None | LargePagePTE base attrs rights \<Rightarrow> Some (base, 16, attrs, rights) | SmallPagePTE base attrs rights \<Rightarrow> Some (base, 12, attrs, rights)) proof (prove)
goal (1 subgoal):
 1. \<And>pdo x21 x22 x23 x2. \<lbrakk>get_pte (ptrFromPAddr x21 + ((vptr >> 12) && 0xFF << 2)) s = ({(pte, s)}, False); kheap s pd_ref = Some (ArchObj (PageDirectory pdo)); lookup_pt_slot pd_ref vptr s = ({(Inr (ptrFromPAddr x21 + ((vptr >> 12) && 0xFF << 2)), s)}, False); is_aligned pd_ref pd_bits; pdo (UCAST(32 \<rightarrow> 12) (vptr >> 20)) = PageTablePDE x21 x22 x23; x = ptrFromPAddr x21 + ((vptr >> 12) && 0xFF << 2); get_pt_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (ptrFromPAddr x21) vptr = Some x2; (get_pt_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (ptrFromPAddr x21) vptr = Some x2) = (get_pte (ptrFromPAddr x21 + ((vptr >> 12) && mask 8 << 2)) s = ({(x2, s)}, False))\<rbrakk> \<Longrightarrow> (case x2 of InvalidPTE \<Rightarrow> None | LargePagePTE base attrs rights \<Rightarrow> Some (base, 16, attrs, rights) | SmallPagePTE base attrs rights \<Rightarrow> Some (base, 12, attrs, rights)) = (case pte of InvalidPTE \<Rightarrow> None | LargePagePTE base attrs rights \<Rightarrow> Some (base, 16, attrs, rights) | SmallPagePTE base attrs rights \<Rightarrow> Some (base, 12, attrs, rights)) proof (prove)
goal:
No subgoals!