theory Finalise_DR

lemma dcorres_unmap_large_page:
  "is_aligned ptr 6
    \<Longrightarrow> dcorres dc \<top> (invs and valid_pdpt_objs
          and pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr {ARMLargePage})
     (delete_cap_simple (transform_pt_slot_ref ptr))
     (mapM (swp store_pte ARM_A.pte.InvalidPTE) (map (\<lambda>x. x + ptr) [0 , 4 .e. 0x3C]))" supply is_aligned_neg_mask_eq[simp del]
         is_aligned_neg_mask_weaken[simp del] apply (subst mapM_Cons_split) apply (simp add:upto_enum_step_def upto_enum_def) apply (simp add: PageTableUnmap_D.unmap_page_def) apply (rule corres_dummy_return_l) apply (simp add:upto_enum_step_def transform_pt_slot_ref_def upto_enum_def hd_map_simp)+ apply (rule corres_guard_imp) apply(rule corres_dummy_return_l) apply (rule corres_split[OF dcorres_store_invalid_pte[where pg_id = pg_id]]) apply(rule corres_dummy_return_l) apply (rule_tac r'=dc in corres_split) apply (rule dcorres_store_invalid_pte_tail_large_page[where slot = ptr]) apply (rule corres_return_trivial) apply wp+ apply (wp store_pte_non_sense_wp) apply simp apply (clarsimp simp:unat_def pt_page_relation_univ) apply (rule conjI,fastforce) apply (rule conj_comms[THEN iffD1]) apply (rule context_conjI) apply (clarsimp simp:tl_map drop_map) apply (simp add:field_simps) apply (subst mask_lower_twice[symmetric,where n = 6]) apply (simp add:pt_bits_def pageBits_def) apply (subst is_aligned_add_helper) apply simp apply (simp add:upto_0_to_n) apply (rule word_less_power_trans_ofnat[where k = 2 and m = 6,simplified]) apply simp apply simp apply simp apply (clarsimp simp:pt_page_relation_def obj_at_def) apply (drule(1) bspec) apply (clarsimp simp:tl_map drop_map upto_0_to_n) apply (simp add: field_simps) apply (drule(1) valid_pdpt_objs_ptD,clarify) apply (drule_tac x = "(ucast (ptr + of_nat x * 4 && mask pt_bits >> 2))"
               and y = "ucast (ptr && mask pt_bits >> 2)"
                in valid_entriesD[rotated]) apply (rule ccontr) apply simp apply (drule_tac x="ucast v" for v in arg_cong[where f = "ucast::(word8\<Rightarrow>word32)"]) apply (drule_tac x="ucast v" for v in arg_cong[where f = "\<lambda>x. shiftl x 2"]) apply (subst (asm) ucast_ucast_len) apply (rule shiftr_less_t2n) apply (rule less_le_trans[OF and_mask_less']) apply (simp add:pt_bits_def pageBits_def) apply (simp add:pt_bits_def pageBits_def) apply (subst (asm) ucast_ucast_len) apply (rule shiftr_less_t2n) apply (rule less_le_trans[OF and_mask_less']) apply (simp add:pt_bits_def pageBits_def) apply (simp add:pt_bits_def pageBits_def) apply (simp add:shiftr_shiftl1) apply (subst (asm) is_aligned_neg_mask_eq[where n = 2]) apply (erule is_aligned_andI1[OF aligned_add_aligned]) apply (simp add: shiftl_t2n[symmetric, where n=2, simplified field_simps, simplified]
                      is_aligned_shiftl_self) apply simp apply (subst (asm) is_aligned_neg_mask_eq[where n = 2]) apply (erule is_aligned_andI1[OF is_aligned_weaken]) apply simp apply (subst (asm) and_mask_plus) apply simp apply (simp add:pt_bits_def pageBits_def)+ apply (simp add:shiftl_t2n[symmetric,where n =2,simplified field_simps,simplified]) apply (rule shiftl_less_t2n[where m = 6,simplified]) apply (simp add:word_of_nat_less) apply simp apply simp apply (subgoal_tac "0 < (of_nat (x * 4)::word32)") apply simp apply (rule le_less_trans[OF _ of_nat_mono_maybe[where y = 0]]) apply fastforce apply simp apply fastforce apply (clarsimp split:if_splits pte.split_asm) apply (rule ccontr) apply (erule_tac x = "ucast (ptr + of_nat x * 4 && mask pt_bits >> 2)" in in_empty_interE) apply (rule non_invalid_in_pte_range) apply simp apply (simp add: ucast_neg_mask) apply (rule arg_cong[where f = ucast]) apply (rule shiftr_eq_neg_mask_eq) apply (simp add:shiftr_shiftr shiftr_over_and_dist) apply (subst aligned_shift') apply (simp add:shiftl_t2n[symmetric,where n =2,simplified field_simps,simplified]) apply (rule shiftl_less_t2n[where m = 6,simplified]) apply (simp add:word_of_nat_less) apply (simp+)[4] apply (simp add: is_aligned_shiftr) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned ptr 6 \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr {ARMLargePage}) (delete_cap_simple (transform_pt_slot_ref ptr)) (mapM (swp store_pte InvalidPTE) (map (\<lambda>x. x + ptr) [0 , 4 .e. 0x3C])) proof (prove)
goal (1 subgoal):
 1. is_aligned ptr 6 \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr {ARMLargePage}) (delete_cap_simple (transform_pt_slot_ref ptr)) (mapM (swp store_pte InvalidPTE) (map (\<lambda>x. x + ptr) [0 , 4 .e. 0x3C])) proof (prove)
goal (2 subgoals):
 1. is_aligned ptr 6 \<Longrightarrow> map (\<lambda>x. x + ptr) [0 , 4 .e. 0x3C] \<noteq> []
 2. is_aligned ptr 6 \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and (\<lambda>s. Ball (ran (kheap s)) obj_valid_pdpt) and pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr {ARMLargePage}) (delete_cap_simple (transform_pt_slot_ref ptr)) (do y <- swp store_pte InvalidPTE (hd (map (\<lambda>x. x + ptr) [0 , 4 .e. 0x3C]));
ys <- mapM (swp store_pte InvalidPTE) (tl (map (\<lambda>x. x + ptr) [0 , 4 .e. 0x3C]));
return (y # ys)
od) proof (prove)
goal (1 subgoal):
 1. is_aligned ptr 6 \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and (\<lambda>s. Ball (ran (kheap s)) obj_valid_pdpt) and pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr {ARMLargePage}) (delete_cap_simple (transform_pt_slot_ref ptr)) (do y <- swp store_pte InvalidPTE (hd (map (\<lambda>x. x + ptr) [0 , 4 .e. 0x3C]));
ys <- mapM (swp store_pte InvalidPTE) (tl (map (\<lambda>x. x + ptr) [0 , 4 .e. 0x3C]));
return (y # ys)
od) proof (prove)
goal (1 subgoal):
 1. is_aligned ptr 6 \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr {ARMLargePage}) (delete_cap_simple (transform_pt_slot_ref ptr)) (do y <- store_pte (hd (map (\<lambda>x. x + ptr) [0 , 4 .e. 0x3C])) InvalidPTE;
ys <- mapM (swp store_pte InvalidPTE) (tl (map (\<lambda>x. x + ptr) [0 , 4 .e. 0x3C]));
return (() # ys)
od) proof (prove)
goal (1 subgoal):
 1. is_aligned ptr 6 \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr {ARMLargePage}) (delete_cap_simple (transform_pt_slot_ref ptr) >>= return) (do y <- store_pte (hd (map (\<lambda>x. x + ptr) [0 , 4 .e. 0x3C])) InvalidPTE;
ys <- mapM (swp store_pte InvalidPTE) (tl (map (\<lambda>x. x + ptr) [0 , 4 .e. 0x3C]));
return (() # ys)
od) proof (prove)
goal (1 subgoal):
 1. is_aligned ptr 6 \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr {ARMLargePage}) (delete_cap_simple (ptr && ~~ mask pt_bits, unat (ptr && mask pt_bits >> 2))) (do y <- store_pte ptr InvalidPTE;
ys <- mapM (swp store_pte InvalidPTE) (tl (map ((\<lambda>x. x + ptr) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]));
return (() # ys)
od) proof (prove)
goal (3 subgoals):
 1. is_aligned ptr 6 \<Longrightarrow> dcorres dc ?Q15 ?Q'15 (delete_cap_simple (ptr && ~~ mask pt_bits, unat (ptr && mask pt_bits >> 2))) (do y <- store_pte ptr InvalidPTE;
ys <- mapM (swp store_pte InvalidPTE) (tl (map ((\<lambda>x. x + ptr) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]));
return (() # ys)
od)
 2. \<And>s. \<lbrakk>is_aligned ptr 6; True\<rbrakk> \<Longrightarrow> ?Q15 s
 3. \<And>s. \<lbrakk>is_aligned ptr 6; (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr {ARMLargePage}) s\<rbrakk> \<Longrightarrow> ?Q'15 s proof (prove)
goal (3 subgoals):
 1. is_aligned ptr 6 \<Longrightarrow> dcorres dc ?Q15 ?Q'15 (delete_cap_simple (ptr && ~~ mask pt_bits, unat (ptr && mask pt_bits >> 2)) >>= return) (do y <- store_pte ptr InvalidPTE;
ys <- mapM (swp store_pte InvalidPTE) (tl (map ((\<lambda>x. x + ptr) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]));
return (() # ys)
od)
 2. \<And>s. \<lbrakk>is_aligned ptr 6; True\<rbrakk> \<Longrightarrow> ?Q15 s
 3. \<And>s. \<lbrakk>is_aligned ptr 6; (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr {ARMLargePage}) s\<rbrakk> \<Longrightarrow> ?Q'15 s proof (prove)
goal (5 subgoals):
 1. \<And>x y. \<lbrakk>is_aligned ptr 6; dc x y\<rbrakk> \<Longrightarrow> dcorres dc (?R21 x) (?R'21 y) (return x) (do ys <- mapM (swp store_pte InvalidPTE) (tl (map ((\<lambda>x. x + ptr) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]));
return (() # ys)
od)
 2. is_aligned ptr 6 \<Longrightarrow> \<lbrace>?Q21\<rbrace> delete_cap_simple (ptr && ~~ mask pt_bits, unat (ptr && mask pt_bits >> 2)) \<lbrace>?R21\<rbrace>
 3. is_aligned ptr 6 \<Longrightarrow> \<lbrace>?Q'21\<rbrace> store_pte ptr InvalidPTE \<lbrace>?R'21\<rbrace>
 4. \<And>s. \<lbrakk>is_aligned ptr 6; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q21) s
 5. \<And>s. \<lbrakk>is_aligned ptr 6; (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr {ARMLargePage}) s\<rbrakk> \<Longrightarrow> (pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr UNIV and invs and ?Q'21) s proof (prove)
goal (5 subgoals):
 1. \<And>x y. \<lbrakk>is_aligned ptr 6; dc x y\<rbrakk> \<Longrightarrow> dcorres dc (?R21 x) (?R'21 y) (return x >>= return) (do ys <- mapM (swp store_pte InvalidPTE) (tl (map ((\<lambda>x. x + ptr) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]));
return (() # ys)
od)
 2. is_aligned ptr 6 \<Longrightarrow> \<lbrace>?Q21\<rbrace> delete_cap_simple (ptr && ~~ mask pt_bits, unat (ptr && mask pt_bits >> 2)) \<lbrace>?R21\<rbrace>
 3. is_aligned ptr 6 \<Longrightarrow> \<lbrace>?Q'21\<rbrace> store_pte ptr InvalidPTE \<lbrace>?R'21\<rbrace>
 4. \<And>s. \<lbrakk>is_aligned ptr 6; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q21) s
 5. \<And>s. \<lbrakk>is_aligned ptr 6; (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr {ARMLargePage}) s\<rbrakk> \<Longrightarrow> (pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr UNIV and invs and ?Q'21) s proof (prove)
goal (8 subgoals):
 1. \<And>x y. \<lbrakk>is_aligned ptr 6; dc x y\<rbrakk> \<Longrightarrow> dcorres dc (?P30 x) (?P'32 y) (return x) (mapM (swp store_pte InvalidPTE) (tl (map ((\<lambda>x. x + ptr) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])))
 2. \<And>x y rv rv'. \<lbrakk>is_aligned ptr 6; dc x y; dc rv rv'\<rbrakk> \<Longrightarrow> dcorres dc (?R28 x y rv) (?R'28 x y rv') (return rv) (return (() # rv'))
 3. \<And>x y. \<lbrakk>is_aligned ptr 6; dc x y\<rbrakk> \<Longrightarrow> \<lbrace>?Q31 x\<rbrace> return x \<lbrace>?R28 x y\<rbrace>
 4. \<And>x y. \<lbrakk>is_aligned ptr 6; dc x y\<rbrakk> \<Longrightarrow> \<lbrace>?Q'33 y\<rbrace> mapM (swp store_pte InvalidPTE) (tl (map ((\<lambda>x. x + ptr) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])) \<lbrace>?R'28 x y\<rbrace>
 5. is_aligned ptr 6 \<Longrightarrow> \<lbrace>?Q21\<rbrace> delete_cap_simple (ptr && ~~ mask pt_bits, unat (ptr && mask pt_bits >> 2)) \<lbrace>\<lambda>x. ?P30 x and ?Q31 x\<rbrace>
 6. is_aligned ptr 6 \<Longrightarrow> \<lbrace>?Q'21\<rbrace> store_pte ptr InvalidPTE \<lbrace>\<lambda>y. ?P'32 y and ?Q'33 y\<rbrace>
 7. \<And>s. \<lbrakk>is_aligned ptr 6; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q21) s
 8. \<And>s. \<lbrakk>is_aligned ptr 6; (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr {ARMLargePage}) s\<rbrakk> \<Longrightarrow> (pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr UNIV and invs and ?Q'21) s proof (prove)
goal (7 subgoals):
 1. \<And>x y rv rv'. \<lbrakk>is_aligned ptr 6; dc x y; dc rv rv'\<rbrakk> \<Longrightarrow> dcorres dc (?R28 x y rv) (?R'28 x y rv') (return rv) (return (() # rv'))
 2. \<And>x y. \<lbrakk>is_aligned ptr 6; dc x y\<rbrakk> \<Longrightarrow> \<lbrace>?Q31 x\<rbrace> return x \<lbrace>?R28 x y\<rbrace>
 3. \<And>x y. \<lbrakk>is_aligned ptr 6; dc x y\<rbrakk> \<Longrightarrow> \<lbrace>?Q'33 y\<rbrace> mapM (swp store_pte InvalidPTE) (tl (map ((\<lambda>x. x + ptr) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])) \<lbrace>?R'28 x y\<rbrace>
 4. is_aligned ptr 6 \<Longrightarrow> \<lbrace>?Q21\<rbrace> delete_cap_simple (ptr && ~~ mask pt_bits, unat (ptr && mask pt_bits >> 2)) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q31 x\<rbrace>
 5. is_aligned ptr 6 \<Longrightarrow> \<lbrace>?Q'21\<rbrace> store_pte ptr InvalidPTE \<lbrace>\<lambda>y. valid_idle and (\<lambda>s. \<exists>f. ako_at (arch_kernel_obj.PageTable f) (ptr && ~~ mask pt_bits) s \<and> (\<forall>slot\<in>set (tl (map ((\<lambda>x. x + ptr) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). f (UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2)) = InvalidPTE)) and K (\<forall>sl\<in>set (tl (map ((\<lambda>x. x + ptr) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). sl && ~~ mask pt_bits = ptr && ~~ mask pt_bits) and ?Q'33 y\<rbrace>
 6. \<And>s. \<lbrakk>is_aligned ptr 6; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q21) s
 7. \<And>s. \<lbrakk>is_aligned ptr 6; (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr {ARMLargePage}) s\<rbrakk> \<Longrightarrow> (pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr UNIV and invs and ?Q'21) s proof (prove)
goal (6 subgoals):
 1. \<And>x y. \<lbrakk>is_aligned ptr 6; dc x y\<rbrakk> \<Longrightarrow> \<lbrace>?Q31 x\<rbrace> return x \<lbrace>\<lambda>rv _. True\<rbrace>
 2. \<And>x y. \<lbrakk>is_aligned ptr 6; dc x y\<rbrakk> \<Longrightarrow> \<lbrace>?Q'33 y\<rbrace> mapM (swp store_pte InvalidPTE) (tl (map ((\<lambda>x. x + ptr) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])) \<lbrace>\<lambda>rv' _. True\<rbrace>
 3. is_aligned ptr 6 \<Longrightarrow> \<lbrace>?Q21\<rbrace> delete_cap_simple (ptr && ~~ mask pt_bits, unat (ptr && mask pt_bits >> 2)) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q31 x\<rbrace>
 4. is_aligned ptr 6 \<Longrightarrow> \<lbrace>?Q'21\<rbrace> store_pte ptr InvalidPTE \<lbrace>\<lambda>y. valid_idle and (\<lambda>s. \<exists>f. ako_at (arch_kernel_obj.PageTable f) (ptr && ~~ mask pt_bits) s \<and> (\<forall>slot\<in>set (tl (map ((\<lambda>x. x + ptr) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). f (UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2)) = InvalidPTE)) and K (\<forall>sl\<in>set (tl (map ((\<lambda>x. x + ptr) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). sl && ~~ mask pt_bits = ptr && ~~ mask pt_bits) and ?Q'33 y\<rbrace>
 5. \<And>s. \<lbrakk>is_aligned ptr 6; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q21) s
 6. \<And>s. \<lbrakk>is_aligned ptr 6; (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr {ARMLargePage}) s\<rbrakk> \<Longrightarrow> (pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr UNIV and invs and ?Q'21) s proof (prove)
goal (3 subgoals):
 1. is_aligned ptr 6 \<Longrightarrow> \<lbrace>?P'54\<rbrace> store_pte ptr InvalidPTE \<lbrace>\<lambda>rv s. (\<exists>f. ako_at (arch_kernel_obj.PageTable f) (ptr && ~~ mask pt_bits) s \<and> (\<forall>slot\<in>set (tl (map ((\<lambda>x. x + ptr) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). f (UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2)) = InvalidPTE)) \<and> K (\<forall>sl\<in>set (tl (map ((\<lambda>x. x + ptr) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). sl && ~~ mask pt_bits = ptr && ~~ mask pt_bits) s \<and> True\<rbrace>
 2. \<And>s. \<lbrakk>is_aligned ptr 6; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True)) s
 3. \<And>s. \<lbrakk>is_aligned ptr 6; (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr {ARMLargePage}) s\<rbrakk> \<Longrightarrow> (pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr UNIV and invs and (\<lambda>s. valid_idle s \<and> ?P'54 s)) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>is_aligned ptr 6; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True)) s
 2. \<And>s. \<lbrakk>is_aligned ptr 6; (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr {ARMLargePage}) s\<rbrakk> \<Longrightarrow> (pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr UNIV and invs and (\<lambda>s. valid_idle s \<and> (\<exists>f. ako_at (arch_kernel_obj.PageTable f) (ptr && ~~ mask pt_bits) s \<and> (\<forall>slot\<in>set (tl (map ((\<lambda>x. x + ptr) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). f (UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2)) = InvalidPTE)) \<and> K (\<forall>sl\<in>set (tl (map ((\<lambda>x. x + ptr) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). sl && ~~ mask pt_bits = ptr && ~~ mask pt_bits) s \<and> True)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_aligned ptr 6; (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr {ARMLargePage}) s\<rbrakk> \<Longrightarrow> (pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr UNIV and invs and (\<lambda>s. valid_idle s \<and> (\<exists>f. ako_at (arch_kernel_obj.PageTable f) (ptr && ~~ mask pt_bits) s \<and> (\<forall>slot\<in>set (tl (map ((\<lambda>x. x + ptr) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). f (UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2)) = InvalidPTE)) \<and> K (\<forall>sl\<in>set (tl (map ((\<lambda>x. x + ptr) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). sl && ~~ mask pt_bits = ptr && ~~ mask pt_bits) s \<and> True)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_aligned ptr 6; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr {ARMLargePage} s\<rbrakk> \<Longrightarrow> valid_idle s \<and> (\<exists>f. ako_at (arch_kernel_obj.PageTable f) (ptr && ~~ mask pt_bits) s \<and> (\<forall>slot\<in>set (tl (map ((\<lambda>x. x + ptr) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). f (UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2)) = InvalidPTE)) \<and> (\<forall>sl\<in>set (tl (map ((\<lambda>x. x + ptr) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). sl && ~~ mask pt_bits = ptr && ~~ mask pt_bits) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_aligned ptr 6; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr {ARMLargePage} s\<rbrakk> \<Longrightarrow> (\<exists>f. ako_at (arch_kernel_obj.PageTable f) (ptr && ~~ mask pt_bits) s \<and> (\<forall>slot\<in>set (tl (map ((\<lambda>x. x + ptr) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). f (UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2)) = InvalidPTE)) \<and> (\<forall>sl\<in>set (tl (map ((\<lambda>x. x + ptr) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). sl && ~~ mask pt_bits = ptr && ~~ mask pt_bits) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_aligned ptr 6; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr {ARMLargePage} s\<rbrakk> \<Longrightarrow> (\<forall>sl\<in>set (tl (map ((\<lambda>x. x + ptr) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). sl && ~~ mask pt_bits = ptr && ~~ mask pt_bits) \<and> (\<exists>f. ako_at (arch_kernel_obj.PageTable f) (ptr && ~~ mask pt_bits) s \<and> (\<forall>slot\<in>set (tl (map ((\<lambda>x. x + ptr) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). f (UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2)) = InvalidPTE)) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>is_aligned ptr 6; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr {ARMLargePage} s\<rbrakk> \<Longrightarrow> \<forall>sl\<in>set (tl (map ((\<lambda>x. x + ptr) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). sl && ~~ mask pt_bits = ptr && ~~ mask pt_bits
 2. \<And>s. \<lbrakk>is_aligned ptr 6; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr {ARMLargePage} s; \<forall>sl\<in>set (tl (map ((\<lambda>x. x + ptr) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). sl && ~~ mask pt_bits = ptr && ~~ mask pt_bits\<rbrakk> \<Longrightarrow> \<exists>f. ako_at (arch_kernel_obj.PageTable f) (ptr && ~~ mask pt_bits) s \<and> (\<forall>slot\<in>set (tl (map ((\<lambda>x. x + ptr) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). f (UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2)) = InvalidPTE) proof (prove)
goal (2 subgoals):
 1. \<And>s sl. \<lbrakk>is_aligned ptr 6; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr {ARMLargePage} s; Suc 0 \<le> sl; sl < 16\<rbrakk> \<Longrightarrow> word_of_nat sl * 4 + ptr && ~~ mask pt_bits = ptr && ~~ mask pt_bits
 2. \<And>s. \<lbrakk>is_aligned ptr 6; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr {ARMLargePage} s; \<forall>sl\<in>set (tl (map ((\<lambda>x. x + ptr) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). sl && ~~ mask pt_bits = ptr && ~~ mask pt_bits\<rbrakk> \<Longrightarrow> \<exists>f. ako_at (arch_kernel_obj.PageTable f) (ptr && ~~ mask pt_bits) s \<and> (\<forall>slot\<in>set (tl (map ((\<lambda>x. x + ptr) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). f (UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2)) = InvalidPTE) proof (prove)
goal (2 subgoals):
 1. \<And>s sl. \<lbrakk>is_aligned ptr 6; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr {ARMLargePage} s; Suc 0 \<le> sl; sl < 16\<rbrakk> \<Longrightarrow> ptr + word_of_nat sl * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits
 2. \<And>s. \<lbrakk>is_aligned ptr 6; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr {ARMLargePage} s; \<forall>sl\<in>set (tl (map ((\<lambda>x. x + ptr) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). sl && ~~ mask pt_bits = ptr && ~~ mask pt_bits\<rbrakk> \<Longrightarrow> \<exists>f. ako_at (arch_kernel_obj.PageTable f) (ptr && ~~ mask pt_bits) s \<and> (\<forall>slot\<in>set (tl (map ((\<lambda>x. x + ptr) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). f (UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2)) = InvalidPTE) proof (prove)
goal (3 subgoals):
 1. \<And>s sl. \<lbrakk>is_aligned ptr 6; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr {ARMLargePage} s; Suc 0 \<le> sl; sl < 16\<rbrakk> \<Longrightarrow> 6 \<le> pt_bits
 2. \<And>s sl. \<lbrakk>is_aligned ptr 6; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr {ARMLargePage} s; Suc 0 \<le> sl; sl < 16\<rbrakk> \<Longrightarrow> (ptr + word_of_nat sl * 4 && ~~ mask 6) && ~~ mask pt_bits = ptr && ~~ mask pt_bits
 3. \<And>s. \<lbrakk>is_aligned ptr 6; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr {ARMLargePage} s; \<forall>sl\<in>set (tl (map ((\<lambda>x. x + ptr) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). sl && ~~ mask pt_bits = ptr && ~~ mask pt_bits\<rbrakk> \<Longrightarrow> \<exists>f. ako_at (arch_kernel_obj.PageTable f) (ptr && ~~ mask pt_bits) s \<and> (\<forall>slot\<in>set (tl (map ((\<lambda>x. x + ptr) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). f (UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2)) = InvalidPTE) proof (prove)
goal (2 subgoals):
 1. \<And>s sl. \<lbrakk>is_aligned ptr 6; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr {ARMLargePage} s; Suc 0 \<le> sl; sl < 16\<rbrakk> \<Longrightarrow> (ptr + word_of_nat sl * 4 && ~~ mask 6) && ~~ mask pt_bits = ptr && ~~ mask pt_bits
 2. \<And>s. \<lbrakk>is_aligned ptr 6; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr {ARMLargePage} s; \<forall>sl\<in>set (tl (map ((\<lambda>x. x + ptr) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). sl && ~~ mask pt_bits = ptr && ~~ mask pt_bits\<rbrakk> \<Longrightarrow> \<exists>f. ako_at (arch_kernel_obj.PageTable f) (ptr && ~~ mask pt_bits) s \<and> (\<forall>slot\<in>set (tl (map ((\<lambda>x. x + ptr) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). f (UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2)) = InvalidPTE) proof (prove)
goal (4 subgoals):
 1. \<And>s sl. \<lbrakk>is_aligned ptr 6; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr {ARMLargePage} s; Suc 0 \<le> sl; sl < 16\<rbrakk> \<Longrightarrow> is_aligned ptr 6
 2. \<And>s sl. \<lbrakk>is_aligned ptr 6; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr {ARMLargePage} s; Suc 0 \<le> sl; sl < 16\<rbrakk> \<Longrightarrow> word_of_nat sl * 4 < 2 ^ 6
 3. \<And>s sl. \<lbrakk>is_aligned ptr 6; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr {ARMLargePage} s; Suc 0 \<le> sl; sl < 16\<rbrakk> \<Longrightarrow> ptr && ~~ mask pt_bits = ptr && ~~ mask pt_bits
 4. \<And>s. \<lbrakk>is_aligned ptr 6; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr {ARMLargePage} s; \<forall>sl\<in>set (tl (map ((\<lambda>x. x + ptr) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). sl && ~~ mask pt_bits = ptr && ~~ mask pt_bits\<rbrakk> \<Longrightarrow> \<exists>f. ako_at (arch_kernel_obj.PageTable f) (ptr && ~~ mask pt_bits) s \<and> (\<forall>slot\<in>set (tl (map ((\<lambda>x. x + ptr) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). f (UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2)) = InvalidPTE) proof (prove)
goal (3 subgoals):
 1. \<And>s sl. \<lbrakk>is_aligned ptr 6; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr {ARMLargePage} s; Suc 0 \<le> sl; sl < 16\<rbrakk> \<Longrightarrow> word_of_nat sl * 4 < 2 ^ 6
 2. \<And>s sl. \<lbrakk>is_aligned ptr 6; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr {ARMLargePage} s; Suc 0 \<le> sl; sl < 16\<rbrakk> \<Longrightarrow> ptr && ~~ mask pt_bits = ptr && ~~ mask pt_bits
 3. \<And>s. \<lbrakk>is_aligned ptr 6; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr {ARMLargePage} s; \<forall>sl\<in>set (tl (map ((\<lambda>x. x + ptr) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). sl && ~~ mask pt_bits = ptr && ~~ mask pt_bits\<rbrakk> \<Longrightarrow> \<exists>f. ako_at (arch_kernel_obj.PageTable f) (ptr && ~~ mask pt_bits) s \<and> (\<forall>slot\<in>set (tl (map ((\<lambda>x. x + ptr) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). f (UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2)) = InvalidPTE) proof (prove)
goal (3 subgoals):
 1. \<And>s sl. \<lbrakk>is_aligned ptr 6; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr {ARMLargePage} s; Suc 0 \<le> sl; sl < 16\<rbrakk> \<Longrightarrow> word_of_nat sl * 4 < 0x40
 2. \<And>s sl. \<lbrakk>is_aligned ptr 6; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr {ARMLargePage} s; Suc 0 \<le> sl; sl < 16\<rbrakk> \<Longrightarrow> ptr && ~~ mask pt_bits = ptr && ~~ mask pt_bits
 3. \<And>s. \<lbrakk>is_aligned ptr 6; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr {ARMLargePage} s; \<forall>sl\<in>set (tl (map ((\<lambda>x. x + ptr) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). sl && ~~ mask pt_bits = ptr && ~~ mask pt_bits\<rbrakk> \<Longrightarrow> \<exists>f. ako_at (arch_kernel_obj.PageTable f) (ptr && ~~ mask pt_bits) s \<and> (\<forall>slot\<in>set (tl (map ((\<lambda>x. x + ptr) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). f (UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2)) = InvalidPTE) proof (prove)
goal (4 subgoals):
 1. \<And>s sl. \<lbrakk>is_aligned ptr 6; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr {ARMLargePage} s; Suc 0 \<le> sl; sl < 16\<rbrakk> \<Longrightarrow> sl < 16
 2. \<And>s sl. \<lbrakk>is_aligned ptr 6; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr {ARMLargePage} s; Suc 0 \<le> sl; sl < 16\<rbrakk> \<Longrightarrow> 6 < LENGTH(32)
 3. \<And>s sl. \<lbrakk>is_aligned ptr 6; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr {ARMLargePage} s; Suc 0 \<le> sl; sl < 16\<rbrakk> \<Longrightarrow> ptr && ~~ mask pt_bits = ptr && ~~ mask pt_bits
 4. \<And>s. \<lbrakk>is_aligned ptr 6; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr {ARMLargePage} s; \<forall>sl\<in>set (tl (map ((\<lambda>x. x + ptr) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). sl && ~~ mask pt_bits = ptr && ~~ mask pt_bits\<rbrakk> \<Longrightarrow> \<exists>f. ako_at (arch_kernel_obj.PageTable f) (ptr && ~~ mask pt_bits) s \<and> (\<forall>slot\<in>set (tl (map ((\<lambda>x. x + ptr) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). f (UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2)) = InvalidPTE) proof (prove)
goal (3 subgoals):
 1. \<And>s sl. \<lbrakk>is_aligned ptr 6; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr {ARMLargePage} s; Suc 0 \<le> sl; sl < 16\<rbrakk> \<Longrightarrow> 6 < LENGTH(32)
 2. \<And>s sl. \<lbrakk>is_aligned ptr 6; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr {ARMLargePage} s; Suc 0 \<le> sl; sl < 16\<rbrakk> \<Longrightarrow> ptr && ~~ mask pt_bits = ptr && ~~ mask pt_bits
 3. \<And>s. \<lbrakk>is_aligned ptr 6; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr {ARMLargePage} s; \<forall>sl\<in>set (tl (map ((\<lambda>x. x + ptr) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). sl && ~~ mask pt_bits = ptr && ~~ mask pt_bits\<rbrakk> \<Longrightarrow> \<exists>f. ako_at (arch_kernel_obj.PageTable f) (ptr && ~~ mask pt_bits) s \<and> (\<forall>slot\<in>set (tl (map ((\<lambda>x. x + ptr) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). f (UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2)) = InvalidPTE) proof (prove)
goal (2 subgoals):
 1. \<And>s sl. \<lbrakk>is_aligned ptr 6; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr {ARMLargePage} s; Suc 0 \<le> sl; sl < 16\<rbrakk> \<Longrightarrow> ptr && ~~ mask pt_bits = ptr && ~~ mask pt_bits
 2. \<And>s. \<lbrakk>is_aligned ptr 6; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr {ARMLargePage} s; \<forall>sl\<in>set (tl (map ((\<lambda>x. x + ptr) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). sl && ~~ mask pt_bits = ptr && ~~ mask pt_bits\<rbrakk> \<Longrightarrow> \<exists>f. ako_at (arch_kernel_obj.PageTable f) (ptr && ~~ mask pt_bits) s \<and> (\<forall>slot\<in>set (tl (map ((\<lambda>x. x + ptr) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). f (UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2)) = InvalidPTE) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_aligned ptr 6; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr {ARMLargePage} s; \<forall>sl\<in>set (tl (map ((\<lambda>x. x + ptr) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). sl && ~~ mask pt_bits = ptr && ~~ mask pt_bits\<rbrakk> \<Longrightarrow> \<exists>f. ako_at (arch_kernel_obj.PageTable f) (ptr && ~~ mask pt_bits) s \<and> (\<forall>slot\<in>set (tl (map ((\<lambda>x. x + ptr) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). f (UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2)) = InvalidPTE) proof (prove)
goal (1 subgoal):
 1. \<And>s fun slot. \<lbrakk>is_aligned ptr 6; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; \<forall>sl\<in>set (tl (map ((\<lambda>x. x + ptr) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). sl && ~~ mask pt_bits = ptr && ~~ mask pt_bits; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; slot \<in> set (tl (map ((\<lambda>x. x + ptr) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]))\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2)) = InvalidPTE proof (prove)
goal (1 subgoal):
 1. \<And>s fun slot. \<lbrakk>is_aligned ptr 6; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; slot \<in> set (tl (map ((\<lambda>x. x + ptr) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])); slot && ~~ mask pt_bits = ptr && ~~ mask pt_bits\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2)) = InvalidPTE proof (prove)
goal (1 subgoal):
 1. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; word_of_nat x * 4 + ptr && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 8) (word_of_nat x * 4 + ptr && mask pt_bits >> 2)) = InvalidPTE proof (prove)
goal (1 subgoal):
 1. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) = InvalidPTE proof (prove)
goal (1 subgoal):
 1. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; valid_entries pte_range fun; entries_align pte_range_sz fun\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) = InvalidPTE proof (prove)
goal (2 subgoals):
 1. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2) \<noteq> UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)
 2. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) \<inter> pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) = InvalidPTE proof (prove)
goal (2 subgoals):
 1. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; \<not> UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2) \<noteq> UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)\<rbrakk> \<Longrightarrow> False
 2. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) \<inter> pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) = InvalidPTE proof (prove)
goal (2 subgoals):
 1. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2) = UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)\<rbrakk> \<Longrightarrow> False
 2. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) \<inter> pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) = InvalidPTE proof (prove)
goal (2 subgoals):
 1. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) = UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2))\<rbrakk> \<Longrightarrow> False
 2. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) \<inter> pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) = InvalidPTE proof (prove)
goal (2 subgoals):
 1. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) << 2 = UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) << 2\<rbrakk> \<Longrightarrow> False
 2. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) \<inter> pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) = InvalidPTE proof (prove)
goal (3 subgoals):
 1. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun\<rbrakk> \<Longrightarrow> ptr + word_of_nat x * 4 && mask pt_bits >> 2 < 2 ^ LENGTH(8)
 2. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; ptr + word_of_nat x * 4 && mask pt_bits >> 2 << 2 = UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) << 2\<rbrakk> \<Longrightarrow> False
 3. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) \<inter> pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) = InvalidPTE proof (prove)
goal (3 subgoals):
 1. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun\<rbrakk> \<Longrightarrow> ptr + word_of_nat x * 4 && mask pt_bits < 2 ^ (2 + LENGTH(8))
 2. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; ptr + word_of_nat x * 4 && mask pt_bits >> 2 << 2 = UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) << 2\<rbrakk> \<Longrightarrow> False
 3. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) \<inter> pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) = InvalidPTE proof (prove)
goal (4 subgoals):
 1. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun\<rbrakk> \<Longrightarrow> pt_bits < LENGTH(32)
 2. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun\<rbrakk> \<Longrightarrow> 2 ^ pt_bits \<le> 2 ^ (2 + LENGTH(8))
 3. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; ptr + word_of_nat x * 4 && mask pt_bits >> 2 << 2 = UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) << 2\<rbrakk> \<Longrightarrow> False
 4. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) \<inter> pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) = InvalidPTE proof (prove)
goal (3 subgoals):
 1. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun\<rbrakk> \<Longrightarrow> 2 ^ pt_bits \<le> 2 ^ (2 + LENGTH(8))
 2. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; ptr + word_of_nat x * 4 && mask pt_bits >> 2 << 2 = UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) << 2\<rbrakk> \<Longrightarrow> False
 3. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) \<inter> pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) = InvalidPTE proof (prove)
goal (2 subgoals):
 1. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; ptr + word_of_nat x * 4 && mask pt_bits >> 2 << 2 = UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) << 2\<rbrakk> \<Longrightarrow> False
 2. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) \<inter> pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) = InvalidPTE proof (prove)
goal (3 subgoals):
 1. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun\<rbrakk> \<Longrightarrow> ptr && mask pt_bits >> 2 < 2 ^ LENGTH(8)
 2. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; ptr + word_of_nat x * 4 && mask pt_bits >> 2 << 2 = ptr && mask pt_bits >> 2 << 2\<rbrakk> \<Longrightarrow> False
 3. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) \<inter> pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) = InvalidPTE proof (prove)
goal (3 subgoals):
 1. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun\<rbrakk> \<Longrightarrow> ptr && mask pt_bits < 2 ^ (2 + LENGTH(8))
 2. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; ptr + word_of_nat x * 4 && mask pt_bits >> 2 << 2 = ptr && mask pt_bits >> 2 << 2\<rbrakk> \<Longrightarrow> False
 3. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) \<inter> pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) = InvalidPTE proof (prove)
goal (4 subgoals):
 1. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun\<rbrakk> \<Longrightarrow> pt_bits < LENGTH(32)
 2. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun\<rbrakk> \<Longrightarrow> 2 ^ pt_bits \<le> 2 ^ (2 + LENGTH(8))
 3. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; ptr + word_of_nat x * 4 && mask pt_bits >> 2 << 2 = ptr && mask pt_bits >> 2 << 2\<rbrakk> \<Longrightarrow> False
 4. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) \<inter> pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) = InvalidPTE proof (prove)
goal (3 subgoals):
 1. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun\<rbrakk> \<Longrightarrow> 2 ^ pt_bits \<le> 2 ^ (2 + LENGTH(8))
 2. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; ptr + word_of_nat x * 4 && mask pt_bits >> 2 << 2 = ptr && mask pt_bits >> 2 << 2\<rbrakk> \<Longrightarrow> False
 3. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) \<inter> pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) = InvalidPTE proof (prove)
goal (2 subgoals):
 1. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; ptr + word_of_nat x * 4 && mask pt_bits >> 2 << 2 = ptr && mask pt_bits >> 2 << 2\<rbrakk> \<Longrightarrow> False
 2. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) \<inter> pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) = InvalidPTE proof (prove)
goal (2 subgoals):
 1. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; (ptr + word_of_nat x * 4 && mask pt_bits) && ~~ mask 2 = (ptr && mask pt_bits) && ~~ mask 2\<rbrakk> \<Longrightarrow> False
 2. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) \<inter> pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) = InvalidPTE proof (prove)
goal (3 subgoals):
 1. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun\<rbrakk> \<Longrightarrow> is_aligned (ptr + word_of_nat x * 4 && mask pt_bits) 2
 2. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; ptr + word_of_nat x * 4 && mask pt_bits = (ptr && mask pt_bits) && ~~ mask 2\<rbrakk> \<Longrightarrow> False
 3. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) \<inter> pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) = InvalidPTE proof (prove)
goal (4 subgoals):
 1. \<And>s fun x. \<lbrakk>invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun\<rbrakk> \<Longrightarrow> is_aligned (word_of_nat x * 4) 2
 2. \<And>s fun x. \<lbrakk>invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun\<rbrakk> \<Longrightarrow> 2 \<le> 6
 3. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; ptr + word_of_nat x * 4 && mask pt_bits = (ptr && mask pt_bits) && ~~ mask 2\<rbrakk> \<Longrightarrow> False
 4. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) \<inter> pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) = InvalidPTE proof (prove)
goal (3 subgoals):
 1. \<And>s fun x. \<lbrakk>invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun\<rbrakk> \<Longrightarrow> 2 \<le> 6
 2. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; ptr + word_of_nat x * 4 && mask pt_bits = (ptr && mask pt_bits) && ~~ mask 2\<rbrakk> \<Longrightarrow> False
 3. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) \<inter> pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) = InvalidPTE proof (prove)
goal (2 subgoals):
 1. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; ptr + word_of_nat x * 4 && mask pt_bits = (ptr && mask pt_bits) && ~~ mask 2\<rbrakk> \<Longrightarrow> False
 2. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) \<inter> pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) = InvalidPTE proof (prove)
goal (3 subgoals):
 1. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun\<rbrakk> \<Longrightarrow> is_aligned (ptr && mask pt_bits) 2
 2. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; ptr + word_of_nat x * 4 && mask pt_bits = ptr && mask pt_bits\<rbrakk> \<Longrightarrow> False
 3. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) \<inter> pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) = InvalidPTE proof (prove)
goal (3 subgoals):
 1. \<And>s fun x. \<lbrakk>invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun\<rbrakk> \<Longrightarrow> 2 \<le> 6
 2. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; ptr + word_of_nat x * 4 && mask pt_bits = ptr && mask pt_bits\<rbrakk> \<Longrightarrow> False
 3. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) \<inter> pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) = InvalidPTE proof (prove)
goal (2 subgoals):
 1. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; ptr + word_of_nat x * 4 && mask pt_bits = ptr && mask pt_bits\<rbrakk> \<Longrightarrow> False
 2. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) \<inter> pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) = InvalidPTE proof (prove)
goal (6 subgoals):
 1. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun\<rbrakk> \<Longrightarrow> is_aligned ptr (?m154 s fun x)
 2. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun\<rbrakk> \<Longrightarrow> ?m154 s fun x \<le> pt_bits
 3. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun\<rbrakk> \<Longrightarrow> pt_bits < 32
 4. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun\<rbrakk> \<Longrightarrow> word_of_nat x * 4 < 2 ^ ?m154 s fun x
 5. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; (ptr && mask pt_bits) + word_of_nat x * 4 = ptr && mask pt_bits\<rbrakk> \<Longrightarrow> False
 6. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) \<inter> pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) = InvalidPTE proof (prove)
goal (5 subgoals):
 1. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun\<rbrakk> \<Longrightarrow> 6 \<le> pt_bits
 2. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun\<rbrakk> \<Longrightarrow> pt_bits < 32
 3. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun\<rbrakk> \<Longrightarrow> word_of_nat x * 4 < 2 ^ 6
 4. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; (ptr && mask pt_bits) + word_of_nat x * 4 = ptr && mask pt_bits\<rbrakk> \<Longrightarrow> False
 5. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) \<inter> pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) = InvalidPTE proof (prove)
goal (3 subgoals):
 1. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask 10) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask 10 >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask 10 = ptr && ~~ mask 10; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun\<rbrakk> \<Longrightarrow> word_of_nat x * 4 < 0x40
 2. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; (ptr && mask pt_bits) + word_of_nat x * 4 = ptr && mask pt_bits\<rbrakk> \<Longrightarrow> False
 3. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) \<inter> pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) = InvalidPTE proof (prove)
goal (3 subgoals):
 1. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask 10) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask 10 >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + (word_of_nat x << 2) && ~~ mask 10 = ptr && ~~ mask 10; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun\<rbrakk> \<Longrightarrow> word_of_nat x << 2 < 0x40
 2. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; (ptr && mask pt_bits) + word_of_nat x * 4 = ptr && mask pt_bits\<rbrakk> \<Longrightarrow> False
 3. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) \<inter> pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) = InvalidPTE proof (prove)
goal (4 subgoals):
 1. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask 10) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask 10 >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + (word_of_nat x << 2) && ~~ mask 10 = ptr && ~~ mask 10; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun\<rbrakk> \<Longrightarrow> word_of_nat x < 2 ^ (6 - 2)
 2. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask 10) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask 10 >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + (word_of_nat x << 2) && ~~ mask 10 = ptr && ~~ mask 10; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun\<rbrakk> \<Longrightarrow> 6 < LENGTH(32)
 3. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; (ptr && mask pt_bits) + word_of_nat x * 4 = ptr && mask pt_bits\<rbrakk> \<Longrightarrow> False
 4. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) \<inter> pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) = InvalidPTE proof (prove)
goal (3 subgoals):
 1. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask 10) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask 10 >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + (word_of_nat x << 2) && ~~ mask 10 = ptr && ~~ mask 10; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun\<rbrakk> \<Longrightarrow> 6 < LENGTH(32)
 2. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; (ptr && mask pt_bits) + word_of_nat x * 4 = ptr && mask pt_bits\<rbrakk> \<Longrightarrow> False
 3. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) \<inter> pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) = InvalidPTE proof (prove)
goal (2 subgoals):
 1. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; (ptr && mask pt_bits) + word_of_nat x * 4 = ptr && mask pt_bits\<rbrakk> \<Longrightarrow> False
 2. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) \<inter> pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) = InvalidPTE proof (prove)
goal (2 subgoals):
 1. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; word_of_nat x * 4 = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) \<inter> pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) = InvalidPTE proof (prove)
goal (3 subgoals):
 1. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; word_of_nat x * 4 = 0; 0 < word_of_nat (x * 4)\<rbrakk> \<Longrightarrow> False
 2. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; word_of_nat x * 4 = 0\<rbrakk> \<Longrightarrow> 0 < word_of_nat (x * 4)
 3. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) \<inter> pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) = InvalidPTE proof (prove)
goal (2 subgoals):
 1. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; word_of_nat x * 4 = 0\<rbrakk> \<Longrightarrow> 0 < word_of_nat (x * 4)
 2. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) \<inter> pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) = InvalidPTE proof (prove)
goal (4 subgoals):
 1. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; word_of_nat x * 4 = 0\<rbrakk> \<Longrightarrow> 0 \<le> word_of_nat 0
 2. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; word_of_nat x * 4 = 0\<rbrakk> \<Longrightarrow> x * 4 < 2 ^ LENGTH(32)
 3. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; word_of_nat x * 4 = 0\<rbrakk> \<Longrightarrow> 0 < x * 4
 4. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) \<inter> pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) = InvalidPTE proof (prove)
goal (3 subgoals):
 1. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; word_of_nat x * 4 = 0\<rbrakk> \<Longrightarrow> x * 4 < 2 ^ LENGTH(32)
 2. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; word_of_nat x * 4 = 0\<rbrakk> \<Longrightarrow> 0 < x * 4
 3. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) \<inter> pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) = InvalidPTE proof (prove)
goal (2 subgoals):
 1. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; word_of_nat x * 4 = 0\<rbrakk> \<Longrightarrow> 0 < x * 4
 2. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) \<inter> pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) = InvalidPTE proof (prove)
goal (1 subgoal):
 1. \<And>s fun x. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> pg_id = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) \<inter> pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) = InvalidPTE proof (prove)
goal (2 subgoals):
 1. \<And>s fun x x21 x22 x23. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) = LargePagePTE x21 x22 x23; pg_id = ptrFromPAddr x21; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; is_aligned (ptr >> 2) 4; pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) \<inter> {x. x && ~~ mask 4 = UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) && ~~ mask 4} = {}\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) = InvalidPTE
 2. \<And>s fun x x21 x22 x23. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) = LargePagePTE x21 x22 x23; pg_id = ptrFromPAddr x21; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; \<not> is_aligned (ptr >> 2) 4; UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) \<notin> pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) = InvalidPTE proof (prove)
goal (2 subgoals):
 1. \<And>s fun x x21 x22 x23. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) = LargePagePTE x21 x22 x23; pg_id = ptrFromPAddr x21; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; is_aligned (ptr >> 2) 4; pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) \<inter> {x. x && ~~ mask 4 = UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) && ~~ mask 4} = {}; fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) \<noteq> InvalidPTE\<rbrakk> \<Longrightarrow> False
 2. \<And>s fun x x21 x22 x23. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) = LargePagePTE x21 x22 x23; pg_id = ptrFromPAddr x21; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; \<not> is_aligned (ptr >> 2) 4; UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) \<notin> pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) = InvalidPTE proof (prove)
goal (3 subgoals):
 1. \<And>s fun x x21 x22 x23. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) = LargePagePTE x21 x22 x23; pg_id = ptrFromPAddr x21; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; is_aligned (ptr >> 2) 4; fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) \<noteq> InvalidPTE\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2) \<in> pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))
 2. \<And>s fun x x21 x22 x23. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) = LargePagePTE x21 x22 x23; pg_id = ptrFromPAddr x21; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; is_aligned (ptr >> 2) 4; fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) \<noteq> InvalidPTE\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2) \<in> {x. x && ~~ mask 4 = UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) && ~~ mask 4}
 3. \<And>s fun x x21 x22 x23. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) = LargePagePTE x21 x22 x23; pg_id = ptrFromPAddr x21; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; \<not> is_aligned (ptr >> 2) 4; UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) \<notin> pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) = InvalidPTE proof (prove)
goal (3 subgoals):
 1. \<And>s fun x x21 x22 x23. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) = LargePagePTE x21 x22 x23; pg_id = ptrFromPAddr x21; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; is_aligned (ptr >> 2) 4; fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) \<noteq> InvalidPTE\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) \<noteq> InvalidPTE
 2. \<And>s fun x x21 x22 x23. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) = LargePagePTE x21 x22 x23; pg_id = ptrFromPAddr x21; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; is_aligned (ptr >> 2) 4; fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) \<noteq> InvalidPTE\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2) \<in> {x. x && ~~ mask 4 = UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) && ~~ mask 4}
 3. \<And>s fun x x21 x22 x23. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) = LargePagePTE x21 x22 x23; pg_id = ptrFromPAddr x21; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; \<not> is_aligned (ptr >> 2) 4; UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) \<notin> pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) = InvalidPTE proof (prove)
goal (2 subgoals):
 1. \<And>s fun x x21 x22 x23. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) = LargePagePTE x21 x22 x23; pg_id = ptrFromPAddr x21; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; is_aligned (ptr >> 2) 4; fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) \<noteq> InvalidPTE\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2) \<in> {x. x && ~~ mask 4 = UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) && ~~ mask 4}
 2. \<And>s fun x x21 x22 x23. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) = LargePagePTE x21 x22 x23; pg_id = ptrFromPAddr x21; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; \<not> is_aligned (ptr >> 2) 4; UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) \<notin> pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) = InvalidPTE proof (prove)
goal (2 subgoals):
 1. \<And>s fun x x21 x22 x23. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) = LargePagePTE x21 x22 x23; pg_id = ptrFromPAddr x21; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; is_aligned (ptr >> 2) 4; fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) \<noteq> InvalidPTE\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 8) ((ptr + word_of_nat x * 4 && mask pt_bits >> 2) && ~~ mask 4) = UCAST(32 \<rightarrow> 8) ((ptr && mask pt_bits >> 2) && ~~ mask 4)
 2. \<And>s fun x x21 x22 x23. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) = LargePagePTE x21 x22 x23; pg_id = ptrFromPAddr x21; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; \<not> is_aligned (ptr >> 2) 4; UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) \<notin> pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) = InvalidPTE proof (prove)
goal (2 subgoals):
 1. \<And>s fun x x21 x22 x23. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) = LargePagePTE x21 x22 x23; pg_id = ptrFromPAddr x21; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; is_aligned (ptr >> 2) 4; fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) \<noteq> InvalidPTE\<rbrakk> \<Longrightarrow> (ptr + word_of_nat x * 4 && mask pt_bits >> 2) && ~~ mask 4 = (ptr && mask pt_bits >> 2) && ~~ mask 4
 2. \<And>s fun x x21 x22 x23. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) = LargePagePTE x21 x22 x23; pg_id = ptrFromPAddr x21; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; \<not> is_aligned (ptr >> 2) 4; UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) \<notin> pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) = InvalidPTE proof (prove)
goal (2 subgoals):
 1. \<And>s fun x x21 x22 x23. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) = LargePagePTE x21 x22 x23; pg_id = ptrFromPAddr x21; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; is_aligned (ptr >> 2) 4; fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) \<noteq> InvalidPTE\<rbrakk> \<Longrightarrow> ptr + word_of_nat x * 4 && mask pt_bits >> 2 >> 4 = ptr && mask pt_bits >> 2 >> 4
 2. \<And>s fun x x21 x22 x23. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) = LargePagePTE x21 x22 x23; pg_id = ptrFromPAddr x21; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; \<not> is_aligned (ptr >> 2) 4; UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) \<notin> pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) = InvalidPTE proof (prove)
goal (2 subgoals):
 1. \<And>s fun x x21 x22 x23. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); fun (UCAST(32 \<rightarrow> 8) ((ptr >> 2) && (mask pt_bits >> 2))) = LargePagePTE x21 x22 x23; pg_id = ptrFromPAddr x21; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; is_aligned (ptr >> 2) 4; fun (UCAST(32 \<rightarrow> 8) ((ptr + word_of_nat x * 4 >> 2) && (mask pt_bits >> 2))) \<noteq> InvalidPTE\<rbrakk> \<Longrightarrow> (ptr + word_of_nat x * 4 >> 6) && (mask pt_bits >> 6) = (ptr >> 6) && (mask pt_bits >> 6)
 2. \<And>s fun x x21 x22 x23. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) = LargePagePTE x21 x22 x23; pg_id = ptrFromPAddr x21; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; \<not> is_aligned (ptr >> 2) 4; UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) \<notin> pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) = InvalidPTE proof (prove)
goal (5 subgoals):
 1. \<And>s fun x x21 x22 x23. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); fun (UCAST(32 \<rightarrow> 8) ((ptr >> 2) && (mask pt_bits >> 2))) = LargePagePTE x21 x22 x23; pg_id = ptrFromPAddr x21; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; is_aligned (ptr >> 2) 4; fun (UCAST(32 \<rightarrow> 8) ((ptr + word_of_nat x * 4 >> 2) && (mask pt_bits >> 2))) \<noteq> InvalidPTE\<rbrakk> \<Longrightarrow> word_of_nat x * 4 < 2 ^ 6
 2. \<And>s fun x x21 x22 x23. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); fun (UCAST(32 \<rightarrow> 8) ((ptr >> 2) && (mask pt_bits >> 2))) = LargePagePTE x21 x22 x23; pg_id = ptrFromPAddr x21; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; is_aligned (ptr >> 2) 4; fun (UCAST(32 \<rightarrow> 8) ((ptr + word_of_nat x * 4 >> 2) && (mask pt_bits >> 2))) \<noteq> InvalidPTE\<rbrakk> \<Longrightarrow> is_aligned ptr 6
 3. \<And>s fun x x21 x22 x23. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); fun (UCAST(32 \<rightarrow> 8) ((ptr >> 2) && (mask pt_bits >> 2))) = LargePagePTE x21 x22 x23; pg_id = ptrFromPAddr x21; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; is_aligned (ptr >> 2) 4; fun (UCAST(32 \<rightarrow> 8) ((ptr + word_of_nat x * 4 >> 2) && (mask pt_bits >> 2))) \<noteq> InvalidPTE\<rbrakk> \<Longrightarrow> 6 \<le> LENGTH(32)
 4. \<And>s fun x x21 x22 x23. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); fun (UCAST(32 \<rightarrow> 8) ((ptr >> 2) && (mask pt_bits >> 2))) = LargePagePTE x21 x22 x23; pg_id = ptrFromPAddr x21; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; is_aligned (ptr >> 2) 4; fun (UCAST(32 \<rightarrow> 8) ((ptr + word_of_nat x * 4 >> 2) && (mask pt_bits >> 2))) \<noteq> InvalidPTE\<rbrakk> \<Longrightarrow> (ptr >> 6) && (mask pt_bits >> 6) = (ptr >> 6) && (mask pt_bits >> 6)
 5. \<And>s fun x x21 x22 x23. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) = LargePagePTE x21 x22 x23; pg_id = ptrFromPAddr x21; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; \<not> is_aligned (ptr >> 2) 4; UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) \<notin> pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) = InvalidPTE proof (prove)
goal (5 subgoals):
 1. \<And>s fun x x21 x22 x23. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); fun (UCAST(32 \<rightarrow> 8) ((ptr >> 2) && (mask pt_bits >> 2))) = LargePagePTE x21 x22 x23; pg_id = ptrFromPAddr x21; ptr + (word_of_nat x << 2) && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; is_aligned (ptr >> 2) 4; fun (UCAST(32 \<rightarrow> 8) ((ptr + (word_of_nat x << 2) >> 2) && (mask pt_bits >> 2))) \<noteq> InvalidPTE\<rbrakk> \<Longrightarrow> word_of_nat x << 2 < 0x40
 2. \<And>s fun x x21 x22 x23. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); fun (UCAST(32 \<rightarrow> 8) ((ptr >> 2) && (mask pt_bits >> 2))) = LargePagePTE x21 x22 x23; pg_id = ptrFromPAddr x21; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; is_aligned (ptr >> 2) 4; fun (UCAST(32 \<rightarrow> 8) ((ptr + word_of_nat x * 4 >> 2) && (mask pt_bits >> 2))) \<noteq> InvalidPTE\<rbrakk> \<Longrightarrow> is_aligned ptr 6
 3. \<And>s fun x x21 x22 x23. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); fun (UCAST(32 \<rightarrow> 8) ((ptr >> 2) && (mask pt_bits >> 2))) = LargePagePTE x21 x22 x23; pg_id = ptrFromPAddr x21; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; is_aligned (ptr >> 2) 4; fun (UCAST(32 \<rightarrow> 8) ((ptr + word_of_nat x * 4 >> 2) && (mask pt_bits >> 2))) \<noteq> InvalidPTE\<rbrakk> \<Longrightarrow> 6 \<le> LENGTH(32)
 4. \<And>s fun x x21 x22 x23. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); fun (UCAST(32 \<rightarrow> 8) ((ptr >> 2) && (mask pt_bits >> 2))) = LargePagePTE x21 x22 x23; pg_id = ptrFromPAddr x21; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; is_aligned (ptr >> 2) 4; fun (UCAST(32 \<rightarrow> 8) ((ptr + word_of_nat x * 4 >> 2) && (mask pt_bits >> 2))) \<noteq> InvalidPTE\<rbrakk> \<Longrightarrow> (ptr >> 6) && (mask pt_bits >> 6) = (ptr >> 6) && (mask pt_bits >> 6)
 5. \<And>s fun x x21 x22 x23. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) = LargePagePTE x21 x22 x23; pg_id = ptrFromPAddr x21; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; \<not> is_aligned (ptr >> 2) 4; UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) \<notin> pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) = InvalidPTE proof (prove)
goal (6 subgoals):
 1. \<And>s fun x x21 x22 x23. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); fun (UCAST(32 \<rightarrow> 8) ((ptr >> 2) && (mask pt_bits >> 2))) = LargePagePTE x21 x22 x23; pg_id = ptrFromPAddr x21; ptr + (word_of_nat x << 2) && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; is_aligned (ptr >> 2) 4; fun (UCAST(32 \<rightarrow> 8) ((ptr + (word_of_nat x << 2) >> 2) && (mask pt_bits >> 2))) \<noteq> InvalidPTE\<rbrakk> \<Longrightarrow> word_of_nat x < 2 ^ (6 - 2)
 2. \<And>s fun x x21 x22 x23. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); fun (UCAST(32 \<rightarrow> 8) ((ptr >> 2) && (mask pt_bits >> 2))) = LargePagePTE x21 x22 x23; pg_id = ptrFromPAddr x21; ptr + (word_of_nat x << 2) && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; is_aligned (ptr >> 2) 4; fun (UCAST(32 \<rightarrow> 8) ((ptr + (word_of_nat x << 2) >> 2) && (mask pt_bits >> 2))) \<noteq> InvalidPTE\<rbrakk> \<Longrightarrow> 6 < LENGTH(32)
 3. \<And>s fun x x21 x22 x23. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); fun (UCAST(32 \<rightarrow> 8) ((ptr >> 2) && (mask pt_bits >> 2))) = LargePagePTE x21 x22 x23; pg_id = ptrFromPAddr x21; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; is_aligned (ptr >> 2) 4; fun (UCAST(32 \<rightarrow> 8) ((ptr + word_of_nat x * 4 >> 2) && (mask pt_bits >> 2))) \<noteq> InvalidPTE\<rbrakk> \<Longrightarrow> is_aligned ptr 6
 4. \<And>s fun x x21 x22 x23. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); fun (UCAST(32 \<rightarrow> 8) ((ptr >> 2) && (mask pt_bits >> 2))) = LargePagePTE x21 x22 x23; pg_id = ptrFromPAddr x21; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; is_aligned (ptr >> 2) 4; fun (UCAST(32 \<rightarrow> 8) ((ptr + word_of_nat x * 4 >> 2) && (mask pt_bits >> 2))) \<noteq> InvalidPTE\<rbrakk> \<Longrightarrow> 6 \<le> LENGTH(32)
 5. \<And>s fun x x21 x22 x23. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); fun (UCAST(32 \<rightarrow> 8) ((ptr >> 2) && (mask pt_bits >> 2))) = LargePagePTE x21 x22 x23; pg_id = ptrFromPAddr x21; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; is_aligned (ptr >> 2) 4; fun (UCAST(32 \<rightarrow> 8) ((ptr + word_of_nat x * 4 >> 2) && (mask pt_bits >> 2))) \<noteq> InvalidPTE\<rbrakk> \<Longrightarrow> (ptr >> 6) && (mask pt_bits >> 6) = (ptr >> 6) && (mask pt_bits >> 6)
 6. \<And>s fun x x21 x22 x23. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) = LargePagePTE x21 x22 x23; pg_id = ptrFromPAddr x21; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; \<not> is_aligned (ptr >> 2) 4; UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) \<notin> pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) = InvalidPTE proof (prove)
goal (5 subgoals):
 1. \<And>s fun x x21 x22 x23. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); fun (UCAST(32 \<rightarrow> 8) ((ptr >> 2) && (mask pt_bits >> 2))) = LargePagePTE x21 x22 x23; pg_id = ptrFromPAddr x21; ptr + (word_of_nat x << 2) && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; is_aligned (ptr >> 2) 4; fun (UCAST(32 \<rightarrow> 8) ((ptr + (word_of_nat x << 2) >> 2) && (mask pt_bits >> 2))) \<noteq> InvalidPTE\<rbrakk> \<Longrightarrow> 6 < LENGTH(32)
 2. \<And>s fun x x21 x22 x23. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); fun (UCAST(32 \<rightarrow> 8) ((ptr >> 2) && (mask pt_bits >> 2))) = LargePagePTE x21 x22 x23; pg_id = ptrFromPAddr x21; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; is_aligned (ptr >> 2) 4; fun (UCAST(32 \<rightarrow> 8) ((ptr + word_of_nat x * 4 >> 2) && (mask pt_bits >> 2))) \<noteq> InvalidPTE\<rbrakk> \<Longrightarrow> is_aligned ptr 6
 3. \<And>s fun x x21 x22 x23. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); fun (UCAST(32 \<rightarrow> 8) ((ptr >> 2) && (mask pt_bits >> 2))) = LargePagePTE x21 x22 x23; pg_id = ptrFromPAddr x21; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; is_aligned (ptr >> 2) 4; fun (UCAST(32 \<rightarrow> 8) ((ptr + word_of_nat x * 4 >> 2) && (mask pt_bits >> 2))) \<noteq> InvalidPTE\<rbrakk> \<Longrightarrow> 6 \<le> LENGTH(32)
 4. \<And>s fun x x21 x22 x23. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); fun (UCAST(32 \<rightarrow> 8) ((ptr >> 2) && (mask pt_bits >> 2))) = LargePagePTE x21 x22 x23; pg_id = ptrFromPAddr x21; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; is_aligned (ptr >> 2) 4; fun (UCAST(32 \<rightarrow> 8) ((ptr + word_of_nat x * 4 >> 2) && (mask pt_bits >> 2))) \<noteq> InvalidPTE\<rbrakk> \<Longrightarrow> (ptr >> 6) && (mask pt_bits >> 6) = (ptr >> 6) && (mask pt_bits >> 6)
 5. \<And>s fun x x21 x22 x23. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) = LargePagePTE x21 x22 x23; pg_id = ptrFromPAddr x21; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; \<not> is_aligned (ptr >> 2) 4; UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) \<notin> pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) = InvalidPTE proof (prove)
goal (1 subgoal):
 1. \<And>s fun x x21 x22 x23. \<lbrakk>is_aligned ptr 6; invs s; kheap s (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); fun (UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2)) = LargePagePTE x21 x22 x23; pg_id = ptrFromPAddr x21; ptr + word_of_nat x * 4 && ~~ mask pt_bits = ptr && ~~ mask pt_bits; Suc 0 \<le> x; x < 16; entries_align pte_range_sz fun; \<not> is_aligned (ptr >> 2) 4; UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) \<notin> pte_range (fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))) (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2))\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 8) (ptr + word_of_nat x * 4 && mask pt_bits >> 2)) = InvalidPTE proof (prove)
goal:
No subgoals!