theory ArchADT_AI

lemma get_pt_entry_Some_eq_get_pte:
  "is_aligned pt_ref pt_bits \<Longrightarrow>
   get_pt_entry (\<lambda>obj. get_arch_obj (kheap s obj)) pt_ref vptr = Some x \<longleftrightarrow>
   get_pte (pt_ref + ((vptr >> 12) && mask 8 << 2)) s = ({(x,s)}, False)" apply (clarsimp simp add: 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) && mask 8 << 2) -
                      (pt_ref + ((vptr >> 12) && mask 8 << 2) && mask pt_bits) =
                      pt_ref") apply (simp (no_asm_simp) add: fail_def return_def) apply (clarsimp simp: mask_add_aligned pt_bits_def pageBits_def
                         word_size and_mask_shiftr_comm and_mask_shiftl_comm shiftr_shiftr) apply (cut_tac shiftl_shiftr_id[of 2 "vptr >> 12"]) apply (simp add: word_bits_def)+ apply (cut_tac shiftr_less_t2n'[of vptr 12 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+) apply (simp add: mask_add_aligned pt_bits_def pageBits_def word_size and_mask_shiftl_comm) 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 = Some x) = (get_pte (pt_ref + ((vptr >> 12) && mask 8 << 2)) s = ({(x, s)}, False)) 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) && mask 8 << 2)) s \<noteq> ({(x, s)}, False)) \<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) && mask 8 << 2)) s \<noteq> ({(x, s)}, False)) \<and> (\<forall>x2a. x2 = TCB x2a \<longrightarrow> kheap s pt_ref = Some (TCB x2a) \<longrightarrow> get_pte (pt_ref + ((vptr >> 12) && mask 8 << 2)) s \<noteq> ({(x, s)}, False)) \<and> (\<forall>x3. x2 = Endpoint x3 \<longrightarrow> kheap s pt_ref = Some (Endpoint x3) \<longrightarrow> get_pte (pt_ref + ((vptr >> 12) && mask 8 << 2)) s \<noteq> ({(x, s)}, False)) \<and> (\<forall>x4. x2 = Notification x4 \<longrightarrow> kheap s pt_ref = Some (Notification x4) \<longrightarrow> get_pte (pt_ref + ((vptr >> 12) && mask 8 << 2)) s \<noteq> ({(x, s)}, False)) \<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) && mask 8 << 2)) s \<noteq> ({(x, s)}, False)) \<and> (\<forall>x2a. x5 = PageTable x2a \<longrightarrow> x2 = ArchObj (PageTable x2a) \<longrightarrow> kheap s pt_ref = Some (ArchObj (PageTable x2a)) \<longrightarrow> (x2a (UCAST(32 \<rightarrow> 8) ((vptr >> 12) && mask 8)) = x) = (get_pte (pt_ref + ((vptr >> 12) && mask 8 << 2)) s = ({(x, s)}, False))) \<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) && mask 8 << 2)) s \<noteq> ({(x, s)}, False)) \<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) && mask 8 << 2)) s \<noteq> ({(x, s)}, False)))) proof (prove)
goal (1 subgoal):
 1. is_aligned pt_ref pt_bits \<Longrightarrow> ((\<exists>y. kheap s (pt_ref + ((vptr >> 12) && mask 8 << 2) - (pt_ref + ((vptr >> 12) && mask 8 << 2) && mask pt_bits)) = Some y) \<longrightarrow> (kheap s pt_ref = None \<longrightarrow> (\<Union>x\<in>fst ((case the (kheap s (pt_ref + ((vptr >> 12) && mask 8 << 2) - (pt_ref + ((vptr >> 12) && mask 8 << 2) && mask pt_bits))) of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s). {(fst x (UCAST(32 \<rightarrow> 8) (pt_ref + ((vptr >> 12) && mask 8 << 2) && mask pt_bits >> 2)), snd x)}) = {(x, s)} \<longrightarrow> snd ((case the (kheap s (pt_ref + ((vptr >> 12) && mask 8 << 2) - (pt_ref + ((vptr >> 12) && mask 8 << 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> (\<Union>x\<in>fst ((case the (kheap s (pt_ref + ((vptr >> 12) && mask 8 << 2) - (pt_ref + ((vptr >> 12) && mask 8 << 2) && mask pt_bits))) of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s). {(fst x (UCAST(32 \<rightarrow> 8) (pt_ref + ((vptr >> 12) && mask 8 << 2) && mask pt_bits >> 2)), snd x)}) = {(x, s)} \<longrightarrow> snd ((case the (kheap s (pt_ref + ((vptr >> 12) && mask 8 << 2) - (pt_ref + ((vptr >> 12) && mask 8 << 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> (\<Union>x\<in>fst ((case the (kheap s (pt_ref + ((vptr >> 12) && mask 8 << 2) - (pt_ref + ((vptr >> 12) && mask 8 << 2) && mask pt_bits))) of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s). {(fst x (UCAST(32 \<rightarrow> 8) (pt_ref + ((vptr >> 12) && mask 8 << 2) && mask pt_bits >> 2)), snd x)}) = {(x, s)} \<longrightarrow> snd ((case the (kheap s (pt_ref + ((vptr >> 12) && mask 8 << 2) - (pt_ref + ((vptr >> 12) && mask 8 << 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> (\<Union>x\<in>fst ((case the (kheap s (pt_ref + ((vptr >> 12) && mask 8 << 2) - (pt_ref + ((vptr >> 12) && mask 8 << 2) && mask pt_bits))) of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s). {(fst x (UCAST(32 \<rightarrow> 8) (pt_ref + ((vptr >> 12) && mask 8 << 2) && mask pt_bits >> 2)), snd x)}) = {(x, s)} \<longrightarrow> snd ((case the (kheap s (pt_ref + ((vptr >> 12) && mask 8 << 2) - (pt_ref + ((vptr >> 12) && mask 8 << 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> (\<Union>x\<in>fst ((case the (kheap s (pt_ref + ((vptr >> 12) && mask 8 << 2) - (pt_ref + ((vptr >> 12) && mask 8 << 2) && mask pt_bits))) of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s). {(fst x (UCAST(32 \<rightarrow> 8) (pt_ref + ((vptr >> 12) && mask 8 << 2) && mask pt_bits >> 2)), snd x)}) = {(x, s)} \<longrightarrow> snd ((case the (kheap s (pt_ref + ((vptr >> 12) && mask 8 << 2) - (pt_ref + ((vptr >> 12) && mask 8 << 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> (\<Union>x\<in>fst ((case the (kheap s (pt_ref + ((vptr >> 12) && mask 8 << 2) - (pt_ref + ((vptr >> 12) && mask 8 << 2) && mask pt_bits))) of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s). {(fst x (UCAST(32 \<rightarrow> 8) (pt_ref + ((vptr >> 12) && mask 8 << 2) && mask pt_bits >> 2)), snd x)}) = {(x, s)} \<longrightarrow> snd ((case the (kheap s (pt_ref + ((vptr >> 12) && mask 8 << 2) - (pt_ref + ((vptr >> 12) && mask 8 << 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> (x2a (UCAST(32 \<rightarrow> 8) ((vptr >> 12) && mask 8)) = x) = ((\<Union>x\<in>fst ((case the (kheap s (pt_ref + ((vptr >> 12) && mask 8 << 2) - (pt_ref + ((vptr >> 12) && mask 8 << 2) && mask pt_bits))) of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s). {(fst x (UCAST(32 \<rightarrow> 8) (pt_ref + ((vptr >> 12) && mask 8 << 2) && mask pt_bits >> 2)), snd x)}) = {(x, s)} \<and> \<not> snd ((case the (kheap s (pt_ref + ((vptr >> 12) && mask 8 << 2) - (pt_ref + ((vptr >> 12) && mask 8 << 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> (\<Union>x\<in>fst ((case the (kheap s (pt_ref + ((vptr >> 12) && mask 8 << 2) - (pt_ref + ((vptr >> 12) && mask 8 << 2) && mask pt_bits))) of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s). {(fst x (UCAST(32 \<rightarrow> 8) (pt_ref + ((vptr >> 12) && mask 8 << 2) && mask pt_bits >> 2)), snd x)}) = {(x, s)} \<longrightarrow> snd ((case the (kheap s (pt_ref + ((vptr >> 12) && mask 8 << 2) - (pt_ref + ((vptr >> 12) && mask 8 << 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> (\<Union>x\<in>fst ((case the (kheap s (pt_ref + ((vptr >> 12) && mask 8 << 2) - (pt_ref + ((vptr >> 12) && mask 8 << 2) && mask pt_bits))) of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s). {(fst x (UCAST(32 \<rightarrow> 8) (pt_ref + ((vptr >> 12) && mask 8 << 2) && mask pt_bits >> 2)), snd x)}) = {(x, s)} \<longrightarrow> snd ((case the (kheap s (pt_ref + ((vptr >> 12) && mask 8 << 2) - (pt_ref + ((vptr >> 12) && mask 8 << 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) && mask 8 << 2) - (pt_ref + ((vptr >> 12) && mask 8 << 2) && mask pt_bits)) = None \<longrightarrow> (\<forall>x2. kheap s pt_ref = Some (ArchObj (PageTable x2)) \<longrightarrow> x2 (UCAST(32 \<rightarrow> 8) ((vptr >> 12) && mask 8)) \<noteq> x)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned pt_ref pt_bits; pt_ref + ((vptr >> 12) && mask 8 << 2) - (pt_ref + ((vptr >> 12) && mask 8 << 2) && mask pt_bits) = pt_ref\<rbrakk> \<Longrightarrow> ((\<exists>y. kheap s (pt_ref + ((vptr >> 12) && mask 8 << 2) - (pt_ref + ((vptr >> 12) && mask 8 << 2) && mask pt_bits)) = Some y) \<longrightarrow> (kheap s pt_ref = None \<longrightarrow> (\<Union>x\<in>fst ((case the (kheap s (pt_ref + ((vptr >> 12) && mask 8 << 2) - (pt_ref + ((vptr >> 12) && mask 8 << 2) && mask pt_bits))) of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s). {(fst x (UCAST(32 \<rightarrow> 8) (pt_ref + ((vptr >> 12) && mask 8 << 2) && mask pt_bits >> 2)), snd x)}) = {(x, s)} \<longrightarrow> snd ((case the (kheap s (pt_ref + ((vptr >> 12) && mask 8 << 2) - (pt_ref + ((vptr >> 12) && mask 8 << 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> (\<Union>x\<in>fst ((case the (kheap s (pt_ref + ((vptr >> 12) && mask 8 << 2) - (pt_ref + ((vptr >> 12) && mask 8 << 2) && mask pt_bits))) of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s). {(fst x (UCAST(32 \<rightarrow> 8) (pt_ref + ((vptr >> 12) && mask 8 << 2) && mask pt_bits >> 2)), snd x)}) = {(x, s)} \<longrightarrow> snd ((case the (kheap s (pt_ref + ((vptr >> 12) && mask 8 << 2) - (pt_ref + ((vptr >> 12) && mask 8 << 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> (\<Union>x\<in>fst ((case the (kheap s (pt_ref + ((vptr >> 12) && mask 8 << 2) - (pt_ref + ((vptr >> 12) && mask 8 << 2) && mask pt_bits))) of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s). {(fst x (UCAST(32 \<rightarrow> 8) (pt_ref + ((vptr >> 12) && mask 8 << 2) && mask pt_bits >> 2)), snd x)}) = {(x, s)} \<longrightarrow> snd ((case the (kheap s (pt_ref + ((vptr >> 12) && mask 8 << 2) - (pt_ref + ((vptr >> 12) && mask 8 << 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> (\<Union>x\<in>fst ((case the (kheap s (pt_ref + ((vptr >> 12) && mask 8 << 2) - (pt_ref + ((vptr >> 12) && mask 8 << 2) && mask pt_bits))) of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s). {(fst x (UCAST(32 \<rightarrow> 8) (pt_ref + ((vptr >> 12) && mask 8 << 2) && mask pt_bits >> 2)), snd x)}) = {(x, s)} \<longrightarrow> snd ((case the (kheap s (pt_ref + ((vptr >> 12) && mask 8 << 2) - (pt_ref + ((vptr >> 12) && mask 8 << 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> (\<Union>x\<in>fst ((case the (kheap s (pt_ref + ((vptr >> 12) && mask 8 << 2) - (pt_ref + ((vptr >> 12) && mask 8 << 2) && mask pt_bits))) of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s). {(fst x (UCAST(32 \<rightarrow> 8) (pt_ref + ((vptr >> 12) && mask 8 << 2) && mask pt_bits >> 2)), snd x)}) = {(x, s)} \<longrightarrow> snd ((case the (kheap s (pt_ref + ((vptr >> 12) && mask 8 << 2) - (pt_ref + ((vptr >> 12) && mask 8 << 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> (\<Union>x\<in>fst ((case the (kheap s (pt_ref + ((vptr >> 12) && mask 8 << 2) - (pt_ref + ((vptr >> 12) && mask 8 << 2) && mask pt_bits))) of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s). {(fst x (UCAST(32 \<rightarrow> 8) (pt_ref + ((vptr >> 12) && mask 8 << 2) && mask pt_bits >> 2)), snd x)}) = {(x, s)} \<longrightarrow> snd ((case the (kheap s (pt_ref + ((vptr >> 12) && mask 8 << 2) - (pt_ref + ((vptr >> 12) && mask 8 << 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> (x2a (UCAST(32 \<rightarrow> 8) ((vptr >> 12) && mask 8)) = x) = ((\<Union>x\<in>fst ((case the (kheap s (pt_ref + ((vptr >> 12) && mask 8 << 2) - (pt_ref + ((vptr >> 12) && mask 8 << 2) && mask pt_bits))) of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s). {(fst x (UCAST(32 \<rightarrow> 8) (pt_ref + ((vptr >> 12) && mask 8 << 2) && mask pt_bits >> 2)), snd x)}) = {(x, s)} \<and> \<not> snd ((case the (kheap s (pt_ref + ((vptr >> 12) && mask 8 << 2) - (pt_ref + ((vptr >> 12) && mask 8 << 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> (\<Union>x\<in>fst ((case the (kheap s (pt_ref + ((vptr >> 12) && mask 8 << 2) - (pt_ref + ((vptr >> 12) && mask 8 << 2) && mask pt_bits))) of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s). {(fst x (UCAST(32 \<rightarrow> 8) (pt_ref + ((vptr >> 12) && mask 8 << 2) && mask pt_bits >> 2)), snd x)}) = {(x, s)} \<longrightarrow> snd ((case the (kheap s (pt_ref + ((vptr >> 12) && mask 8 << 2) - (pt_ref + ((vptr >> 12) && mask 8 << 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> (\<Union>x\<in>fst ((case the (kheap s (pt_ref + ((vptr >> 12) && mask 8 << 2) - (pt_ref + ((vptr >> 12) && mask 8 << 2) && mask pt_bits))) of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s). {(fst x (UCAST(32 \<rightarrow> 8) (pt_ref + ((vptr >> 12) && mask 8 << 2) && mask pt_bits >> 2)), snd x)}) = {(x, s)} \<longrightarrow> snd ((case the (kheap s (pt_ref + ((vptr >> 12) && mask 8 << 2) - (pt_ref + ((vptr >> 12) && mask 8 << 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) && mask 8 << 2) - (pt_ref + ((vptr >> 12) && mask 8 << 2) && mask pt_bits)) = None \<longrightarrow> (\<forall>x2. kheap s pt_ref = Some (ArchObj (PageTable x2)) \<longrightarrow> x2 (UCAST(32 \<rightarrow> 8) ((vptr >> 12) && mask 8)) \<noteq> x))
 2. is_aligned pt_ref pt_bits \<Longrightarrow> pt_ref + ((vptr >> 12) && mask 8 << 2) - (pt_ref + ((vptr >> 12) && mask 8 << 2) && mask pt_bits) = pt_ref proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned pt_ref pt_bits; pt_ref + ((vptr >> 12) && mask 8 << 2) - (pt_ref + ((vptr >> 12) && mask 8 << 2) && mask pt_bits) = pt_ref\<rbrakk> \<Longrightarrow> (\<exists>y. kheap s pt_ref = Some y) \<longrightarrow> (kheap s pt_ref = None \<longrightarrow> (\<Union>x\<in>fst ((case the None of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s). {(fst x (UCAST(32 \<rightarrow> 8) (pt_ref + ((vptr >> 12) && mask 8 << 2) && mask pt_bits >> 2)), snd x)}) = {(x, s)} \<longrightarrow> snd ((case the None of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> \<lambda>s. ({}, True) | _ \<Rightarrow> \<lambda>s. ({}, True)) s)) \<and> (\<forall>x2. kheap s pt_ref = Some (ArchObj (PageTable x2)) \<longrightarrow> (x2 (UCAST(32 \<rightarrow> 8) ((vptr >> 12) && mask 8)) = x) = (x2 (UCAST(32 \<rightarrow> 8) (pt_ref + ((vptr >> 12) && mask 8 << 2) && mask pt_bits >> 2)) = x))
 2. is_aligned pt_ref pt_bits \<Longrightarrow> pt_ref + ((vptr >> 12) && mask 8 << 2) - (pt_ref + ((vptr >> 12) && mask 8 << 2) && mask pt_bits) = pt_ref proof (prove)
goal (2 subgoals):
 1. \<And>x2. \<lbrakk>is_aligned pt_ref 10; kheap s pt_ref = Some (ArchObj (PageTable x2))\<rbrakk> \<Longrightarrow> (x2 (UCAST(32 \<rightarrow> 8) ((vptr >> 12) && mask 8)) = x) = (x2 (UCAST(32 \<rightarrow> 8) ((vptr >> 12 << 2 >> 2) && mask 8)) = x)
 2. is_aligned pt_ref pt_bits \<Longrightarrow> pt_ref + ((vptr >> 12) && mask 8 << 2) - (pt_ref + ((vptr >> 12) && mask 8 << 2) && mask pt_bits) = pt_ref proof (prove)
goal (4 subgoals):
 1. \<And>x2. \<lbrakk>is_aligned pt_ref 10; kheap s pt_ref = Some (ArchObj (PageTable x2)); vptr >> 12 << 2 >> 2 = vptr >> 12\<rbrakk> \<Longrightarrow> (x2 (UCAST(32 \<rightarrow> 8) ((vptr >> 12) && mask 8)) = x) = (x2 (UCAST(32 \<rightarrow> 8) ((vptr >> 12 << 2 >> 2) && mask 8)) = x)
 2. \<And>x2. \<lbrakk>is_aligned pt_ref 10; kheap s pt_ref = Some (ArchObj (PageTable x2))\<rbrakk> \<Longrightarrow> 2 < LENGTH(32)
 3. \<And>x2. \<lbrakk>is_aligned pt_ref 10; kheap s pt_ref = Some (ArchObj (PageTable x2))\<rbrakk> \<Longrightarrow> vptr >> 12 < 2 ^ (LENGTH(32) - 2)
 4. is_aligned pt_ref pt_bits \<Longrightarrow> pt_ref + ((vptr >> 12) && mask 8 << 2) - (pt_ref + ((vptr >> 12) && mask 8 << 2) && mask pt_bits) = pt_ref proof (prove)
goal (2 subgoals):
 1. \<And>x2. \<lbrakk>is_aligned pt_ref 10; kheap s pt_ref = Some (ArchObj (PageTable x2))\<rbrakk> \<Longrightarrow> vptr >> 12 < 0x40000000
 2. is_aligned pt_ref pt_bits \<Longrightarrow> pt_ref + ((vptr >> 12) && mask 8 << 2) - (pt_ref + ((vptr >> 12) && mask 8 << 2) && mask pt_bits) = pt_ref proof (prove)
goal (4 subgoals):
 1. \<And>x2. \<lbrakk>is_aligned pt_ref 10; kheap s pt_ref = Some (ArchObj (PageTable x2)); vptr >> 12 < 2 ^ 30\<rbrakk> \<Longrightarrow> vptr >> 12 < 0x40000000
 2. \<And>x2. \<lbrakk>is_aligned pt_ref 10; kheap s pt_ref = Some (ArchObj (PageTable x2))\<rbrakk> \<Longrightarrow> vptr && mask (12 + 30) = vptr
 3. \<And>x2. \<lbrakk>is_aligned pt_ref 10; kheap s pt_ref = Some (ArchObj (PageTable x2))\<rbrakk> \<Longrightarrow> 30 < LENGTH(32)
 4. is_aligned pt_ref pt_bits \<Longrightarrow> pt_ref + ((vptr >> 12) && mask 8 << 2) - (pt_ref + ((vptr >> 12) && mask 8 << 2) && mask pt_bits) = pt_ref proof (prove)
goal (3 subgoals):
 1. \<And>x2. \<lbrakk>is_aligned pt_ref 10; kheap s pt_ref = Some (ArchObj (PageTable x2))\<rbrakk> \<Longrightarrow> vptr && mask (12 + 30) = vptr
 2. \<And>x2. \<lbrakk>is_aligned pt_ref 10; kheap s pt_ref = Some (ArchObj (PageTable x2))\<rbrakk> \<Longrightarrow> 30 < LENGTH(32)
 3. is_aligned pt_ref pt_bits \<Longrightarrow> pt_ref + ((vptr >> 12) && mask 8 << 2) - (pt_ref + ((vptr >> 12) && mask 8 << 2) && mask pt_bits) = pt_ref proof (prove)
goal (3 subgoals):
 1. \<And>x2. \<lbrakk>is_aligned pt_ref 10; kheap s pt_ref = Some (ArchObj (PageTable x2))\<rbrakk> \<Longrightarrow> uint vptr < 4398046511104
 2. \<And>x2. \<lbrakk>is_aligned pt_ref 10; kheap s pt_ref = Some (ArchObj (PageTable x2))\<rbrakk> \<Longrightarrow> 30 < LENGTH(32)
 3. is_aligned pt_ref pt_bits \<Longrightarrow> pt_ref + ((vptr >> 12) && mask 8 << 2) - (pt_ref + ((vptr >> 12) && mask 8 << 2) && mask pt_bits) = pt_ref proof (prove)
goal (4 subgoals):
 1. \<And>x2. \<lbrakk>is_aligned pt_ref 10; kheap s pt_ref = Some (ArchObj (PageTable x2)); uint vptr < 2 ^ 32\<rbrakk> \<Longrightarrow> uint vptr < 4398046511104
 2. \<And>x2. \<lbrakk>is_aligned pt_ref 10; kheap s pt_ref = Some (ArchObj (PageTable x2))\<rbrakk> \<Longrightarrow> LENGTH(32) \<le> 32
 3. \<And>x2. \<lbrakk>is_aligned pt_ref 10; kheap s pt_ref = Some (ArchObj (PageTable x2))\<rbrakk> \<Longrightarrow> 30 < LENGTH(32)
 4. is_aligned pt_ref pt_bits \<Longrightarrow> pt_ref + ((vptr >> 12) && mask 8 << 2) - (pt_ref + ((vptr >> 12) && mask 8 << 2) && mask pt_bits) = pt_ref proof (prove)
goal (1 subgoal):
 1. is_aligned pt_ref pt_bits \<Longrightarrow> (vptr >> 12) && mask 8 << 2 = pt_ref + ((vptr >> 12) && mask 8 << 2) && mask pt_bits proof (prove)
goal:
No subgoals!