theory Arch_DR

lemma store_pde_page_inv_entries_safe:
  "\<lbrace>page_inv_entries_safe (Inr (ab, bb)) and valid_pdpt_objs\<rbrace>
   store_pde (hd bb) ab
   \<lbrace>\<lambda>rv s. (\<exists>f. ko_at (ArchObj (arch_kernel_obj.PageDirectory f)) (hd bb && ~~ mask pd_bits)  s
    \<and> (\<forall>slot\<in>set (tl bb). f (ucast (slot && mask pd_bits >> 2)) = ARM_A.pde.InvalidPDE))
    \<and> (\<forall>sl\<in>set (tl bb). sl && ~~ mask pd_bits = hd bb && ~~ mask pd_bits)\<rbrace>" apply (simp add:store_pde_def set_pd_def set_object_def) apply (wp get_object_wp) apply (clarsimp simp:obj_at_def page_inv_entries_safe_def split:if_splits) apply (intro conjI impI) apply (clarsimp simp: hd_map_simp upto_enum_def upto_enum_step_def drop_map
                         tl_map_simp map_eq_Cons_conv upt_eq_Cons_conv upto_0_to_n) apply (clarsimp simp add:field_simps) apply (subst (asm) shiftl_t2n[where n = 2,simplified field_simps,simplified,symmetric])+ apply (subst (asm) and_mask_plus[where a = "of_nat slot << 2"]) apply (simp add:pd_bits_def pageBits_def)+ apply (rule shiftl_less_t2n[where m = 6,simplified]) apply (rule word_of_nat_less,simp) apply simp apply (subst (asm) is_aligned_shiftr_add) apply (erule is_aligned_after_mask) apply (simp add:pd_bits_def pageBits_def)+ apply (simp add:is_aligned_shiftl_self) apply (rule shiftl_less_t2n) apply (rule word_of_nat_less,simp) apply simp+ apply (subst (asm) ucast_add) apply simp apply simp apply (subst (asm) shiftl_shiftr_id) apply simp apply (rule word_of_nat_less) apply simp apply (simp add:ucast_of_nat_small of_nat_neq_0 del: word_of_nat_eq_0_iff) apply (clarsimp simp: hd_map_simp upto_enum_def upto_enum_step_def tl_map_simp map_eq_Cons_conv
                        upt_eq_Cons_conv upto_0_to_n image_def) apply (simp add: field_simps) apply (erule page_directory_address_eq[symmetric]) apply (fastforce simp:upto_enum_def upto_enum_step_def image_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>page_inv_entries_safe (Inr (ab, bb)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x)\<rbrace> store_pde (hd bb) ab \<lbrace>\<lambda>rv s. (\<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (hd bb && ~~ mask pd_bits) s \<and> (\<forall>slot\<in>set (tl bb). f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)) = InvalidPDE)) \<and> (\<forall>sl\<in>set (tl bb). sl && ~~ mask pd_bits = hd bb && ~~ mask pd_bits)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>page_inv_entries_safe (Inr (ab, bb)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x)\<rbrace> do pd <- get_pd (hd bb && ~~ mask pd_bits);
kobj <- KHeap_A.get_object (hd bb && ~~ mask pd_bits);
y <- assert (a_type kobj = a_type (ArchObj (arch_kernel_obj.PageDirectory (pd(UCAST(32 \<rightarrow> 12) (hd bb && mask pd_bits >> 2) := ab)))));
s <- get;
put (update_kheap ((kheap s)(hd bb && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (pd(UCAST(32 \<rightarrow> 12) (hd bb && mask pd_bits >> 2) := ab))))) s)
od \<lbrace>\<lambda>rv s. (\<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (hd bb && ~~ mask pd_bits) s \<and> (\<forall>slot\<in>set (tl bb). f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)) = InvalidPDE)) \<and> (\<forall>sl\<in>set (tl bb). sl && ~~ mask pd_bits = hd bb && ~~ mask pd_bits)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (page_inv_entries_safe (Inr (ab, bb)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x)) s \<Longrightarrow> \<forall>pd. ako_at (arch_kernel_obj.PageDirectory pd) (hd bb && ~~ mask pd_bits) s \<longrightarrow> (\<forall>ko. ko_at ko (hd bb && ~~ mask pd_bits) s \<longrightarrow> a_type ko = a_type (ArchObj (arch_kernel_obj.PageDirectory (pd(UCAST(32 \<rightarrow> 12) (hd bb && mask pd_bits >> 2) := ab)))) \<longrightarrow> (\<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (hd bb && ~~ mask pd_bits) (update_kheap ((kheap s)(hd bb && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (pd(UCAST(32 \<rightarrow> 12) (hd bb && mask pd_bits >> 2) := ab))))) s) \<and> (\<forall>slot\<in>set (tl bb). f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)) = InvalidPDE)) \<and> (\<forall>sl\<in>set (tl bb). sl && ~~ mask pd_bits = hd bb && ~~ mask pd_bits)) proof (prove)
goal (1 subgoal):
 1. \<And>s p pda. \<lbrakk>\<forall>sl. map (\<lambda>x. x + p) [0 , 4 .e. 0x3C] \<noteq> [sl]; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]; \<forall>x\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap s (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && mask pd_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> ((\<exists>slot\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2) = UCAST(32 \<rightarrow> 12) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && mask pd_bits >> 2)) \<longrightarrow> ab = InvalidPDE) \<and> (\<forall>sl\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). sl && ~~ mask pd_bits = hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits) proof (prove)
goal (2 subgoals):
 1. \<And>s p pda. \<lbrakk>\<forall>sl. map (\<lambda>x. x + p) [0 , 4 .e. 0x3C] \<noteq> [sl]; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]; \<forall>x\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap s (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && mask pd_bits >> 2) := ab)))); \<exists>slot\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2) = UCAST(32 \<rightarrow> 12) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && mask pd_bits >> 2)\<rbrakk> \<Longrightarrow> ab = InvalidPDE
 2. \<And>s p pda. \<lbrakk>\<forall>sl. map (\<lambda>x. x + p) [0 , 4 .e. 0x3C] \<noteq> [sl]; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]; \<forall>x\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap s (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && mask pd_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> \<forall>sl\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). sl && ~~ mask pd_bits = hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits proof (prove)
goal (2 subgoals):
 1. \<And>s p pda slot. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pda (UCAST(32 \<rightarrow> 12) (word_of_nat x * 4 + p && mask pd_bits >> 2)) = InvalidPDE; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := ab)))); UCAST(32 \<rightarrow> 12) (word_of_nat slot * 4 + p && mask pd_bits >> 2) = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); Suc 0 \<le> slot; slot < 16\<rbrakk> \<Longrightarrow> ab = InvalidPDE
 2. \<And>s p pda. \<lbrakk>\<forall>sl. map (\<lambda>x. x + p) [0 , 4 .e. 0x3C] \<noteq> [sl]; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]; \<forall>x\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap s (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && mask pd_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> \<forall>sl\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). sl && ~~ mask pd_bits = hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits proof (prove)
goal (2 subgoals):
 1. \<And>s p pda slot. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map ((+) p \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pda (UCAST(32 \<rightarrow> 12) (p + word_of_nat x * 4 && mask pd_bits >> 2)) = InvalidPDE; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := ab)))); UCAST(32 \<rightarrow> 12) (p + word_of_nat slot * 4 && mask pd_bits >> 2) = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); Suc 0 \<le> slot; slot < 16\<rbrakk> \<Longrightarrow> ab = InvalidPDE
 2. \<And>s p pda. \<lbrakk>\<forall>sl. map (\<lambda>x. x + p) [0 , 4 .e. 0x3C] \<noteq> [sl]; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]; \<forall>x\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap s (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && mask pd_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> \<forall>sl\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). sl && ~~ mask pd_bits = hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits proof (prove)
goal (2 subgoals):
 1. \<And>s p pda slot. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map ((+) p \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pda (UCAST(32 \<rightarrow> 12) (p + (word_of_nat x << 2) && mask pd_bits >> 2)) = InvalidPDE; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := ab)))); UCAST(32 \<rightarrow> 12) (p + (word_of_nat slot << 2) && mask pd_bits >> 2) = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); Suc 0 \<le> slot; slot < 16\<rbrakk> \<Longrightarrow> ab = InvalidPDE
 2. \<And>s p pda. \<lbrakk>\<forall>sl. map (\<lambda>x. x + p) [0 , 4 .e. 0x3C] \<noteq> [sl]; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]; \<forall>x\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap s (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && mask pd_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> \<forall>sl\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). sl && ~~ mask pd_bits = hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits proof (prove)
goal (6 subgoals):
 1. \<And>s p pda slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map ((+) p \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pda (UCAST(32 \<rightarrow> 12) (p + (word_of_nat x << 2) && mask pd_bits >> 2)) = InvalidPDE; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> is_aligned p (?m69 s p pda slot)
 2. \<And>s p pda slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map ((+) p \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pda (UCAST(32 \<rightarrow> 12) (p + (word_of_nat x << 2) && mask pd_bits >> 2)) = InvalidPDE; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> ?m69 s p pda slot \<le> pd_bits
 3. \<And>s p pda slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map ((+) p \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pda (UCAST(32 \<rightarrow> 12) (p + (word_of_nat x << 2) && mask pd_bits >> 2)) = InvalidPDE; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> pd_bits < 32
 4. \<And>s p pda slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map ((+) p \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pda (UCAST(32 \<rightarrow> 12) (p + (word_of_nat x << 2) && mask pd_bits >> 2)) = InvalidPDE; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> word_of_nat slot << 2 < 2 ^ ?m69 s p pda slot
 5. \<And>s p pda slot. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map ((+) p \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pda (UCAST(32 \<rightarrow> 12) (p + (word_of_nat x << 2) && mask pd_bits >> 2)) = InvalidPDE; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := ab)))); UCAST(32 \<rightarrow> 12) ((p && mask pd_bits) + (word_of_nat slot << 2) >> 2) = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); Suc 0 \<le> slot; slot < 16\<rbrakk> \<Longrightarrow> ab = InvalidPDE
 6. \<And>s p pda. \<lbrakk>\<forall>sl. map (\<lambda>x. x + p) [0 , 4 .e. 0x3C] \<noteq> [sl]; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]; \<forall>x\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap s (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && mask pd_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> \<forall>sl\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). sl && ~~ mask pd_bits = hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits proof (prove)
goal (3 subgoals):
 1. \<And>s p pda slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map ((+) p \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pda (UCAST(32 \<rightarrow> 12) (p + (word_of_nat x << 2) && mask 14 >> 2)) = InvalidPDE; kheap s (p && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask 14 >> 2) := ab))))\<rbrakk> \<Longrightarrow> word_of_nat slot << 2 < 0x40
 2. \<And>s p pda slot. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map ((+) p \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pda (UCAST(32 \<rightarrow> 12) (p + (word_of_nat x << 2) && mask pd_bits >> 2)) = InvalidPDE; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := ab)))); UCAST(32 \<rightarrow> 12) ((p && mask pd_bits) + (word_of_nat slot << 2) >> 2) = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); Suc 0 \<le> slot; slot < 16\<rbrakk> \<Longrightarrow> ab = InvalidPDE
 3. \<And>s p pda. \<lbrakk>\<forall>sl. map (\<lambda>x. x + p) [0 , 4 .e. 0x3C] \<noteq> [sl]; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]; \<forall>x\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap s (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && mask pd_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> \<forall>sl\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). sl && ~~ mask pd_bits = hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits proof (prove)
goal (4 subgoals):
 1. \<And>s p pda slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map ((+) p \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pda (UCAST(32 \<rightarrow> 12) (p + (word_of_nat x << 2) && mask 14 >> 2)) = InvalidPDE; kheap s (p && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask 14 >> 2) := ab))))\<rbrakk> \<Longrightarrow> word_of_nat slot < 2 ^ (6 - 2)
 2. \<And>s p pda slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map ((+) p \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pda (UCAST(32 \<rightarrow> 12) (p + (word_of_nat x << 2) && mask 14 >> 2)) = InvalidPDE; kheap s (p && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask 14 >> 2) := ab))))\<rbrakk> \<Longrightarrow> 6 < LENGTH(32)
 3. \<And>s p pda slot. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map ((+) p \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pda (UCAST(32 \<rightarrow> 12) (p + (word_of_nat x << 2) && mask pd_bits >> 2)) = InvalidPDE; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := ab)))); UCAST(32 \<rightarrow> 12) ((p && mask pd_bits) + (word_of_nat slot << 2) >> 2) = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); Suc 0 \<le> slot; slot < 16\<rbrakk> \<Longrightarrow> ab = InvalidPDE
 4. \<And>s p pda. \<lbrakk>\<forall>sl. map (\<lambda>x. x + p) [0 , 4 .e. 0x3C] \<noteq> [sl]; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]; \<forall>x\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap s (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && mask pd_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> \<forall>sl\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). sl && ~~ mask pd_bits = hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits proof (prove)
goal (3 subgoals):
 1. \<And>s p pda slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map ((+) p \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pda (UCAST(32 \<rightarrow> 12) (p + (word_of_nat x << 2) && mask 14 >> 2)) = InvalidPDE; kheap s (p && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask 14 >> 2) := ab))))\<rbrakk> \<Longrightarrow> 6 < LENGTH(32)
 2. \<And>s p pda slot. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map ((+) p \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pda (UCAST(32 \<rightarrow> 12) (p + (word_of_nat x << 2) && mask pd_bits >> 2)) = InvalidPDE; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := ab)))); UCAST(32 \<rightarrow> 12) ((p && mask pd_bits) + (word_of_nat slot << 2) >> 2) = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); Suc 0 \<le> slot; slot < 16\<rbrakk> \<Longrightarrow> ab = InvalidPDE
 3. \<And>s p pda. \<lbrakk>\<forall>sl. map (\<lambda>x. x + p) [0 , 4 .e. 0x3C] \<noteq> [sl]; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]; \<forall>x\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap s (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && mask pd_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> \<forall>sl\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). sl && ~~ mask pd_bits = hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits proof (prove)
goal (2 subgoals):
 1. \<And>s p pda slot. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map ((+) p \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pda (UCAST(32 \<rightarrow> 12) (p + (word_of_nat x << 2) && mask pd_bits >> 2)) = InvalidPDE; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := ab)))); UCAST(32 \<rightarrow> 12) ((p && mask pd_bits) + (word_of_nat slot << 2) >> 2) = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); Suc 0 \<le> slot; slot < 16\<rbrakk> \<Longrightarrow> ab = InvalidPDE
 2. \<And>s p pda. \<lbrakk>\<forall>sl. map (\<lambda>x. x + p) [0 , 4 .e. 0x3C] \<noteq> [sl]; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]; \<forall>x\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap s (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && mask pd_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> \<forall>sl\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). sl && ~~ mask pd_bits = hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits proof (prove)
goal (7 subgoals):
 1. \<And>s p pda slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map ((+) p \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pda (UCAST(32 \<rightarrow> 12) (p + (word_of_nat x << 2) && mask pd_bits >> 2)) = InvalidPDE; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> is_aligned (p && mask pd_bits) (?n82 s p pda slot)
 2. \<And>s p pda slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map ((+) p \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pda (UCAST(32 \<rightarrow> 12) (p + (word_of_nat x << 2) && mask pd_bits >> 2)) = InvalidPDE; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> is_aligned (word_of_nat slot << 2) 2
 3. \<And>s p pda slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map ((+) p \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pda (UCAST(32 \<rightarrow> 12) (p + (word_of_nat x << 2) && mask pd_bits >> 2)) = InvalidPDE; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> word_of_nat slot << 2 < 2 ^ ?n82 s p pda slot
 4. \<And>s p pda slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map ((+) p \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pda (UCAST(32 \<rightarrow> 12) (p + (word_of_nat x << 2) && mask pd_bits >> 2)) = InvalidPDE; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> 2 \<le> ?n82 s p pda slot
 5. \<And>s p pda slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map ((+) p \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pda (UCAST(32 \<rightarrow> 12) (p + (word_of_nat x << 2) && mask pd_bits >> 2)) = InvalidPDE; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> ?n82 s p pda slot < LENGTH(32)
 6. \<And>s p pda slot. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map ((+) p \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pda (UCAST(32 \<rightarrow> 12) (p + (word_of_nat x << 2) && mask pd_bits >> 2)) = InvalidPDE; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := ab)))); UCAST(32 \<rightarrow> 12) ((p && mask pd_bits >> 2) + (word_of_nat slot << 2 >> 2)) = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); Suc 0 \<le> slot; slot < 16\<rbrakk> \<Longrightarrow> ab = InvalidPDE
 7. \<And>s p pda. \<lbrakk>\<forall>sl. map (\<lambda>x. x + p) [0 , 4 .e. 0x3C] \<noteq> [sl]; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]; \<forall>x\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap s (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && mask pd_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> \<forall>sl\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). sl && ~~ mask pd_bits = hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits proof (prove)
goal (7 subgoals):
 1. \<And>s p pda slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; bb = map ((+) p \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pda (UCAST(32 \<rightarrow> 12) (p + (word_of_nat x << 2) && mask pd_bits >> 2)) = InvalidPDE; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> 6 \<le> pd_bits
 2. \<And>s p pda slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map ((+) p \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pda (UCAST(32 \<rightarrow> 12) (p + (word_of_nat x << 2) && mask pd_bits >> 2)) = InvalidPDE; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> is_aligned (word_of_nat slot << 2) 2
 3. \<And>s p pda slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map ((+) p \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pda (UCAST(32 \<rightarrow> 12) (p + (word_of_nat x << 2) && mask pd_bits >> 2)) = InvalidPDE; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> word_of_nat slot << 2 < 2 ^ 6
 4. \<And>s p pda slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map ((+) p \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pda (UCAST(32 \<rightarrow> 12) (p + (word_of_nat x << 2) && mask pd_bits >> 2)) = InvalidPDE; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> 2 \<le> 6
 5. \<And>s p pda slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map ((+) p \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pda (UCAST(32 \<rightarrow> 12) (p + (word_of_nat x << 2) && mask pd_bits >> 2)) = InvalidPDE; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> 6 < LENGTH(32)
 6. \<And>s p pda slot. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map ((+) p \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pda (UCAST(32 \<rightarrow> 12) (p + (word_of_nat x << 2) && mask pd_bits >> 2)) = InvalidPDE; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := ab)))); UCAST(32 \<rightarrow> 12) ((p && mask pd_bits >> 2) + (word_of_nat slot << 2 >> 2)) = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); Suc 0 \<le> slot; slot < 16\<rbrakk> \<Longrightarrow> ab = InvalidPDE
 7. \<And>s p pda. \<lbrakk>\<forall>sl. map (\<lambda>x. x + p) [0 , 4 .e. 0x3C] \<noteq> [sl]; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]; \<forall>x\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap s (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && mask pd_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> \<forall>sl\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). sl && ~~ mask pd_bits = hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits proof (prove)
goal (6 subgoals):
 1. \<And>s p pda slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map ((+) p \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pda (UCAST(32 \<rightarrow> 12) (p + (word_of_nat x << 2) && mask 14 >> 2)) = InvalidPDE; kheap s (p && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask 14 >> 2) := ab))))\<rbrakk> \<Longrightarrow> is_aligned (word_of_nat slot << 2) 2
 2. \<And>s p pda slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map ((+) p \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pda (UCAST(32 \<rightarrow> 12) (p + (word_of_nat x << 2) && mask pd_bits >> 2)) = InvalidPDE; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> word_of_nat slot << 2 < 2 ^ 6
 3. \<And>s p pda slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map ((+) p \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pda (UCAST(32 \<rightarrow> 12) (p + (word_of_nat x << 2) && mask pd_bits >> 2)) = InvalidPDE; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> 2 \<le> 6
 4. \<And>s p pda slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map ((+) p \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pda (UCAST(32 \<rightarrow> 12) (p + (word_of_nat x << 2) && mask pd_bits >> 2)) = InvalidPDE; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> 6 < LENGTH(32)
 5. \<And>s p pda slot. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map ((+) p \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pda (UCAST(32 \<rightarrow> 12) (p + (word_of_nat x << 2) && mask pd_bits >> 2)) = InvalidPDE; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := ab)))); UCAST(32 \<rightarrow> 12) ((p && mask pd_bits >> 2) + (word_of_nat slot << 2 >> 2)) = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); Suc 0 \<le> slot; slot < 16\<rbrakk> \<Longrightarrow> ab = InvalidPDE
 6. \<And>s p pda. \<lbrakk>\<forall>sl. map (\<lambda>x. x + p) [0 , 4 .e. 0x3C] \<noteq> [sl]; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]; \<forall>x\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap s (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && mask pd_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> \<forall>sl\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). sl && ~~ mask pd_bits = hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits proof (prove)
goal (5 subgoals):
 1. \<And>s p pda slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map ((+) p \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pda (UCAST(32 \<rightarrow> 12) (p + (word_of_nat x << 2) && mask pd_bits >> 2)) = InvalidPDE; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> word_of_nat slot << 2 < 2 ^ 6
 2. \<And>s p pda slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map ((+) p \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pda (UCAST(32 \<rightarrow> 12) (p + (word_of_nat x << 2) && mask pd_bits >> 2)) = InvalidPDE; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> 2 \<le> 6
 3. \<And>s p pda slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map ((+) p \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pda (UCAST(32 \<rightarrow> 12) (p + (word_of_nat x << 2) && mask pd_bits >> 2)) = InvalidPDE; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> 6 < LENGTH(32)
 4. \<And>s p pda slot. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map ((+) p \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pda (UCAST(32 \<rightarrow> 12) (p + (word_of_nat x << 2) && mask pd_bits >> 2)) = InvalidPDE; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := ab)))); UCAST(32 \<rightarrow> 12) ((p && mask pd_bits >> 2) + (word_of_nat slot << 2 >> 2)) = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); Suc 0 \<le> slot; slot < 16\<rbrakk> \<Longrightarrow> ab = InvalidPDE
 5. \<And>s p pda. \<lbrakk>\<forall>sl. map (\<lambda>x. x + p) [0 , 4 .e. 0x3C] \<noteq> [sl]; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]; \<forall>x\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap s (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && mask pd_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> \<forall>sl\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). sl && ~~ mask pd_bits = hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits proof (prove)
goal (6 subgoals):
 1. \<And>s p pda slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map ((+) p \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pda (UCAST(32 \<rightarrow> 12) (p + (word_of_nat x << 2) && mask pd_bits >> 2)) = InvalidPDE; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> word_of_nat slot < 2 ^ (6 - 2)
 2. \<And>s p pda slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map ((+) p \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pda (UCAST(32 \<rightarrow> 12) (p + (word_of_nat x << 2) && mask pd_bits >> 2)) = InvalidPDE; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> 6 < LENGTH(32)
 3. \<And>s p pda slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map ((+) p \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pda (UCAST(32 \<rightarrow> 12) (p + (word_of_nat x << 2) && mask pd_bits >> 2)) = InvalidPDE; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> 2 \<le> 6
 4. \<And>s p pda slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map ((+) p \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pda (UCAST(32 \<rightarrow> 12) (p + (word_of_nat x << 2) && mask pd_bits >> 2)) = InvalidPDE; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> 6 < LENGTH(32)
 5. \<And>s p pda slot. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map ((+) p \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pda (UCAST(32 \<rightarrow> 12) (p + (word_of_nat x << 2) && mask pd_bits >> 2)) = InvalidPDE; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := ab)))); UCAST(32 \<rightarrow> 12) ((p && mask pd_bits >> 2) + (word_of_nat slot << 2 >> 2)) = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); Suc 0 \<le> slot; slot < 16\<rbrakk> \<Longrightarrow> ab = InvalidPDE
 6. \<And>s p pda. \<lbrakk>\<forall>sl. map (\<lambda>x. x + p) [0 , 4 .e. 0x3C] \<noteq> [sl]; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]; \<forall>x\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap s (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && mask pd_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> \<forall>sl\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). sl && ~~ mask pd_bits = hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits proof (prove)
goal (5 subgoals):
 1. \<And>s p pda slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map ((+) p \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pda (UCAST(32 \<rightarrow> 12) (p + (word_of_nat x << 2) && mask pd_bits >> 2)) = InvalidPDE; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> 6 < LENGTH(32)
 2. \<And>s p pda slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map ((+) p \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pda (UCAST(32 \<rightarrow> 12) (p + (word_of_nat x << 2) && mask pd_bits >> 2)) = InvalidPDE; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> 2 \<le> 6
 3. \<And>s p pda slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map ((+) p \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pda (UCAST(32 \<rightarrow> 12) (p + (word_of_nat x << 2) && mask pd_bits >> 2)) = InvalidPDE; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> 6 < LENGTH(32)
 4. \<And>s p pda slot. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map ((+) p \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pda (UCAST(32 \<rightarrow> 12) (p + (word_of_nat x << 2) && mask pd_bits >> 2)) = InvalidPDE; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := ab)))); UCAST(32 \<rightarrow> 12) ((p && mask pd_bits >> 2) + (word_of_nat slot << 2 >> 2)) = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); Suc 0 \<le> slot; slot < 16\<rbrakk> \<Longrightarrow> ab = InvalidPDE
 5. \<And>s p pda. \<lbrakk>\<forall>sl. map (\<lambda>x. x + p) [0 , 4 .e. 0x3C] \<noteq> [sl]; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]; \<forall>x\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap s (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && mask pd_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> \<forall>sl\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). sl && ~~ mask pd_bits = hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits proof (prove)
goal (2 subgoals):
 1. \<And>s p pda slot. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map ((+) p \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pda (UCAST(32 \<rightarrow> 12) (p + (word_of_nat x << 2) && mask pd_bits >> 2)) = InvalidPDE; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := ab)))); UCAST(32 \<rightarrow> 12) ((p && mask pd_bits >> 2) + (word_of_nat slot << 2 >> 2)) = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); Suc 0 \<le> slot; slot < 16\<rbrakk> \<Longrightarrow> ab = InvalidPDE
 2. \<And>s p pda. \<lbrakk>\<forall>sl. map (\<lambda>x. x + p) [0 , 4 .e. 0x3C] \<noteq> [sl]; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]; \<forall>x\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap s (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && mask pd_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> \<forall>sl\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). sl && ~~ mask pd_bits = hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits proof (prove)
goal (3 subgoals):
 1. \<And>s p pda slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map ((+) p \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pda (UCAST(32 \<rightarrow> 12) (p + (word_of_nat x << 2) && mask pd_bits >> 2)) = InvalidPDE; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> LENGTH(12) \<le> LENGTH(32)
 2. \<And>s p pda slot. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map ((+) p \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pda (UCAST(32 \<rightarrow> 12) (p + (word_of_nat x << 2) && mask pd_bits >> 2)) = InvalidPDE; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := ab)))); UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) + UCAST(32 \<rightarrow> 12) (word_of_nat slot << 2 >> 2) = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); Suc 0 \<le> slot; slot < 16\<rbrakk> \<Longrightarrow> ab = InvalidPDE
 3. \<And>s p pda. \<lbrakk>\<forall>sl. map (\<lambda>x. x + p) [0 , 4 .e. 0x3C] \<noteq> [sl]; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]; \<forall>x\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap s (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && mask pd_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> \<forall>sl\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). sl && ~~ mask pd_bits = hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits proof (prove)
goal (2 subgoals):
 1. \<And>s p pda slot. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map ((+) p \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pda (UCAST(32 \<rightarrow> 12) (p + (word_of_nat x << 2) && mask pd_bits >> 2)) = InvalidPDE; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := ab)))); UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) + UCAST(32 \<rightarrow> 12) (word_of_nat slot << 2 >> 2) = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); Suc 0 \<le> slot; slot < 16\<rbrakk> \<Longrightarrow> ab = InvalidPDE
 2. \<And>s p pda. \<lbrakk>\<forall>sl. map (\<lambda>x. x + p) [0 , 4 .e. 0x3C] \<noteq> [sl]; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]; \<forall>x\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap s (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && mask pd_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> \<forall>sl\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). sl && ~~ mask pd_bits = hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits proof (prove)
goal (2 subgoals):
 1. \<And>s p pda slot. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map ((+) p \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pda (UCAST(32 \<rightarrow> 12) (p + (word_of_nat x << 2) && mask pd_bits >> 2)) = InvalidPDE; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := ab)))); UCAST(32 \<rightarrow> 12) (word_of_nat slot << 2 >> 2) = 0; Suc 0 \<le> slot; slot < 16\<rbrakk> \<Longrightarrow> ab = InvalidPDE
 2. \<And>s p pda. \<lbrakk>\<forall>sl. map (\<lambda>x. x + p) [0 , 4 .e. 0x3C] \<noteq> [sl]; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]; \<forall>x\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap s (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && mask pd_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> \<forall>sl\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). sl && ~~ mask pd_bits = hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits proof (prove)
goal (4 subgoals):
 1. \<And>s p pda slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map ((+) p \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pda (UCAST(32 \<rightarrow> 12) (p + (word_of_nat x << 2) && mask pd_bits >> 2)) = InvalidPDE; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> 2 < LENGTH(32)
 2. \<And>s p pda slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map ((+) p \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pda (UCAST(32 \<rightarrow> 12) (p + (word_of_nat x << 2) && mask pd_bits >> 2)) = InvalidPDE; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> word_of_nat slot < 2 ^ (LENGTH(32) - 2)
 3. \<And>s p pda slot. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map ((+) p \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pda (UCAST(32 \<rightarrow> 12) (p + (word_of_nat x << 2) && mask pd_bits >> 2)) = InvalidPDE; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := ab)))); UCAST(32 \<rightarrow> 12) (word_of_nat slot) = 0; Suc 0 \<le> slot; slot < 16\<rbrakk> \<Longrightarrow> ab = InvalidPDE
 4. \<And>s p pda. \<lbrakk>\<forall>sl. map (\<lambda>x. x + p) [0 , 4 .e. 0x3C] \<noteq> [sl]; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]; \<forall>x\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap s (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && mask pd_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> \<forall>sl\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). sl && ~~ mask pd_bits = hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits proof (prove)
goal (3 subgoals):
 1. \<And>s p pda slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map ((+) p \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pda (UCAST(32 \<rightarrow> 12) (p + (word_of_nat x << 2) && mask pd_bits >> 2)) = InvalidPDE; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> word_of_nat slot < 2 ^ (LENGTH(32) - 2)
 2. \<And>s p pda slot. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map ((+) p \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pda (UCAST(32 \<rightarrow> 12) (p + (word_of_nat x << 2) && mask pd_bits >> 2)) = InvalidPDE; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := ab)))); UCAST(32 \<rightarrow> 12) (word_of_nat slot) = 0; Suc 0 \<le> slot; slot < 16\<rbrakk> \<Longrightarrow> ab = InvalidPDE
 3. \<And>s p pda. \<lbrakk>\<forall>sl. map (\<lambda>x. x + p) [0 , 4 .e. 0x3C] \<noteq> [sl]; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]; \<forall>x\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap s (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && mask pd_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> \<forall>sl\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). sl && ~~ mask pd_bits = hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits proof (prove)
goal (3 subgoals):
 1. \<And>s p pda slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map ((+) p \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pda (UCAST(32 \<rightarrow> 12) (p + (word_of_nat x << 2) && mask pd_bits >> 2)) = InvalidPDE; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> slot < unat (2 ^ (LENGTH(32) - 2))
 2. \<And>s p pda slot. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map ((+) p \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pda (UCAST(32 \<rightarrow> 12) (p + (word_of_nat x << 2) && mask pd_bits >> 2)) = InvalidPDE; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := ab)))); UCAST(32 \<rightarrow> 12) (word_of_nat slot) = 0; Suc 0 \<le> slot; slot < 16\<rbrakk> \<Longrightarrow> ab = InvalidPDE
 3. \<And>s p pda. \<lbrakk>\<forall>sl. map (\<lambda>x. x + p) [0 , 4 .e. 0x3C] \<noteq> [sl]; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]; \<forall>x\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap s (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && mask pd_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> \<forall>sl\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). sl && ~~ mask pd_bits = hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits proof (prove)
goal (2 subgoals):
 1. \<And>s p pda slot. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map ((+) p \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pda (UCAST(32 \<rightarrow> 12) (p + (word_of_nat x << 2) && mask pd_bits >> 2)) = InvalidPDE; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := ab)))); UCAST(32 \<rightarrow> 12) (word_of_nat slot) = 0; Suc 0 \<le> slot; slot < 16\<rbrakk> \<Longrightarrow> ab = InvalidPDE
 2. \<And>s p pda. \<lbrakk>\<forall>sl. map (\<lambda>x. x + p) [0 , 4 .e. 0x3C] \<noteq> [sl]; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]; \<forall>x\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap s (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && mask pd_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> \<forall>sl\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). sl && ~~ mask pd_bits = hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits proof (prove)
goal (1 subgoal):
 1. \<And>s p pda. \<lbrakk>\<forall>sl. map (\<lambda>x. x + p) [0 , 4 .e. 0x3C] \<noteq> [sl]; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]; \<forall>x\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap s (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && mask pd_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> \<forall>sl\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). sl && ~~ mask pd_bits = hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits proof (prove)
goal (1 subgoal):
 1. \<And>s p pda x. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x. (\<exists>xa\<in>{Suc 0..<16}. x = word_of_nat xa * 4 + p) \<longrightarrow> pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := ab)))); Suc 0 \<le> x; x < 16\<rbrakk> \<Longrightarrow> word_of_nat x * 4 + p && ~~ mask pd_bits = p && ~~ mask pd_bits proof (prove)
goal (1 subgoal):
 1. \<And>s p pda x. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; bb = map ((+) p \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x. (\<exists>xa\<in>{Suc 0..<16}. x = p + word_of_nat xa * 4) \<longrightarrow> pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := ab)))); Suc 0 \<le> x; x < 16\<rbrakk> \<Longrightarrow> p + word_of_nat x * 4 && ~~ mask pd_bits = p && ~~ mask pd_bits proof (prove)
goal (1 subgoal):
 1. \<And>s p pda x. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; bb = map ((+) p \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x. (\<exists>xa\<in>{Suc 0..<16}. x = p + word_of_nat xa * 4) \<longrightarrow> pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pda)); a_type (ArchObj (arch_kernel_obj.PageDirectory pda)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := ab)))); Suc 0 \<le> x; x < 16\<rbrakk> \<Longrightarrow> word_of_nat x * 4 \<in> set [0 , 4 .e. 0x3C] proof (prove)
goal:
No subgoals!