theory Arch_DR

lemma store_pte_page_inv_entries_safe:
  "\<lbrace>page_inv_entries_safe (Inl (ab, bb)) and valid_pdpt_objs\<rbrace>
   store_pte (hd bb) ab
   \<lbrace>\<lambda>rv s. (\<exists>f. ko_at (ArchObj (arch_kernel_obj.PageTable f)) (hd bb && ~~ mask pt_bits)  s
    \<and> (\<forall>slot\<in>set (tl bb). f (ucast (slot && mask pt_bits >> 2)) = ARM_A.pte.InvalidPTE))
    \<and> (\<forall>sl\<in>set (tl bb). sl && ~~ mask pt_bits = hd bb && ~~ mask pt_bits)\<rbrace>" apply (simp add:store_pte_def set_pt_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 tl_map_simp
                         map_eq_Cons_conv upt_eq_Cons_conv upto_0_to_n) apply (simp add:field_simps) apply (subst (asm) shiftl_t2n[where n = 2,simplified field_simps,simplified,symmetric])+ apply (rename_tac s ptr pt slot) apply (subst (asm) and_mask_plus[where a = "of_nat slot << 2"]) apply (simp add:pt_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:pt_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_table_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 (Inl (ab, bb)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x)\<rbrace> store_pte (hd bb) ab \<lbrace>\<lambda>rv s. (\<exists>f. ako_at (arch_kernel_obj.PageTable f) (hd bb && ~~ mask pt_bits) s \<and> (\<forall>slot\<in>set (tl bb). f (UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2)) = InvalidPTE)) \<and> (\<forall>sl\<in>set (tl bb). sl && ~~ mask pt_bits = hd bb && ~~ mask pt_bits)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>page_inv_entries_safe (Inl (ab, bb)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x)\<rbrace> do pt <- get_pt (hd bb && ~~ mask pt_bits);
kobj <- KHeap_A.get_object (hd bb && ~~ mask pt_bits);
y <- assert (a_type kobj = a_type (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (hd bb && mask pt_bits >> 2) := ab)))));
s <- get;
put (update_kheap ((kheap s)(hd bb && ~~ mask pt_bits \<mapsto> ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (hd bb && mask pt_bits >> 2) := ab))))) s)
od \<lbrace>\<lambda>rv s. (\<exists>f. ako_at (arch_kernel_obj.PageTable f) (hd bb && ~~ mask pt_bits) s \<and> (\<forall>slot\<in>set (tl bb). f (UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2)) = InvalidPTE)) \<and> (\<forall>sl\<in>set (tl bb). sl && ~~ mask pt_bits = hd bb && ~~ mask pt_bits)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (page_inv_entries_safe (Inl (ab, bb)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x)) s \<Longrightarrow> \<forall>pt. ako_at (arch_kernel_obj.PageTable pt) (hd bb && ~~ mask pt_bits) s \<longrightarrow> (\<forall>ko. ko_at ko (hd bb && ~~ mask pt_bits) s \<longrightarrow> a_type ko = a_type (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (hd bb && mask pt_bits >> 2) := ab)))) \<longrightarrow> (\<exists>f. ako_at (arch_kernel_obj.PageTable f) (hd bb && ~~ mask pt_bits) (update_kheap ((kheap s)(hd bb && ~~ mask pt_bits \<mapsto> ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (hd bb && mask pt_bits >> 2) := ab))))) s) \<and> (\<forall>slot\<in>set (tl bb). f (UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2)) = InvalidPTE)) \<and> (\<forall>sl\<in>set (tl bb). sl && ~~ mask pt_bits = hd bb && ~~ mask pt_bits)) proof (prove)
goal (1 subgoal):
 1. \<And>s p pta. \<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])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap s (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pta)); a_type (ArchObj (arch_kernel_obj.PageTable pta)) = a_type (ArchObj (arch_kernel_obj.PageTable (pta(UCAST(32 \<rightarrow> 8) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && mask pt_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> ((\<exists>slot\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2) = UCAST(32 \<rightarrow> 8) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && mask pt_bits >> 2)) \<longrightarrow> ab = InvalidPTE) \<and> (\<forall>sl\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). sl && ~~ mask pt_bits = hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits) proof (prove)
goal (2 subgoals):
 1. \<And>s p pta. \<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])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap s (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pta)); a_type (ArchObj (arch_kernel_obj.PageTable pta)) = a_type (ArchObj (arch_kernel_obj.PageTable (pta(UCAST(32 \<rightarrow> 8) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && mask pt_bits >> 2) := ab)))); \<exists>slot\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2) = UCAST(32 \<rightarrow> 8) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && mask pt_bits >> 2)\<rbrakk> \<Longrightarrow> ab = InvalidPTE
 2. \<And>s p pta. \<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])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap s (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pta)); a_type (ArchObj (arch_kernel_obj.PageTable pta)) = a_type (ArchObj (arch_kernel_obj.PageTable (pta(UCAST(32 \<rightarrow> 8) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && mask pt_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> \<forall>sl\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). sl && ~~ mask pt_bits = hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits proof (prove)
goal (2 subgoals):
 1. \<And>s p pta 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}. pta (UCAST(32 \<rightarrow> 8) (word_of_nat x * 4 + p && mask pt_bits >> 2)) = InvalidPTE; kheap s (p && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pta)); a_type (ArchObj (arch_kernel_obj.PageTable pta)) = a_type (ArchObj (arch_kernel_obj.PageTable (pta(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := ab)))); UCAST(32 \<rightarrow> 8) (word_of_nat slot * 4 + p && mask pt_bits >> 2) = UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); Suc 0 \<le> slot; slot < 16\<rbrakk> \<Longrightarrow> ab = InvalidPTE
 2. \<And>s p pta. \<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])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap s (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pta)); a_type (ArchObj (arch_kernel_obj.PageTable pta)) = a_type (ArchObj (arch_kernel_obj.PageTable (pta(UCAST(32 \<rightarrow> 8) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && mask pt_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> \<forall>sl\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). sl && ~~ mask pt_bits = hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits proof (prove)
goal (2 subgoals):
 1. \<And>s p pta 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}. pta (UCAST(32 \<rightarrow> 8) (p + word_of_nat x * 4 && mask pt_bits >> 2)) = InvalidPTE; kheap s (p && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pta)); a_type (ArchObj (arch_kernel_obj.PageTable pta)) = a_type (ArchObj (arch_kernel_obj.PageTable (pta(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := ab)))); UCAST(32 \<rightarrow> 8) (p + word_of_nat slot * 4 && mask pt_bits >> 2) = UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); Suc 0 \<le> slot; slot < 16\<rbrakk> \<Longrightarrow> ab = InvalidPTE
 2. \<And>s p pta. \<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])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap s (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pta)); a_type (ArchObj (arch_kernel_obj.PageTable pta)) = a_type (ArchObj (arch_kernel_obj.PageTable (pta(UCAST(32 \<rightarrow> 8) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && mask pt_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> \<forall>sl\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). sl && ~~ mask pt_bits = hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits proof (prove)
goal (2 subgoals):
 1. \<And>s p pta 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}. pta (UCAST(32 \<rightarrow> 8) (p + (word_of_nat x << 2) && mask pt_bits >> 2)) = InvalidPTE; kheap s (p && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pta)); a_type (ArchObj (arch_kernel_obj.PageTable pta)) = a_type (ArchObj (arch_kernel_obj.PageTable (pta(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := ab)))); UCAST(32 \<rightarrow> 8) (p + (word_of_nat slot << 2) && mask pt_bits >> 2) = UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); Suc 0 \<le> slot; slot < 16\<rbrakk> \<Longrightarrow> ab = InvalidPTE
 2. \<And>s p pta. \<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])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap s (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pta)); a_type (ArchObj (arch_kernel_obj.PageTable pta)) = a_type (ArchObj (arch_kernel_obj.PageTable (pta(UCAST(32 \<rightarrow> 8) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && mask pt_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> \<forall>sl\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). sl && ~~ mask pt_bits = hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits proof (prove)
goal (2 subgoals):
 1. \<And>s ptr pt slot. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned ptr 6; bb = map ((+) ptr \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pt (UCAST(32 \<rightarrow> 8) (ptr + (word_of_nat x << 2) && mask pt_bits >> 2)) = InvalidPTE; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pt)); a_type (ArchObj (arch_kernel_obj.PageTable pt)) = a_type (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := ab)))); UCAST(32 \<rightarrow> 8) (ptr + (word_of_nat slot << 2) && mask pt_bits >> 2) = UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2); Suc 0 \<le> slot; slot < 16\<rbrakk> \<Longrightarrow> ab = InvalidPTE
 2. \<And>s p pta. \<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])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap s (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pta)); a_type (ArchObj (arch_kernel_obj.PageTable pta)) = a_type (ArchObj (arch_kernel_obj.PageTable (pta(UCAST(32 \<rightarrow> 8) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && mask pt_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> \<forall>sl\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). sl && ~~ mask pt_bits = hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits proof (prove)
goal (6 subgoals):
 1. \<And>s ptr pt slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned ptr 6; bb = map ((+) ptr \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pt (UCAST(32 \<rightarrow> 8) (ptr + (word_of_nat x << 2) && mask pt_bits >> 2)) = InvalidPTE; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pt)); a_type (ArchObj (arch_kernel_obj.PageTable pt)) = a_type (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> is_aligned ptr (?m67 s ptr pt slot)
 2. \<And>s ptr pt slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned ptr 6; bb = map ((+) ptr \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pt (UCAST(32 \<rightarrow> 8) (ptr + (word_of_nat x << 2) && mask pt_bits >> 2)) = InvalidPTE; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pt)); a_type (ArchObj (arch_kernel_obj.PageTable pt)) = a_type (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> ?m67 s ptr pt slot \<le> pt_bits
 3. \<And>s ptr pt slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned ptr 6; bb = map ((+) ptr \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pt (UCAST(32 \<rightarrow> 8) (ptr + (word_of_nat x << 2) && mask pt_bits >> 2)) = InvalidPTE; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pt)); a_type (ArchObj (arch_kernel_obj.PageTable pt)) = a_type (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> pt_bits < 32
 4. \<And>s ptr pt slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned ptr 6; bb = map ((+) ptr \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pt (UCAST(32 \<rightarrow> 8) (ptr + (word_of_nat x << 2) && mask pt_bits >> 2)) = InvalidPTE; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pt)); a_type (ArchObj (arch_kernel_obj.PageTable pt)) = a_type (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> word_of_nat slot << 2 < 2 ^ ?m67 s ptr pt slot
 5. \<And>s ptr pt slot. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned ptr 6; bb = map ((+) ptr \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pt (UCAST(32 \<rightarrow> 8) (ptr + (word_of_nat x << 2) && mask pt_bits >> 2)) = InvalidPTE; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pt)); a_type (ArchObj (arch_kernel_obj.PageTable pt)) = a_type (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := ab)))); UCAST(32 \<rightarrow> 8) ((ptr && mask pt_bits) + (word_of_nat slot << 2) >> 2) = UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2); Suc 0 \<le> slot; slot < 16\<rbrakk> \<Longrightarrow> ab = InvalidPTE
 6. \<And>s p pta. \<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])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap s (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pta)); a_type (ArchObj (arch_kernel_obj.PageTable pta)) = a_type (ArchObj (arch_kernel_obj.PageTable (pta(UCAST(32 \<rightarrow> 8) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && mask pt_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> \<forall>sl\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). sl && ~~ mask pt_bits = hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits proof (prove)
goal (3 subgoals):
 1. \<And>s ptr pt slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned ptr 6; bb = map ((+) ptr \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pt (UCAST(32 \<rightarrow> 8) (ptr + (word_of_nat x << 2) && mask 10 >> 2)) = InvalidPTE; kheap s (ptr && ~~ mask 10) = Some (ArchObj (arch_kernel_obj.PageTable pt)); a_type (ArchObj (arch_kernel_obj.PageTable pt)) = a_type (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (ptr && mask 10 >> 2) := ab))))\<rbrakk> \<Longrightarrow> word_of_nat slot << 2 < 0x40
 2. \<And>s ptr pt slot. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned ptr 6; bb = map ((+) ptr \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pt (UCAST(32 \<rightarrow> 8) (ptr + (word_of_nat x << 2) && mask pt_bits >> 2)) = InvalidPTE; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pt)); a_type (ArchObj (arch_kernel_obj.PageTable pt)) = a_type (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := ab)))); UCAST(32 \<rightarrow> 8) ((ptr && mask pt_bits) + (word_of_nat slot << 2) >> 2) = UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2); Suc 0 \<le> slot; slot < 16\<rbrakk> \<Longrightarrow> ab = InvalidPTE
 3. \<And>s p pta. \<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])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap s (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pta)); a_type (ArchObj (arch_kernel_obj.PageTable pta)) = a_type (ArchObj (arch_kernel_obj.PageTable (pta(UCAST(32 \<rightarrow> 8) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && mask pt_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> \<forall>sl\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). sl && ~~ mask pt_bits = hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits proof (prove)
goal (4 subgoals):
 1. \<And>s ptr pt slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned ptr 6; bb = map ((+) ptr \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pt (UCAST(32 \<rightarrow> 8) (ptr + (word_of_nat x << 2) && mask 10 >> 2)) = InvalidPTE; kheap s (ptr && ~~ mask 10) = Some (ArchObj (arch_kernel_obj.PageTable pt)); a_type (ArchObj (arch_kernel_obj.PageTable pt)) = a_type (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (ptr && mask 10 >> 2) := ab))))\<rbrakk> \<Longrightarrow> word_of_nat slot < 2 ^ (6 - 2)
 2. \<And>s ptr pt slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned ptr 6; bb = map ((+) ptr \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pt (UCAST(32 \<rightarrow> 8) (ptr + (word_of_nat x << 2) && mask 10 >> 2)) = InvalidPTE; kheap s (ptr && ~~ mask 10) = Some (ArchObj (arch_kernel_obj.PageTable pt)); a_type (ArchObj (arch_kernel_obj.PageTable pt)) = a_type (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (ptr && mask 10 >> 2) := ab))))\<rbrakk> \<Longrightarrow> 6 < LENGTH(32)
 3. \<And>s ptr pt slot. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned ptr 6; bb = map ((+) ptr \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pt (UCAST(32 \<rightarrow> 8) (ptr + (word_of_nat x << 2) && mask pt_bits >> 2)) = InvalidPTE; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pt)); a_type (ArchObj (arch_kernel_obj.PageTable pt)) = a_type (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := ab)))); UCAST(32 \<rightarrow> 8) ((ptr && mask pt_bits) + (word_of_nat slot << 2) >> 2) = UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2); Suc 0 \<le> slot; slot < 16\<rbrakk> \<Longrightarrow> ab = InvalidPTE
 4. \<And>s p pta. \<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])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap s (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pta)); a_type (ArchObj (arch_kernel_obj.PageTable pta)) = a_type (ArchObj (arch_kernel_obj.PageTable (pta(UCAST(32 \<rightarrow> 8) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && mask pt_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> \<forall>sl\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). sl && ~~ mask pt_bits = hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits proof (prove)
goal (3 subgoals):
 1. \<And>s ptr pt slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned ptr 6; bb = map ((+) ptr \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pt (UCAST(32 \<rightarrow> 8) (ptr + (word_of_nat x << 2) && mask 10 >> 2)) = InvalidPTE; kheap s (ptr && ~~ mask 10) = Some (ArchObj (arch_kernel_obj.PageTable pt)); a_type (ArchObj (arch_kernel_obj.PageTable pt)) = a_type (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (ptr && mask 10 >> 2) := ab))))\<rbrakk> \<Longrightarrow> 6 < LENGTH(32)
 2. \<And>s ptr pt slot. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned ptr 6; bb = map ((+) ptr \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pt (UCAST(32 \<rightarrow> 8) (ptr + (word_of_nat x << 2) && mask pt_bits >> 2)) = InvalidPTE; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pt)); a_type (ArchObj (arch_kernel_obj.PageTable pt)) = a_type (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := ab)))); UCAST(32 \<rightarrow> 8) ((ptr && mask pt_bits) + (word_of_nat slot << 2) >> 2) = UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2); Suc 0 \<le> slot; slot < 16\<rbrakk> \<Longrightarrow> ab = InvalidPTE
 3. \<And>s p pta. \<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])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap s (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pta)); a_type (ArchObj (arch_kernel_obj.PageTable pta)) = a_type (ArchObj (arch_kernel_obj.PageTable (pta(UCAST(32 \<rightarrow> 8) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && mask pt_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> \<forall>sl\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). sl && ~~ mask pt_bits = hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits proof (prove)
goal (2 subgoals):
 1. \<And>s ptr pt slot. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned ptr 6; bb = map ((+) ptr \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pt (UCAST(32 \<rightarrow> 8) (ptr + (word_of_nat x << 2) && mask pt_bits >> 2)) = InvalidPTE; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pt)); a_type (ArchObj (arch_kernel_obj.PageTable pt)) = a_type (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := ab)))); UCAST(32 \<rightarrow> 8) ((ptr && mask pt_bits) + (word_of_nat slot << 2) >> 2) = UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2); Suc 0 \<le> slot; slot < 16\<rbrakk> \<Longrightarrow> ab = InvalidPTE
 2. \<And>s p pta. \<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])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap s (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pta)); a_type (ArchObj (arch_kernel_obj.PageTable pta)) = a_type (ArchObj (arch_kernel_obj.PageTable (pta(UCAST(32 \<rightarrow> 8) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && mask pt_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> \<forall>sl\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). sl && ~~ mask pt_bits = hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits proof (prove)
goal (7 subgoals):
 1. \<And>s ptr pt slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned ptr 6; bb = map ((+) ptr \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pt (UCAST(32 \<rightarrow> 8) (ptr + (word_of_nat x << 2) && mask pt_bits >> 2)) = InvalidPTE; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pt)); a_type (ArchObj (arch_kernel_obj.PageTable pt)) = a_type (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> is_aligned (ptr && mask pt_bits) (?n80 s ptr pt slot)
 2. \<And>s ptr pt slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned ptr 6; bb = map ((+) ptr \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pt (UCAST(32 \<rightarrow> 8) (ptr + (word_of_nat x << 2) && mask pt_bits >> 2)) = InvalidPTE; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pt)); a_type (ArchObj (arch_kernel_obj.PageTable pt)) = a_type (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> is_aligned (word_of_nat slot << 2) 2
 3. \<And>s ptr pt slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned ptr 6; bb = map ((+) ptr \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pt (UCAST(32 \<rightarrow> 8) (ptr + (word_of_nat x << 2) && mask pt_bits >> 2)) = InvalidPTE; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pt)); a_type (ArchObj (arch_kernel_obj.PageTable pt)) = a_type (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> word_of_nat slot << 2 < 2 ^ ?n80 s ptr pt slot
 4. \<And>s ptr pt slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned ptr 6; bb = map ((+) ptr \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pt (UCAST(32 \<rightarrow> 8) (ptr + (word_of_nat x << 2) && mask pt_bits >> 2)) = InvalidPTE; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pt)); a_type (ArchObj (arch_kernel_obj.PageTable pt)) = a_type (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> 2 \<le> ?n80 s ptr pt slot
 5. \<And>s ptr pt slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned ptr 6; bb = map ((+) ptr \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pt (UCAST(32 \<rightarrow> 8) (ptr + (word_of_nat x << 2) && mask pt_bits >> 2)) = InvalidPTE; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pt)); a_type (ArchObj (arch_kernel_obj.PageTable pt)) = a_type (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> ?n80 s ptr pt slot < LENGTH(32)
 6. \<And>s ptr pt slot. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned ptr 6; bb = map ((+) ptr \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pt (UCAST(32 \<rightarrow> 8) (ptr + (word_of_nat x << 2) && mask pt_bits >> 2)) = InvalidPTE; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pt)); a_type (ArchObj (arch_kernel_obj.PageTable pt)) = a_type (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := ab)))); UCAST(32 \<rightarrow> 8) ((ptr && mask pt_bits >> 2) + (word_of_nat slot << 2 >> 2)) = UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2); Suc 0 \<le> slot; slot < 16\<rbrakk> \<Longrightarrow> ab = InvalidPTE
 7. \<And>s p pta. \<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])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap s (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pta)); a_type (ArchObj (arch_kernel_obj.PageTable pta)) = a_type (ArchObj (arch_kernel_obj.PageTable (pta(UCAST(32 \<rightarrow> 8) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && mask pt_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> \<forall>sl\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). sl && ~~ mask pt_bits = hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits proof (prove)
goal (7 subgoals):
 1. \<And>s ptr pt slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; bb = map ((+) ptr \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pt (UCAST(32 \<rightarrow> 8) (ptr + (word_of_nat x << 2) && mask pt_bits >> 2)) = InvalidPTE; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pt)); a_type (ArchObj (arch_kernel_obj.PageTable pt)) = a_type (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> 6 \<le> pt_bits
 2. \<And>s ptr pt slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned ptr 6; bb = map ((+) ptr \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pt (UCAST(32 \<rightarrow> 8) (ptr + (word_of_nat x << 2) && mask pt_bits >> 2)) = InvalidPTE; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pt)); a_type (ArchObj (arch_kernel_obj.PageTable pt)) = a_type (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> is_aligned (word_of_nat slot << 2) 2
 3. \<And>s ptr pt slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned ptr 6; bb = map ((+) ptr \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pt (UCAST(32 \<rightarrow> 8) (ptr + (word_of_nat x << 2) && mask pt_bits >> 2)) = InvalidPTE; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pt)); a_type (ArchObj (arch_kernel_obj.PageTable pt)) = a_type (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> word_of_nat slot << 2 < 2 ^ 6
 4. \<And>s ptr pt slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned ptr 6; bb = map ((+) ptr \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pt (UCAST(32 \<rightarrow> 8) (ptr + (word_of_nat x << 2) && mask pt_bits >> 2)) = InvalidPTE; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pt)); a_type (ArchObj (arch_kernel_obj.PageTable pt)) = a_type (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> 2 \<le> 6
 5. \<And>s ptr pt slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned ptr 6; bb = map ((+) ptr \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pt (UCAST(32 \<rightarrow> 8) (ptr + (word_of_nat x << 2) && mask pt_bits >> 2)) = InvalidPTE; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pt)); a_type (ArchObj (arch_kernel_obj.PageTable pt)) = a_type (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> 6 < LENGTH(32)
 6. \<And>s ptr pt slot. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned ptr 6; bb = map ((+) ptr \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pt (UCAST(32 \<rightarrow> 8) (ptr + (word_of_nat x << 2) && mask pt_bits >> 2)) = InvalidPTE; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pt)); a_type (ArchObj (arch_kernel_obj.PageTable pt)) = a_type (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := ab)))); UCAST(32 \<rightarrow> 8) ((ptr && mask pt_bits >> 2) + (word_of_nat slot << 2 >> 2)) = UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2); Suc 0 \<le> slot; slot < 16\<rbrakk> \<Longrightarrow> ab = InvalidPTE
 7. \<And>s p pta. \<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])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap s (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pta)); a_type (ArchObj (arch_kernel_obj.PageTable pta)) = a_type (ArchObj (arch_kernel_obj.PageTable (pta(UCAST(32 \<rightarrow> 8) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && mask pt_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> \<forall>sl\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). sl && ~~ mask pt_bits = hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits proof (prove)
goal (6 subgoals):
 1. \<And>s ptr pt slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned ptr 6; bb = map ((+) ptr \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pt (UCAST(32 \<rightarrow> 8) (ptr + (word_of_nat x << 2) && mask 10 >> 2)) = InvalidPTE; kheap s (ptr && ~~ mask 10) = Some (ArchObj (arch_kernel_obj.PageTable pt)); a_type (ArchObj (arch_kernel_obj.PageTable pt)) = a_type (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (ptr && mask 10 >> 2) := ab))))\<rbrakk> \<Longrightarrow> is_aligned (word_of_nat slot << 2) 2
 2. \<And>s ptr pt slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned ptr 6; bb = map ((+) ptr \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pt (UCAST(32 \<rightarrow> 8) (ptr + (word_of_nat x << 2) && mask pt_bits >> 2)) = InvalidPTE; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pt)); a_type (ArchObj (arch_kernel_obj.PageTable pt)) = a_type (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> word_of_nat slot << 2 < 2 ^ 6
 3. \<And>s ptr pt slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned ptr 6; bb = map ((+) ptr \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pt (UCAST(32 \<rightarrow> 8) (ptr + (word_of_nat x << 2) && mask pt_bits >> 2)) = InvalidPTE; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pt)); a_type (ArchObj (arch_kernel_obj.PageTable pt)) = a_type (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> 2 \<le> 6
 4. \<And>s ptr pt slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned ptr 6; bb = map ((+) ptr \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pt (UCAST(32 \<rightarrow> 8) (ptr + (word_of_nat x << 2) && mask pt_bits >> 2)) = InvalidPTE; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pt)); a_type (ArchObj (arch_kernel_obj.PageTable pt)) = a_type (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> 6 < LENGTH(32)
 5. \<And>s ptr pt slot. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned ptr 6; bb = map ((+) ptr \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pt (UCAST(32 \<rightarrow> 8) (ptr + (word_of_nat x << 2) && mask pt_bits >> 2)) = InvalidPTE; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pt)); a_type (ArchObj (arch_kernel_obj.PageTable pt)) = a_type (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := ab)))); UCAST(32 \<rightarrow> 8) ((ptr && mask pt_bits >> 2) + (word_of_nat slot << 2 >> 2)) = UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2); Suc 0 \<le> slot; slot < 16\<rbrakk> \<Longrightarrow> ab = InvalidPTE
 6. \<And>s p pta. \<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])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap s (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pta)); a_type (ArchObj (arch_kernel_obj.PageTable pta)) = a_type (ArchObj (arch_kernel_obj.PageTable (pta(UCAST(32 \<rightarrow> 8) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && mask pt_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> \<forall>sl\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). sl && ~~ mask pt_bits = hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits proof (prove)
goal (5 subgoals):
 1. \<And>s ptr pt slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned ptr 6; bb = map ((+) ptr \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pt (UCAST(32 \<rightarrow> 8) (ptr + (word_of_nat x << 2) && mask pt_bits >> 2)) = InvalidPTE; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pt)); a_type (ArchObj (arch_kernel_obj.PageTable pt)) = a_type (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> word_of_nat slot << 2 < 2 ^ 6
 2. \<And>s ptr pt slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned ptr 6; bb = map ((+) ptr \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pt (UCAST(32 \<rightarrow> 8) (ptr + (word_of_nat x << 2) && mask pt_bits >> 2)) = InvalidPTE; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pt)); a_type (ArchObj (arch_kernel_obj.PageTable pt)) = a_type (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> 2 \<le> 6
 3. \<And>s ptr pt slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned ptr 6; bb = map ((+) ptr \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pt (UCAST(32 \<rightarrow> 8) (ptr + (word_of_nat x << 2) && mask pt_bits >> 2)) = InvalidPTE; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pt)); a_type (ArchObj (arch_kernel_obj.PageTable pt)) = a_type (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> 6 < LENGTH(32)
 4. \<And>s ptr pt slot. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned ptr 6; bb = map ((+) ptr \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pt (UCAST(32 \<rightarrow> 8) (ptr + (word_of_nat x << 2) && mask pt_bits >> 2)) = InvalidPTE; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pt)); a_type (ArchObj (arch_kernel_obj.PageTable pt)) = a_type (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := ab)))); UCAST(32 \<rightarrow> 8) ((ptr && mask pt_bits >> 2) + (word_of_nat slot << 2 >> 2)) = UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2); Suc 0 \<le> slot; slot < 16\<rbrakk> \<Longrightarrow> ab = InvalidPTE
 5. \<And>s p pta. \<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])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap s (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pta)); a_type (ArchObj (arch_kernel_obj.PageTable pta)) = a_type (ArchObj (arch_kernel_obj.PageTable (pta(UCAST(32 \<rightarrow> 8) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && mask pt_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> \<forall>sl\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). sl && ~~ mask pt_bits = hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits proof (prove)
goal (6 subgoals):
 1. \<And>s ptr pt slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned ptr 6; bb = map ((+) ptr \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pt (UCAST(32 \<rightarrow> 8) (ptr + (word_of_nat x << 2) && mask pt_bits >> 2)) = InvalidPTE; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pt)); a_type (ArchObj (arch_kernel_obj.PageTable pt)) = a_type (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> word_of_nat slot < 2 ^ (6 - 2)
 2. \<And>s ptr pt slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned ptr 6; bb = map ((+) ptr \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pt (UCAST(32 \<rightarrow> 8) (ptr + (word_of_nat x << 2) && mask pt_bits >> 2)) = InvalidPTE; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pt)); a_type (ArchObj (arch_kernel_obj.PageTable pt)) = a_type (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> 6 < LENGTH(32)
 3. \<And>s ptr pt slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned ptr 6; bb = map ((+) ptr \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pt (UCAST(32 \<rightarrow> 8) (ptr + (word_of_nat x << 2) && mask pt_bits >> 2)) = InvalidPTE; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pt)); a_type (ArchObj (arch_kernel_obj.PageTable pt)) = a_type (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> 2 \<le> 6
 4. \<And>s ptr pt slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned ptr 6; bb = map ((+) ptr \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pt (UCAST(32 \<rightarrow> 8) (ptr + (word_of_nat x << 2) && mask pt_bits >> 2)) = InvalidPTE; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pt)); a_type (ArchObj (arch_kernel_obj.PageTable pt)) = a_type (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> 6 < LENGTH(32)
 5. \<And>s ptr pt slot. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned ptr 6; bb = map ((+) ptr \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pt (UCAST(32 \<rightarrow> 8) (ptr + (word_of_nat x << 2) && mask pt_bits >> 2)) = InvalidPTE; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pt)); a_type (ArchObj (arch_kernel_obj.PageTable pt)) = a_type (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := ab)))); UCAST(32 \<rightarrow> 8) ((ptr && mask pt_bits >> 2) + (word_of_nat slot << 2 >> 2)) = UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2); Suc 0 \<le> slot; slot < 16\<rbrakk> \<Longrightarrow> ab = InvalidPTE
 6. \<And>s p pta. \<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])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap s (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pta)); a_type (ArchObj (arch_kernel_obj.PageTable pta)) = a_type (ArchObj (arch_kernel_obj.PageTable (pta(UCAST(32 \<rightarrow> 8) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && mask pt_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> \<forall>sl\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). sl && ~~ mask pt_bits = hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits proof (prove)
goal (5 subgoals):
 1. \<And>s ptr pt slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned ptr 6; bb = map ((+) ptr \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pt (UCAST(32 \<rightarrow> 8) (ptr + (word_of_nat x << 2) && mask pt_bits >> 2)) = InvalidPTE; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pt)); a_type (ArchObj (arch_kernel_obj.PageTable pt)) = a_type (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> 6 < LENGTH(32)
 2. \<And>s ptr pt slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned ptr 6; bb = map ((+) ptr \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pt (UCAST(32 \<rightarrow> 8) (ptr + (word_of_nat x << 2) && mask pt_bits >> 2)) = InvalidPTE; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pt)); a_type (ArchObj (arch_kernel_obj.PageTable pt)) = a_type (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> 2 \<le> 6
 3. \<And>s ptr pt slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned ptr 6; bb = map ((+) ptr \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pt (UCAST(32 \<rightarrow> 8) (ptr + (word_of_nat x << 2) && mask pt_bits >> 2)) = InvalidPTE; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pt)); a_type (ArchObj (arch_kernel_obj.PageTable pt)) = a_type (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> 6 < LENGTH(32)
 4. \<And>s ptr pt slot. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned ptr 6; bb = map ((+) ptr \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pt (UCAST(32 \<rightarrow> 8) (ptr + (word_of_nat x << 2) && mask pt_bits >> 2)) = InvalidPTE; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pt)); a_type (ArchObj (arch_kernel_obj.PageTable pt)) = a_type (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := ab)))); UCAST(32 \<rightarrow> 8) ((ptr && mask pt_bits >> 2) + (word_of_nat slot << 2 >> 2)) = UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2); Suc 0 \<le> slot; slot < 16\<rbrakk> \<Longrightarrow> ab = InvalidPTE
 5. \<And>s p pta. \<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])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap s (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pta)); a_type (ArchObj (arch_kernel_obj.PageTable pta)) = a_type (ArchObj (arch_kernel_obj.PageTable (pta(UCAST(32 \<rightarrow> 8) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && mask pt_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> \<forall>sl\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). sl && ~~ mask pt_bits = hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits proof (prove)
goal (2 subgoals):
 1. \<And>s ptr pt slot. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned ptr 6; bb = map ((+) ptr \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pt (UCAST(32 \<rightarrow> 8) (ptr + (word_of_nat x << 2) && mask pt_bits >> 2)) = InvalidPTE; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pt)); a_type (ArchObj (arch_kernel_obj.PageTable pt)) = a_type (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := ab)))); UCAST(32 \<rightarrow> 8) ((ptr && mask pt_bits >> 2) + (word_of_nat slot << 2 >> 2)) = UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2); Suc 0 \<le> slot; slot < 16\<rbrakk> \<Longrightarrow> ab = InvalidPTE
 2. \<And>s p pta. \<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])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap s (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pta)); a_type (ArchObj (arch_kernel_obj.PageTable pta)) = a_type (ArchObj (arch_kernel_obj.PageTable (pta(UCAST(32 \<rightarrow> 8) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && mask pt_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> \<forall>sl\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). sl && ~~ mask pt_bits = hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits proof (prove)
goal (3 subgoals):
 1. \<And>s ptr pt slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned ptr 6; bb = map ((+) ptr \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pt (UCAST(32 \<rightarrow> 8) (ptr + (word_of_nat x << 2) && mask pt_bits >> 2)) = InvalidPTE; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pt)); a_type (ArchObj (arch_kernel_obj.PageTable pt)) = a_type (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> LENGTH(8) \<le> LENGTH(32)
 2. \<And>s ptr pt slot. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned ptr 6; bb = map ((+) ptr \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pt (UCAST(32 \<rightarrow> 8) (ptr + (word_of_nat x << 2) && mask pt_bits >> 2)) = InvalidPTE; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pt)); a_type (ArchObj (arch_kernel_obj.PageTable pt)) = a_type (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := ab)))); UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) + UCAST(32 \<rightarrow> 8) (word_of_nat slot << 2 >> 2) = UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2); Suc 0 \<le> slot; slot < 16\<rbrakk> \<Longrightarrow> ab = InvalidPTE
 3. \<And>s p pta. \<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])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap s (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pta)); a_type (ArchObj (arch_kernel_obj.PageTable pta)) = a_type (ArchObj (arch_kernel_obj.PageTable (pta(UCAST(32 \<rightarrow> 8) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && mask pt_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> \<forall>sl\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). sl && ~~ mask pt_bits = hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits proof (prove)
goal (2 subgoals):
 1. \<And>s ptr pt slot. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned ptr 6; bb = map ((+) ptr \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pt (UCAST(32 \<rightarrow> 8) (ptr + (word_of_nat x << 2) && mask pt_bits >> 2)) = InvalidPTE; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pt)); a_type (ArchObj (arch_kernel_obj.PageTable pt)) = a_type (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := ab)))); UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) + UCAST(32 \<rightarrow> 8) (word_of_nat slot << 2 >> 2) = UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2); Suc 0 \<le> slot; slot < 16\<rbrakk> \<Longrightarrow> ab = InvalidPTE
 2. \<And>s p pta. \<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])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap s (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pta)); a_type (ArchObj (arch_kernel_obj.PageTable pta)) = a_type (ArchObj (arch_kernel_obj.PageTable (pta(UCAST(32 \<rightarrow> 8) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && mask pt_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> \<forall>sl\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). sl && ~~ mask pt_bits = hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits proof (prove)
goal (2 subgoals):
 1. \<And>s ptr pt slot. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned ptr 6; bb = map ((+) ptr \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pt (UCAST(32 \<rightarrow> 8) (ptr + (word_of_nat x << 2) && mask pt_bits >> 2)) = InvalidPTE; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pt)); a_type (ArchObj (arch_kernel_obj.PageTable pt)) = a_type (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := ab)))); UCAST(32 \<rightarrow> 8) (word_of_nat slot << 2 >> 2) = 0; Suc 0 \<le> slot; slot < 16\<rbrakk> \<Longrightarrow> ab = InvalidPTE
 2. \<And>s p pta. \<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])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap s (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pta)); a_type (ArchObj (arch_kernel_obj.PageTable pta)) = a_type (ArchObj (arch_kernel_obj.PageTable (pta(UCAST(32 \<rightarrow> 8) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && mask pt_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> \<forall>sl\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). sl && ~~ mask pt_bits = hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits proof (prove)
goal (4 subgoals):
 1. \<And>s ptr pt slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned ptr 6; bb = map ((+) ptr \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pt (UCAST(32 \<rightarrow> 8) (ptr + (word_of_nat x << 2) && mask pt_bits >> 2)) = InvalidPTE; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pt)); a_type (ArchObj (arch_kernel_obj.PageTable pt)) = a_type (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> 2 < LENGTH(32)
 2. \<And>s ptr pt slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned ptr 6; bb = map ((+) ptr \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pt (UCAST(32 \<rightarrow> 8) (ptr + (word_of_nat x << 2) && mask pt_bits >> 2)) = InvalidPTE; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pt)); a_type (ArchObj (arch_kernel_obj.PageTable pt)) = a_type (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> word_of_nat slot < 2 ^ (LENGTH(32) - 2)
 3. \<And>s ptr pt slot. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned ptr 6; bb = map ((+) ptr \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pt (UCAST(32 \<rightarrow> 8) (ptr + (word_of_nat x << 2) && mask pt_bits >> 2)) = InvalidPTE; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pt)); a_type (ArchObj (arch_kernel_obj.PageTable pt)) = a_type (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := ab)))); UCAST(32 \<rightarrow> 8) (word_of_nat slot) = 0; Suc 0 \<le> slot; slot < 16\<rbrakk> \<Longrightarrow> ab = InvalidPTE
 4. \<And>s p pta. \<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])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap s (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pta)); a_type (ArchObj (arch_kernel_obj.PageTable pta)) = a_type (ArchObj (arch_kernel_obj.PageTable (pta(UCAST(32 \<rightarrow> 8) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && mask pt_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> \<forall>sl\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). sl && ~~ mask pt_bits = hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits proof (prove)
goal (3 subgoals):
 1. \<And>s ptr pt slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned ptr 6; bb = map ((+) ptr \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pt (UCAST(32 \<rightarrow> 8) (ptr + (word_of_nat x << 2) && mask pt_bits >> 2)) = InvalidPTE; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pt)); a_type (ArchObj (arch_kernel_obj.PageTable pt)) = a_type (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> word_of_nat slot < 2 ^ (LENGTH(32) - 2)
 2. \<And>s ptr pt slot. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned ptr 6; bb = map ((+) ptr \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pt (UCAST(32 \<rightarrow> 8) (ptr + (word_of_nat x << 2) && mask pt_bits >> 2)) = InvalidPTE; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pt)); a_type (ArchObj (arch_kernel_obj.PageTable pt)) = a_type (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := ab)))); UCAST(32 \<rightarrow> 8) (word_of_nat slot) = 0; Suc 0 \<le> slot; slot < 16\<rbrakk> \<Longrightarrow> ab = InvalidPTE
 3. \<And>s p pta. \<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])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap s (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pta)); a_type (ArchObj (arch_kernel_obj.PageTable pta)) = a_type (ArchObj (arch_kernel_obj.PageTable (pta(UCAST(32 \<rightarrow> 8) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && mask pt_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> \<forall>sl\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). sl && ~~ mask pt_bits = hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits proof (prove)
goal (3 subgoals):
 1. \<And>s ptr pt slot. \<lbrakk>Suc 0 \<le> slot; slot < 16; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned ptr 6; bb = map ((+) ptr \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pt (UCAST(32 \<rightarrow> 8) (ptr + (word_of_nat x << 2) && mask pt_bits >> 2)) = InvalidPTE; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pt)); a_type (ArchObj (arch_kernel_obj.PageTable pt)) = a_type (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> slot < unat (2 ^ (LENGTH(32) - 2))
 2. \<And>s ptr pt slot. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned ptr 6; bb = map ((+) ptr \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pt (UCAST(32 \<rightarrow> 8) (ptr + (word_of_nat x << 2) && mask pt_bits >> 2)) = InvalidPTE; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pt)); a_type (ArchObj (arch_kernel_obj.PageTable pt)) = a_type (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := ab)))); UCAST(32 \<rightarrow> 8) (word_of_nat slot) = 0; Suc 0 \<le> slot; slot < 16\<rbrakk> \<Longrightarrow> ab = InvalidPTE
 3. \<And>s p pta. \<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])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap s (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pta)); a_type (ArchObj (arch_kernel_obj.PageTable pta)) = a_type (ArchObj (arch_kernel_obj.PageTable (pta(UCAST(32 \<rightarrow> 8) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && mask pt_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> \<forall>sl\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). sl && ~~ mask pt_bits = hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits proof (prove)
goal (2 subgoals):
 1. \<And>s ptr pt slot. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned ptr 6; bb = map ((+) ptr \<circ> ((\<lambda>x. x << 2) \<circ> toEnum)) [0..<16]; \<forall>x\<in>{Suc 0..<16}. pt (UCAST(32 \<rightarrow> 8) (ptr + (word_of_nat x << 2) && mask pt_bits >> 2)) = InvalidPTE; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pt)); a_type (ArchObj (arch_kernel_obj.PageTable pt)) = a_type (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := ab)))); UCAST(32 \<rightarrow> 8) (word_of_nat slot) = 0; Suc 0 \<le> slot; slot < 16\<rbrakk> \<Longrightarrow> ab = InvalidPTE
 2. \<And>s p pta. \<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])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap s (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pta)); a_type (ArchObj (arch_kernel_obj.PageTable pta)) = a_type (ArchObj (arch_kernel_obj.PageTable (pta(UCAST(32 \<rightarrow> 8) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && mask pt_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> \<forall>sl\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). sl && ~~ mask pt_bits = hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits proof (prove)
goal (1 subgoal):
 1. \<And>s p pta. \<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])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap s (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pta)); a_type (ArchObj (arch_kernel_obj.PageTable pta)) = a_type (ArchObj (arch_kernel_obj.PageTable (pta(UCAST(32 \<rightarrow> 8) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && mask pt_bits >> 2) := ab))))\<rbrakk> \<Longrightarrow> \<forall>sl\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). sl && ~~ mask pt_bits = hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits proof (prove)
goal (1 subgoal):
 1. \<And>s p pta 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> pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap s (p && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pta)); a_type (ArchObj (arch_kernel_obj.PageTable pta)) = a_type (ArchObj (arch_kernel_obj.PageTable (pta(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := ab)))); Suc 0 \<le> x; x < 16\<rbrakk> \<Longrightarrow> word_of_nat x * 4 + p && ~~ mask pt_bits = p && ~~ mask pt_bits proof (prove)
goal (1 subgoal):
 1. \<And>s p pta 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> pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap s (p && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pta)); a_type (ArchObj (arch_kernel_obj.PageTable pta)) = a_type (ArchObj (arch_kernel_obj.PageTable (pta(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := ab)))); Suc 0 \<le> x; x < 16\<rbrakk> \<Longrightarrow> p + word_of_nat x * 4 && ~~ mask pt_bits = p && ~~ mask pt_bits proof (prove)
goal (1 subgoal):
 1. \<And>s p pta 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> pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap s (p && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable pta)); a_type (ArchObj (arch_kernel_obj.PageTable pta)) = a_type (ArchObj (arch_kernel_obj.PageTable (pta(UCAST(32 \<rightarrow> 8) (p && mask pt_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!