theory ArchVSpaceEntries_AI

lemma store_pde_valid_pdpt:
  "\<lbrace>valid_pdpt_objs and page_inv_entries_safe (Inr (pde, slots))\<rbrace>
       store_pde (hd slots) pde \<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_pde_def set_pd_def) apply (wp get_pd_wp get_object_wp) apply (clarsimp simp:obj_at_def
     split:pde.splits arch_kernel_obj.splits) apply (drule(1) valid_pdpt_objs_pdD) apply (rule conjI) apply (rule valid_entries_overwrite_0) apply simp apply (case_tac pde,simp_all) apply (case_tac "pda p",simp_all) apply clarsimp apply (case_tac "pda p",simp_all) apply clarsimp apply (simp add:fun_upd_def) apply (rule entries_align_pde_update) apply simp+ apply (simp add:hd_map_simp upto_enum_def upto_enum_step_def) apply (clarsimp simp:store_pde_def set_pd_def) apply (wp get_pd_wp get_object_wp) apply (clarsimp simp:obj_at_def
     split:pde.splits arch_kernel_obj.splits) apply (drule(1) valid_pdpt_objs_pdD) apply (rule conjI) apply (rule valid_entries_overwrite_0) apply simp apply (rule ccontr) apply (drule pde_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 pd_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 pd_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 pd_bits >> 2)" in sym) apply (simp add:mask_out_sub_mask field_simps) apply (drule_tac f = "ucast::(12 word\<Rightarrow>word32)" in arg_cong) apply (simp add:ucast_pd_index) apply (simp add:unat_ucast_12_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 = pd_bits]) apply (rule shiftl_less_t2n) apply (simp add:pd_bits_def pageBits_def) apply word_bitwise apply (simp add:pd_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:entries_align_def) apply (rule is_aligned_weaken[OF _ pde_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 (Inr (pde, slots))\<rbrace> store_pde (hd slots) pde \<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 (Inr (pde, slots))) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> store_pde (hd slots) pde \<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>pd. ko = ArchObj (PageDirectory pd) \<and> pde_range_sz (pd (UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) && ~~ mask 4)) = 0) (sl && ~~ mask pd_bits) s; pde_range_sz pde = 0\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> store_pde sl pde \<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>pd. ko = ArchObj (PageDirectory pd) \<and> (\<forall>x\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). pd (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE)) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits) s; slots = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> store_pde (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])) pde \<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>pd. ko = ArchObj (PageDirectory pd) \<and> pde_range_sz (pd (UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) && ~~ mask 4)) = 0) (sl && ~~ mask pd_bits) s; pde_range_sz pde = 0\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do pd <- get_pd (sl && ~~ mask pd_bits);
set_object (sl && ~~ mask pd_bits) (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) := pde))))
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>pd. ko = ArchObj (PageDirectory pd) \<and> (\<forall>x\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). pd (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE)) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits) s; slots = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> store_pde (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])) pde \<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>pd. ko = ArchObj (PageDirectory pd) \<and> pde_range_sz (pd (UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) && ~~ mask 4)) = 0) (sl && ~~ mask pd_bits) s; pde_range_sz pde = 0; s = sa\<rbrakk> \<Longrightarrow> \<forall>pd. ako_at (PageDirectory pd) (sl && ~~ mask pd_bits) sa \<longrightarrow> ((\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and K (obj_valid_pdpt (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) := pde)))))) 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>pd. ko = ArchObj (PageDirectory pd) \<and> (\<forall>x\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). pd (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE)) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits) s; slots = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> store_pde (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])) pde \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>sl sa pda. \<lbrakk>slots = [sl]; \<forall>x\<in>ran (kheap sa). obj_valid_pdpt x; pde_range_sz pde = 0; pde_range_sz (pda (UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) && ~~ mask 4)) = 0; kheap sa (sl && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda))\<rbrakk> \<Longrightarrow> valid_entries pde_range (pda(UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) := pde)) \<and> entries_align pde_range_sz (pda(UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) := pde))
 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>pd. ko = ArchObj (PageDirectory pd) \<and> (\<forall>x\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). pd (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE)) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits) s; slots = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> store_pde (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])) pde \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>sl sa pda. \<lbrakk>slots = [sl]; pde_range_sz pde = 0; pde_range_sz (pda (UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) && ~~ mask 4)) = 0; kheap sa (sl && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda\<rbrakk> \<Longrightarrow> valid_entries pde_range (pda(UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) := pde)) \<and> entries_align pde_range_sz (pda(UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) := pde))
 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>pd. ko = ArchObj (PageDirectory pd) \<and> (\<forall>x\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). pd (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE)) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits) s; slots = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> store_pde (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])) pde \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>sl sa pda. \<lbrakk>slots = [sl]; pde_range_sz pde = 0; pde_range_sz (pda (UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) && ~~ mask 4)) = 0; kheap sa (sl && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda\<rbrakk> \<Longrightarrow> valid_entries pde_range (pda(UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) := pde))
 2. \<And>sl sa pda. \<lbrakk>slots = [sl]; pde_range_sz pde = 0; pde_range_sz (pda (UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) && ~~ mask 4)) = 0; kheap sa (sl && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (pda(UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) := pde))
 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>pd. ko = ArchObj (PageDirectory pd) \<and> (\<forall>x\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). pd (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE)) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits) s; slots = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> store_pde (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])) pde \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>sl sa pda. \<lbrakk>slots = [sl]; pde_range_sz pde = 0; pde_range_sz (pda (UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) && ~~ mask 4)) = 0; kheap sa (sl && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda\<rbrakk> \<Longrightarrow> valid_entries pde_range pda
 2. \<And>sl sa pda p. \<lbrakk>slots = [sl]; pde_range_sz pde = 0; pde_range_sz (pda (UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) && ~~ mask 4)) = 0; kheap sa (sl && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda; p \<noteq> UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2)\<rbrakk> \<Longrightarrow> pde_range pde (UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2)) \<inter> pde_range (pda p) p = {}
 3. \<And>sl sa pda. \<lbrakk>slots = [sl]; pde_range_sz pde = 0; pde_range_sz (pda (UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) && ~~ mask 4)) = 0; kheap sa (sl && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (pda(UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) := pde))
 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>pd. ko = ArchObj (PageDirectory pd) \<and> (\<forall>x\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). pd (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE)) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits) s; slots = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> store_pde (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])) pde \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>sl sa pda p. \<lbrakk>slots = [sl]; pde_range_sz pde = 0; pde_range_sz (pda (UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) && ~~ mask 4)) = 0; kheap sa (sl && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda; p \<noteq> UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2)\<rbrakk> \<Longrightarrow> pde_range pde (UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2)) \<inter> pde_range (pda p) p = {}
 2. \<And>sl sa pda. \<lbrakk>slots = [sl]; pde_range_sz pde = 0; pde_range_sz (pda (UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) && ~~ mask 4)) = 0; kheap sa (sl && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (pda(UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) := pde))
 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>pd. ko = ArchObj (PageDirectory pd) \<and> (\<forall>x\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). pd (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE)) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits) s; slots = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> store_pde (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])) pde \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>sl sa pda p x21 x22 x23. \<lbrakk>slots = [sl]; pde_range_sz (pda (UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) && ~~ mask 4)) = 0; kheap sa (sl && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda; p \<noteq> UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2); pde = PageTablePDE x21 x22 x23\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) \<notin> pde_range (pda p) p
 2. \<And>sl sa pda p x31 x32 x33 x34. \<lbrakk>slots = [sl]; pde_range_sz (pda (UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) && ~~ mask 4)) = 0; kheap sa (sl && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda; p \<noteq> UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2); pde = SectionPDE x31 x32 x33 x34\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) \<notin> pde_range (pda p) p
 3. \<And>sl sa pda. \<lbrakk>slots = [sl]; pde_range_sz pde = 0; pde_range_sz (pda (UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) && ~~ mask 4)) = 0; kheap sa (sl && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (pda(UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) := pde))
 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>pd. ko = ArchObj (PageDirectory pd) \<and> (\<forall>x\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). pd (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE)) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits) s; slots = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> store_pde (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])) pde \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>sl sa pda p x21 x22 x23 x41 x42 x43. \<lbrakk>slots = [sl]; pde_range_sz (pda (UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) && ~~ mask 4)) = 0; kheap sa (sl && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda; p \<noteq> UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2); pde = PageTablePDE x21 x22 x23; pda p = SuperSectionPDE x41 x42 x43\<rbrakk> \<Longrightarrow> is_aligned p 4 \<longrightarrow> UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) && ~~ mask 4 \<noteq> p
 2. \<And>sl sa pda p x31 x32 x33 x34. \<lbrakk>slots = [sl]; pde_range_sz (pda (UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) && ~~ mask 4)) = 0; kheap sa (sl && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda; p \<noteq> UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2); pde = SectionPDE x31 x32 x33 x34\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) \<notin> pde_range (pda p) p
 3. \<And>sl sa pda. \<lbrakk>slots = [sl]; pde_range_sz pde = 0; pde_range_sz (pda (UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) && ~~ mask 4)) = 0; kheap sa (sl && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (pda(UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) := pde))
 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>pd. ko = ArchObj (PageDirectory pd) \<and> (\<forall>x\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). pd (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE)) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits) s; slots = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> store_pde (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])) pde \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>sl sa pda p x31 x32 x33 x34. \<lbrakk>slots = [sl]; pde_range_sz (pda (UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) && ~~ mask 4)) = 0; kheap sa (sl && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda; p \<noteq> UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2); pde = SectionPDE x31 x32 x33 x34\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) \<notin> pde_range (pda p) p
 2. \<And>sl sa pda. \<lbrakk>slots = [sl]; pde_range_sz pde = 0; pde_range_sz (pda (UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) && ~~ mask 4)) = 0; kheap sa (sl && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (pda(UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) := pde))
 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>pd. ko = ArchObj (PageDirectory pd) \<and> (\<forall>x\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). pd (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE)) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits) s; slots = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> store_pde (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])) pde \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>sl sa pda p x31 x32 x33 x34 x41 x42 x43. \<lbrakk>slots = [sl]; pde_range_sz (pda (UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) && ~~ mask 4)) = 0; kheap sa (sl && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda; p \<noteq> UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2); pde = SectionPDE x31 x32 x33 x34; pda p = SuperSectionPDE x41 x42 x43\<rbrakk> \<Longrightarrow> is_aligned p 4 \<longrightarrow> UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) && ~~ mask 4 \<noteq> p
 2. \<And>sl sa pda. \<lbrakk>slots = [sl]; pde_range_sz pde = 0; pde_range_sz (pda (UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) && ~~ mask 4)) = 0; kheap sa (sl && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (pda(UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) := pde))
 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>pd. ko = ArchObj (PageDirectory pd) \<and> (\<forall>x\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). pd (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE)) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits) s; slots = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> store_pde (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])) pde \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>sl sa pda. \<lbrakk>slots = [sl]; pde_range_sz pde = 0; pde_range_sz (pda (UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) && ~~ mask 4)) = 0; kheap sa (sl && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (pda(UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) := pde))
 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>pd. ko = ArchObj (PageDirectory pd) \<and> (\<forall>x\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). pd (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE)) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits) s; slots = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> store_pde (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])) pde \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>sl sa pda. \<lbrakk>slots = [sl]; pde_range_sz pde = 0; pde_range_sz (pda (UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) && ~~ mask 4)) = 0; kheap sa (sl && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>x. if x = UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) then pde else pda 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>pd. ko = ArchObj (PageDirectory pd) \<and> (\<forall>x\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). pd (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE)) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits) s; slots = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> store_pde (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])) pde \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>sl sa pda. \<lbrakk>slots = [sl]; pde_range_sz pde = 0; pde_range_sz (pda (UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) && ~~ mask 4)) = 0; kheap sa (sl && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda\<rbrakk> \<Longrightarrow> entries_align pde_range_sz pda
 2. \<And>sl sa pda. \<lbrakk>slots = [sl]; pde_range_sz pde = 0; pde_range_sz (pda (UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) && ~~ mask 4)) = 0; kheap sa (sl && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda\<rbrakk> \<Longrightarrow> \<forall>x. x = UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) \<longrightarrow> is_aligned x (pde_range_sz pde)
 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>pd. ko = ArchObj (PageDirectory pd) \<and> (\<forall>x\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). pd (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE)) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits) s; slots = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> store_pde (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])) pde \<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>pd. ko = ArchObj (PageDirectory pd) \<and> (\<forall>x\<in>set (tl (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])). pd (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE)) (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]) && ~~ mask pd_bits) s; slots = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> store_pde (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])) pde \<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>pd. ko = ArchObj (PageDirectory pd) \<and> (\<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pd (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE)) (p && ~~ mask pd_bits) s; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> store_pde p pde \<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>pd. ko = ArchObj (PageDirectory pd) \<and> (\<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pd (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE)) (p && ~~ mask pd_bits) s; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do pd <- get_pd (p && ~~ mask pd_bits);
set_object (p && ~~ mask pd_bits) (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))
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>pd. ko = ArchObj (PageDirectory pd) \<and> (\<forall>x\<in>set (tl (map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). pd (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE)) (p && ~~ mask pd_bits) s; slots = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]; s = sa\<rbrakk> \<Longrightarrow> \<forall>pd. ako_at (PageDirectory pd) (p && ~~ mask pd_bits) sa \<longrightarrow> ((\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and K (obj_valid_pdpt (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))))) sa proof (prove)
goal (1 subgoal):
 1. \<And>p sa pda. \<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])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda))\<rbrakk> \<Longrightarrow> valid_entries pde_range (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) \<and> entries_align pde_range_sz (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) proof (prove)
goal (1 subgoal):
 1. \<And>p sa pda. \<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])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda\<rbrakk> \<Longrightarrow> valid_entries pde_range (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) \<and> entries_align pde_range_sz (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) proof (prove)
goal (2 subgoals):
 1. \<And>p sa pda. \<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])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda\<rbrakk> \<Longrightarrow> valid_entries pde_range (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))
 2. \<And>p sa pda. \<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])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) proof (prove)
goal (3 subgoals):
 1. \<And>p sa pda. \<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])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda\<rbrakk> \<Longrightarrow> valid_entries pde_range pda
 2. \<And>p sa pda 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])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda; pa \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)\<rbrakk> \<Longrightarrow> pde_range pde (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)) \<inter> pde_range (pda pa) pa = {}
 3. \<And>p sa pda. \<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])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) proof (prove)
goal (2 subgoals):
 1. \<And>p sa pda 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])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda; pa \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)\<rbrakk> \<Longrightarrow> pde_range pde (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)) \<inter> pde_range (pda pa) pa = {}
 2. \<And>p sa pda. \<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])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) proof (prove)
goal (2 subgoals):
 1. \<And>p sa pda 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])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda; pa \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); pde_range pde (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)) \<inter> pde_range (pda pa) pa \<noteq> {}\<rbrakk> \<Longrightarrow> False
 2. \<And>p sa pda. \<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])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) proof (prove)
goal (2 subgoals):
 1. \<And>p sa pda 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])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda; pa \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); pde \<noteq> InvalidPDE \<and> pda pa \<noteq> InvalidPDE \<and> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) && ~~ mask 4 = pa && ~~ mask 4\<rbrakk> \<Longrightarrow> False
 2. \<And>p sa pda. \<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])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) proof (prove)
goal (2 subgoals):
 1. \<And>p sa pda 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])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); pa \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) && ~~ mask 4 = pa && ~~ mask 4\<rbrakk> \<Longrightarrow> False
 2. \<And>p sa pda. \<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])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) proof (prove)
goal (2 subgoals):
 1. \<And>p sa pda 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])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); pa \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(32 \<rightarrow> 12) ((p && mask pd_bits >> 2) && ~~ mask 4) = pa && ~~ mask 4\<rbrakk> \<Longrightarrow> False
 2. \<And>p sa pda. \<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])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) proof (prove)
goal (3 subgoals):
 1. \<And>p sa pda 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])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); pa \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE\<rbrakk> \<Longrightarrow> is_aligned (p && mask pd_bits >> 2) 4
 2. \<And>p sa pda 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])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); pa \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) = pa && ~~ mask 4\<rbrakk> \<Longrightarrow> False
 3. \<And>p sa pda. \<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])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) proof (prove)
goal (3 subgoals):
 1. \<And>p sa pda 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])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); pa \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE\<rbrakk> \<Longrightarrow> is_aligned p (4 + 2)
 2. \<And>p sa pda 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])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); pa \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) = pa && ~~ mask 4\<rbrakk> \<Longrightarrow> False
 3. \<And>p sa pda. \<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])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) proof (prove)
goal (2 subgoals):
 1. \<And>p sa pda 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])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); pa \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) = pa && ~~ mask 4\<rbrakk> \<Longrightarrow> False
 2. \<And>p sa pda. \<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])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) proof (prove)
goal (3 subgoals):
 1. \<And>p sa pda 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 pd_bits) = Some (ArchObj (PageDirectory pda)); pa \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) = pa && ~~ mask 4\<rbrakk> \<Longrightarrow> (p && ~~ mask pd_bits) + (UCAST(12 \<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 pda 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 pd_bits) = Some (ArchObj (PageDirectory pda)); pa \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) = pa && ~~ mask 4; pda (UCAST(32 \<rightarrow> 12) ((p && ~~ mask pd_bits) + (UCAST(12 \<rightarrow> 32) pa << 2) && mask pd_bits >> 2)) = InvalidPDE\<rbrakk> \<Longrightarrow> False
 3. \<And>p sa pda. \<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])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) proof (prove)
goal (3 subgoals):
 1. \<And>p sa pda 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 pd_bits) = Some (ArchObj (PageDirectory pda)); pa \<noteq> pa && ~~ mask 4; valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) = pa && ~~ mask 4\<rbrakk> \<Longrightarrow> \<exists>x\<in>{Suc 0..<16}. (p && ~~ mask pd_bits) + (UCAST(12 \<rightarrow> 32) pa << 2) = word_of_nat x * 4 + p
 2. \<And>p sa pda 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 pd_bits) = Some (ArchObj (PageDirectory pda)); pa \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) = pa && ~~ mask 4; pda (UCAST(32 \<rightarrow> 12) ((p && ~~ mask pd_bits) + (UCAST(12 \<rightarrow> 32) pa << 2) && mask pd_bits >> 2)) = InvalidPDE\<rbrakk> \<Longrightarrow> False
 3. \<And>p sa pda. \<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])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) proof (prove)
goal (4 subgoals):
 1. \<And>p sa pda 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 pd_bits) = Some (ArchObj (PageDirectory pda)); pa \<noteq> pa && ~~ mask 4; valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) = pa && ~~ mask 4\<rbrakk> \<Longrightarrow> (p && ~~ mask pd_bits) + (UCAST(12 \<rightarrow> 32) pa << 2) = word_of_nat (unat (UCAST(12 \<rightarrow> 32) pa - (p && mask pd_bits >> 2))) * 4 + p
 2. \<And>p sa pda 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 pd_bits) = Some (ArchObj (PageDirectory pda)); pa \<noteq> pa && ~~ mask 4; valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) = pa && ~~ mask 4\<rbrakk> \<Longrightarrow> unat (UCAST(12 \<rightarrow> 32) pa - (p && mask pd_bits >> 2)) \<in> {Suc 0..<16}
 3. \<And>p sa pda 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 pd_bits) = Some (ArchObj (PageDirectory pda)); pa \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) = pa && ~~ mask 4; pda (UCAST(32 \<rightarrow> 12) ((p && ~~ mask pd_bits) + (UCAST(12 \<rightarrow> 32) pa << 2) && mask pd_bits >> 2)) = InvalidPDE\<rbrakk> \<Longrightarrow> False
 4. \<And>p sa pda. \<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])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) proof (prove)
goal (4 subgoals):
 1. \<And>p sa pda 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 pd_bits)) = Some (ArchObj (PageDirectory pda)); pa && mask 4 \<noteq> 0; valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) = pa - (pa && mask 4)\<rbrakk> \<Longrightarrow> p && mask pd_bits = (p && mask pd_bits >> 2) * 4
 2. \<And>p sa pda 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 pd_bits) = Some (ArchObj (PageDirectory pda)); pa \<noteq> pa && ~~ mask 4; valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) = pa && ~~ mask 4\<rbrakk> \<Longrightarrow> unat (UCAST(12 \<rightarrow> 32) pa - (p && mask pd_bits >> 2)) \<in> {Suc 0..<16}
 3. \<And>p sa pda 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 pd_bits) = Some (ArchObj (PageDirectory pda)); pa \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) = pa && ~~ mask 4; pda (UCAST(32 \<rightarrow> 12) ((p && ~~ mask pd_bits) + (UCAST(12 \<rightarrow> 32) pa << 2) && mask pd_bits >> 2)) = InvalidPDE\<rbrakk> \<Longrightarrow> False
 4. \<And>p sa pda. \<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])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) proof (prove)
goal (4 subgoals):
 1. \<And>p sa pda 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 pd_bits)) = Some (ArchObj (PageDirectory pda)); pa && mask 4 \<noteq> 0; valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) = pa - (pa && mask 4)\<rbrakk> \<Longrightarrow> p && mask pd_bits = p && mask pd_bits >> 2 << 2
 2. \<And>p sa pda 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 pd_bits) = Some (ArchObj (PageDirectory pda)); pa \<noteq> pa && ~~ mask 4; valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) = pa && ~~ mask 4\<rbrakk> \<Longrightarrow> unat (UCAST(12 \<rightarrow> 32) pa - (p && mask pd_bits >> 2)) \<in> {Suc 0..<16}
 3. \<And>p sa pda 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 pd_bits) = Some (ArchObj (PageDirectory pda)); pa \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) = pa && ~~ mask 4; pda (UCAST(32 \<rightarrow> 12) ((p && ~~ mask pd_bits) + (UCAST(12 \<rightarrow> 32) pa << 2) && mask pd_bits >> 2)) = InvalidPDE\<rbrakk> \<Longrightarrow> False
 4. \<And>p sa pda. \<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])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) proof (prove)
goal (5 subgoals):
 1. \<And>p sa pda 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 pd_bits)) = Some (ArchObj (PageDirectory pda)); pa && mask 4 \<noteq> 0; valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) = pa - (pa && mask 4)\<rbrakk> \<Longrightarrow> 2 \<le> 2
 2. \<And>p sa pda 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 pd_bits)) = Some (ArchObj (PageDirectory pda)); pa && mask 4 \<noteq> 0; valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) = pa - (pa && mask 4)\<rbrakk> \<Longrightarrow> p && mask pd_bits = (p && mask pd_bits >> 2 - 2) && ~~ mask 2
 3. \<And>p sa pda 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 pd_bits) = Some (ArchObj (PageDirectory pda)); pa \<noteq> pa && ~~ mask 4; valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) = pa && ~~ mask 4\<rbrakk> \<Longrightarrow> unat (UCAST(12 \<rightarrow> 32) pa - (p && mask pd_bits >> 2)) \<in> {Suc 0..<16}
 4. \<And>p sa pda 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 pd_bits) = Some (ArchObj (PageDirectory pda)); pa \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) = pa && ~~ mask 4; pda (UCAST(32 \<rightarrow> 12) ((p && ~~ mask pd_bits) + (UCAST(12 \<rightarrow> 32) pa << 2) && mask pd_bits >> 2)) = InvalidPDE\<rbrakk> \<Longrightarrow> False
 5. \<And>p sa pda. \<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])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) proof (prove)
goal (4 subgoals):
 1. \<And>p sa pda 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 pd_bits)) = Some (ArchObj (PageDirectory pda)); pa && mask 4 \<noteq> 0; valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) = pa - (pa && mask 4)\<rbrakk> \<Longrightarrow> p && mask pd_bits = (p && mask pd_bits) && ~~ mask 2
 2. \<And>p sa pda 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 pd_bits) = Some (ArchObj (PageDirectory pda)); pa \<noteq> pa && ~~ mask 4; valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) = pa && ~~ mask 4\<rbrakk> \<Longrightarrow> unat (UCAST(12 \<rightarrow> 32) pa - (p && mask pd_bits >> 2)) \<in> {Suc 0..<16}
 3. \<And>p sa pda 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 pd_bits) = Some (ArchObj (PageDirectory pda)); pa \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) = pa && ~~ mask 4; pda (UCAST(32 \<rightarrow> 12) ((p && ~~ mask pd_bits) + (UCAST(12 \<rightarrow> 32) pa << 2) && mask pd_bits >> 2)) = InvalidPDE\<rbrakk> \<Longrightarrow> False
 4. \<And>p sa pda. \<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])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) proof (prove)
goal (5 subgoals):
 1. \<And>p sa pda 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 pd_bits)) = Some (ArchObj (PageDirectory pda)); pa && mask 4 \<noteq> 0; valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) = pa - (pa && mask 4)\<rbrakk> \<Longrightarrow> is_aligned (p && mask pd_bits) 2
 2. \<And>p sa pda 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 pd_bits)) = Some (ArchObj (PageDirectory pda)); pa && mask 4 \<noteq> 0; valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) = pa - (pa && mask 4)\<rbrakk> \<Longrightarrow> p && mask pd_bits = p && mask pd_bits
 3. \<And>p sa pda 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 pd_bits) = Some (ArchObj (PageDirectory pda)); pa \<noteq> pa && ~~ mask 4; valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) = pa && ~~ mask 4\<rbrakk> \<Longrightarrow> unat (UCAST(12 \<rightarrow> 32) pa - (p && mask pd_bits >> 2)) \<in> {Suc 0..<16}
 4. \<And>p sa pda 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 pd_bits) = Some (ArchObj (PageDirectory pda)); pa \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) = pa && ~~ mask 4; pda (UCAST(32 \<rightarrow> 12) ((p && ~~ mask pd_bits) + (UCAST(12 \<rightarrow> 32) pa << 2) && mask pd_bits >> 2)) = InvalidPDE\<rbrakk> \<Longrightarrow> False
 5. \<And>p sa pda. \<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])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) proof (prove)
goal (5 subgoals):
 1. \<And>p sa pda pa. \<lbrakk>slots = p # map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [Suc 0..<16]; kheap sa (p - (p && mask pd_bits)) = Some (ArchObj (PageDirectory pda)); pa && mask 4 \<noteq> 0; valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) = pa - (pa && mask 4)\<rbrakk> \<Longrightarrow> 2 \<le> 6
 2. \<And>p sa pda 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 pd_bits)) = Some (ArchObj (PageDirectory pda)); pa && mask 4 \<noteq> 0; valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) = pa - (pa && mask 4)\<rbrakk> \<Longrightarrow> p && mask pd_bits = p && mask pd_bits
 3. \<And>p sa pda 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 pd_bits) = Some (ArchObj (PageDirectory pda)); pa \<noteq> pa && ~~ mask 4; valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) = pa && ~~ mask 4\<rbrakk> \<Longrightarrow> unat (UCAST(12 \<rightarrow> 32) pa - (p && mask pd_bits >> 2)) \<in> {Suc 0..<16}
 4. \<And>p sa pda 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 pd_bits) = Some (ArchObj (PageDirectory pda)); pa \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) = pa && ~~ mask 4; pda (UCAST(32 \<rightarrow> 12) ((p && ~~ mask pd_bits) + (UCAST(12 \<rightarrow> 32) pa << 2) && mask pd_bits >> 2)) = InvalidPDE\<rbrakk> \<Longrightarrow> False
 5. \<And>p sa pda. \<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])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) proof (prove)
goal (4 subgoals):
 1. \<And>p sa pda 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 pd_bits)) = Some (ArchObj (PageDirectory pda)); pa && mask 4 \<noteq> 0; valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) = pa - (pa && mask 4)\<rbrakk> \<Longrightarrow> p && mask pd_bits = p && mask pd_bits
 2. \<And>p sa pda 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 pd_bits) = Some (ArchObj (PageDirectory pda)); pa \<noteq> pa && ~~ mask 4; valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) = pa && ~~ mask 4\<rbrakk> \<Longrightarrow> unat (UCAST(12 \<rightarrow> 32) pa - (p && mask pd_bits >> 2)) \<in> {Suc 0..<16}
 3. \<And>p sa pda 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 pd_bits) = Some (ArchObj (PageDirectory pda)); pa \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) = pa && ~~ mask 4; pda (UCAST(32 \<rightarrow> 12) ((p && ~~ mask pd_bits) + (UCAST(12 \<rightarrow> 32) pa << 2) && mask pd_bits >> 2)) = InvalidPDE\<rbrakk> \<Longrightarrow> False
 4. \<And>p sa pda. \<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])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) proof (prove)
goal (3 subgoals):
 1. \<And>p sa pda 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 pd_bits) = Some (ArchObj (PageDirectory pda)); pa \<noteq> pa && ~~ mask 4; valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) = pa && ~~ mask 4\<rbrakk> \<Longrightarrow> unat (UCAST(12 \<rightarrow> 32) pa - (p && mask pd_bits >> 2)) \<in> {Suc 0..<16}
 2. \<And>p sa pda 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 pd_bits) = Some (ArchObj (PageDirectory pda)); pa \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) = pa && ~~ mask 4; pda (UCAST(32 \<rightarrow> 12) ((p && ~~ mask pd_bits) + (UCAST(12 \<rightarrow> 32) pa << 2) && mask pd_bits >> 2)) = InvalidPDE\<rbrakk> \<Longrightarrow> False
 3. \<And>p sa pda. \<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])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) proof (prove)
goal (3 subgoals):
 1. \<And>p sa pda 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 pd_bits) = Some (ArchObj (PageDirectory pda)); pa \<noteq> pa && ~~ mask 4; valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) = pa && ~~ mask 4\<rbrakk> \<Longrightarrow> Suc 0 \<le> unat (UCAST(12 \<rightarrow> 32) pa - (p && mask pd_bits >> 2)) \<and> unat (UCAST(12 \<rightarrow> 32) pa - (p && mask pd_bits >> 2)) < 16
 2. \<And>p sa pda 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 pd_bits) = Some (ArchObj (PageDirectory pda)); pa \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) = pa && ~~ mask 4; pda (UCAST(32 \<rightarrow> 12) ((p && ~~ mask pd_bits) + (UCAST(12 \<rightarrow> 32) pa << 2) && mask pd_bits >> 2)) = InvalidPDE\<rbrakk> \<Longrightarrow> False
 3. \<And>p sa pda. \<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])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) proof (prove)
goal (3 subgoals):
 1. \<And>p sa pda 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 pd_bits) = Some (ArchObj (PageDirectory pda)); pa \<noteq> pa && ~~ mask 4; valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; pa && ~~ mask 4 = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)\<rbrakk> \<Longrightarrow> Suc 0 \<le> unat (UCAST(12 \<rightarrow> 32) pa - (p && mask pd_bits >> 2)) \<and> unat (UCAST(12 \<rightarrow> 32) pa - (p && mask pd_bits >> 2)) < 16
 2. \<And>p sa pda 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 pd_bits) = Some (ArchObj (PageDirectory pda)); pa \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) = pa && ~~ mask 4; pda (UCAST(32 \<rightarrow> 12) ((p && ~~ mask pd_bits) + (UCAST(12 \<rightarrow> 32) pa << 2) && mask pd_bits >> 2)) = InvalidPDE\<rbrakk> \<Longrightarrow> False
 3. \<And>p sa pda. \<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])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) proof (prove)
goal (3 subgoals):
 1. \<And>p sa pda 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 pd_bits)) = Some (ArchObj (PageDirectory pda)); pa && mask 4 \<noteq> 0; valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; pa = (pa && mask 4) + UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)\<rbrakk> \<Longrightarrow> Suc 0 \<le> unat (UCAST(12 \<rightarrow> 32) pa - (p && mask pd_bits >> 2)) \<and> unat (UCAST(12 \<rightarrow> 32) pa - (p && mask pd_bits >> 2)) < 16
 2. \<And>p sa pda 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 pd_bits) = Some (ArchObj (PageDirectory pda)); pa \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) = pa && ~~ mask 4; pda (UCAST(32 \<rightarrow> 12) ((p && ~~ mask pd_bits) + (UCAST(12 \<rightarrow> 32) pa << 2) && mask pd_bits >> 2)) = InvalidPDE\<rbrakk> \<Longrightarrow> False
 3. \<And>p sa pda. \<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])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) proof (prove)
goal (3 subgoals):
 1. \<And>p sa pda 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 pd_bits)) = Some (ArchObj (PageDirectory pda)); pa && mask 4 \<noteq> 0; valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(12 \<rightarrow> 32) pa = UCAST(12 \<rightarrow> 32) ((pa && mask 4) + UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))\<rbrakk> \<Longrightarrow> Suc 0 \<le> unat (UCAST(12 \<rightarrow> 32) pa - (p && mask pd_bits >> 2)) \<and> unat (UCAST(12 \<rightarrow> 32) pa - (p && mask pd_bits >> 2)) < 16
 2. \<And>p sa pda 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 pd_bits) = Some (ArchObj (PageDirectory pda)); pa \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) = pa && ~~ mask 4; pda (UCAST(32 \<rightarrow> 12) ((p && ~~ mask pd_bits) + (UCAST(12 \<rightarrow> 32) pa << 2) && mask pd_bits >> 2)) = InvalidPDE\<rbrakk> \<Longrightarrow> False
 3. \<And>p sa pda. \<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])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) proof (prove)
goal (3 subgoals):
 1. \<And>p sa pda 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 pd_bits)) = Some (ArchObj (PageDirectory pda)); pa && mask 4 \<noteq> 0; valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(12 \<rightarrow> 32) pa = UCAST(12 \<rightarrow> 32) (pa && mask 4) + (p && mask pd_bits >> 2)\<rbrakk> \<Longrightarrow> Suc 0 \<le> unat (UCAST(12 \<rightarrow> 32) (pa && mask 4)) \<and> unat (UCAST(12 \<rightarrow> 32) (pa && mask 4)) < 16
 2. \<And>p sa pda 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 pd_bits) = Some (ArchObj (PageDirectory pda)); pa \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) = pa && ~~ mask 4; pda (UCAST(32 \<rightarrow> 12) ((p && ~~ mask pd_bits) + (UCAST(12 \<rightarrow> 32) pa << 2) && mask pd_bits >> 2)) = InvalidPDE\<rbrakk> \<Longrightarrow> False
 3. \<And>p sa pda. \<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])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) proof (prove)
goal (3 subgoals):
 1. \<And>p sa pda 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 pd_bits)) = Some (ArchObj (PageDirectory pda)); pa && mask 4 \<noteq> 0; valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(12 \<rightarrow> 32) pa = UCAST(12 \<rightarrow> 32) (pa && mask 4) + (p && mask pd_bits >> 2)\<rbrakk> \<Longrightarrow> Suc 0 \<le> unat (pa && mask 4) \<and> unat (pa && mask 4) < 16
 2. \<And>p sa pda 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 pd_bits) = Some (ArchObj (PageDirectory pda)); pa \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) = pa && ~~ mask 4; pda (UCAST(32 \<rightarrow> 12) ((p && ~~ mask pd_bits) + (UCAST(12 \<rightarrow> 32) pa << 2) && mask pd_bits >> 2)) = InvalidPDE\<rbrakk> \<Longrightarrow> False
 3. \<And>p sa pda. \<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])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) proof (prove)
goal (4 subgoals):
 1. \<And>p sa pda 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 pd_bits)) = Some (ArchObj (PageDirectory pda)); pa && mask 4 \<noteq> 0; valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(12 \<rightarrow> 32) pa = UCAST(12 \<rightarrow> 32) (pa && mask 4) + (p && mask pd_bits >> 2)\<rbrakk> \<Longrightarrow> Suc 0 \<le> unat (pa && mask 4)
 2. \<And>p sa pda 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 pd_bits)) = Some (ArchObj (PageDirectory pda)); pa && mask 4 \<noteq> 0; valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(12 \<rightarrow> 32) pa = UCAST(12 \<rightarrow> 32) (pa && mask 4) + (p && mask pd_bits >> 2)\<rbrakk> \<Longrightarrow> unat (pa && mask 4) < 16
 3. \<And>p sa pda 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 pd_bits) = Some (ArchObj (PageDirectory pda)); pa \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) = pa && ~~ mask 4; pda (UCAST(32 \<rightarrow> 12) ((p && ~~ mask pd_bits) + (UCAST(12 \<rightarrow> 32) pa << 2) && mask pd_bits >> 2)) = InvalidPDE\<rbrakk> \<Longrightarrow> False
 4. \<And>p sa pda. \<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])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) proof (prove)
goal (5 subgoals):
 1. \<And>p sa pda 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 pd_bits)) = Some (ArchObj (PageDirectory pda)); pa && mask 4 \<noteq> 0; valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(12 \<rightarrow> 32) pa = UCAST(12 \<rightarrow> 32) (pa && mask 4) + (p && mask pd_bits >> 2); unat (pa && mask 4) \<noteq> 0\<rbrakk> \<Longrightarrow> Suc 0 \<le> unat (pa && mask 4)
 2. \<And>p sa pda 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 pd_bits)) = Some (ArchObj (PageDirectory pda)); pa && mask 4 \<noteq> 0; valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(12 \<rightarrow> 32) pa = UCAST(12 \<rightarrow> 32) (pa && mask 4) + (p && mask pd_bits >> 2)\<rbrakk> \<Longrightarrow> unat (pa && mask 4) \<noteq> 0
 3. \<And>p sa pda 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 pd_bits)) = Some (ArchObj (PageDirectory pda)); pa && mask 4 \<noteq> 0; valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(12 \<rightarrow> 32) pa = UCAST(12 \<rightarrow> 32) (pa && mask 4) + (p && mask pd_bits >> 2)\<rbrakk> \<Longrightarrow> unat (pa && mask 4) < 16
 4. \<And>p sa pda 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 pd_bits) = Some (ArchObj (PageDirectory pda)); pa \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) = pa && ~~ mask 4; pda (UCAST(32 \<rightarrow> 12) ((p && ~~ mask pd_bits) + (UCAST(12 \<rightarrow> 32) pa << 2) && mask pd_bits >> 2)) = InvalidPDE\<rbrakk> \<Longrightarrow> False
 5. \<And>p sa pda. \<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])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) proof (prove)
goal (4 subgoals):
 1. \<And>p sa pda 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 pd_bits)) = Some (ArchObj (PageDirectory pda)); pa && mask 4 \<noteq> 0; valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(12 \<rightarrow> 32) pa = UCAST(12 \<rightarrow> 32) (pa && mask 4) + (p && mask pd_bits >> 2)\<rbrakk> \<Longrightarrow> unat (pa && mask 4) \<noteq> 0
 2. \<And>p sa pda 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 pd_bits)) = Some (ArchObj (PageDirectory pda)); pa && mask 4 \<noteq> 0; valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(12 \<rightarrow> 32) pa = UCAST(12 \<rightarrow> 32) (pa && mask 4) + (p && mask pd_bits >> 2)\<rbrakk> \<Longrightarrow> unat (pa && mask 4) < 16
 3. \<And>p sa pda 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 pd_bits) = Some (ArchObj (PageDirectory pda)); pa \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) = pa && ~~ mask 4; pda (UCAST(32 \<rightarrow> 12) ((p && ~~ mask pd_bits) + (UCAST(12 \<rightarrow> 32) pa << 2) && mask pd_bits >> 2)) = InvalidPDE\<rbrakk> \<Longrightarrow> False
 4. \<And>p sa pda. \<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])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) proof (prove)
goal (3 subgoals):
 1. \<And>p sa pda 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 pd_bits)) = Some (ArchObj (PageDirectory pda)); pa && mask 4 \<noteq> 0; valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(12 \<rightarrow> 32) pa = UCAST(12 \<rightarrow> 32) (pa && mask 4) + (p && mask pd_bits >> 2)\<rbrakk> \<Longrightarrow> unat (pa && mask 4) < 16
 2. \<And>p sa pda 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 pd_bits) = Some (ArchObj (PageDirectory pda)); pa \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) = pa && ~~ mask 4; pda (UCAST(32 \<rightarrow> 12) ((p && ~~ mask pd_bits) + (UCAST(12 \<rightarrow> 32) pa << 2) && mask pd_bits >> 2)) = InvalidPDE\<rbrakk> \<Longrightarrow> False
 3. \<And>p sa pda. \<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])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) proof (prove)
goal (3 subgoals):
 1. \<And>p sa pda 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 pd_bits)) = Some (ArchObj (PageDirectory pda)); pa && mask 4 \<noteq> 0; valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(12 \<rightarrow> 32) pa = UCAST(12 \<rightarrow> 32) (pa && mask 4) + (p && mask pd_bits >> 2)\<rbrakk> \<Longrightarrow> pa && mask 4 < word_of_nat 16
 2. \<And>p sa pda 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 pd_bits) = Some (ArchObj (PageDirectory pda)); pa \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) = pa && ~~ mask 4; pda (UCAST(32 \<rightarrow> 12) ((p && ~~ mask pd_bits) + (UCAST(12 \<rightarrow> 32) pa << 2) && mask pd_bits >> 2)) = InvalidPDE\<rbrakk> \<Longrightarrow> False
 3. \<And>p sa pda. \<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])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) proof (prove)
goal (3 subgoals):
 1. \<And>p sa pda 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 pd_bits)) = Some (ArchObj (PageDirectory pda)); pa && mask 4 \<noteq> 0; valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(12 \<rightarrow> 32) pa = UCAST(12 \<rightarrow> 32) (pa && mask 4) + (p && mask pd_bits >> 2)\<rbrakk> \<Longrightarrow> mask 4 < word_of_nat 16
 2. \<And>p sa pda 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 pd_bits) = Some (ArchObj (PageDirectory pda)); pa \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) = pa && ~~ mask 4; pda (UCAST(32 \<rightarrow> 12) ((p && ~~ mask pd_bits) + (UCAST(12 \<rightarrow> 32) pa << 2) && mask pd_bits >> 2)) = InvalidPDE\<rbrakk> \<Longrightarrow> False
 3. \<And>p sa pda. \<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])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) proof (prove)
goal (2 subgoals):
 1. \<And>p sa pda 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 pd_bits) = Some (ArchObj (PageDirectory pda)); pa \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) = pa && ~~ mask 4; pda (UCAST(32 \<rightarrow> 12) ((p && ~~ mask pd_bits) + (UCAST(12 \<rightarrow> 32) pa << 2) && mask pd_bits >> 2)) = InvalidPDE\<rbrakk> \<Longrightarrow> False
 2. \<And>p sa pda. \<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])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) proof (prove)
goal (2 subgoals):
 1. \<And>p sa pda 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 pd_bits) = Some (ArchObj (PageDirectory pda)); pa \<noteq> pa && ~~ mask 4; valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) = pa && ~~ mask 4; pda (UCAST(32 \<rightarrow> 12) ((UCAST(12 \<rightarrow> 32) pa << 2) && mask pd_bits >> 2)) = InvalidPDE\<rbrakk> \<Longrightarrow> False
 2. \<And>p sa pda. \<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])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) proof (prove)
goal (2 subgoals):
 1. \<And>p sa pda 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 pd_bits) = Some (ArchObj (PageDirectory pda)); pa \<noteq> pa && ~~ mask 4; valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; pda (UCAST(32 \<rightarrow> 12) ((UCAST(12 \<rightarrow> 32) pa << 2) && mask pd_bits >> 2)) = InvalidPDE\<rbrakk> \<Longrightarrow> False
 2. \<And>p sa pda. \<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])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) proof (prove)
goal (3 subgoals):
 1. \<And>p sa pda 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 pd_bits) = Some (ArchObj (PageDirectory pda)); pa \<noteq> pa && ~~ mask 4; valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE\<rbrakk> \<Longrightarrow> UCAST(12 \<rightarrow> 32) pa << 2 < 2 ^ pd_bits
 2. \<And>p sa pda 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 pd_bits) = Some (ArchObj (PageDirectory pda)); pa \<noteq> pa && ~~ mask 4; valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; pda (UCAST(32 \<rightarrow> 12) (UCAST(12 \<rightarrow> 32) pa << 2 >> 2)) = InvalidPDE\<rbrakk> \<Longrightarrow> False
 3. \<And>p sa pda. \<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])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) proof (prove)
goal (4 subgoals):
 1. \<And>p sa pda 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 pd_bits) = Some (ArchObj (PageDirectory pda)); pa \<noteq> pa && ~~ mask 4; valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE\<rbrakk> \<Longrightarrow> UCAST(12 \<rightarrow> 32) pa < 2 ^ (pd_bits - 2)
 2. \<And>p sa pda 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 pd_bits) = Some (ArchObj (PageDirectory pda)); pa \<noteq> pa && ~~ mask 4; valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE\<rbrakk> \<Longrightarrow> pd_bits < LENGTH(32)
 3. \<And>p sa pda 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 pd_bits) = Some (ArchObj (PageDirectory pda)); pa \<noteq> pa && ~~ mask 4; valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; pda (UCAST(32 \<rightarrow> 12) (UCAST(12 \<rightarrow> 32) pa << 2 >> 2)) = InvalidPDE\<rbrakk> \<Longrightarrow> False
 4. \<And>p sa pda. \<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])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) proof (prove)
goal (4 subgoals):
 1. \<And>p sa pda 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 14) = Some (ArchObj (PageDirectory pda)); pa \<noteq> pa && ~~ mask 4; valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE\<rbrakk> \<Longrightarrow> UCAST(12 \<rightarrow> 32) pa < 0x1000
 2. \<And>p sa pda 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 pd_bits) = Some (ArchObj (PageDirectory pda)); pa \<noteq> pa && ~~ mask 4; valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE\<rbrakk> \<Longrightarrow> pd_bits < LENGTH(32)
 3. \<And>p sa pda 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 pd_bits) = Some (ArchObj (PageDirectory pda)); pa \<noteq> pa && ~~ mask 4; valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; pda (UCAST(32 \<rightarrow> 12) (UCAST(12 \<rightarrow> 32) pa << 2 >> 2)) = InvalidPDE\<rbrakk> \<Longrightarrow> False
 4. \<And>p sa pda. \<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])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) proof (prove)
goal (3 subgoals):
 1. \<And>p sa pda 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 pd_bits) = Some (ArchObj (PageDirectory pda)); pa \<noteq> pa && ~~ mask 4; valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE\<rbrakk> \<Longrightarrow> pd_bits < LENGTH(32)
 2. \<And>p sa pda 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 pd_bits) = Some (ArchObj (PageDirectory pda)); pa \<noteq> pa && ~~ mask 4; valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; pda (UCAST(32 \<rightarrow> 12) (UCAST(12 \<rightarrow> 32) pa << 2 >> 2)) = InvalidPDE\<rbrakk> \<Longrightarrow> False
 3. \<And>p sa pda. \<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])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) proof (prove)
goal (2 subgoals):
 1. \<And>p sa pda 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 pd_bits) = Some (ArchObj (PageDirectory pda)); pa \<noteq> pa && ~~ mask 4; valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; pda (UCAST(32 \<rightarrow> 12) (UCAST(12 \<rightarrow> 32) pa << 2 >> 2)) = InvalidPDE\<rbrakk> \<Longrightarrow> False
 2. \<And>p sa pda. \<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])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) proof (prove)
goal (4 subgoals):
 1. \<And>p sa pda 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 pd_bits) = Some (ArchObj (PageDirectory pda)); pa \<noteq> pa && ~~ mask 4; valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE\<rbrakk> \<Longrightarrow> 2 < LENGTH(32)
 2. \<And>p sa pda 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 pd_bits) = Some (ArchObj (PageDirectory pda)); pa \<noteq> pa && ~~ mask 4; valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE\<rbrakk> \<Longrightarrow> UCAST(12 \<rightarrow> 32) pa < 2 ^ (LENGTH(32) - 2)
 3. \<And>p sa pda 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 pd_bits) = Some (ArchObj (PageDirectory pda)); pa \<noteq> pa && ~~ mask 4; valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; pda (UCAST(32 \<rightarrow> 12) (UCAST(12 \<rightarrow> 32) pa)) = InvalidPDE\<rbrakk> \<Longrightarrow> False
 4. \<And>p sa pda. \<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])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) proof (prove)
goal (3 subgoals):
 1. \<And>p sa pda 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 pd_bits) = Some (ArchObj (PageDirectory pda)); pa \<noteq> pa && ~~ mask 4; valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE\<rbrakk> \<Longrightarrow> UCAST(12 \<rightarrow> 32) pa < 2 ^ (LENGTH(32) - 2)
 2. \<And>p sa pda 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 pd_bits) = Some (ArchObj (PageDirectory pda)); pa \<noteq> pa && ~~ mask 4; valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; pda (UCAST(32 \<rightarrow> 12) (UCAST(12 \<rightarrow> 32) pa)) = InvalidPDE\<rbrakk> \<Longrightarrow> False
 3. \<And>p sa pda. \<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])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) proof (prove)
goal (2 subgoals):
 1. \<And>p sa pda 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 pd_bits) = Some (ArchObj (PageDirectory pda)); pa \<noteq> pa && ~~ mask 4; valid_entries pde_range pda; entries_align pde_range_sz pda; pde \<noteq> InvalidPDE; pda pa \<noteq> InvalidPDE; pda (UCAST(32 \<rightarrow> 12) (UCAST(12 \<rightarrow> 32) pa)) = InvalidPDE\<rbrakk> \<Longrightarrow> False
 2. \<And>p sa pda. \<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])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) proof (prove)
goal (1 subgoal):
 1. \<And>p sa pda. \<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])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> entries_align pde_range_sz pda\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) proof (prove)
goal (1 subgoal):
 1. \<And>p sa pda. \<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])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> (\<forall>x. is_aligned x (pde_range_sz (pda x)))\<rbrakk> \<Longrightarrow> is_aligned (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)) (pde_range_sz pde) proof (prove)
goal (1 subgoal):
 1. \<And>p sa pda. \<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])). pda (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_entries pde_range pda \<and> (\<forall>x. is_aligned x (pde_range_sz (pda x)))\<rbrakk> \<Longrightarrow> is_aligned (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)) 4 proof (prove)
goal:
No subgoals!