theory ArchVSpaceEntries_AI

lemma store_pte_valid_pdpt:
  "\<lbrace>valid_pdpt_objs and page_inv_entries_safe (Inl (pte, slots))\<rbrace>
       store_pte (hd slots) pte \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>" apply (rule hoare_name_pre_state) apply (clarsimp simp:page_inv_entries_safe_def split:if_splits) apply (clarsimp simp:store_pte_def set_pt_def) apply (wp get_pt_wp get_object_wp) apply (clarsimp simp:obj_at_def
     split:pte.splits arch_kernel_obj.splits) apply (rule conjI) apply (drule(1) valid_pdpt_objs_ptD) apply (rule valid_entries_overwrite_0) apply simp apply (case_tac pte) apply simp+ apply (case_tac "pta p",simp_all) apply clarsimp apply (simp add:fun_upd_def) apply (rule entries_align_pte_update) apply (drule (1) valid_pdpt_objs_ptD,simp) apply simp apply (simp add:hd_map_simp upto_enum_def upto_enum_step_def) apply (clarsimp simp:store_pte_def set_pt_def) apply (wp get_pt_wp get_object_wp) apply (clarsimp simp:obj_at_def
     split:pte.splits arch_kernel_obj.splits) apply (drule(1) valid_pdpt_objs_ptD) apply (rule conjI) apply (rule valid_entries_overwrite_0) apply simp apply (rule ccontr) apply (drule pte_range_interD) apply clarsimp apply (simp add:ucast_neg_mask) apply (subst (asm) is_aligned_neg_mask_eq[where n = 4]) apply (rule is_aligned_shiftr[OF is_aligned_andI1]) apply simp apply (drule_tac x = "((p && ~~ mask pt_bits)  + ((ucast pa) << 2))" in bspec) apply (clarsimp simp: tl_map_simp upto_0_to_n2 image_def) apply (rule_tac x = "unat (((ucast pa)::word32) - (p && mask pt_bits >> 2))" in bexI) apply (simp add:ucast_nat_def shiftl_t2n mask_out_sub_mask) apply (subst shiftl_t2n[where n = 2,simplified field_simps,simplified,symmetric]) apply (subst shiftr_shiftl1) apply simp+ apply (subst is_aligned_neg_mask_eq) apply (erule is_aligned_andI1[OF is_aligned_weaken]) apply simp apply simp apply simp apply (drule_tac s = "ucast (p && mask pt_bits >> 2)" in sym) apply (simp add:mask_out_sub_mask field_simps) apply (drule_tac f = "ucast::(word8\<Rightarrow>word32)" in arg_cong) apply (simp add:ucast_pt_index) apply (simp add:unat_ucast_8_32) apply (rule conjI) apply (subgoal_tac "unat (pa && mask 4)\<noteq> 0") apply simp apply (simp add:unat_gt_0) apply (rule unat_less_helper) apply (rule le_less_trans[OF word_and_le1]) apply (simp add:mask_def) apply (simp add:field_simps neg_mask_add_mask) apply (thin_tac "ucast y = x" for y x) apply (subst (asm) less_mask_eq[where n = pt_bits]) apply (rule shiftl_less_t2n) apply (simp add:pt_bits_def pageBits_def) apply word_bitwise apply (simp add:pt_bits_def pageBits_def) apply (subst (asm) shiftl_shiftr_id) apply simp apply (simp,word_bitwise) apply (simp add:ucast_ucast_id) apply (simp add:fun_upd_def entries_align_def) apply (rule is_aligned_weaken[OF _ pte_range_sz_le]) apply (simp add:is_aligned_shiftr) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and page_inv_entries_safe (Inl (pte, slots))\<rbrace> store_pte (hd slots) pte \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and page_inv_entries_safe (Inl (pte, slots))) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> store_pte (hd slots) pte \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s sl. \<lbrakk>slots = [sl]; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) \<and> pte_range_sz (pt (UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2) && ~~ mask 4)) = 0) (sl && ~~ mask pt_bits) s; pte_range_sz pte = 0\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> store_pte sl pte \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace>
 2. \<And>s p. \<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; obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) \<and> (\<forall>x\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). pt (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE)) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits) s; slots = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> store_pte (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])) pte \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s sl. \<lbrakk>slots = [sl]; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) \<and> pte_range_sz (pt (UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2) && ~~ mask 4)) = 0) (sl && ~~ mask pt_bits) s; pte_range_sz pte = 0\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do pt <- get_pt (sl && ~~ mask pt_bits);
set_object (sl && ~~ mask pt_bits) (ArchObj (PageTable (pt(UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2) := pte))))
od \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace>
 2. \<And>s p. \<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; obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) \<and> (\<forall>x\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). pt (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE)) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits) s; slots = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> store_pte (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])) pte \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s sl sa. \<lbrakk>slots = [sl]; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) \<and> pte_range_sz (pt (UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2) && ~~ mask 4)) = 0) (sl && ~~ mask pt_bits) s; pte_range_sz pte = 0; s = sa\<rbrakk> \<Longrightarrow> \<forall>pt. ako_at (PageTable pt) (sl && ~~ mask pt_bits) sa \<longrightarrow> ((\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and K (obj_valid_pdpt (ArchObj (PageTable (pt(UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2) := pte)))))) sa
 2. \<And>s p. \<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; obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) \<and> (\<forall>x\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). pt (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE)) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits) s; slots = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> store_pte (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])) pte \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>sl sa pta. \<lbrakk>slots = [sl]; \<forall>x\<in>ran (kheap sa). obj_valid_pdpt x; pte_range_sz pte = 0; pte_range_sz (pta (UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2) && ~~ mask 4)) = 0; kheap sa (sl && ~~ mask pt_bits) = Some (ArchObj (PageTable pta))\<rbrakk> \<Longrightarrow> valid_entries pte_range (pta(UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2) := pte)) \<and> entries_align pte_range_sz (pta(UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2) := pte))
 2. \<And>s p. \<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; obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) \<and> (\<forall>x\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). pt (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE)) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits) s; slots = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> store_pte (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])) pte \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>sl sa pta. \<lbrakk>slots = [sl]; \<forall>x\<in>ran (kheap sa). obj_valid_pdpt x; pte_range_sz pte = 0; pte_range_sz (pta (UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2) && ~~ mask 4)) = 0; kheap sa (sl && ~~ mask pt_bits) = Some (ArchObj (PageTable pta))\<rbrakk> \<Longrightarrow> valid_entries pte_range (pta(UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2) := pte))
 2. \<And>sl sa pta. \<lbrakk>slots = [sl]; \<forall>x\<in>ran (kheap sa). obj_valid_pdpt x; pte_range_sz pte = 0; pte_range_sz (pta (UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2) && ~~ mask 4)) = 0; kheap sa (sl && ~~ mask pt_bits) = Some (ArchObj (PageTable pta))\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pta(UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2) := pte))
 3. \<And>s p. \<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; obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) \<and> (\<forall>x\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). pt (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE)) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits) s; slots = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> store_pte (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])) pte \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>sl sa pta. \<lbrakk>slots = [sl]; pte_range_sz pte = 0; pte_range_sz (pta (UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2) && ~~ mask 4)) = 0; kheap sa (sl && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); valid_entries pte_range pta \<and> entries_align pte_range_sz pta\<rbrakk> \<Longrightarrow> valid_entries pte_range (pta(UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2) := pte))
 2. \<And>sl sa pta. \<lbrakk>slots = [sl]; \<forall>x\<in>ran (kheap sa). obj_valid_pdpt x; pte_range_sz pte = 0; pte_range_sz (pta (UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2) && ~~ mask 4)) = 0; kheap sa (sl && ~~ mask pt_bits) = Some (ArchObj (PageTable pta))\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pta(UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2) := pte))
 3. \<And>s p. \<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; obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) \<and> (\<forall>x\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). pt (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE)) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits) s; slots = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> store_pte (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])) pte \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>sl sa pta. \<lbrakk>slots = [sl]; pte_range_sz pte = 0; pte_range_sz (pta (UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2) && ~~ mask 4)) = 0; kheap sa (sl && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); valid_entries pte_range pta \<and> entries_align pte_range_sz pta\<rbrakk> \<Longrightarrow> valid_entries pte_range pta
 2. \<And>sl sa pta p. \<lbrakk>slots = [sl]; pte_range_sz pte = 0; pte_range_sz (pta (UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2) && ~~ mask 4)) = 0; kheap sa (sl && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); valid_entries pte_range pta \<and> entries_align pte_range_sz pta; p \<noteq> UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2)\<rbrakk> \<Longrightarrow> pte_range pte (UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2)) \<inter> pte_range (pta p) p = {}
 3. \<And>sl sa pta. \<lbrakk>slots = [sl]; \<forall>x\<in>ran (kheap sa). obj_valid_pdpt x; pte_range_sz pte = 0; pte_range_sz (pta (UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2) && ~~ mask 4)) = 0; kheap sa (sl && ~~ mask pt_bits) = Some (ArchObj (PageTable pta))\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pta(UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2) := pte))
 4. \<And>s p. \<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; obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) \<and> (\<forall>x\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). pt (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE)) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits) s; slots = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> store_pte (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])) pte \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>sl sa pta p. \<lbrakk>slots = [sl]; pte_range_sz pte = 0; pte_range_sz (pta (UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2) && ~~ mask 4)) = 0; kheap sa (sl && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); valid_entries pte_range pta \<and> entries_align pte_range_sz pta; p \<noteq> UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2)\<rbrakk> \<Longrightarrow> pte_range pte (UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2)) \<inter> pte_range (pta p) p = {}
 2. \<And>sl sa pta. \<lbrakk>slots = [sl]; \<forall>x\<in>ran (kheap sa). obj_valid_pdpt x; pte_range_sz pte = 0; pte_range_sz (pta (UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2) && ~~ mask 4)) = 0; kheap sa (sl && ~~ mask pt_bits) = Some (ArchObj (PageTable pta))\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pta(UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2) := pte))
 3. \<And>s p. \<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; obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) \<and> (\<forall>x\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). pt (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE)) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits) s; slots = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> store_pte (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])) pte \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>sl sa pta p. \<lbrakk>slots = [sl]; pte_range_sz pte = 0; pte_range_sz (pta (UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2) && ~~ mask 4)) = 0; kheap sa (sl && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); valid_entries pte_range pta \<and> entries_align pte_range_sz pta; p \<noteq> UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2); pte = InvalidPTE\<rbrakk> \<Longrightarrow> pte_range pte (UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2)) \<inter> pte_range (pta p) p = {}
 2. \<And>sl sa pta p x21 x22 x23. \<lbrakk>slots = [sl]; pte_range_sz pte = 0; pte_range_sz (pta (UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2) && ~~ mask 4)) = 0; kheap sa (sl && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); valid_entries pte_range pta \<and> entries_align pte_range_sz pta; p \<noteq> UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2); pte = LargePagePTE x21 x22 x23\<rbrakk> \<Longrightarrow> pte_range pte (UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2)) \<inter> pte_range (pta p) p = {}
 3. \<And>sl sa pta p x31 x32 x33. \<lbrakk>slots = [sl]; pte_range_sz pte = 0; pte_range_sz (pta (UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2) && ~~ mask 4)) = 0; kheap sa (sl && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); valid_entries pte_range pta \<and> entries_align pte_range_sz pta; p \<noteq> UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2); pte = SmallPagePTE x31 x32 x33\<rbrakk> \<Longrightarrow> pte_range pte (UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2)) \<inter> pte_range (pta p) p = {}
 4. \<And>sl sa pta. \<lbrakk>slots = [sl]; \<forall>x\<in>ran (kheap sa). obj_valid_pdpt x; pte_range_sz pte = 0; pte_range_sz (pta (UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2) && ~~ mask 4)) = 0; kheap sa (sl && ~~ mask pt_bits) = Some (ArchObj (PageTable pta))\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pta(UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2) := pte))
 5. \<And>s p. \<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; obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) \<and> (\<forall>x\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). pt (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE)) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits) s; slots = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> store_pte (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])) pte \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>sl sa pta p x31 x32 x33. \<lbrakk>slots = [sl]; pte_range_sz (pta (UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2) && ~~ mask 4)) = 0; kheap sa (sl && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); valid_entries pte_range pta \<and> entries_align pte_range_sz pta; p \<noteq> UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2); pte = SmallPagePTE x31 x32 x33\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2) \<notin> pte_range (pta p) p
 2. \<And>sl sa pta. \<lbrakk>slots = [sl]; \<forall>x\<in>ran (kheap sa). obj_valid_pdpt x; pte_range_sz pte = 0; pte_range_sz (pta (UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2) && ~~ mask 4)) = 0; kheap sa (sl && ~~ mask pt_bits) = Some (ArchObj (PageTable pta))\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pta(UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2) := pte))
 3. \<And>s p. \<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; obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) \<and> (\<forall>x\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). pt (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE)) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits) s; slots = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> store_pte (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])) pte \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>sl sa pta p x31 x32 x33 x21 x22 x23. \<lbrakk>slots = [sl]; pte_range_sz (pta (UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2) && ~~ mask 4)) = 0; kheap sa (sl && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); valid_entries pte_range pta \<and> entries_align pte_range_sz pta; p \<noteq> UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2); pte = SmallPagePTE x31 x32 x33; pta p = LargePagePTE x21 x22 x23\<rbrakk> \<Longrightarrow> is_aligned p 4 \<longrightarrow> UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2) && ~~ mask 4 \<noteq> p
 2. \<And>sl sa pta. \<lbrakk>slots = [sl]; \<forall>x\<in>ran (kheap sa). obj_valid_pdpt x; pte_range_sz pte = 0; pte_range_sz (pta (UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2) && ~~ mask 4)) = 0; kheap sa (sl && ~~ mask pt_bits) = Some (ArchObj (PageTable pta))\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pta(UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2) := pte))
 3. \<And>s p. \<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; obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) \<and> (\<forall>x\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). pt (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE)) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits) s; slots = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> store_pte (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])) pte \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>sl sa pta. \<lbrakk>slots = [sl]; \<forall>x\<in>ran (kheap sa). obj_valid_pdpt x; pte_range_sz pte = 0; pte_range_sz (pta (UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2) && ~~ mask 4)) = 0; kheap sa (sl && ~~ mask pt_bits) = Some (ArchObj (PageTable pta))\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pta(UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2) := pte))
 2. \<And>s p. \<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; obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) \<and> (\<forall>x\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). pt (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE)) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits) s; slots = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> store_pte (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])) pte \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>sl sa pta. \<lbrakk>slots = [sl]; \<forall>x\<in>ran (kheap sa). obj_valid_pdpt x; pte_range_sz pte = 0; pte_range_sz (pta (UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2) && ~~ mask 4)) = 0; kheap sa (sl && ~~ mask pt_bits) = Some (ArchObj (PageTable pta))\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (\<lambda>x. if x = UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2) then pte else pta x)
 2. \<And>s p. \<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; obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) \<and> (\<forall>x\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). pt (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE)) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits) s; slots = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> store_pte (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])) pte \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>sl sa pta. \<lbrakk>slots = [sl]; \<forall>x\<in>ran (kheap sa). obj_valid_pdpt x; pte_range_sz pte = 0; pte_range_sz (pta (UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2) && ~~ mask 4)) = 0; kheap sa (sl && ~~ mask pt_bits) = Some (ArchObj (PageTable pta))\<rbrakk> \<Longrightarrow> entries_align pte_range_sz pta
 2. \<And>sl sa pta. \<lbrakk>slots = [sl]; \<forall>x\<in>ran (kheap sa). obj_valid_pdpt x; pte_range_sz pte = 0; pte_range_sz (pta (UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2) && ~~ mask 4)) = 0; kheap sa (sl && ~~ mask pt_bits) = Some (ArchObj (PageTable pta))\<rbrakk> \<Longrightarrow> \<forall>x. x = UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2) \<longrightarrow> is_aligned x (pte_range_sz pte)
 3. \<And>s p. \<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; obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) \<and> (\<forall>x\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). pt (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE)) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits) s; slots = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> store_pte (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])) pte \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>sl sa pta. \<lbrakk>slots = [sl]; \<forall>x\<in>ran (kheap sa). obj_valid_pdpt x; pte_range_sz pte = 0; pte_range_sz (pta (UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2) && ~~ mask 4)) = 0; kheap sa (sl && ~~ mask pt_bits) = Some (ArchObj (PageTable pta))\<rbrakk> \<Longrightarrow> \<forall>x. x = UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2) \<longrightarrow> is_aligned x (pte_range_sz pte)
 2. \<And>s p. \<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; obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) \<and> (\<forall>x\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). pt (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE)) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits) s; slots = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> store_pte (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])) pte \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s p. \<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; obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) \<and> (\<forall>x\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). pt (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE)) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pt_bits) s; slots = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> store_pte (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])) pte \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s p. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) \<and> (\<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pt (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE)) (p && ~~ mask pt_bits) s; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> store_pte p pte \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s p. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) \<and> (\<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pt (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE)) (p && ~~ mask pt_bits) s; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do pt <- get_pt (p && ~~ mask pt_bits);
set_object (p && ~~ mask pt_bits) (ArchObj (PageTable (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte))))
od \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s p sa. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_aligned p 6; obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) \<and> (\<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pt (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE)) (p && ~~ mask pt_bits) s; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; s = sa\<rbrakk> \<Longrightarrow> \<forall>pt. ako_at (PageTable pt) (p && ~~ mask pt_bits) sa \<longrightarrow> ((\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and K (obj_valid_pdpt (ArchObj (PageTable (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)))))) sa proof (prove)
goal (1 subgoal):
 1. \<And>p sa pta. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; \<forall>x\<in>ran (kheap sa). obj_valid_pdpt x; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta))\<rbrakk> \<Longrightarrow> valid_entries pte_range (pta(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)) \<and> entries_align pte_range_sz (pta(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)) proof (prove)
goal (1 subgoal):
 1. \<And>p sa pta. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); valid_entries pte_range pta \<and> entries_align pte_range_sz pta\<rbrakk> \<Longrightarrow> valid_entries pte_range (pta(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)) \<and> entries_align pte_range_sz (pta(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)) proof (prove)
goal (2 subgoals):
 1. \<And>p sa pta. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); valid_entries pte_range pta \<and> entries_align pte_range_sz pta\<rbrakk> \<Longrightarrow> valid_entries pte_range (pta(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte))
 2. \<And>p sa pta. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); valid_entries pte_range pta \<and> entries_align pte_range_sz pta\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pta(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)) proof (prove)
goal (3 subgoals):
 1. \<And>p sa pta. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); valid_entries pte_range pta \<and> entries_align pte_range_sz pta\<rbrakk> \<Longrightarrow> valid_entries pte_range pta
 2. \<And>p sa pta pa. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); valid_entries pte_range pta \<and> entries_align pte_range_sz pta; pa \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2)\<rbrakk> \<Longrightarrow> pte_range pte (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2)) \<inter> pte_range (pta pa) pa = {}
 3. \<And>p sa pta. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); valid_entries pte_range pta \<and> entries_align pte_range_sz pta\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pta(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)) proof (prove)
goal (2 subgoals):
 1. \<And>p sa pta pa. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); valid_entries pte_range pta \<and> entries_align pte_range_sz pta; pa \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2)\<rbrakk> \<Longrightarrow> pte_range pte (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2)) \<inter> pte_range (pta pa) pa = {}
 2. \<And>p sa pta. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); valid_entries pte_range pta \<and> entries_align pte_range_sz pta\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pta(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)) proof (prove)
goal (2 subgoals):
 1. \<And>p sa pta pa. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); valid_entries pte_range pta \<and> entries_align pte_range_sz pta; pa \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); pte_range pte (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2)) \<inter> pte_range (pta pa) pa \<noteq> {}\<rbrakk> \<Longrightarrow> False
 2. \<And>p sa pta. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); valid_entries pte_range pta \<and> entries_align pte_range_sz pta\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pta(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)) proof (prove)
goal (2 subgoals):
 1. \<And>p sa pta pa. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); valid_entries pte_range pta \<and> entries_align pte_range_sz pta; pa \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); pte \<noteq> InvalidPTE \<and> pta pa \<noteq> InvalidPTE \<and> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) && ~~ mask 4 = pa && ~~ mask 4\<rbrakk> \<Longrightarrow> False
 2. \<And>p sa pta. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); valid_entries pte_range pta \<and> entries_align pte_range_sz pta\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pta(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)) proof (prove)
goal (2 subgoals):
 1. \<And>p sa pta pa. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); pa \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) && ~~ mask 4 = pa && ~~ mask 4\<rbrakk> \<Longrightarrow> False
 2. \<And>p sa pta. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); valid_entries pte_range pta \<and> entries_align pte_range_sz pta\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pta(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)) proof (prove)
goal (2 subgoals):
 1. \<And>p sa pta pa. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); pa \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(32 \<rightarrow> 8) ((p && mask pt_bits >> 2) && ~~ mask 4) = pa && ~~ mask 4\<rbrakk> \<Longrightarrow> False
 2. \<And>p sa pta. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); valid_entries pte_range pta \<and> entries_align pte_range_sz pta\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pta(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)) proof (prove)
goal (3 subgoals):
 1. \<And>p sa pta pa. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); pa \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE\<rbrakk> \<Longrightarrow> is_aligned (p && mask pt_bits >> 2) 4
 2. \<And>p sa pta pa. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); pa \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) = pa && ~~ mask 4\<rbrakk> \<Longrightarrow> False
 3. \<And>p sa pta. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); valid_entries pte_range pta \<and> entries_align pte_range_sz pta\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pta(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)) proof (prove)
goal (3 subgoals):
 1. \<And>p sa pta pa. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); pa \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE\<rbrakk> \<Longrightarrow> is_aligned p (4 + 2)
 2. \<And>p sa pta pa. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); pa \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) = pa && ~~ mask 4\<rbrakk> \<Longrightarrow> False
 3. \<And>p sa pta. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); valid_entries pte_range pta \<and> entries_align pte_range_sz pta\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pta(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)) proof (prove)
goal (2 subgoals):
 1. \<And>p sa pta pa. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); pa \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) = pa && ~~ mask 4\<rbrakk> \<Longrightarrow> False
 2. \<And>p sa pta. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); valid_entries pte_range pta \<and> entries_align pte_range_sz pta\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pta(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)) proof (prove)
goal (3 subgoals):
 1. \<And>p sa pta pa. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); pa \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) = pa && ~~ mask 4\<rbrakk> \<Longrightarrow> (p && ~~ mask pt_bits) + (UCAST(8 \<rightarrow> 32) pa << 2) \<in> set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]))
 2. \<And>p sa pta pa. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); pa \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) = pa && ~~ mask 4; pta (UCAST(32 \<rightarrow> 8) ((p && ~~ mask pt_bits) + (UCAST(8 \<rightarrow> 32) pa << 2) && mask pt_bits >> 2)) = InvalidPTE\<rbrakk> \<Longrightarrow> False
 3. \<And>p sa pta. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); valid_entries pte_range pta \<and> entries_align pte_range_sz pta\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pta(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)) proof (prove)
goal (3 subgoals):
 1. \<And>p sa pta pa. \<lbrakk>is_aligned p 6; slots = p # map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [Suc 0..<16]; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); pa \<noteq> pa && ~~ mask 4; valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) = pa && ~~ mask 4\<rbrakk> \<Longrightarrow> \<exists>x\<in>{Suc 0..<16}. (p && ~~ mask pt_bits) + (UCAST(8 \<rightarrow> 32) pa << 2) = word_of_nat x * 4 + p
 2. \<And>p sa pta pa. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); pa \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) = pa && ~~ mask 4; pta (UCAST(32 \<rightarrow> 8) ((p && ~~ mask pt_bits) + (UCAST(8 \<rightarrow> 32) pa << 2) && mask pt_bits >> 2)) = InvalidPTE\<rbrakk> \<Longrightarrow> False
 3. \<And>p sa pta. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); valid_entries pte_range pta \<and> entries_align pte_range_sz pta\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pta(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)) proof (prove)
goal (4 subgoals):
 1. \<And>p sa pta pa. \<lbrakk>is_aligned p 6; slots = p # map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [Suc 0..<16]; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); pa \<noteq> pa && ~~ mask 4; valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) = pa && ~~ mask 4\<rbrakk> \<Longrightarrow> (p && ~~ mask pt_bits) + (UCAST(8 \<rightarrow> 32) pa << 2) = word_of_nat (unat (UCAST(8 \<rightarrow> 32) pa - (p && mask pt_bits >> 2))) * 4 + p
 2. \<And>p sa pta pa. \<lbrakk>is_aligned p 6; slots = p # map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [Suc 0..<16]; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); pa \<noteq> pa && ~~ mask 4; valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) = pa && ~~ mask 4\<rbrakk> \<Longrightarrow> unat (UCAST(8 \<rightarrow> 32) pa - (p && mask pt_bits >> 2)) \<in> {Suc 0..<16}
 3. \<And>p sa pta pa. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); pa \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) = pa && ~~ mask 4; pta (UCAST(32 \<rightarrow> 8) ((p && ~~ mask pt_bits) + (UCAST(8 \<rightarrow> 32) pa << 2) && mask pt_bits >> 2)) = InvalidPTE\<rbrakk> \<Longrightarrow> False
 4. \<And>p sa pta. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); valid_entries pte_range pta \<and> entries_align pte_range_sz pta\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pta(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)) proof (prove)
goal (4 subgoals):
 1. \<And>p sa pta pa. \<lbrakk>is_aligned p 6; slots = p # map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [Suc 0..<16]; kheap sa (p - (p && mask pt_bits)) = Some (ArchObj (PageTable pta)); pa && mask 4 \<noteq> 0; valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) = pa - (pa && mask 4)\<rbrakk> \<Longrightarrow> p && mask pt_bits = (p && mask pt_bits >> 2) * 4
 2. \<And>p sa pta pa. \<lbrakk>is_aligned p 6; slots = p # map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [Suc 0..<16]; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); pa \<noteq> pa && ~~ mask 4; valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) = pa && ~~ mask 4\<rbrakk> \<Longrightarrow> unat (UCAST(8 \<rightarrow> 32) pa - (p && mask pt_bits >> 2)) \<in> {Suc 0..<16}
 3. \<And>p sa pta pa. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); pa \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) = pa && ~~ mask 4; pta (UCAST(32 \<rightarrow> 8) ((p && ~~ mask pt_bits) + (UCAST(8 \<rightarrow> 32) pa << 2) && mask pt_bits >> 2)) = InvalidPTE\<rbrakk> \<Longrightarrow> False
 4. \<And>p sa pta. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); valid_entries pte_range pta \<and> entries_align pte_range_sz pta\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pta(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)) proof (prove)
goal (4 subgoals):
 1. \<And>p sa pta pa. \<lbrakk>is_aligned p 6; slots = p # map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [Suc 0..<16]; kheap sa (p - (p && mask pt_bits)) = Some (ArchObj (PageTable pta)); pa && mask 4 \<noteq> 0; valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) = pa - (pa && mask 4)\<rbrakk> \<Longrightarrow> p && mask pt_bits = p && mask pt_bits >> 2 << 2
 2. \<And>p sa pta pa. \<lbrakk>is_aligned p 6; slots = p # map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [Suc 0..<16]; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); pa \<noteq> pa && ~~ mask 4; valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) = pa && ~~ mask 4\<rbrakk> \<Longrightarrow> unat (UCAST(8 \<rightarrow> 32) pa - (p && mask pt_bits >> 2)) \<in> {Suc 0..<16}
 3. \<And>p sa pta pa. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); pa \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) = pa && ~~ mask 4; pta (UCAST(32 \<rightarrow> 8) ((p && ~~ mask pt_bits) + (UCAST(8 \<rightarrow> 32) pa << 2) && mask pt_bits >> 2)) = InvalidPTE\<rbrakk> \<Longrightarrow> False
 4. \<And>p sa pta. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); valid_entries pte_range pta \<and> entries_align pte_range_sz pta\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pta(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)) proof (prove)
goal (5 subgoals):
 1. \<And>p sa pta pa. \<lbrakk>is_aligned p 6; slots = p # map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [Suc 0..<16]; kheap sa (p - (p && mask pt_bits)) = Some (ArchObj (PageTable pta)); pa && mask 4 \<noteq> 0; valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) = pa - (pa && mask 4)\<rbrakk> \<Longrightarrow> 2 \<le> 2
 2. \<And>p sa pta pa. \<lbrakk>is_aligned p 6; slots = p # map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [Suc 0..<16]; kheap sa (p - (p && mask pt_bits)) = Some (ArchObj (PageTable pta)); pa && mask 4 \<noteq> 0; valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) = pa - (pa && mask 4)\<rbrakk> \<Longrightarrow> p && mask pt_bits = (p && mask pt_bits >> 2 - 2) && ~~ mask 2
 3. \<And>p sa pta pa. \<lbrakk>is_aligned p 6; slots = p # map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [Suc 0..<16]; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); pa \<noteq> pa && ~~ mask 4; valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) = pa && ~~ mask 4\<rbrakk> \<Longrightarrow> unat (UCAST(8 \<rightarrow> 32) pa - (p && mask pt_bits >> 2)) \<in> {Suc 0..<16}
 4. \<And>p sa pta pa. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); pa \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) = pa && ~~ mask 4; pta (UCAST(32 \<rightarrow> 8) ((p && ~~ mask pt_bits) + (UCAST(8 \<rightarrow> 32) pa << 2) && mask pt_bits >> 2)) = InvalidPTE\<rbrakk> \<Longrightarrow> False
 5. \<And>p sa pta. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); valid_entries pte_range pta \<and> entries_align pte_range_sz pta\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pta(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)) proof (prove)
goal (4 subgoals):
 1. \<And>p sa pta pa. \<lbrakk>is_aligned p 6; slots = p # map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [Suc 0..<16]; kheap sa (p - (p && mask pt_bits)) = Some (ArchObj (PageTable pta)); pa && mask 4 \<noteq> 0; valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) = pa - (pa && mask 4)\<rbrakk> \<Longrightarrow> p && mask pt_bits = (p && mask pt_bits) && ~~ mask 2
 2. \<And>p sa pta pa. \<lbrakk>is_aligned p 6; slots = p # map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [Suc 0..<16]; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); pa \<noteq> pa && ~~ mask 4; valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) = pa && ~~ mask 4\<rbrakk> \<Longrightarrow> unat (UCAST(8 \<rightarrow> 32) pa - (p && mask pt_bits >> 2)) \<in> {Suc 0..<16}
 3. \<And>p sa pta pa. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); pa \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) = pa && ~~ mask 4; pta (UCAST(32 \<rightarrow> 8) ((p && ~~ mask pt_bits) + (UCAST(8 \<rightarrow> 32) pa << 2) && mask pt_bits >> 2)) = InvalidPTE\<rbrakk> \<Longrightarrow> False
 4. \<And>p sa pta. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); valid_entries pte_range pta \<and> entries_align pte_range_sz pta\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pta(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)) proof (prove)
goal (5 subgoals):
 1. \<And>p sa pta pa. \<lbrakk>is_aligned p 6; slots = p # map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [Suc 0..<16]; kheap sa (p - (p && mask pt_bits)) = Some (ArchObj (PageTable pta)); pa && mask 4 \<noteq> 0; valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) = pa - (pa && mask 4)\<rbrakk> \<Longrightarrow> is_aligned (p && mask pt_bits) 2
 2. \<And>p sa pta pa. \<lbrakk>is_aligned p 6; slots = p # map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [Suc 0..<16]; kheap sa (p - (p && mask pt_bits)) = Some (ArchObj (PageTable pta)); pa && mask 4 \<noteq> 0; valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) = pa - (pa && mask 4)\<rbrakk> \<Longrightarrow> p && mask pt_bits = p && mask pt_bits
 3. \<And>p sa pta pa. \<lbrakk>is_aligned p 6; slots = p # map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [Suc 0..<16]; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); pa \<noteq> pa && ~~ mask 4; valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) = pa && ~~ mask 4\<rbrakk> \<Longrightarrow> unat (UCAST(8 \<rightarrow> 32) pa - (p && mask pt_bits >> 2)) \<in> {Suc 0..<16}
 4. \<And>p sa pta pa. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); pa \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) = pa && ~~ mask 4; pta (UCAST(32 \<rightarrow> 8) ((p && ~~ mask pt_bits) + (UCAST(8 \<rightarrow> 32) pa << 2) && mask pt_bits >> 2)) = InvalidPTE\<rbrakk> \<Longrightarrow> False
 5. \<And>p sa pta. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); valid_entries pte_range pta \<and> entries_align pte_range_sz pta\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pta(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)) proof (prove)
goal (5 subgoals):
 1. \<And>p sa pta pa. \<lbrakk>slots = p # map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [Suc 0..<16]; kheap sa (p - (p && mask pt_bits)) = Some (ArchObj (PageTable pta)); pa && mask 4 \<noteq> 0; valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) = pa - (pa && mask 4)\<rbrakk> \<Longrightarrow> 2 \<le> 6
 2. \<And>p sa pta pa. \<lbrakk>is_aligned p 6; slots = p # map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [Suc 0..<16]; kheap sa (p - (p && mask pt_bits)) = Some (ArchObj (PageTable pta)); pa && mask 4 \<noteq> 0; valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) = pa - (pa && mask 4)\<rbrakk> \<Longrightarrow> p && mask pt_bits = p && mask pt_bits
 3. \<And>p sa pta pa. \<lbrakk>is_aligned p 6; slots = p # map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [Suc 0..<16]; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); pa \<noteq> pa && ~~ mask 4; valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) = pa && ~~ mask 4\<rbrakk> \<Longrightarrow> unat (UCAST(8 \<rightarrow> 32) pa - (p && mask pt_bits >> 2)) \<in> {Suc 0..<16}
 4. \<And>p sa pta pa. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); pa \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) = pa && ~~ mask 4; pta (UCAST(32 \<rightarrow> 8) ((p && ~~ mask pt_bits) + (UCAST(8 \<rightarrow> 32) pa << 2) && mask pt_bits >> 2)) = InvalidPTE\<rbrakk> \<Longrightarrow> False
 5. \<And>p sa pta. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); valid_entries pte_range pta \<and> entries_align pte_range_sz pta\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pta(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)) proof (prove)
goal (4 subgoals):
 1. \<And>p sa pta pa. \<lbrakk>is_aligned p 6; slots = p # map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [Suc 0..<16]; kheap sa (p - (p && mask pt_bits)) = Some (ArchObj (PageTable pta)); pa && mask 4 \<noteq> 0; valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) = pa - (pa && mask 4)\<rbrakk> \<Longrightarrow> p && mask pt_bits = p && mask pt_bits
 2. \<And>p sa pta pa. \<lbrakk>is_aligned p 6; slots = p # map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [Suc 0..<16]; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); pa \<noteq> pa && ~~ mask 4; valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) = pa && ~~ mask 4\<rbrakk> \<Longrightarrow> unat (UCAST(8 \<rightarrow> 32) pa - (p && mask pt_bits >> 2)) \<in> {Suc 0..<16}
 3. \<And>p sa pta pa. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); pa \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) = pa && ~~ mask 4; pta (UCAST(32 \<rightarrow> 8) ((p && ~~ mask pt_bits) + (UCAST(8 \<rightarrow> 32) pa << 2) && mask pt_bits >> 2)) = InvalidPTE\<rbrakk> \<Longrightarrow> False
 4. \<And>p sa pta. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); valid_entries pte_range pta \<and> entries_align pte_range_sz pta\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pta(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)) proof (prove)
goal (3 subgoals):
 1. \<And>p sa pta pa. \<lbrakk>is_aligned p 6; slots = p # map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [Suc 0..<16]; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); pa \<noteq> pa && ~~ mask 4; valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) = pa && ~~ mask 4\<rbrakk> \<Longrightarrow> unat (UCAST(8 \<rightarrow> 32) pa - (p && mask pt_bits >> 2)) \<in> {Suc 0..<16}
 2. \<And>p sa pta pa. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); pa \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) = pa && ~~ mask 4; pta (UCAST(32 \<rightarrow> 8) ((p && ~~ mask pt_bits) + (UCAST(8 \<rightarrow> 32) pa << 2) && mask pt_bits >> 2)) = InvalidPTE\<rbrakk> \<Longrightarrow> False
 3. \<And>p sa pta. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); valid_entries pte_range pta \<and> entries_align pte_range_sz pta\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pta(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)) proof (prove)
goal (3 subgoals):
 1. \<And>p sa pta pa. \<lbrakk>is_aligned p 6; slots = p # map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [Suc 0..<16]; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); pa \<noteq> pa && ~~ mask 4; valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) = pa && ~~ mask 4\<rbrakk> \<Longrightarrow> Suc 0 \<le> unat (UCAST(8 \<rightarrow> 32) pa - (p && mask pt_bits >> 2)) \<and> unat (UCAST(8 \<rightarrow> 32) pa - (p && mask pt_bits >> 2)) < 16
 2. \<And>p sa pta pa. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); pa \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) = pa && ~~ mask 4; pta (UCAST(32 \<rightarrow> 8) ((p && ~~ mask pt_bits) + (UCAST(8 \<rightarrow> 32) pa << 2) && mask pt_bits >> 2)) = InvalidPTE\<rbrakk> \<Longrightarrow> False
 3. \<And>p sa pta. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); valid_entries pte_range pta \<and> entries_align pte_range_sz pta\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pta(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)) proof (prove)
goal (3 subgoals):
 1. \<And>p sa pta pa. \<lbrakk>is_aligned p 6; slots = p # map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [Suc 0..<16]; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); pa \<noteq> pa && ~~ mask 4; valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; pa && ~~ mask 4 = UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2)\<rbrakk> \<Longrightarrow> Suc 0 \<le> unat (UCAST(8 \<rightarrow> 32) pa - (p && mask pt_bits >> 2)) \<and> unat (UCAST(8 \<rightarrow> 32) pa - (p && mask pt_bits >> 2)) < 16
 2. \<And>p sa pta pa. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); pa \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) = pa && ~~ mask 4; pta (UCAST(32 \<rightarrow> 8) ((p && ~~ mask pt_bits) + (UCAST(8 \<rightarrow> 32) pa << 2) && mask pt_bits >> 2)) = InvalidPTE\<rbrakk> \<Longrightarrow> False
 3. \<And>p sa pta. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); valid_entries pte_range pta \<and> entries_align pte_range_sz pta\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pta(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)) proof (prove)
goal (3 subgoals):
 1. \<And>p sa pta pa. \<lbrakk>is_aligned p 6; slots = p # map ((+) p \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [Suc 0..<16]; kheap sa (p - (p && mask pt_bits)) = Some (ArchObj (PageTable pta)); pa && mask 4 \<noteq> 0; valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; pa = (pa && mask 4) + UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2)\<rbrakk> \<Longrightarrow> Suc 0 \<le> unat (UCAST(8 \<rightarrow> 32) pa - (p && mask pt_bits >> 2)) \<and> unat (UCAST(8 \<rightarrow> 32) pa - (p && mask pt_bits >> 2)) < 16
 2. \<And>p sa pta pa. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); pa \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) = pa && ~~ mask 4; pta (UCAST(32 \<rightarrow> 8) ((p && ~~ mask pt_bits) + (UCAST(8 \<rightarrow> 32) pa << 2) && mask pt_bits >> 2)) = InvalidPTE\<rbrakk> \<Longrightarrow> False
 3. \<And>p sa pta. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); valid_entries pte_range pta \<and> entries_align pte_range_sz pta\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pta(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)) proof (prove)
goal (3 subgoals):
 1. \<And>p sa pta pa. \<lbrakk>is_aligned p 6; slots = p # map ((+) p \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [Suc 0..<16]; kheap sa (p - (p && mask pt_bits)) = Some (ArchObj (PageTable pta)); pa && mask 4 \<noteq> 0; valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(8 \<rightarrow> 32) pa = UCAST(8 \<rightarrow> 32) ((pa && mask 4) + UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2))\<rbrakk> \<Longrightarrow> Suc 0 \<le> unat (UCAST(8 \<rightarrow> 32) pa - (p && mask pt_bits >> 2)) \<and> unat (UCAST(8 \<rightarrow> 32) pa - (p && mask pt_bits >> 2)) < 16
 2. \<And>p sa pta pa. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); pa \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) = pa && ~~ mask 4; pta (UCAST(32 \<rightarrow> 8) ((p && ~~ mask pt_bits) + (UCAST(8 \<rightarrow> 32) pa << 2) && mask pt_bits >> 2)) = InvalidPTE\<rbrakk> \<Longrightarrow> False
 3. \<And>p sa pta. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); valid_entries pte_range pta \<and> entries_align pte_range_sz pta\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pta(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)) proof (prove)
goal (3 subgoals):
 1. \<And>p sa pta pa. \<lbrakk>is_aligned p 6; slots = p # map ((+) p \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [Suc 0..<16]; kheap sa (p - (p && mask pt_bits)) = Some (ArchObj (PageTable pta)); pa && mask 4 \<noteq> 0; valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(8 \<rightarrow> 32) pa = UCAST(8 \<rightarrow> 32) (pa && mask 4) + (p && mask pt_bits >> 2)\<rbrakk> \<Longrightarrow> Suc 0 \<le> unat (UCAST(8 \<rightarrow> 32) (pa && mask 4)) \<and> unat (UCAST(8 \<rightarrow> 32) (pa && mask 4)) < 16
 2. \<And>p sa pta pa. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); pa \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) = pa && ~~ mask 4; pta (UCAST(32 \<rightarrow> 8) ((p && ~~ mask pt_bits) + (UCAST(8 \<rightarrow> 32) pa << 2) && mask pt_bits >> 2)) = InvalidPTE\<rbrakk> \<Longrightarrow> False
 3. \<And>p sa pta. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); valid_entries pte_range pta \<and> entries_align pte_range_sz pta\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pta(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)) proof (prove)
goal (3 subgoals):
 1. \<And>p sa pta pa. \<lbrakk>is_aligned p 6; slots = p # map ((+) p \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [Suc 0..<16]; kheap sa (p - (p && mask pt_bits)) = Some (ArchObj (PageTable pta)); pa && mask 4 \<noteq> 0; valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(8 \<rightarrow> 32) pa = UCAST(8 \<rightarrow> 32) (pa && mask 4) + (p && mask pt_bits >> 2)\<rbrakk> \<Longrightarrow> Suc 0 \<le> unat (pa && mask 4) \<and> unat (pa && mask 4) < 16
 2. \<And>p sa pta pa. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); pa \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) = pa && ~~ mask 4; pta (UCAST(32 \<rightarrow> 8) ((p && ~~ mask pt_bits) + (UCAST(8 \<rightarrow> 32) pa << 2) && mask pt_bits >> 2)) = InvalidPTE\<rbrakk> \<Longrightarrow> False
 3. \<And>p sa pta. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); valid_entries pte_range pta \<and> entries_align pte_range_sz pta\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pta(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)) proof (prove)
goal (4 subgoals):
 1. \<And>p sa pta pa. \<lbrakk>is_aligned p 6; slots = p # map ((+) p \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [Suc 0..<16]; kheap sa (p - (p && mask pt_bits)) = Some (ArchObj (PageTable pta)); pa && mask 4 \<noteq> 0; valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(8 \<rightarrow> 32) pa = UCAST(8 \<rightarrow> 32) (pa && mask 4) + (p && mask pt_bits >> 2)\<rbrakk> \<Longrightarrow> Suc 0 \<le> unat (pa && mask 4)
 2. \<And>p sa pta pa. \<lbrakk>is_aligned p 6; slots = p # map ((+) p \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [Suc 0..<16]; kheap sa (p - (p && mask pt_bits)) = Some (ArchObj (PageTable pta)); pa && mask 4 \<noteq> 0; valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(8 \<rightarrow> 32) pa = UCAST(8 \<rightarrow> 32) (pa && mask 4) + (p && mask pt_bits >> 2)\<rbrakk> \<Longrightarrow> unat (pa && mask 4) < 16
 3. \<And>p sa pta pa. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); pa \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) = pa && ~~ mask 4; pta (UCAST(32 \<rightarrow> 8) ((p && ~~ mask pt_bits) + (UCAST(8 \<rightarrow> 32) pa << 2) && mask pt_bits >> 2)) = InvalidPTE\<rbrakk> \<Longrightarrow> False
 4. \<And>p sa pta. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); valid_entries pte_range pta \<and> entries_align pte_range_sz pta\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pta(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)) proof (prove)
goal (5 subgoals):
 1. \<And>p sa pta pa. \<lbrakk>is_aligned p 6; slots = p # map ((+) p \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [Suc 0..<16]; kheap sa (p - (p && mask pt_bits)) = Some (ArchObj (PageTable pta)); pa && mask 4 \<noteq> 0; valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(8 \<rightarrow> 32) pa = UCAST(8 \<rightarrow> 32) (pa && mask 4) + (p && mask pt_bits >> 2); unat (pa && mask 4) \<noteq> 0\<rbrakk> \<Longrightarrow> Suc 0 \<le> unat (pa && mask 4)
 2. \<And>p sa pta pa. \<lbrakk>is_aligned p 6; slots = p # map ((+) p \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [Suc 0..<16]; kheap sa (p - (p && mask pt_bits)) = Some (ArchObj (PageTable pta)); pa && mask 4 \<noteq> 0; valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(8 \<rightarrow> 32) pa = UCAST(8 \<rightarrow> 32) (pa && mask 4) + (p && mask pt_bits >> 2)\<rbrakk> \<Longrightarrow> unat (pa && mask 4) \<noteq> 0
 3. \<And>p sa pta pa. \<lbrakk>is_aligned p 6; slots = p # map ((+) p \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [Suc 0..<16]; kheap sa (p - (p && mask pt_bits)) = Some (ArchObj (PageTable pta)); pa && mask 4 \<noteq> 0; valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(8 \<rightarrow> 32) pa = UCAST(8 \<rightarrow> 32) (pa && mask 4) + (p && mask pt_bits >> 2)\<rbrakk> \<Longrightarrow> unat (pa && mask 4) < 16
 4. \<And>p sa pta pa. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); pa \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) = pa && ~~ mask 4; pta (UCAST(32 \<rightarrow> 8) ((p && ~~ mask pt_bits) + (UCAST(8 \<rightarrow> 32) pa << 2) && mask pt_bits >> 2)) = InvalidPTE\<rbrakk> \<Longrightarrow> False
 5. \<And>p sa pta. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); valid_entries pte_range pta \<and> entries_align pte_range_sz pta\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pta(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)) proof (prove)
goal (4 subgoals):
 1. \<And>p sa pta pa. \<lbrakk>is_aligned p 6; slots = p # map ((+) p \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [Suc 0..<16]; kheap sa (p - (p && mask pt_bits)) = Some (ArchObj (PageTable pta)); pa && mask 4 \<noteq> 0; valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(8 \<rightarrow> 32) pa = UCAST(8 \<rightarrow> 32) (pa && mask 4) + (p && mask pt_bits >> 2)\<rbrakk> \<Longrightarrow> unat (pa && mask 4) \<noteq> 0
 2. \<And>p sa pta pa. \<lbrakk>is_aligned p 6; slots = p # map ((+) p \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [Suc 0..<16]; kheap sa (p - (p && mask pt_bits)) = Some (ArchObj (PageTable pta)); pa && mask 4 \<noteq> 0; valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(8 \<rightarrow> 32) pa = UCAST(8 \<rightarrow> 32) (pa && mask 4) + (p && mask pt_bits >> 2)\<rbrakk> \<Longrightarrow> unat (pa && mask 4) < 16
 3. \<And>p sa pta pa. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); pa \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) = pa && ~~ mask 4; pta (UCAST(32 \<rightarrow> 8) ((p && ~~ mask pt_bits) + (UCAST(8 \<rightarrow> 32) pa << 2) && mask pt_bits >> 2)) = InvalidPTE\<rbrakk> \<Longrightarrow> False
 4. \<And>p sa pta. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); valid_entries pte_range pta \<and> entries_align pte_range_sz pta\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pta(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)) proof (prove)
goal (3 subgoals):
 1. \<And>p sa pta pa. \<lbrakk>is_aligned p 6; slots = p # map ((+) p \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [Suc 0..<16]; kheap sa (p - (p && mask pt_bits)) = Some (ArchObj (PageTable pta)); pa && mask 4 \<noteq> 0; valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(8 \<rightarrow> 32) pa = UCAST(8 \<rightarrow> 32) (pa && mask 4) + (p && mask pt_bits >> 2)\<rbrakk> \<Longrightarrow> unat (pa && mask 4) < 16
 2. \<And>p sa pta pa. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); pa \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) = pa && ~~ mask 4; pta (UCAST(32 \<rightarrow> 8) ((p && ~~ mask pt_bits) + (UCAST(8 \<rightarrow> 32) pa << 2) && mask pt_bits >> 2)) = InvalidPTE\<rbrakk> \<Longrightarrow> False
 3. \<And>p sa pta. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); valid_entries pte_range pta \<and> entries_align pte_range_sz pta\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pta(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)) proof (prove)
goal (3 subgoals):
 1. \<And>p sa pta pa. \<lbrakk>is_aligned p 6; slots = p # map ((+) p \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [Suc 0..<16]; kheap sa (p - (p && mask pt_bits)) = Some (ArchObj (PageTable pta)); pa && mask 4 \<noteq> 0; valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(8 \<rightarrow> 32) pa = UCAST(8 \<rightarrow> 32) (pa && mask 4) + (p && mask pt_bits >> 2)\<rbrakk> \<Longrightarrow> pa && mask 4 < word_of_nat 16
 2. \<And>p sa pta pa. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); pa \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) = pa && ~~ mask 4; pta (UCAST(32 \<rightarrow> 8) ((p && ~~ mask pt_bits) + (UCAST(8 \<rightarrow> 32) pa << 2) && mask pt_bits >> 2)) = InvalidPTE\<rbrakk> \<Longrightarrow> False
 3. \<And>p sa pta. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); valid_entries pte_range pta \<and> entries_align pte_range_sz pta\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pta(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)) proof (prove)
goal (3 subgoals):
 1. \<And>p sa pta pa. \<lbrakk>is_aligned p 6; slots = p # map ((+) p \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [Suc 0..<16]; kheap sa (p - (p && mask pt_bits)) = Some (ArchObj (PageTable pta)); pa && mask 4 \<noteq> 0; valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(8 \<rightarrow> 32) pa = UCAST(8 \<rightarrow> 32) (pa && mask 4) + (p && mask pt_bits >> 2)\<rbrakk> \<Longrightarrow> mask 4 < word_of_nat 16
 2. \<And>p sa pta pa. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); pa \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) = pa && ~~ mask 4; pta (UCAST(32 \<rightarrow> 8) ((p && ~~ mask pt_bits) + (UCAST(8 \<rightarrow> 32) pa << 2) && mask pt_bits >> 2)) = InvalidPTE\<rbrakk> \<Longrightarrow> False
 3. \<And>p sa pta. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); valid_entries pte_range pta \<and> entries_align pte_range_sz pta\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pta(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)) proof (prove)
goal (2 subgoals):
 1. \<And>p sa pta pa. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); pa \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) = pa && ~~ mask 4; pta (UCAST(32 \<rightarrow> 8) ((p && ~~ mask pt_bits) + (UCAST(8 \<rightarrow> 32) pa << 2) && mask pt_bits >> 2)) = InvalidPTE\<rbrakk> \<Longrightarrow> False
 2. \<And>p sa pta. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); valid_entries pte_range pta \<and> entries_align pte_range_sz pta\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pta(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)) proof (prove)
goal (2 subgoals):
 1. \<And>p sa pta pa. \<lbrakk>\<forall>sl. map ((+) p \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((+) p \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); pa \<noteq> pa && ~~ mask 4; valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) = pa && ~~ mask 4; pta (UCAST(32 \<rightarrow> 8) ((UCAST(8 \<rightarrow> 32) pa << 2) && mask pt_bits >> 2)) = InvalidPTE\<rbrakk> \<Longrightarrow> False
 2. \<And>p sa pta. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); valid_entries pte_range pta \<and> entries_align pte_range_sz pta\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pta(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)) proof (prove)
goal (2 subgoals):
 1. \<And>p sa pta pa. \<lbrakk>\<forall>sl. map ((+) p \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((+) p \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); pa \<noteq> pa && ~~ mask 4; valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; pta (UCAST(32 \<rightarrow> 8) ((UCAST(8 \<rightarrow> 32) pa << 2) && mask pt_bits >> 2)) = InvalidPTE\<rbrakk> \<Longrightarrow> False
 2. \<And>p sa pta. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); valid_entries pte_range pta \<and> entries_align pte_range_sz pta\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pta(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)) proof (prove)
goal (3 subgoals):
 1. \<And>p sa pta pa. \<lbrakk>\<forall>sl. map ((+) p \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((+) p \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); pa \<noteq> pa && ~~ mask 4; valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE\<rbrakk> \<Longrightarrow> UCAST(8 \<rightarrow> 32) pa << 2 < 2 ^ pt_bits
 2. \<And>p sa pta pa. \<lbrakk>\<forall>sl. map ((+) p \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((+) p \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); pa \<noteq> pa && ~~ mask 4; valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; pta (UCAST(32 \<rightarrow> 8) (UCAST(8 \<rightarrow> 32) pa << 2 >> 2)) = InvalidPTE\<rbrakk> \<Longrightarrow> False
 3. \<And>p sa pta. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); valid_entries pte_range pta \<and> entries_align pte_range_sz pta\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pta(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)) proof (prove)
goal (4 subgoals):
 1. \<And>p sa pta pa. \<lbrakk>\<forall>sl. map ((+) p \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((+) p \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); pa \<noteq> pa && ~~ mask 4; valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE\<rbrakk> \<Longrightarrow> UCAST(8 \<rightarrow> 32) pa < 2 ^ (pt_bits - 2)
 2. \<And>p sa pta pa. \<lbrakk>\<forall>sl. map ((+) p \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((+) p \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); pa \<noteq> pa && ~~ mask 4; valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE\<rbrakk> \<Longrightarrow> pt_bits < LENGTH(32)
 3. \<And>p sa pta pa. \<lbrakk>\<forall>sl. map ((+) p \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((+) p \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); pa \<noteq> pa && ~~ mask 4; valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; pta (UCAST(32 \<rightarrow> 8) (UCAST(8 \<rightarrow> 32) pa << 2 >> 2)) = InvalidPTE\<rbrakk> \<Longrightarrow> False
 4. \<And>p sa pta. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); valid_entries pte_range pta \<and> entries_align pte_range_sz pta\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pta(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)) proof (prove)
goal (4 subgoals):
 1. \<And>p sa pta pa. \<lbrakk>\<forall>sl. map ((+) p \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((+) p \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; kheap sa (p && ~~ mask 10) = Some (ArchObj (PageTable pta)); pa \<noteq> pa && ~~ mask 4; valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE\<rbrakk> \<Longrightarrow> UCAST(8 \<rightarrow> 32) pa < 0x100
 2. \<And>p sa pta pa. \<lbrakk>\<forall>sl. map ((+) p \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((+) p \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); pa \<noteq> pa && ~~ mask 4; valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE\<rbrakk> \<Longrightarrow> pt_bits < LENGTH(32)
 3. \<And>p sa pta pa. \<lbrakk>\<forall>sl. map ((+) p \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((+) p \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); pa \<noteq> pa && ~~ mask 4; valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; pta (UCAST(32 \<rightarrow> 8) (UCAST(8 \<rightarrow> 32) pa << 2 >> 2)) = InvalidPTE\<rbrakk> \<Longrightarrow> False
 4. \<And>p sa pta. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); valid_entries pte_range pta \<and> entries_align pte_range_sz pta\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pta(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)) proof (prove)
goal (3 subgoals):
 1. \<And>p sa pta pa. \<lbrakk>\<forall>sl. map ((+) p \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((+) p \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); pa \<noteq> pa && ~~ mask 4; valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE\<rbrakk> \<Longrightarrow> pt_bits < LENGTH(32)
 2. \<And>p sa pta pa. \<lbrakk>\<forall>sl. map ((+) p \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((+) p \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); pa \<noteq> pa && ~~ mask 4; valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; pta (UCAST(32 \<rightarrow> 8) (UCAST(8 \<rightarrow> 32) pa << 2 >> 2)) = InvalidPTE\<rbrakk> \<Longrightarrow> False
 3. \<And>p sa pta. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); valid_entries pte_range pta \<and> entries_align pte_range_sz pta\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pta(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)) proof (prove)
goal (2 subgoals):
 1. \<And>p sa pta pa. \<lbrakk>\<forall>sl. map ((+) p \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((+) p \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); pa \<noteq> pa && ~~ mask 4; valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; pta (UCAST(32 \<rightarrow> 8) (UCAST(8 \<rightarrow> 32) pa << 2 >> 2)) = InvalidPTE\<rbrakk> \<Longrightarrow> False
 2. \<And>p sa pta. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); valid_entries pte_range pta \<and> entries_align pte_range_sz pta\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pta(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)) proof (prove)
goal (4 subgoals):
 1. \<And>p sa pta pa. \<lbrakk>\<forall>sl. map ((+) p \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((+) p \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); pa \<noteq> pa && ~~ mask 4; valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE\<rbrakk> \<Longrightarrow> 2 < LENGTH(32)
 2. \<And>p sa pta pa. \<lbrakk>\<forall>sl. map ((+) p \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((+) p \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); pa \<noteq> pa && ~~ mask 4; valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE\<rbrakk> \<Longrightarrow> UCAST(8 \<rightarrow> 32) pa < 2 ^ (LENGTH(32) - 2)
 3. \<And>p sa pta pa. \<lbrakk>\<forall>sl. map ((+) p \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((+) p \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); pa \<noteq> pa && ~~ mask 4; valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; pta (UCAST(32 \<rightarrow> 8) (UCAST(8 \<rightarrow> 32) pa)) = InvalidPTE\<rbrakk> \<Longrightarrow> False
 4. \<And>p sa pta. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); valid_entries pte_range pta \<and> entries_align pte_range_sz pta\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pta(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)) proof (prove)
goal (3 subgoals):
 1. \<And>p sa pta pa. \<lbrakk>\<forall>sl. map ((+) p \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((+) p \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); pa \<noteq> pa && ~~ mask 4; valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE\<rbrakk> \<Longrightarrow> UCAST(8 \<rightarrow> 32) pa < 2 ^ (LENGTH(32) - 2)
 2. \<And>p sa pta pa. \<lbrakk>\<forall>sl. map ((+) p \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((+) p \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); pa \<noteq> pa && ~~ mask 4; valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; pta (UCAST(32 \<rightarrow> 8) (UCAST(8 \<rightarrow> 32) pa)) = InvalidPTE\<rbrakk> \<Longrightarrow> False
 3. \<And>p sa pta. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); valid_entries pte_range pta \<and> entries_align pte_range_sz pta\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pta(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)) proof (prove)
goal (2 subgoals):
 1. \<And>p sa pta pa. \<lbrakk>\<forall>sl. map ((+) p \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((+) p \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); pa \<noteq> pa && ~~ mask 4; valid_entries pte_range pta; entries_align pte_range_sz pta; pte \<noteq> InvalidPTE; pta pa \<noteq> InvalidPTE; pta (UCAST(32 \<rightarrow> 8) (UCAST(8 \<rightarrow> 32) pa)) = InvalidPTE\<rbrakk> \<Longrightarrow> False
 2. \<And>p sa pta. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); valid_entries pte_range pta \<and> entries_align pte_range_sz pta\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pta(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)) proof (prove)
goal (1 subgoal):
 1. \<And>p sa pta. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); valid_entries pte_range pta \<and> entries_align pte_range_sz pta\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pta(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)) proof (prove)
goal (1 subgoal):
 1. \<And>p sa pta. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); valid_entries pte_range pta \<and> (\<forall>x. is_aligned x (pte_range_sz (pta x)))\<rbrakk> \<Longrightarrow> is_aligned (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2)) (pte_range_sz pte) proof (prove)
goal (1 subgoal):
 1. \<And>p sa pta. \<lbrakk>\<forall>sl. map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [sl]; is_aligned p 6; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; \<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pta (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE; kheap sa (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); valid_entries pte_range pta \<and> (\<forall>x. is_aligned x (pte_range_sz (pta x)))\<rbrakk> \<Longrightarrow> is_aligned (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2)) 4 proof (prove)
goal:
No subgoals!