theory ArchADT_AI

lemma lookup_pt_slot_no_fail:
  "is_aligned pd pd_bits \<Longrightarrow>
   kheap s pd = Some (ArchObj (PageDirectory pdo)) \<Longrightarrow>
   lookup_pt_slot pd vptr s =
   (case pdo (ucast (vptr >> 20)) of
      InvalidPDE \<Rightarrow>
        ({(Inl (ExceptionTypes_A.MissingCapability 20),s)},False)
    | PageTablePDE p _ _ \<Rightarrow>
        ({(Inr (ptrFromPAddr p + ((vptr >> 12) && 0xFF << 2)),s)},
         False)
    | SectionPDE _ _ _ _ \<Rightarrow>
        ({(Inl (ExceptionTypes_A.MissingCapability 20),s)},False)
    | SuperSectionPDE _ _ _ \<Rightarrow>
        ({(Inl (ExceptionTypes_A.MissingCapability 20),s)},False)  )" apply (frule pd_shifting'[of _ vptr]) apply (cut_tac shiftr_shiftl_mask_pd_bits[of vptr]) apply (subgoal_tac "vptr >> 20 << 2 >> 2 = vptr >> 20") defer apply (rule shiftl_shiftr_id) apply (simp_all add: word_bits_def) apply (cut_tac shiftr_less_t2n'[of vptr 20 30]) apply (simp add: word_bits_def) apply (simp add: mask_eq_iff) apply (cut_tac lt2p_lem[of 32 vptr]) apply (cut_tac word_bits_len_of, simp_all) by (clarsimp simp add: lookup_pt_slot_def lookup_pd_slot_def liftE_def bindE_def
        returnOk_def lift_def bind_def split_def throwError_def return_def
        get_pde_def get_pd_def Union_eq get_object_def simpler_gets_def
        assert_def fail_def mask_add_aligned
      split: sum.splits if_split_asm kernel_object.splits arch_kernel_obj.splits
             pde.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned pd pd_bits; kheap s pd = Some (ArchObj (PageDirectory pdo))\<rbrakk> \<Longrightarrow> lookup_pt_slot pd 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)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned pd pd_bits; kheap s pd = Some (ArchObj (PageDirectory pdo)); pd + (vptr >> 20 << 2) && ~~ mask pd_bits = pd\<rbrakk> \<Longrightarrow> lookup_pt_slot pd 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)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned pd pd_bits; kheap s pd = Some (ArchObj (PageDirectory pdo)); pd + (vptr >> 20 << 2) && ~~ mask pd_bits = pd; (vptr >> 20 << 2) && mask pd_bits = vptr >> 20 << 2\<rbrakk> \<Longrightarrow> lookup_pt_slot pd 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)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned pd pd_bits; kheap s pd = Some (ArchObj (PageDirectory pdo)); pd + (vptr >> 20 << 2) && ~~ mask pd_bits = pd; (vptr >> 20 << 2) && mask pd_bits = vptr >> 20 << 2; vptr >> 20 << 2 >> 2 = vptr >> 20\<rbrakk> \<Longrightarrow> lookup_pt_slot pd 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))
 2. \<lbrakk>is_aligned pd pd_bits; kheap s pd = Some (ArchObj (PageDirectory pdo)); pd + (vptr >> 20 << 2) && ~~ mask pd_bits = pd; (vptr >> 20 << 2) && mask pd_bits = vptr >> 20 << 2\<rbrakk> \<Longrightarrow> vptr >> 20 << 2 >> 2 = vptr >> 20 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned pd pd_bits; kheap s pd = Some (ArchObj (PageDirectory pdo)); pd + (vptr >> 20 << 2) && ~~ mask pd_bits = pd; (vptr >> 20 << 2) && mask pd_bits = vptr >> 20 << 2\<rbrakk> \<Longrightarrow> vptr >> 20 << 2 >> 2 = vptr >> 20
 2. \<lbrakk>is_aligned pd pd_bits; kheap s pd = Some (ArchObj (PageDirectory pdo)); pd + (vptr >> 20 << 2) && ~~ mask pd_bits = pd; (vptr >> 20 << 2) && mask pd_bits = vptr >> 20 << 2; vptr >> 20 << 2 >> 2 = vptr >> 20\<rbrakk> \<Longrightarrow> lookup_pt_slot pd 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)) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned pd pd_bits; kheap s pd = Some (ArchObj (PageDirectory pdo)); pd + (vptr >> 20 << 2) && ~~ mask pd_bits = pd; (vptr >> 20 << 2) && mask pd_bits = vptr >> 20 << 2\<rbrakk> \<Longrightarrow> 2 < LENGTH(32)
 2. \<lbrakk>is_aligned pd pd_bits; kheap s pd = Some (ArchObj (PageDirectory pdo)); pd + (vptr >> 20 << 2) && ~~ mask pd_bits = pd; (vptr >> 20 << 2) && mask pd_bits = vptr >> 20 << 2\<rbrakk> \<Longrightarrow> vptr >> 20 < 2 ^ (LENGTH(32) - 2)
 3. \<lbrakk>is_aligned pd pd_bits; kheap s pd = Some (ArchObj (PageDirectory pdo)); pd + (vptr >> 20 << 2) && ~~ mask pd_bits = pd; (vptr >> 20 << 2) && mask pd_bits = vptr >> 20 << 2; vptr >> 20 << 2 >> 2 = vptr >> 20\<rbrakk> \<Longrightarrow> lookup_pt_slot pd 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)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned pd pd_bits; kheap s pd = Some (ArchObj (PageDirectory pdo)); pd + (vptr >> 20 << 2) && ~~ mask pd_bits = pd; (vptr >> 20 << 2) && mask pd_bits = vptr >> 20 << 2\<rbrakk> \<Longrightarrow> vptr >> 20 < 0x40000000
 2. \<lbrakk>is_aligned pd pd_bits; kheap s pd = Some (ArchObj (PageDirectory pdo)); pd + (vptr >> 20 << 2) && ~~ mask pd_bits = pd; (vptr >> 20 << 2) && mask pd_bits = vptr >> 20 << 2; vptr >> 20 << 2 >> 2 = vptr >> 20\<rbrakk> \<Longrightarrow> lookup_pt_slot pd 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)) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>is_aligned pd pd_bits; kheap s pd = Some (ArchObj (PageDirectory pdo)); pd + (vptr >> 20 << 2) && ~~ mask pd_bits = pd; (vptr >> 20 << 2) && mask pd_bits = vptr >> 20 << 2; vptr >> 20 < 2 ^ 30\<rbrakk> \<Longrightarrow> vptr >> 20 < 0x40000000
 2. \<lbrakk>is_aligned pd pd_bits; kheap s pd = Some (ArchObj (PageDirectory pdo)); pd + (vptr >> 20 << 2) && ~~ mask pd_bits = pd; (vptr >> 20 << 2) && mask pd_bits = vptr >> 20 << 2\<rbrakk> \<Longrightarrow> vptr && mask (20 + 30) = vptr
 3. \<lbrakk>is_aligned pd pd_bits; kheap s pd = Some (ArchObj (PageDirectory pdo)); pd + (vptr >> 20 << 2) && ~~ mask pd_bits = pd; (vptr >> 20 << 2) && mask pd_bits = vptr >> 20 << 2\<rbrakk> \<Longrightarrow> 30 < LENGTH(32)
 4. \<lbrakk>is_aligned pd pd_bits; kheap s pd = Some (ArchObj (PageDirectory pdo)); pd + (vptr >> 20 << 2) && ~~ mask pd_bits = pd; (vptr >> 20 << 2) && mask pd_bits = vptr >> 20 << 2; vptr >> 20 << 2 >> 2 = vptr >> 20\<rbrakk> \<Longrightarrow> lookup_pt_slot pd 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)) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned pd pd_bits; kheap s pd = Some (ArchObj (PageDirectory pdo)); pd + (vptr >> 20 << 2) && ~~ mask pd_bits = pd; (vptr >> 20 << 2) && mask pd_bits = vptr >> 20 << 2\<rbrakk> \<Longrightarrow> vptr && mask (20 + 30) = vptr
 2. \<lbrakk>is_aligned pd pd_bits; kheap s pd = Some (ArchObj (PageDirectory pdo)); pd + (vptr >> 20 << 2) && ~~ mask pd_bits = pd; (vptr >> 20 << 2) && mask pd_bits = vptr >> 20 << 2\<rbrakk> \<Longrightarrow> 30 < LENGTH(32)
 3. \<lbrakk>is_aligned pd pd_bits; kheap s pd = Some (ArchObj (PageDirectory pdo)); pd + (vptr >> 20 << 2) && ~~ mask pd_bits = pd; (vptr >> 20 << 2) && mask pd_bits = vptr >> 20 << 2; vptr >> 20 << 2 >> 2 = vptr >> 20\<rbrakk> \<Longrightarrow> lookup_pt_slot pd 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)) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned pd pd_bits; kheap s pd = Some (ArchObj (PageDirectory pdo)); pd + (vptr >> 20 << 2) && ~~ mask pd_bits = pd; uint (vptr >> 20 << 2) < 2 ^ pd_bits\<rbrakk> \<Longrightarrow> uint vptr < 1125899906842624
 2. \<lbrakk>is_aligned pd pd_bits; kheap s pd = Some (ArchObj (PageDirectory pdo)); pd + (vptr >> 20 << 2) && ~~ mask pd_bits = pd; (vptr >> 20 << 2) && mask pd_bits = vptr >> 20 << 2\<rbrakk> \<Longrightarrow> 30 < LENGTH(32)
 3. \<lbrakk>is_aligned pd pd_bits; kheap s pd = Some (ArchObj (PageDirectory pdo)); pd + (vptr >> 20 << 2) && ~~ mask pd_bits = pd; (vptr >> 20 << 2) && mask pd_bits = vptr >> 20 << 2; vptr >> 20 << 2 >> 2 = vptr >> 20\<rbrakk> \<Longrightarrow> lookup_pt_slot pd 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)) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>is_aligned pd pd_bits; kheap s pd = Some (ArchObj (PageDirectory pdo)); pd + (vptr >> 20 << 2) && ~~ mask pd_bits = pd; uint (vptr >> 20 << 2) < 2 ^ pd_bits; uint vptr < 2 ^ 32\<rbrakk> \<Longrightarrow> uint vptr < 1125899906842624
 2. \<lbrakk>is_aligned pd pd_bits; kheap s pd = Some (ArchObj (PageDirectory pdo)); pd + (vptr >> 20 << 2) && ~~ mask pd_bits = pd; uint (vptr >> 20 << 2) < 2 ^ pd_bits\<rbrakk> \<Longrightarrow> LENGTH(32) \<le> 32
 3. \<lbrakk>is_aligned pd pd_bits; kheap s pd = Some (ArchObj (PageDirectory pdo)); pd + (vptr >> 20 << 2) && ~~ mask pd_bits = pd; (vptr >> 20 << 2) && mask pd_bits = vptr >> 20 << 2\<rbrakk> \<Longrightarrow> 30 < LENGTH(32)
 4. \<lbrakk>is_aligned pd pd_bits; kheap s pd = Some (ArchObj (PageDirectory pdo)); pd + (vptr >> 20 << 2) && ~~ mask pd_bits = pd; (vptr >> 20 << 2) && mask pd_bits = vptr >> 20 << 2; vptr >> 20 << 2 >> 2 = vptr >> 20\<rbrakk> \<Longrightarrow> lookup_pt_slot pd 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)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned pd pd_bits; kheap s pd = Some (ArchObj (PageDirectory pdo)); pd + (vptr >> 20 << 2) && ~~ mask pd_bits = pd; (vptr >> 20 << 2) && mask pd_bits = vptr >> 20 << 2; vptr >> 20 << 2 >> 2 = vptr >> 20\<rbrakk> \<Longrightarrow> lookup_pt_slot pd 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))