theory ArchADT_AI

lemma get_pd_entry_None_iff_get_pde_fail:
  "is_aligned pd_ref pd_bits \<Longrightarrow>
   get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) pd_ref vptr = None \<longleftrightarrow>
   get_pde (pd_ref + (vptr >> 20 << 2)) s = ({}, True)" apply (subgoal_tac "(vptr >> 20 << 2) && ~~ mask pd_bits = 0") apply (clarsimp simp add: get_pd_entry_def get_arch_obj_def
            split: option.splits Structures_A.kernel_object.splits
                   arch_kernel_obj.splits) apply (clarsimp simp add: get_pde_def get_pd_def bind_def return_def assert_def
  get_object_def simpler_gets_def fail_def split_def mask_out_sub_mask mask_eqs) apply (subgoal_tac "pd_ref + (vptr >> 20 << 2) -
                    (pd_ref + (vptr >> 20 << 2) && mask pd_bits) = pd_ref") apply (simp (no_asm_simp) add: fail_def return_def) apply clarsimp apply (simp add: mask_add_aligned pd_bits_def pageBits_def) apply (simp add: pd_bits_def pageBits_def) apply (simp add: and_not_mask) apply (simp add: shiftl_shiftr3 word_size shiftr_shiftr) apply (subgoal_tac "vptr >> 32 = 0", simp) apply (cut_tac shiftr_less_t2n'[of vptr 32 0], simp) apply (simp add: mask_eq_iff) apply (cut_tac lt2p_lem[of 32 vptr]) apply (cut_tac word_bits_len_of, simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned pd_ref pd_bits \<Longrightarrow> (get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) pd_ref vptr = None) = (get_pde (pd_ref + (vptr >> 20 << 2)) s = ({}, True)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned pd_ref pd_bits; (vptr >> 20 << 2) && ~~ mask pd_bits = 0\<rbrakk> \<Longrightarrow> (get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) pd_ref vptr = None) = (get_pde (pd_ref + (vptr >> 20 << 2)) s = ({}, True))
 2. is_aligned pd_ref pd_bits \<Longrightarrow> (vptr >> 20 << 2) && ~~ mask pd_bits = 0 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned pd_ref pd_bits; (vptr >> 20 << 2) && ~~ mask pd_bits = 0\<rbrakk> \<Longrightarrow> (kheap s pd_ref = None \<longrightarrow> get_pde (pd_ref + (vptr >> 20 << 2)) s = ({}, True)) \<and> (\<forall>x2. (\<forall>x11 x12. x2 = CNode x11 x12 \<longrightarrow> kheap s pd_ref = Some (CNode x11 x12) \<longrightarrow> get_pde (pd_ref + (vptr >> 20 << 2)) s = ({}, True)) \<and> (\<forall>x2a. x2 = TCB x2a \<longrightarrow> kheap s pd_ref = Some (TCB x2a) \<longrightarrow> get_pde (pd_ref + (vptr >> 20 << 2)) s = ({}, True)) \<and> (\<forall>x3. x2 = Endpoint x3 \<longrightarrow> kheap s pd_ref = Some (Endpoint x3) \<longrightarrow> get_pde (pd_ref + (vptr >> 20 << 2)) s = ({}, True)) \<and> (\<forall>x4. x2 = Notification x4 \<longrightarrow> kheap s pd_ref = Some (Notification x4) \<longrightarrow> get_pde (pd_ref + (vptr >> 20 << 2)) s = ({}, True)) \<and> (\<forall>x5. (\<forall>x1. x5 = ASIDPool x1 \<longrightarrow> x2 = ArchObj (ASIDPool x1) \<longrightarrow> kheap s pd_ref = Some (ArchObj (ASIDPool x1)) \<longrightarrow> get_pde (pd_ref + (vptr >> 20 << 2)) s = ({}, True)) \<and> (\<forall>x2a. x5 = PageTable x2a \<longrightarrow> x2 = ArchObj (PageTable x2a) \<longrightarrow> kheap s pd_ref = Some (ArchObj (PageTable x2a)) \<longrightarrow> get_pde (pd_ref + (vptr >> 20 << 2)) s = ({}, True)) \<and> (\<forall>x3. x5 = PageDirectory x3 \<longrightarrow> x2 = ArchObj (PageDirectory x3) \<longrightarrow> kheap s pd_ref = Some (ArchObj (PageDirectory x3)) \<longrightarrow> get_pde (pd_ref + (vptr >> 20 << 2)) s \<noteq> ({}, True)) \<and> (\<forall>x41 x42. x5 = DataPage x41 x42 \<longrightarrow> x2 = ArchObj (DataPage x41 x42) \<longrightarrow> kheap s pd_ref = Some (ArchObj (DataPage x41 x42)) \<longrightarrow> get_pde (pd_ref + (vptr >> 20 << 2)) s = ({}, True))))
 2. is_aligned pd_ref pd_bits \<Longrightarrow> (vptr >> 20 << 2) && ~~ mask pd_bits = 0 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned pd_ref pd_bits; vptr >> 20 << 2 = (vptr >> 20 << 2) && mask pd_bits\<rbrakk> \<Longrightarrow> ((\<exists>y. kheap s (pd_ref + (vptr >> 20 << 2) - (pd_ref + (vptr >> 20 << 2) && mask pd_bits)) = Some y) \<longrightarrow> (kheap s pd_ref = None \<longrightarrow> (\<forall>a b. (a, b) \<notin> fst ((case the (kheap s (pd_ref + (vptr >> 20 << 2) - (pd_ref + (vptr >> 20 << 2) && mask pd_bits))) of ArchObj (PageDirectory xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s)) \<and> snd ((case the (kheap s (pd_ref + (vptr >> 20 << 2) - (pd_ref + (vptr >> 20 << 2) && mask pd_bits))) of ArchObj (PageDirectory xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s)) \<and> (\<forall>x2. (\<forall>x11 x12. x2 = CNode x11 x12 \<longrightarrow> kheap s pd_ref = Some (CNode x11 x12) \<longrightarrow> (\<forall>a b. (a, b) \<notin> fst ((case the (kheap s (pd_ref + (vptr >> 20 << 2) - (pd_ref + (vptr >> 20 << 2) && mask pd_bits))) of ArchObj (PageDirectory xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s)) \<and> snd ((case the (kheap s (pd_ref + (vptr >> 20 << 2) - (pd_ref + (vptr >> 20 << 2) && mask pd_bits))) of ArchObj (PageDirectory xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s)) \<and> (\<forall>x2a. x2 = TCB x2a \<longrightarrow> kheap s pd_ref = Some (TCB x2a) \<longrightarrow> (\<forall>a b. (a, b) \<notin> fst ((case the (kheap s (pd_ref + (vptr >> 20 << 2) - (pd_ref + (vptr >> 20 << 2) && mask pd_bits))) of ArchObj (PageDirectory xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s)) \<and> snd ((case the (kheap s (pd_ref + (vptr >> 20 << 2) - (pd_ref + (vptr >> 20 << 2) && mask pd_bits))) of ArchObj (PageDirectory xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s)) \<and> (\<forall>x3. x2 = Endpoint x3 \<longrightarrow> kheap s pd_ref = Some (Endpoint x3) \<longrightarrow> (\<forall>a b. (a, b) \<notin> fst ((case the (kheap s (pd_ref + (vptr >> 20 << 2) - (pd_ref + (vptr >> 20 << 2) && mask pd_bits))) of ArchObj (PageDirectory xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s)) \<and> snd ((case the (kheap s (pd_ref + (vptr >> 20 << 2) - (pd_ref + (vptr >> 20 << 2) && mask pd_bits))) of ArchObj (PageDirectory xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s)) \<and> (\<forall>x4. x2 = Notification x4 \<longrightarrow> kheap s pd_ref = Some (Notification x4) \<longrightarrow> (\<forall>a b. (a, b) \<notin> fst ((case the (kheap s (pd_ref + (vptr >> 20 << 2) - (pd_ref + (vptr >> 20 << 2) && mask pd_bits))) of ArchObj (PageDirectory xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s)) \<and> snd ((case the (kheap s (pd_ref + (vptr >> 20 << 2) - (pd_ref + (vptr >> 20 << 2) && mask pd_bits))) of ArchObj (PageDirectory xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s)) \<and> (\<forall>x5. (\<forall>x1. x5 = ASIDPool x1 \<longrightarrow> x2 = ArchObj (ASIDPool x1) \<longrightarrow> kheap s pd_ref = Some (ArchObj (ASIDPool x1)) \<longrightarrow> (\<forall>a b. (a, b) \<notin> fst ((case the (kheap s (pd_ref + (vptr >> 20 << 2) - (pd_ref + (vptr >> 20 << 2) && mask pd_bits))) of ArchObj (PageDirectory xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s)) \<and> snd ((case the (kheap s (pd_ref + (vptr >> 20 << 2) - (pd_ref + (vptr >> 20 << 2) && mask pd_bits))) of ArchObj (PageDirectory xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s)) \<and> (\<forall>x2a. x5 = PageTable x2a \<longrightarrow> x2 = ArchObj (PageTable x2a) \<longrightarrow> kheap s pd_ref = Some (ArchObj (PageTable x2a)) \<longrightarrow> (\<forall>a b. (a, b) \<notin> fst ((case the (kheap s (pd_ref + (vptr >> 20 << 2) - (pd_ref + (vptr >> 20 << 2) && mask pd_bits))) of ArchObj (PageDirectory xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s)) \<and> snd ((case the (kheap s (pd_ref + (vptr >> 20 << 2) - (pd_ref + (vptr >> 20 << 2) && mask pd_bits))) of ArchObj (PageDirectory xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s)) \<and> (\<forall>x3. x5 = PageDirectory x3 \<longrightarrow> x2 = ArchObj (PageDirectory x3) \<longrightarrow> kheap s pd_ref = Some (ArchObj (PageDirectory x3)) \<longrightarrow> (\<exists>a b. (a, b) \<in> fst ((case the (kheap s (pd_ref + (vptr >> 20 << 2) - (pd_ref + (vptr >> 20 << 2) && mask pd_bits))) of ArchObj (PageDirectory xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s)) \<or> \<not> snd ((case the (kheap s (pd_ref + (vptr >> 20 << 2) - (pd_ref + (vptr >> 20 << 2) && mask pd_bits))) of ArchObj (PageDirectory xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s)) \<and> (\<forall>x41 x42. x5 = DataPage x41 x42 \<longrightarrow> x2 = ArchObj (DataPage x41 x42) \<longrightarrow> kheap s pd_ref = Some (ArchObj (DataPage x41 x42)) \<longrightarrow> (\<forall>a b. (a, b) \<notin> fst ((case the (kheap s (pd_ref + (vptr >> 20 << 2) - (pd_ref + (vptr >> 20 << 2) && mask pd_bits))) of ArchObj (PageDirectory xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s)) \<and> snd ((case the (kheap s (pd_ref + (vptr >> 20 << 2) - (pd_ref + (vptr >> 20 << 2) && mask pd_bits))) of ArchObj (PageDirectory xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s))))) \<and> (kheap s (pd_ref + (vptr >> 20 << 2) - (pd_ref + (vptr >> 20 << 2) && mask pd_bits)) = None \<longrightarrow> (\<forall>x3. kheap s pd_ref \<noteq> Some (ArchObj (PageDirectory x3))))
 2. is_aligned pd_ref pd_bits \<Longrightarrow> (vptr >> 20 << 2) && ~~ mask pd_bits = 0 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned pd_ref pd_bits; vptr >> 20 << 2 = (vptr >> 20 << 2) && mask pd_bits; pd_ref + (vptr >> 20 << 2) - (pd_ref + (vptr >> 20 << 2) && mask pd_bits) = pd_ref\<rbrakk> \<Longrightarrow> ((\<exists>y. kheap s (pd_ref + (vptr >> 20 << 2) - (pd_ref + (vptr >> 20 << 2) && mask pd_bits)) = Some y) \<longrightarrow> (kheap s pd_ref = None \<longrightarrow> (\<forall>a b. (a, b) \<notin> fst ((case the (kheap s (pd_ref + (vptr >> 20 << 2) - (pd_ref + (vptr >> 20 << 2) && mask pd_bits))) of ArchObj (PageDirectory xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s)) \<and> snd ((case the (kheap s (pd_ref + (vptr >> 20 << 2) - (pd_ref + (vptr >> 20 << 2) && mask pd_bits))) of ArchObj (PageDirectory xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s)) \<and> (\<forall>x2. (\<forall>x11 x12. x2 = CNode x11 x12 \<longrightarrow> kheap s pd_ref = Some (CNode x11 x12) \<longrightarrow> (\<forall>a b. (a, b) \<notin> fst ((case the (kheap s (pd_ref + (vptr >> 20 << 2) - (pd_ref + (vptr >> 20 << 2) && mask pd_bits))) of ArchObj (PageDirectory xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s)) \<and> snd ((case the (kheap s (pd_ref + (vptr >> 20 << 2) - (pd_ref + (vptr >> 20 << 2) && mask pd_bits))) of ArchObj (PageDirectory xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s)) \<and> (\<forall>x2a. x2 = TCB x2a \<longrightarrow> kheap s pd_ref = Some (TCB x2a) \<longrightarrow> (\<forall>a b. (a, b) \<notin> fst ((case the (kheap s (pd_ref + (vptr >> 20 << 2) - (pd_ref + (vptr >> 20 << 2) && mask pd_bits))) of ArchObj (PageDirectory xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s)) \<and> snd ((case the (kheap s (pd_ref + (vptr >> 20 << 2) - (pd_ref + (vptr >> 20 << 2) && mask pd_bits))) of ArchObj (PageDirectory xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s)) \<and> (\<forall>x3. x2 = Endpoint x3 \<longrightarrow> kheap s pd_ref = Some (Endpoint x3) \<longrightarrow> (\<forall>a b. (a, b) \<notin> fst ((case the (kheap s (pd_ref + (vptr >> 20 << 2) - (pd_ref + (vptr >> 20 << 2) && mask pd_bits))) of ArchObj (PageDirectory xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s)) \<and> snd ((case the (kheap s (pd_ref + (vptr >> 20 << 2) - (pd_ref + (vptr >> 20 << 2) && mask pd_bits))) of ArchObj (PageDirectory xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s)) \<and> (\<forall>x4. x2 = Notification x4 \<longrightarrow> kheap s pd_ref = Some (Notification x4) \<longrightarrow> (\<forall>a b. (a, b) \<notin> fst ((case the (kheap s (pd_ref + (vptr >> 20 << 2) - (pd_ref + (vptr >> 20 << 2) && mask pd_bits))) of ArchObj (PageDirectory xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s)) \<and> snd ((case the (kheap s (pd_ref + (vptr >> 20 << 2) - (pd_ref + (vptr >> 20 << 2) && mask pd_bits))) of ArchObj (PageDirectory xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s)) \<and> (\<forall>x5. (\<forall>x1. x5 = ASIDPool x1 \<longrightarrow> x2 = ArchObj (ASIDPool x1) \<longrightarrow> kheap s pd_ref = Some (ArchObj (ASIDPool x1)) \<longrightarrow> (\<forall>a b. (a, b) \<notin> fst ((case the (kheap s (pd_ref + (vptr >> 20 << 2) - (pd_ref + (vptr >> 20 << 2) && mask pd_bits))) of ArchObj (PageDirectory xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s)) \<and> snd ((case the (kheap s (pd_ref + (vptr >> 20 << 2) - (pd_ref + (vptr >> 20 << 2) && mask pd_bits))) of ArchObj (PageDirectory xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s)) \<and> (\<forall>x2a. x5 = PageTable x2a \<longrightarrow> x2 = ArchObj (PageTable x2a) \<longrightarrow> kheap s pd_ref = Some (ArchObj (PageTable x2a)) \<longrightarrow> (\<forall>a b. (a, b) \<notin> fst ((case the (kheap s (pd_ref + (vptr >> 20 << 2) - (pd_ref + (vptr >> 20 << 2) && mask pd_bits))) of ArchObj (PageDirectory xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s)) \<and> snd ((case the (kheap s (pd_ref + (vptr >> 20 << 2) - (pd_ref + (vptr >> 20 << 2) && mask pd_bits))) of ArchObj (PageDirectory xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s)) \<and> (\<forall>x3. x5 = PageDirectory x3 \<longrightarrow> x2 = ArchObj (PageDirectory x3) \<longrightarrow> kheap s pd_ref = Some (ArchObj (PageDirectory x3)) \<longrightarrow> (\<exists>a b. (a, b) \<in> fst ((case the (kheap s (pd_ref + (vptr >> 20 << 2) - (pd_ref + (vptr >> 20 << 2) && mask pd_bits))) of ArchObj (PageDirectory xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s)) \<or> \<not> snd ((case the (kheap s (pd_ref + (vptr >> 20 << 2) - (pd_ref + (vptr >> 20 << 2) && mask pd_bits))) of ArchObj (PageDirectory xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s)) \<and> (\<forall>x41 x42. x5 = DataPage x41 x42 \<longrightarrow> x2 = ArchObj (DataPage x41 x42) \<longrightarrow> kheap s pd_ref = Some (ArchObj (DataPage x41 x42)) \<longrightarrow> (\<forall>a b. (a, b) \<notin> fst ((case the (kheap s (pd_ref + (vptr >> 20 << 2) - (pd_ref + (vptr >> 20 << 2) && mask pd_bits))) of ArchObj (PageDirectory xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s)) \<and> snd ((case the (kheap s (pd_ref + (vptr >> 20 << 2) - (pd_ref + (vptr >> 20 << 2) && mask pd_bits))) of ArchObj (PageDirectory xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s))))) \<and> (kheap s (pd_ref + (vptr >> 20 << 2) - (pd_ref + (vptr >> 20 << 2) && mask pd_bits)) = None \<longrightarrow> (\<forall>x3. kheap s pd_ref \<noteq> Some (ArchObj (PageDirectory x3))))
 2. \<lbrakk>is_aligned pd_ref pd_bits; vptr >> 20 << 2 = (vptr >> 20 << 2) && mask pd_bits\<rbrakk> \<Longrightarrow> pd_ref + (vptr >> 20 << 2) - (pd_ref + (vptr >> 20 << 2) && mask pd_bits) = pd_ref
 3. is_aligned pd_ref pd_bits \<Longrightarrow> (vptr >> 20 << 2) && ~~ mask pd_bits = 0 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned pd_ref pd_bits; vptr >> 20 << 2 = (vptr >> 20 << 2) && mask pd_bits; pd_ref + (vptr >> 20 << 2) - (pd_ref + (vptr >> 20 << 2) && mask pd_bits) = pd_ref\<rbrakk> \<Longrightarrow> (\<exists>y. kheap s pd_ref = Some y) \<longrightarrow> kheap s pd_ref = None \<longrightarrow> (\<forall>a b. (a, b) \<notin> fst ((case the None of ArchObj (PageDirectory xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s)) \<and> snd ((case the None of ArchObj (PageDirectory xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s)
 2. \<lbrakk>is_aligned pd_ref pd_bits; vptr >> 20 << 2 = (vptr >> 20 << 2) && mask pd_bits\<rbrakk> \<Longrightarrow> pd_ref + (vptr >> 20 << 2) - (pd_ref + (vptr >> 20 << 2) && mask pd_bits) = pd_ref
 3. is_aligned pd_ref pd_bits \<Longrightarrow> (vptr >> 20 << 2) && ~~ mask pd_bits = 0 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned pd_ref pd_bits; vptr >> 20 << 2 = (vptr >> 20 << 2) && mask pd_bits\<rbrakk> \<Longrightarrow> pd_ref + (vptr >> 20 << 2) - (pd_ref + (vptr >> 20 << 2) && mask pd_bits) = pd_ref
 2. is_aligned pd_ref pd_bits \<Longrightarrow> (vptr >> 20 << 2) && ~~ mask pd_bits = 0 proof (prove)
goal (1 subgoal):
 1. is_aligned pd_ref pd_bits \<Longrightarrow> (vptr >> 20 << 2) && ~~ mask pd_bits = 0 proof (prove)
goal (1 subgoal):
 1. is_aligned pd_ref 14 \<Longrightarrow> (vptr >> 20 << 2) && ~~ mask 14 = 0 proof (prove)
goal (1 subgoal):
 1. is_aligned pd_ref 14 \<Longrightarrow> vptr >> 20 << 2 >> 14 << 14 = 0 proof (prove)
goal (1 subgoal):
 1. is_aligned pd_ref 14 \<Longrightarrow> (vptr >> 32) && mask 18 << 14 = 0 proof (prove)
goal (1 subgoal):
 1. is_aligned pd_ref 14 \<Longrightarrow> vptr >> 32 = 0 proof (prove)
goal (2 subgoals):
 1. is_aligned pd_ref 14 \<Longrightarrow> vptr && mask (32 + 0) = vptr
 2. is_aligned pd_ref 14 \<Longrightarrow> 0 < LENGTH(32) proof (prove)
goal (1 subgoal):
 1. is_aligned pd_ref 14 \<Longrightarrow> 0 < LENGTH(32) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned pd_ref 14; uint vptr < 2 ^ 32\<rbrakk> \<Longrightarrow> 0 < LENGTH(32)
 2. is_aligned pd_ref 14 \<Longrightarrow> LENGTH(32) \<le> 32 proof (prove)
goal:
No subgoals!