theory ArchADT_AI

lemma get_pt_entry_None_iff_get_pte_fail:
  "is_aligned pt_ref pt_bits \<Longrightarrow>
   get_pt_entry (\<lambda>obj. get_arch_obj (kheap s obj)) pt_ref vptr = None \<longleftrightarrow>
   get_pte (pt_ref + ((vptr >> 12) && 0xFF << 2)) s = ({}, True)" apply (clarsimp simp: get_pt_entry_def get_arch_obj_def
                  split: option.splits Structures_A.kernel_object.splits
                         arch_kernel_obj.splits) apply (clarsimp simp: get_pte_def get_pt_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 "pt_ref + ((vptr >> 12) && 0xFF << 2) -
                      (pt_ref + ((vptr >> 12) && 0xFF << 2) && mask pt_bits) =
                      pt_ref") apply (simp (no_asm_simp) add: fail_def return_def) apply clarsimp apply (simp add: mask_add_aligned pt_bits_def pageBits_def) apply (cut_tac and_mask_shiftl_comm[of 8 2 "vptr >> 12"]) apply (simp_all add: word_size mask_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned pt_ref pt_bits \<Longrightarrow> (get_pt_entry (\<lambda>obj. get_arch_obj (kheap s obj)) pt_ref vptr = None) = (get_pte (pt_ref + ((vptr >> 12) && 0xFF << 2)) s = ({}, True)) proof (prove)
goal (1 subgoal):
 1. is_aligned pt_ref pt_bits \<Longrightarrow> (kheap s pt_ref = None \<longrightarrow> get_pte (pt_ref + ((vptr >> 12) && 0xFF << 2)) s = ({}, True)) \<and> (\<forall>x2. (\<forall>x11 x12. x2 = CNode x11 x12 \<longrightarrow> kheap s pt_ref = Some (CNode x11 x12) \<longrightarrow> get_pte (pt_ref + ((vptr >> 12) && 0xFF << 2)) s = ({}, True)) \<and> (\<forall>x2a. x2 = TCB x2a \<longrightarrow> kheap s pt_ref = Some (TCB x2a) \<longrightarrow> get_pte (pt_ref + ((vptr >> 12) && 0xFF << 2)) s = ({}, True)) \<and> (\<forall>x3. x2 = Endpoint x3 \<longrightarrow> kheap s pt_ref = Some (Endpoint x3) \<longrightarrow> get_pte (pt_ref + ((vptr >> 12) && 0xFF << 2)) s = ({}, True)) \<and> (\<forall>x4. x2 = Notification x4 \<longrightarrow> kheap s pt_ref = Some (Notification x4) \<longrightarrow> get_pte (pt_ref + ((vptr >> 12) && 0xFF << 2)) s = ({}, True)) \<and> (\<forall>x5. (\<forall>x1. x5 = ASIDPool x1 \<longrightarrow> x2 = ArchObj (ASIDPool x1) \<longrightarrow> kheap s pt_ref = Some (ArchObj (ASIDPool x1)) \<longrightarrow> get_pte (pt_ref + ((vptr >> 12) && 0xFF << 2)) s = ({}, True)) \<and> (\<forall>x2a. x5 = PageTable x2a \<longrightarrow> x2 = ArchObj (PageTable x2a) \<longrightarrow> kheap s pt_ref = Some (ArchObj (PageTable x2a)) \<longrightarrow> get_pte (pt_ref + ((vptr >> 12) && 0xFF << 2)) s \<noteq> ({}, True)) \<and> (\<forall>x3. x5 = PageDirectory x3 \<longrightarrow> x2 = ArchObj (PageDirectory x3) \<longrightarrow> kheap s pt_ref = Some (ArchObj (PageDirectory x3)) \<longrightarrow> get_pte (pt_ref + ((vptr >> 12) && 0xFF << 2)) s = ({}, True)) \<and> (\<forall>x41 x42. x5 = DataPage x41 x42 \<longrightarrow> x2 = ArchObj (DataPage x41 x42) \<longrightarrow> kheap s pt_ref = Some (ArchObj (DataPage x41 x42)) \<longrightarrow> get_pte (pt_ref + ((vptr >> 12) && 0xFF << 2)) s = ({}, True)))) proof (prove)
goal (1 subgoal):
 1. is_aligned pt_ref pt_bits \<Longrightarrow> ((\<exists>y. kheap s (pt_ref + ((vptr >> 12) && 0xFF << 2) - (pt_ref + ((vptr >> 12) && 0xFF << 2) && mask pt_bits)) = Some y) \<longrightarrow> (kheap s pt_ref = None \<longrightarrow> (\<forall>a b. (a, b) \<notin> fst ((case the (kheap s (pt_ref + ((vptr >> 12) && 0xFF << 2) - (pt_ref + ((vptr >> 12) && 0xFF << 2) && mask pt_bits))) of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s)) \<and> snd ((case the (kheap s (pt_ref + ((vptr >> 12) && 0xFF << 2) - (pt_ref + ((vptr >> 12) && 0xFF << 2) && mask pt_bits))) of ArchObj (PageTable 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 pt_ref = Some (CNode x11 x12) \<longrightarrow> (\<forall>a b. (a, b) \<notin> fst ((case the (kheap s (pt_ref + ((vptr >> 12) && 0xFF << 2) - (pt_ref + ((vptr >> 12) && 0xFF << 2) && mask pt_bits))) of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s)) \<and> snd ((case the (kheap s (pt_ref + ((vptr >> 12) && 0xFF << 2) - (pt_ref + ((vptr >> 12) && 0xFF << 2) && mask pt_bits))) of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s)) \<and> (\<forall>x2a. x2 = TCB x2a \<longrightarrow> kheap s pt_ref = Some (TCB x2a) \<longrightarrow> (\<forall>a b. (a, b) \<notin> fst ((case the (kheap s (pt_ref + ((vptr >> 12) && 0xFF << 2) - (pt_ref + ((vptr >> 12) && 0xFF << 2) && mask pt_bits))) of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s)) \<and> snd ((case the (kheap s (pt_ref + ((vptr >> 12) && 0xFF << 2) - (pt_ref + ((vptr >> 12) && 0xFF << 2) && mask pt_bits))) of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s)) \<and> (\<forall>x3. x2 = Endpoint x3 \<longrightarrow> kheap s pt_ref = Some (Endpoint x3) \<longrightarrow> (\<forall>a b. (a, b) \<notin> fst ((case the (kheap s (pt_ref + ((vptr >> 12) && 0xFF << 2) - (pt_ref + ((vptr >> 12) && 0xFF << 2) && mask pt_bits))) of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s)) \<and> snd ((case the (kheap s (pt_ref + ((vptr >> 12) && 0xFF << 2) - (pt_ref + ((vptr >> 12) && 0xFF << 2) && mask pt_bits))) of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s)) \<and> (\<forall>x4. x2 = Notification x4 \<longrightarrow> kheap s pt_ref = Some (Notification x4) \<longrightarrow> (\<forall>a b. (a, b) \<notin> fst ((case the (kheap s (pt_ref + ((vptr >> 12) && 0xFF << 2) - (pt_ref + ((vptr >> 12) && 0xFF << 2) && mask pt_bits))) of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s)) \<and> snd ((case the (kheap s (pt_ref + ((vptr >> 12) && 0xFF << 2) - (pt_ref + ((vptr >> 12) && 0xFF << 2) && mask pt_bits))) of ArchObj (PageTable 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 pt_ref = Some (ArchObj (ASIDPool x1)) \<longrightarrow> (\<forall>a b. (a, b) \<notin> fst ((case the (kheap s (pt_ref + ((vptr >> 12) && 0xFF << 2) - (pt_ref + ((vptr >> 12) && 0xFF << 2) && mask pt_bits))) of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s)) \<and> snd ((case the (kheap s (pt_ref + ((vptr >> 12) && 0xFF << 2) - (pt_ref + ((vptr >> 12) && 0xFF << 2) && mask pt_bits))) of ArchObj (PageTable 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 pt_ref = Some (ArchObj (PageTable x2a)) \<longrightarrow> (\<exists>a b. (a, b) \<in> fst ((case the (kheap s (pt_ref + ((vptr >> 12) && 0xFF << 2) - (pt_ref + ((vptr >> 12) && 0xFF << 2) && mask pt_bits))) of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s)) \<or> \<not> snd ((case the (kheap s (pt_ref + ((vptr >> 12) && 0xFF << 2) - (pt_ref + ((vptr >> 12) && 0xFF << 2) && mask pt_bits))) of ArchObj (PageTable 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 pt_ref = Some (ArchObj (PageDirectory x3)) \<longrightarrow> (\<forall>a b. (a, b) \<notin> fst ((case the (kheap s (pt_ref + ((vptr >> 12) && 0xFF << 2) - (pt_ref + ((vptr >> 12) && 0xFF << 2) && mask pt_bits))) of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s)) \<and> snd ((case the (kheap s (pt_ref + ((vptr >> 12) && 0xFF << 2) - (pt_ref + ((vptr >> 12) && 0xFF << 2) && mask pt_bits))) of ArchObj (PageTable 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 pt_ref = Some (ArchObj (DataPage x41 x42)) \<longrightarrow> (\<forall>a b. (a, b) \<notin> fst ((case the (kheap s (pt_ref + ((vptr >> 12) && 0xFF << 2) - (pt_ref + ((vptr >> 12) && 0xFF << 2) && mask pt_bits))) of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s)) \<and> snd ((case the (kheap s (pt_ref + ((vptr >> 12) && 0xFF << 2) - (pt_ref + ((vptr >> 12) && 0xFF << 2) && mask pt_bits))) of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s))))) \<and> (kheap s (pt_ref + ((vptr >> 12) && 0xFF << 2) - (pt_ref + ((vptr >> 12) && 0xFF << 2) && mask pt_bits)) = None \<longrightarrow> (\<forall>x2. kheap s pt_ref \<noteq> Some (ArchObj (PageTable x2)))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned pt_ref pt_bits; pt_ref + ((vptr >> 12) && 0xFF << 2) - (pt_ref + ((vptr >> 12) && 0xFF << 2) && mask pt_bits) = pt_ref\<rbrakk> \<Longrightarrow> ((\<exists>y. kheap s (pt_ref + ((vptr >> 12) && 0xFF << 2) - (pt_ref + ((vptr >> 12) && 0xFF << 2) && mask pt_bits)) = Some y) \<longrightarrow> (kheap s pt_ref = None \<longrightarrow> (\<forall>a b. (a, b) \<notin> fst ((case the (kheap s (pt_ref + ((vptr >> 12) && 0xFF << 2) - (pt_ref + ((vptr >> 12) && 0xFF << 2) && mask pt_bits))) of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s)) \<and> snd ((case the (kheap s (pt_ref + ((vptr >> 12) && 0xFF << 2) - (pt_ref + ((vptr >> 12) && 0xFF << 2) && mask pt_bits))) of ArchObj (PageTable 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 pt_ref = Some (CNode x11 x12) \<longrightarrow> (\<forall>a b. (a, b) \<notin> fst ((case the (kheap s (pt_ref + ((vptr >> 12) && 0xFF << 2) - (pt_ref + ((vptr >> 12) && 0xFF << 2) && mask pt_bits))) of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s)) \<and> snd ((case the (kheap s (pt_ref + ((vptr >> 12) && 0xFF << 2) - (pt_ref + ((vptr >> 12) && 0xFF << 2) && mask pt_bits))) of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s)) \<and> (\<forall>x2a. x2 = TCB x2a \<longrightarrow> kheap s pt_ref = Some (TCB x2a) \<longrightarrow> (\<forall>a b. (a, b) \<notin> fst ((case the (kheap s (pt_ref + ((vptr >> 12) && 0xFF << 2) - (pt_ref + ((vptr >> 12) && 0xFF << 2) && mask pt_bits))) of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s)) \<and> snd ((case the (kheap s (pt_ref + ((vptr >> 12) && 0xFF << 2) - (pt_ref + ((vptr >> 12) && 0xFF << 2) && mask pt_bits))) of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s)) \<and> (\<forall>x3. x2 = Endpoint x3 \<longrightarrow> kheap s pt_ref = Some (Endpoint x3) \<longrightarrow> (\<forall>a b. (a, b) \<notin> fst ((case the (kheap s (pt_ref + ((vptr >> 12) && 0xFF << 2) - (pt_ref + ((vptr >> 12) && 0xFF << 2) && mask pt_bits))) of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s)) \<and> snd ((case the (kheap s (pt_ref + ((vptr >> 12) && 0xFF << 2) - (pt_ref + ((vptr >> 12) && 0xFF << 2) && mask pt_bits))) of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s)) \<and> (\<forall>x4. x2 = Notification x4 \<longrightarrow> kheap s pt_ref = Some (Notification x4) \<longrightarrow> (\<forall>a b. (a, b) \<notin> fst ((case the (kheap s (pt_ref + ((vptr >> 12) && 0xFF << 2) - (pt_ref + ((vptr >> 12) && 0xFF << 2) && mask pt_bits))) of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s)) \<and> snd ((case the (kheap s (pt_ref + ((vptr >> 12) && 0xFF << 2) - (pt_ref + ((vptr >> 12) && 0xFF << 2) && mask pt_bits))) of ArchObj (PageTable 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 pt_ref = Some (ArchObj (ASIDPool x1)) \<longrightarrow> (\<forall>a b. (a, b) \<notin> fst ((case the (kheap s (pt_ref + ((vptr >> 12) && 0xFF << 2) - (pt_ref + ((vptr >> 12) && 0xFF << 2) && mask pt_bits))) of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s)) \<and> snd ((case the (kheap s (pt_ref + ((vptr >> 12) && 0xFF << 2) - (pt_ref + ((vptr >> 12) && 0xFF << 2) && mask pt_bits))) of ArchObj (PageTable 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 pt_ref = Some (ArchObj (PageTable x2a)) \<longrightarrow> (\<exists>a b. (a, b) \<in> fst ((case the (kheap s (pt_ref + ((vptr >> 12) && 0xFF << 2) - (pt_ref + ((vptr >> 12) && 0xFF << 2) && mask pt_bits))) of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s)) \<or> \<not> snd ((case the (kheap s (pt_ref + ((vptr >> 12) && 0xFF << 2) - (pt_ref + ((vptr >> 12) && 0xFF << 2) && mask pt_bits))) of ArchObj (PageTable 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 pt_ref = Some (ArchObj (PageDirectory x3)) \<longrightarrow> (\<forall>a b. (a, b) \<notin> fst ((case the (kheap s (pt_ref + ((vptr >> 12) && 0xFF << 2) - (pt_ref + ((vptr >> 12) && 0xFF << 2) && mask pt_bits))) of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s)) \<and> snd ((case the (kheap s (pt_ref + ((vptr >> 12) && 0xFF << 2) - (pt_ref + ((vptr >> 12) && 0xFF << 2) && mask pt_bits))) of ArchObj (PageTable 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 pt_ref = Some (ArchObj (DataPage x41 x42)) \<longrightarrow> (\<forall>a b. (a, b) \<notin> fst ((case the (kheap s (pt_ref + ((vptr >> 12) && 0xFF << 2) - (pt_ref + ((vptr >> 12) && 0xFF << 2) && mask pt_bits))) of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s)) \<and> snd ((case the (kheap s (pt_ref + ((vptr >> 12) && 0xFF << 2) - (pt_ref + ((vptr >> 12) && 0xFF << 2) && mask pt_bits))) of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s))))) \<and> (kheap s (pt_ref + ((vptr >> 12) && 0xFF << 2) - (pt_ref + ((vptr >> 12) && 0xFF << 2) && mask pt_bits)) = None \<longrightarrow> (\<forall>x2. kheap s pt_ref \<noteq> Some (ArchObj (PageTable x2))))
 2. is_aligned pt_ref pt_bits \<Longrightarrow> pt_ref + ((vptr >> 12) && 0xFF << 2) - (pt_ref + ((vptr >> 12) && 0xFF << 2) && mask pt_bits) = pt_ref proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned pt_ref pt_bits; pt_ref + ((vptr >> 12) && 0xFF << 2) - (pt_ref + ((vptr >> 12) && 0xFF << 2) && mask pt_bits) = pt_ref\<rbrakk> \<Longrightarrow> (\<exists>y. kheap s pt_ref = Some y) \<longrightarrow> kheap s pt_ref = None \<longrightarrow> (\<forall>a b. (a, b) \<notin> fst ((case the None of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s)) \<and> snd ((case the None of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s)
 2. is_aligned pt_ref pt_bits \<Longrightarrow> pt_ref + ((vptr >> 12) && 0xFF << 2) - (pt_ref + ((vptr >> 12) && 0xFF << 2) && mask pt_bits) = pt_ref proof (prove)
goal (1 subgoal):
 1. is_aligned pt_ref pt_bits \<Longrightarrow> pt_ref + ((vptr >> 12) && 0xFF << 2) - (pt_ref + ((vptr >> 12) && 0xFF << 2) && mask pt_bits) = pt_ref proof (prove)
goal (1 subgoal):
 1. is_aligned pt_ref 10 \<Longrightarrow> (vptr >> 12) && 0xFF << 2 = ((vptr >> 12) && 0xFF << 2) && mask 10 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned pt_ref 10; (vptr >> 12) && mask 8 << 2 = (vptr >> 12 << 2) && mask (8 + 2)\<rbrakk> \<Longrightarrow> (vptr >> 12) && 0xFF << 2 = ((vptr >> 12) && 0xFF << 2) && mask 10
 2. is_aligned pt_ref 10 \<Longrightarrow> 8 + 2 \<le> size (vptr >> 12) proof (prove)
goal:
No subgoals!