theory Finalise_DR

lemma dcorres_unmap_large_section:
  "\<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14;
    v < kernel_base \<rbrakk>
  \<Longrightarrow> dcorres dc \<top>
     (invs and valid_pdpt_objs
           and (pd_super_section_relation ((lookup_pd_slot ptr v) && ~~ mask pd_bits)
               pg_id (lookup_pd_slot ptr v)))
     (delete_cap_simple (cdl_lookup_pd_slot ptr v))
     (mapM (swp store_pde ARM_A.pde.InvalidPDE)
           (map (\<lambda>x. x + lookup_pd_slot ptr v) [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:store_pte_def 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
                   dcorres_lookup_pd_slot)+ apply (rule corres_guard_imp) apply (simp add:transform_pd_slot_ref_def) apply (rule corres_dummy_return_l) apply (rule corres_split[OF dcorres_store_invalid_pde_super_section[where pg_id = pg_id]]) apply(rule corres_dummy_return_l) apply (rule_tac r'=dc in corres_split) apply (rule dcorres_store_invalid_pde_tail_super_section[where slot = ptr]) apply (rule corres_free_return[where P=\<top> and P'=\<top>]) apply wp+ apply (wp store_pde_non_sense_wp) apply simp apply (simp add: hd_map_simp upto_enum_step_def upto_enum_def drop_map) apply (rule conjI) apply (rule less_kernel_base_mapping_slots) apply (simp add:pd_bits_def pageBits_def)+ apply (rule conjI, fastforce) \<comment> \<open>valid_idle\<close> apply (rule conj_comms[THEN iffD1]) apply (rule context_conjI) apply (clarsimp simp: tl_map) apply (clarsimp simp: field_simps) apply (subst mask_lower_twice[symmetric,where n = 6]) apply (simp add:pd_bits_def pageBits_def) apply (subst is_aligned_add_helper) apply (erule(1) lookup_pd_slot_aligned_6) 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 add: lookup_pd_slot_def is_aligned_neg_mask_eq
                    pd_shifting[unfolded pd_bits_def pageBits_def,simplified]) apply (clarsimp simp:pd_super_section_relation_def obj_at_def) apply (simp add: lookup_pd_slot_pd[unfolded pd_bits_def pageBits_def,simplified]
                   is_aligned_neg_mask_eq pd_shifting[unfolded pd_bits_def pageBits_def,simplified]) apply (rule ballI, drule (1) bspec) supply is_aligned_neg_mask2[simp del] apply (clarsimp simp: upto_0_to_n tl_map) apply (frule (1) lookup_pd_slot_aligned_6[unfolded pd_bits_def pageBits_def,simplified]) apply (drule(1) valid_pdpt_objs_pdD) apply clarsimp apply (frule (1) lookup_pd_slot_aligned_6[unfolded pd_bits_def pageBits_def,simplified]) apply (rename_tac pd rights attr ref s slot) apply (drule_tac x = "(ucast (lookup_pd_slot ptr v + of_nat slot * 4 && mask pd_bits >> 2))"
               and y = "ucast (lookup_pd_slot ptr v && mask pd_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::(12 word\<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:pd_bits_def pageBits_def) apply (simp add:pd_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:pd_bits_def pageBits_def) apply (simp add:pd_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 (erule lookup_pd_slot_aligned_6, simp) apply (simp add:pd_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 (slot * 4)::word32)") apply simp apply (rule le_less_trans[OF _ of_nat_mono_maybe[where y = 0]]) apply fastforce apply simp apply fastforce apply (rule ccontr) apply (erule_tac x = "ucast (lookup_pd_slot ptr v + of_nat slot * 4 && mask pd_bits >> 2)"
                   in in_empty_interE) apply (rule non_invalid_in_pde_range) apply (simp add: pd_bits_def pageBits_def field_simps) apply (simp add: ucast_neg_mask) apply (simp add:is_aligned_shiftr) 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+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask pd_bits) pg_id (lookup_pd_slot ptr v)) (delete_cap_simple (cdl_lookup_pd_slot ptr v)) (mapM (swp store_pde InvalidPDE) (map (\<lambda>x. x + lookup_pd_slot ptr v) [0 , 4 .e. 0x3C])) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask pd_bits) pg_id (lookup_pd_slot ptr v)) (delete_cap_simple (cdl_lookup_pd_slot ptr v)) (mapM (swp store_pde InvalidPDE) (map (\<lambda>x. x + lookup_pd_slot ptr v) [0 , 4 .e. 0x3C])) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base\<rbrakk> \<Longrightarrow> map (\<lambda>x. x + lookup_pd_slot ptr v) [0 , 4 .e. 0x3C] \<noteq> []
 2. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and (\<lambda>s. Ball (ran (kheap s)) obj_valid_pdpt) and pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask pd_bits) pg_id (lookup_pd_slot ptr v)) (delete_cap_simple (cdl_lookup_pd_slot ptr v)) (do y <- swp store_pde InvalidPDE (hd (map (\<lambda>x. x + lookup_pd_slot ptr v) [0 , 4 .e. 0x3C]));
ys <- mapM (swp store_pde InvalidPDE) (tl (map (\<lambda>x. x + lookup_pd_slot ptr v) [0 , 4 .e. 0x3C]));
return (y # ys)
od) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and (\<lambda>s. Ball (ran (kheap s)) obj_valid_pdpt) and pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask pd_bits) pg_id (lookup_pd_slot ptr v)) (delete_cap_simple (cdl_lookup_pd_slot ptr v)) (do y <- swp store_pde InvalidPDE (hd (map (\<lambda>x. x + lookup_pd_slot ptr v) [0 , 4 .e. 0x3C]));
ys <- mapM (swp store_pde InvalidPDE) (tl (map (\<lambda>x. x + lookup_pd_slot ptr v) [0 , 4 .e. 0x3C]));
return (y # ys)
od) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask pd_bits) pg_id (lookup_pd_slot ptr v)) (delete_cap_simple (cdl_lookup_pd_slot ptr v)) (do y <- store_pde (hd (map (\<lambda>x. x + lookup_pd_slot ptr v) [0 , 4 .e. 0x3C])) InvalidPDE;
ys <- mapM (swp store_pde InvalidPDE) (tl (map (\<lambda>x. x + lookup_pd_slot ptr v) [0 , 4 .e. 0x3C]));
return (() # ys)
od) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask pd_bits) pg_id (lookup_pd_slot ptr v)) (delete_cap_simple (cdl_lookup_pd_slot ptr v) >>= return) (do y <- store_pde (hd (map (\<lambda>x. x + lookup_pd_slot ptr v) [0 , 4 .e. 0x3C])) InvalidPDE;
ys <- mapM (swp store_pde InvalidPDE) (tl (map (\<lambda>x. x + lookup_pd_slot ptr v) [0 , 4 .e. 0x3C]));
return (() # ys)
od) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask pd_bits) pg_id (lookup_pd_slot ptr v)) (delete_cap_simple (transform_pd_slot_ref (lookup_pd_slot ptr v))) (do y <- store_pde (lookup_pd_slot ptr v) InvalidPDE;
ys <- mapM (swp store_pde InvalidPDE) (tl (map ((\<lambda>x. x + lookup_pd_slot ptr v) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]));
return (() # ys)
od) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base\<rbrakk> \<Longrightarrow> dcorres dc ?Q15 ?Q'15 (delete_cap_simple (transform_pd_slot_ref (lookup_pd_slot ptr v))) (do y <- store_pde (lookup_pd_slot ptr v) InvalidPDE;
ys <- mapM (swp store_pde InvalidPDE) (tl (map ((\<lambda>x. x + lookup_pd_slot ptr v) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]));
return (() # ys)
od)
 2. \<And>s. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; True\<rbrakk> \<Longrightarrow> ?Q15 s
 3. \<And>s. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask pd_bits) pg_id (lookup_pd_slot ptr v)) s\<rbrakk> \<Longrightarrow> ?Q'15 s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base\<rbrakk> \<Longrightarrow> dcorres dc ?Q15 ?Q'15 (delete_cap_simple (lookup_pd_slot ptr v && ~~ mask pd_bits, unat (lookup_pd_slot ptr v && mask pd_bits >> 2))) (do y <- store_pde (lookup_pd_slot ptr v) InvalidPDE;
ys <- mapM (swp store_pde InvalidPDE) (tl (map ((\<lambda>x. x + lookup_pd_slot ptr v) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]));
return (() # ys)
od)
 2. \<And>s. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; True\<rbrakk> \<Longrightarrow> ?Q15 s
 3. \<And>s. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask pd_bits) pg_id (lookup_pd_slot ptr v)) s\<rbrakk> \<Longrightarrow> ?Q'15 s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base\<rbrakk> \<Longrightarrow> dcorres dc ?Q15 ?Q'15 (delete_cap_simple (lookup_pd_slot ptr v && ~~ mask pd_bits, unat (lookup_pd_slot ptr v && mask pd_bits >> 2)) >>= return) (do y <- store_pde (lookup_pd_slot ptr v) InvalidPDE;
ys <- mapM (swp store_pde InvalidPDE) (tl (map ((\<lambda>x. x + lookup_pd_slot ptr v) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]));
return (() # ys)
od)
 2. \<And>s. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; True\<rbrakk> \<Longrightarrow> ?Q15 s
 3. \<And>s. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask pd_bits) pg_id (lookup_pd_slot ptr v)) s\<rbrakk> \<Longrightarrow> ?Q'15 s proof (prove)
goal (5 subgoals):
 1. \<And>x y. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; dc x y\<rbrakk> \<Longrightarrow> dcorres dc (?R21 x) (?R'21 y) (return x) (do ys <- mapM (swp store_pde InvalidPDE) (tl (map ((\<lambda>x. x + lookup_pd_slot ptr v) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]));
return (() # ys)
od)
 2. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base\<rbrakk> \<Longrightarrow> \<lbrace>?Q21\<rbrace> delete_cap_simple (lookup_pd_slot ptr v && ~~ mask pd_bits, unat (lookup_pd_slot ptr v && mask pd_bits >> 2)) \<lbrace>?R21\<rbrace>
 3. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base\<rbrakk> \<Longrightarrow> \<lbrace>?Q'21\<rbrace> store_pde (lookup_pd_slot ptr v) InvalidPDE \<lbrace>?R'21\<rbrace>
 4. \<And>s. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q21) s
 5. \<And>s. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask pd_bits) pg_id (lookup_pd_slot ptr v)) s\<rbrakk> \<Longrightarrow> (pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask pd_bits) pg_id (lookup_pd_slot ptr v) and invs and K (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and ?Q'21) s proof (prove)
goal (5 subgoals):
 1. \<And>x y. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; dc x y\<rbrakk> \<Longrightarrow> dcorres dc (?R21 x) (?R'21 y) (return x >>= return) (do ys <- mapM (swp store_pde InvalidPDE) (tl (map ((\<lambda>x. x + lookup_pd_slot ptr v) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]));
return (() # ys)
od)
 2. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base\<rbrakk> \<Longrightarrow> \<lbrace>?Q21\<rbrace> delete_cap_simple (lookup_pd_slot ptr v && ~~ mask pd_bits, unat (lookup_pd_slot ptr v && mask pd_bits >> 2)) \<lbrace>?R21\<rbrace>
 3. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base\<rbrakk> \<Longrightarrow> \<lbrace>?Q'21\<rbrace> store_pde (lookup_pd_slot ptr v) InvalidPDE \<lbrace>?R'21\<rbrace>
 4. \<And>s. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q21) s
 5. \<And>s. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask pd_bits) pg_id (lookup_pd_slot ptr v)) s\<rbrakk> \<Longrightarrow> (pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask pd_bits) pg_id (lookup_pd_slot ptr v) and invs and K (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and ?Q'21) s proof (prove)
goal (8 subgoals):
 1. \<And>x y. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; dc x y\<rbrakk> \<Longrightarrow> dcorres dc (?P30 x) (?P'32 y) (return x) (mapM (swp store_pde InvalidPDE) (tl (map ((\<lambda>x. x + lookup_pd_slot ptr v) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])))
 2. \<And>x y rv rv'. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; 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>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; dc x y\<rbrakk> \<Longrightarrow> \<lbrace>?Q31 x\<rbrace> return x \<lbrace>?R28 x y\<rbrace>
 4. \<And>x y. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; dc x y\<rbrakk> \<Longrightarrow> \<lbrace>?Q'33 y\<rbrace> mapM (swp store_pde InvalidPDE) (tl (map ((\<lambda>x. x + lookup_pd_slot ptr v) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])) \<lbrace>?R'28 x y\<rbrace>
 5. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base\<rbrakk> \<Longrightarrow> \<lbrace>?Q21\<rbrace> delete_cap_simple (lookup_pd_slot ptr v && ~~ mask pd_bits, unat (lookup_pd_slot ptr v && mask pd_bits >> 2)) \<lbrace>\<lambda>x. ?P30 x and ?Q31 x\<rbrace>
 6. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base\<rbrakk> \<Longrightarrow> \<lbrace>?Q'21\<rbrace> store_pde (lookup_pd_slot ptr v) InvalidPDE \<lbrace>\<lambda>y. ?P'32 y and ?Q'33 y\<rbrace>
 7. \<And>s. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q21) s
 8. \<And>s. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask pd_bits) pg_id (lookup_pd_slot ptr v)) s\<rbrakk> \<Longrightarrow> (pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask pd_bits) pg_id (lookup_pd_slot ptr v) and invs and K (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and ?Q'21) s proof (prove)
goal (7 subgoals):
 1. \<And>x y rv rv'. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; 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>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; dc x y\<rbrakk> \<Longrightarrow> \<lbrace>?Q31 x\<rbrace> return x \<lbrace>?R28 x y\<rbrace>
 3. \<And>x y. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; dc x y\<rbrakk> \<Longrightarrow> \<lbrace>?Q'33 y\<rbrace> mapM (swp store_pde InvalidPDE) (tl (map ((\<lambda>x. x + lookup_pd_slot ptr v) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])) \<lbrace>?R'28 x y\<rbrace>
 4. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base\<rbrakk> \<Longrightarrow> \<lbrace>?Q21\<rbrace> delete_cap_simple (lookup_pd_slot ptr v && ~~ mask pd_bits, unat (lookup_pd_slot ptr v && mask pd_bits >> 2)) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q31 x\<rbrace>
 5. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base\<rbrakk> \<Longrightarrow> \<lbrace>?Q'21\<rbrace> store_pde (lookup_pd_slot ptr v) InvalidPDE \<lbrace>\<lambda>y. valid_idle and (\<lambda>s. \<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (ptr && ~~ mask pd_bits) s \<and> (\<forall>slot\<in>set (tl (map ((\<lambda>x. x + lookup_pd_slot ptr v) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)) = InvalidPDE)) and K (\<forall>sl\<in>set (tl (map ((\<lambda>x. x + lookup_pd_slot ptr v) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). sl && ~~ mask pd_bits = ptr && ~~ mask pd_bits) and ?Q'33 y\<rbrace>
 6. \<And>s. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q21) s
 7. \<And>s. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask pd_bits) pg_id (lookup_pd_slot ptr v)) s\<rbrakk> \<Longrightarrow> (pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask pd_bits) pg_id (lookup_pd_slot ptr v) and invs and K (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and ?Q'21) s proof (prove)
goal (6 subgoals):
 1. \<And>x y. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; dc x y\<rbrakk> \<Longrightarrow> \<lbrace>?Q31 x\<rbrace> return x \<lbrace>\<lambda>rv _. True\<rbrace>
 2. \<And>x y. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; dc x y\<rbrakk> \<Longrightarrow> \<lbrace>?Q'33 y\<rbrace> mapM (swp store_pde InvalidPDE) (tl (map ((\<lambda>x. x + lookup_pd_slot ptr v) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])) \<lbrace>\<lambda>rv' _. True\<rbrace>
 3. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base\<rbrakk> \<Longrightarrow> \<lbrace>?Q21\<rbrace> delete_cap_simple (lookup_pd_slot ptr v && ~~ mask pd_bits, unat (lookup_pd_slot ptr v && mask pd_bits >> 2)) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q31 x\<rbrace>
 4. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base\<rbrakk> \<Longrightarrow> \<lbrace>?Q'21\<rbrace> store_pde (lookup_pd_slot ptr v) InvalidPDE \<lbrace>\<lambda>y. valid_idle and (\<lambda>s. \<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (ptr && ~~ mask pd_bits) s \<and> (\<forall>slot\<in>set (tl (map ((\<lambda>x. x + lookup_pd_slot ptr v) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)) = InvalidPDE)) and K (\<forall>sl\<in>set (tl (map ((\<lambda>x. x + lookup_pd_slot ptr v) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). sl && ~~ mask pd_bits = ptr && ~~ mask pd_bits) and ?Q'33 y\<rbrace>
 5. \<And>s. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q21) s
 6. \<And>s. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask pd_bits) pg_id (lookup_pd_slot ptr v)) s\<rbrakk> \<Longrightarrow> (pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask pd_bits) pg_id (lookup_pd_slot ptr v) and invs and K (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and ?Q'21) s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base\<rbrakk> \<Longrightarrow> \<lbrace>?P'54\<rbrace> store_pde (lookup_pd_slot ptr v) InvalidPDE \<lbrace>\<lambda>rv s. (\<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (ptr && ~~ mask pd_bits) s \<and> (\<forall>slot\<in>set (tl (map ((\<lambda>x. x + lookup_pd_slot ptr v) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)) = InvalidPDE)) \<and> K (\<forall>sl\<in>set (tl (map ((\<lambda>x. x + lookup_pd_slot ptr v) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). sl && ~~ mask pd_bits = ptr && ~~ mask pd_bits) s \<and> True\<rbrace>
 2. \<And>s. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True)) s
 3. \<And>s. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask pd_bits) pg_id (lookup_pd_slot ptr v)) s\<rbrakk> \<Longrightarrow> (pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask pd_bits) pg_id (lookup_pd_slot ptr v) and invs and K (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and (\<lambda>s. valid_idle s \<and> ?P'54 s)) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True)) s
 2. \<And>s. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask pd_bits) pg_id (lookup_pd_slot ptr v)) s\<rbrakk> \<Longrightarrow> (pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask pd_bits) pg_id (lookup_pd_slot ptr v) and invs and K (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and (\<lambda>s. valid_idle s \<and> (\<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (ptr && ~~ mask pd_bits) s \<and> (\<forall>slot\<in>set (tl (map ((\<lambda>x. x + lookup_pd_slot ptr v) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)) = InvalidPDE)) \<and> K (\<forall>sl\<in>set (tl (map ((\<lambda>x. x + lookup_pd_slot ptr v) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). sl && ~~ mask pd_bits = ptr && ~~ mask pd_bits) s \<and> True)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask pd_bits) pg_id (lookup_pd_slot ptr v)) s\<rbrakk> \<Longrightarrow> (pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask pd_bits) pg_id (lookup_pd_slot ptr v) and invs and K (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and (\<lambda>s. valid_idle s \<and> (\<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (ptr && ~~ mask pd_bits) s \<and> (\<forall>slot\<in>set (tl (map ((\<lambda>x. x + lookup_pd_slot ptr v) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)) = InvalidPDE)) \<and> K (\<forall>sl\<in>set (tl (map ((\<lambda>x. x + lookup_pd_slot ptr v) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). sl && ~~ mask pd_bits = ptr && ~~ mask pd_bits) s \<and> True)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; invs s \<and> Ball (ran (kheap s)) obj_valid_pdpt \<and> pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask pd_bits) pg_id (lookup_pd_slot ptr v) s\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2) \<notin> kernel_mapping_slots \<and> valid_idle s \<and> (\<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (ptr && ~~ mask pd_bits) s \<and> (\<forall>slot\<in>set (tl (map ((\<lambda>x. x + lookup_pd_slot ptr v) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)) = InvalidPDE)) \<and> (\<forall>sl\<in>set (tl (map ((\<lambda>x. x + lookup_pd_slot ptr v) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). sl && ~~ mask pd_bits = ptr && ~~ mask pd_bits) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; invs s \<and> Ball (ran (kheap s)) obj_valid_pdpt \<and> pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask pd_bits) pg_id (lookup_pd_slot ptr v) s\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2) \<notin> kernel_mapping_slots
 2. \<And>s. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; invs s \<and> Ball (ran (kheap s)) obj_valid_pdpt \<and> pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask pd_bits) pg_id (lookup_pd_slot ptr v) s\<rbrakk> \<Longrightarrow> valid_idle s \<and> (\<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (ptr && ~~ mask pd_bits) s \<and> (\<forall>slot\<in>set (tl (map ((\<lambda>x. x + lookup_pd_slot ptr v) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)) = InvalidPDE)) \<and> (\<forall>sl\<in>set (tl (map ((\<lambda>x. x + lookup_pd_slot ptr v) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). sl && ~~ mask pd_bits = ptr && ~~ mask pd_bits) proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; invs s \<and> Ball (ran (kheap s)) obj_valid_pdpt \<and> pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask pd_bits) pg_id (lookup_pd_slot ptr v) s\<rbrakk> \<Longrightarrow> v < kernel_base
 2. \<And>s. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; invs s \<and> Ball (ran (kheap s)) obj_valid_pdpt \<and> pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask pd_bits) pg_id (lookup_pd_slot ptr v) s\<rbrakk> \<Longrightarrow> is_aligned ptr pd_bits
 3. \<And>s. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; invs s \<and> Ball (ran (kheap s)) obj_valid_pdpt \<and> pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask pd_bits) pg_id (lookup_pd_slot ptr v) s\<rbrakk> \<Longrightarrow> valid_idle s \<and> (\<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (ptr && ~~ mask pd_bits) s \<and> (\<forall>slot\<in>set (tl (map ((\<lambda>x. x + lookup_pd_slot ptr v) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)) = InvalidPDE)) \<and> (\<forall>sl\<in>set (tl (map ((\<lambda>x. x + lookup_pd_slot ptr v) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). sl && ~~ mask pd_bits = ptr && ~~ mask pd_bits) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; invs s \<and> (\<forall>x\<in>ran (kheap s). obj_valid_pdpt x) \<and> pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask 14) pg_id (lookup_pd_slot ptr v) s\<rbrakk> \<Longrightarrow> valid_idle s \<and> (\<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (ptr && ~~ mask 14) s \<and> (\<forall>slot\<in>set (tl (map ((\<lambda>x. x + lookup_pd_slot ptr v) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). f (UCAST(32 \<rightarrow> 12) (slot && mask 14 >> 2)) = InvalidPDE)) \<and> (\<forall>sl\<in>set (tl (map ((\<lambda>x. x + lookup_pd_slot ptr v) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). sl && ~~ mask 14 = ptr && ~~ mask 14) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; invs s \<and> (\<forall>x\<in>ran (kheap s). obj_valid_pdpt x) \<and> pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask 14) pg_id (lookup_pd_slot ptr v) s\<rbrakk> \<Longrightarrow> (\<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (ptr && ~~ mask 14) s \<and> (\<forall>slot\<in>set (tl (map ((\<lambda>x. x + lookup_pd_slot ptr v) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). f (UCAST(32 \<rightarrow> 12) (slot && mask 14 >> 2)) = InvalidPDE)) \<and> (\<forall>sl\<in>set (tl (map ((\<lambda>x. x + lookup_pd_slot ptr v) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). sl && ~~ mask 14 = ptr && ~~ mask 14) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; invs s \<and> (\<forall>x\<in>ran (kheap s). obj_valid_pdpt x) \<and> pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask 14) pg_id (lookup_pd_slot ptr v) s\<rbrakk> \<Longrightarrow> (\<forall>sl\<in>set (tl (map ((\<lambda>x. x + lookup_pd_slot ptr v) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). sl && ~~ mask 14 = ptr && ~~ mask 14) \<and> (\<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (ptr && ~~ mask 14) s \<and> (\<forall>slot\<in>set (tl (map ((\<lambda>x. x + lookup_pd_slot ptr v) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). f (UCAST(32 \<rightarrow> 12) (slot && mask 14 >> 2)) = InvalidPDE)) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; invs s \<and> (\<forall>x\<in>ran (kheap s). obj_valid_pdpt x) \<and> pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask 14) pg_id (lookup_pd_slot ptr v) s\<rbrakk> \<Longrightarrow> \<forall>sl\<in>set (tl (map ((\<lambda>x. x + lookup_pd_slot ptr v) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). sl && ~~ mask 14 = ptr && ~~ mask 14
 2. \<And>s. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; invs s \<and> (\<forall>x\<in>ran (kheap s). obj_valid_pdpt x) \<and> pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask 14) pg_id (lookup_pd_slot ptr v) s; \<forall>sl\<in>set (tl (map ((\<lambda>x. x + lookup_pd_slot ptr v) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). sl && ~~ mask 14 = ptr && ~~ mask 14\<rbrakk> \<Longrightarrow> \<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (ptr && ~~ mask 14) s \<and> (\<forall>slot\<in>set (tl (map ((\<lambda>x. x + lookup_pd_slot ptr v) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). f (UCAST(32 \<rightarrow> 12) (slot && mask 14 >> 2)) = InvalidPDE) proof (prove)
goal (2 subgoals):
 1. \<And>s sl. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask 14) pg_id (lookup_pd_slot ptr v) s; Suc 0 \<le> sl; sl < 16\<rbrakk> \<Longrightarrow> word_of_nat sl * 4 + lookup_pd_slot ptr v && ~~ mask 14 = ptr && ~~ mask 14
 2. \<And>s. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; invs s \<and> (\<forall>x\<in>ran (kheap s). obj_valid_pdpt x) \<and> pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask 14) pg_id (lookup_pd_slot ptr v) s; \<forall>sl\<in>set (tl (map ((\<lambda>x. x + lookup_pd_slot ptr v) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). sl && ~~ mask 14 = ptr && ~~ mask 14\<rbrakk> \<Longrightarrow> \<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (ptr && ~~ mask 14) s \<and> (\<forall>slot\<in>set (tl (map ((\<lambda>x. x + lookup_pd_slot ptr v) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). f (UCAST(32 \<rightarrow> 12) (slot && mask 14 >> 2)) = InvalidPDE) proof (prove)
goal (2 subgoals):
 1. \<And>s sl. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask 14) pg_id (lookup_pd_slot ptr v) s; Suc 0 \<le> sl; sl < 16\<rbrakk> \<Longrightarrow> lookup_pd_slot ptr v + word_of_nat sl * 4 && ~~ mask 14 = ptr && ~~ mask 14
 2. \<And>s. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; invs s \<and> (\<forall>x\<in>ran (kheap s). obj_valid_pdpt x) \<and> pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask 14) pg_id (lookup_pd_slot ptr v) s; \<forall>sl\<in>set (tl (map ((\<lambda>x. x + lookup_pd_slot ptr v) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). sl && ~~ mask 14 = ptr && ~~ mask 14\<rbrakk> \<Longrightarrow> \<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (ptr && ~~ mask 14) s \<and> (\<forall>slot\<in>set (tl (map ((\<lambda>x. x + lookup_pd_slot ptr v) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). f (UCAST(32 \<rightarrow> 12) (slot && mask 14 >> 2)) = InvalidPDE) proof (prove)
goal (3 subgoals):
 1. \<And>s sl. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask 14) pg_id (lookup_pd_slot ptr v) s; Suc 0 \<le> sl; sl < 16\<rbrakk> \<Longrightarrow> 6 \<le> 14
 2. \<And>s sl. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask 14) pg_id (lookup_pd_slot ptr v) s; Suc 0 \<le> sl; sl < 16\<rbrakk> \<Longrightarrow> (lookup_pd_slot ptr v + word_of_nat sl * 4 && ~~ mask 6) && ~~ mask 14 = ptr && ~~ mask 14
 3. \<And>s. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; invs s \<and> (\<forall>x\<in>ran (kheap s). obj_valid_pdpt x) \<and> pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask 14) pg_id (lookup_pd_slot ptr v) s; \<forall>sl\<in>set (tl (map ((\<lambda>x. x + lookup_pd_slot ptr v) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). sl && ~~ mask 14 = ptr && ~~ mask 14\<rbrakk> \<Longrightarrow> \<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (ptr && ~~ mask 14) s \<and> (\<forall>slot\<in>set (tl (map ((\<lambda>x. x + lookup_pd_slot ptr v) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). f (UCAST(32 \<rightarrow> 12) (slot && mask 14 >> 2)) = InvalidPDE) proof (prove)
goal (2 subgoals):
 1. \<And>s sl. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask 14) pg_id (lookup_pd_slot ptr v) s; Suc 0 \<le> sl; sl < 16\<rbrakk> \<Longrightarrow> (lookup_pd_slot ptr v + word_of_nat sl * 4 && ~~ mask 6) && ~~ mask 14 = ptr && ~~ mask 14
 2. \<And>s. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; invs s \<and> (\<forall>x\<in>ran (kheap s). obj_valid_pdpt x) \<and> pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask 14) pg_id (lookup_pd_slot ptr v) s; \<forall>sl\<in>set (tl (map ((\<lambda>x. x + lookup_pd_slot ptr v) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). sl && ~~ mask 14 = ptr && ~~ mask 14\<rbrakk> \<Longrightarrow> \<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (ptr && ~~ mask 14) s \<and> (\<forall>slot\<in>set (tl (map ((\<lambda>x. x + lookup_pd_slot ptr v) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). f (UCAST(32 \<rightarrow> 12) (slot && mask 14 >> 2)) = InvalidPDE) proof (prove)
goal (4 subgoals):
 1. \<And>s sl. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask 14) pg_id (lookup_pd_slot ptr v) s; Suc 0 \<le> sl; sl < 16\<rbrakk> \<Longrightarrow> is_aligned (lookup_pd_slot ptr v) 6
 2. \<And>s sl. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask 14) pg_id (lookup_pd_slot ptr v) s; Suc 0 \<le> sl; sl < 16\<rbrakk> \<Longrightarrow> word_of_nat sl * 4 < 2 ^ 6
 3. \<And>s sl. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask 14) pg_id (lookup_pd_slot ptr v) s; Suc 0 \<le> sl; sl < 16\<rbrakk> \<Longrightarrow> lookup_pd_slot ptr v && ~~ mask 14 = ptr && ~~ mask 14
 4. \<And>s. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; invs s \<and> (\<forall>x\<in>ran (kheap s). obj_valid_pdpt x) \<and> pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask 14) pg_id (lookup_pd_slot ptr v) s; \<forall>sl\<in>set (tl (map ((\<lambda>x. x + lookup_pd_slot ptr v) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). sl && ~~ mask 14 = ptr && ~~ mask 14\<rbrakk> \<Longrightarrow> \<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (ptr && ~~ mask 14) s \<and> (\<forall>slot\<in>set (tl (map ((\<lambda>x. x + lookup_pd_slot ptr v) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). f (UCAST(32 \<rightarrow> 12) (slot && mask 14 >> 2)) = InvalidPDE) proof (prove)
goal (3 subgoals):
 1. \<And>s sl. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask 14) pg_id (lookup_pd_slot ptr v) s; Suc 0 \<le> sl; sl < 16\<rbrakk> \<Longrightarrow> word_of_nat sl * 4 < 2 ^ 6
 2. \<And>s sl. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask 14) pg_id (lookup_pd_slot ptr v) s; Suc 0 \<le> sl; sl < 16\<rbrakk> \<Longrightarrow> lookup_pd_slot ptr v && ~~ mask 14 = ptr && ~~ mask 14
 3. \<And>s. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; invs s \<and> (\<forall>x\<in>ran (kheap s). obj_valid_pdpt x) \<and> pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask 14) pg_id (lookup_pd_slot ptr v) s; \<forall>sl\<in>set (tl (map ((\<lambda>x. x + lookup_pd_slot ptr v) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). sl && ~~ mask 14 = ptr && ~~ mask 14\<rbrakk> \<Longrightarrow> \<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (ptr && ~~ mask 14) s \<and> (\<forall>slot\<in>set (tl (map ((\<lambda>x. x + lookup_pd_slot ptr v) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). f (UCAST(32 \<rightarrow> 12) (slot && mask 14 >> 2)) = InvalidPDE) proof (prove)
goal (3 subgoals):
 1. \<And>s sl. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask 14) pg_id (lookup_pd_slot ptr v) s; Suc 0 \<le> sl; sl < 16\<rbrakk> \<Longrightarrow> word_of_nat sl * 4 < 0x40
 2. \<And>s sl. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask 14) pg_id (lookup_pd_slot ptr v) s; Suc 0 \<le> sl; sl < 16\<rbrakk> \<Longrightarrow> lookup_pd_slot ptr v && ~~ mask 14 = ptr && ~~ mask 14
 3. \<And>s. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; invs s \<and> (\<forall>x\<in>ran (kheap s). obj_valid_pdpt x) \<and> pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask 14) pg_id (lookup_pd_slot ptr v) s; \<forall>sl\<in>set (tl (map ((\<lambda>x. x + lookup_pd_slot ptr v) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). sl && ~~ mask 14 = ptr && ~~ mask 14\<rbrakk> \<Longrightarrow> \<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (ptr && ~~ mask 14) s \<and> (\<forall>slot\<in>set (tl (map ((\<lambda>x. x + lookup_pd_slot ptr v) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). f (UCAST(32 \<rightarrow> 12) (slot && mask 14 >> 2)) = InvalidPDE) proof (prove)
goal (4 subgoals):
 1. \<And>s sl. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask 14) pg_id (lookup_pd_slot ptr v) s; Suc 0 \<le> sl; sl < 16\<rbrakk> \<Longrightarrow> sl < 16
 2. \<And>s sl. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask 14) pg_id (lookup_pd_slot ptr v) s; Suc 0 \<le> sl; sl < 16\<rbrakk> \<Longrightarrow> 6 < LENGTH(32)
 3. \<And>s sl. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask 14) pg_id (lookup_pd_slot ptr v) s; Suc 0 \<le> sl; sl < 16\<rbrakk> \<Longrightarrow> lookup_pd_slot ptr v && ~~ mask 14 = ptr && ~~ mask 14
 4. \<And>s. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; invs s \<and> (\<forall>x\<in>ran (kheap s). obj_valid_pdpt x) \<and> pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask 14) pg_id (lookup_pd_slot ptr v) s; \<forall>sl\<in>set (tl (map ((\<lambda>x. x + lookup_pd_slot ptr v) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). sl && ~~ mask 14 = ptr && ~~ mask 14\<rbrakk> \<Longrightarrow> \<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (ptr && ~~ mask 14) s \<and> (\<forall>slot\<in>set (tl (map ((\<lambda>x. x + lookup_pd_slot ptr v) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). f (UCAST(32 \<rightarrow> 12) (slot && mask 14 >> 2)) = InvalidPDE) proof (prove)
goal (3 subgoals):
 1. \<And>s sl. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask 14) pg_id (lookup_pd_slot ptr v) s; Suc 0 \<le> sl; sl < 16\<rbrakk> \<Longrightarrow> 6 < LENGTH(32)
 2. \<And>s sl. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask 14) pg_id (lookup_pd_slot ptr v) s; Suc 0 \<le> sl; sl < 16\<rbrakk> \<Longrightarrow> lookup_pd_slot ptr v && ~~ mask 14 = ptr && ~~ mask 14
 3. \<And>s. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; invs s \<and> (\<forall>x\<in>ran (kheap s). obj_valid_pdpt x) \<and> pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask 14) pg_id (lookup_pd_slot ptr v) s; \<forall>sl\<in>set (tl (map ((\<lambda>x. x + lookup_pd_slot ptr v) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). sl && ~~ mask 14 = ptr && ~~ mask 14\<rbrakk> \<Longrightarrow> \<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (ptr && ~~ mask 14) s \<and> (\<forall>slot\<in>set (tl (map ((\<lambda>x. x + lookup_pd_slot ptr v) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). f (UCAST(32 \<rightarrow> 12) (slot && mask 14 >> 2)) = InvalidPDE) proof (prove)
goal (2 subgoals):
 1. \<And>s sl. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask 14) pg_id (lookup_pd_slot ptr v) s; Suc 0 \<le> sl; sl < 16\<rbrakk> \<Longrightarrow> lookup_pd_slot ptr v && ~~ mask 14 = ptr && ~~ mask 14
 2. \<And>s. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; invs s \<and> (\<forall>x\<in>ran (kheap s). obj_valid_pdpt x) \<and> pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask 14) pg_id (lookup_pd_slot ptr v) s; \<forall>sl\<in>set (tl (map ((\<lambda>x. x + lookup_pd_slot ptr v) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). sl && ~~ mask 14 = ptr && ~~ mask 14\<rbrakk> \<Longrightarrow> \<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (ptr && ~~ mask 14) s \<and> (\<forall>slot\<in>set (tl (map ((\<lambda>x. x + lookup_pd_slot ptr v) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). f (UCAST(32 \<rightarrow> 12) (slot && mask 14 >> 2)) = InvalidPDE) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; invs s \<and> (\<forall>x\<in>ran (kheap s). obj_valid_pdpt x) \<and> pd_super_section_relation (lookup_pd_slot ptr v && ~~ mask 14) pg_id (lookup_pd_slot ptr v) s; \<forall>sl\<in>set (tl (map ((\<lambda>x. x + lookup_pd_slot ptr v) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). sl && ~~ mask 14 = ptr && ~~ mask 14\<rbrakk> \<Longrightarrow> \<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (ptr && ~~ mask 14) s \<and> (\<forall>slot\<in>set (tl (map ((\<lambda>x. x + lookup_pd_slot ptr v) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). f (UCAST(32 \<rightarrow> 12) (slot && mask 14 >> 2)) = InvalidPDE) proof (prove)
goal (1 subgoal):
 1. \<And>s fun u va ref1. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; \<forall>sl\<in>set (tl (map ((\<lambda>x. x + lookup_pd_slot ptr v) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). sl && ~~ mask 14 = ptr && ~~ mask 14; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; kheap s (lookup_pd_slot ptr v && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory fun)); fun (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2)) = SuperSectionPDE ref1 u va; pg_id = ptrFromPAddr ref1\<rbrakk> \<Longrightarrow> \<exists>f. kheap s (ptr && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory f)) \<and> (\<forall>slot\<in>set (tl (map ((\<lambda>x. x + lookup_pd_slot ptr v) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). f (UCAST(32 \<rightarrow> 12) (slot && mask 14 >> 2)) = InvalidPDE) proof (prove)
goal (1 subgoal):
 1. \<And>s fun u va ref1. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; \<forall>sl\<in>set (tl (map ((\<lambda>x. x + lookup_pd_slot ptr v) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). sl && ~~ mask 14 = ptr; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; kheap s ptr = Some (ArchObj (arch_kernel_obj.PageDirectory fun)); fun (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2)) = SuperSectionPDE ref1 u va; pg_id = ptrFromPAddr ref1\<rbrakk> \<Longrightarrow> \<forall>slot\<in>set (tl (map ((\<lambda>x. x + lookup_pd_slot ptr v) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])). fun (UCAST(32 \<rightarrow> 12) (slot && mask 14 >> 2)) = InvalidPDE proof (prove)
goal (1 subgoal):
 1. \<And>s fun u va ref1 slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; kheap s ptr = Some (ArchObj (arch_kernel_obj.PageDirectory fun)); fun (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2)) = SuperSectionPDE ref1 u va; pg_id = ptrFromPAddr ref1; slot \<in> set (tl (map ((\<lambda>x. x + lookup_pd_slot ptr v) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])); slot && ~~ mask 14 = ptr\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 12) (slot && mask 14 >> 2)) = InvalidPDE proof (prove)
goal (1 subgoal):
 1. \<And>s fun u va ref1 slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; v < kernel_base; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; kheap s ptr = Some (ArchObj (arch_kernel_obj.PageDirectory fun)); fun (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2)) = SuperSectionPDE ref1 u va; pg_id = ptrFromPAddr ref1; slot \<in> set (tl (map ((\<lambda>x. x + lookup_pd_slot ptr v) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16])); slot && ~~ mask 14 = ptr\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 12) (slot && mask 14 >> 2)) = InvalidPDE proof (prove)
goal (1 subgoal):
 1. \<And>s fun u va ref1 slot x. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (slot && ~~ mask 14) 14; v < kernel_base; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; kheap s (slot && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory fun)); fun (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (slot && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref1 u va; pg_id = ptrFromPAddr ref1; ptr = slot && ~~ mask 14; slot = word_of_nat x * 4 + lookup_pd_slot (slot && ~~ mask 14) v; Suc 0 \<le> x; x < 16\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 12) (slot && mask 14 >> 2)) = InvalidPDE proof (prove)
goal (1 subgoal):
 1. \<And>s fun u va ref1 slot x. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (slot && ~~ mask 14) 14; v < kernel_base; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; kheap s (slot && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory fun)); fun (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (slot && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref1 u va; pg_id = ptrFromPAddr ref1; ptr = slot && ~~ mask 14; slot = word_of_nat x * 4 + lookup_pd_slot (slot && ~~ mask 14) v; Suc 0 \<le> x; x < 16; is_aligned (lookup_pd_slot (slot && ~~ mask 14) v) 6\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 12) (slot && mask 14 >> 2)) = InvalidPDE proof (prove)
goal (1 subgoal):
 1. \<And>s fun u va ref1 slot x. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (slot && ~~ mask 14) 14; v < kernel_base; invs s; kheap s (slot && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory fun)); fun (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (slot && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref1 u va; pg_id = ptrFromPAddr ref1; ptr = slot && ~~ mask 14; slot = word_of_nat x * 4 + lookup_pd_slot (slot && ~~ mask 14) v; Suc 0 \<le> x; x < 16; is_aligned (lookup_pd_slot (slot && ~~ mask 14) v) 6; valid_entries pde_range fun \<and> entries_align pde_range_sz fun\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 12) (slot && mask 14 >> 2)) = InvalidPDE proof (prove)
goal (1 subgoal):
 1. \<And>s fun u va ref1 slot x. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (slot && ~~ mask 14) 14; v < kernel_base; invs s; kheap s (slot && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory fun)); fun (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (slot && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref1 u va; pg_id = ptrFromPAddr ref1; ptr = slot && ~~ mask 14; slot = word_of_nat x * 4 + lookup_pd_slot (slot && ~~ mask 14) v; Suc 0 \<le> x; x < 16; is_aligned (lookup_pd_slot (slot && ~~ mask 14) v) 6; valid_entries pde_range fun; entries_align pde_range_sz fun\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 12) (slot && mask 14 >> 2)) = InvalidPDE proof (prove)
goal (1 subgoal):
 1. \<And>s fun u va ref1 slot x. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (slot && ~~ mask 14) 14; v < kernel_base; invs s; kheap s (slot && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory fun)); fun (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (slot && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref1 u va; pg_id = ptrFromPAddr ref1; ptr = slot && ~~ mask 14; slot = word_of_nat x * 4 + lookup_pd_slot (slot && ~~ mask 14) v; Suc 0 \<le> x; x < 16; is_aligned (lookup_pd_slot (slot && ~~ mask 14) v) 6; valid_entries pde_range fun; entries_align pde_range_sz fun; is_aligned (lookup_pd_slot (slot && ~~ mask 14) v) 6\<rbrakk> \<Longrightarrow> fun (UCAST(32 \<rightarrow> 12) (slot && mask 14 >> 2)) = InvalidPDE proof (prove)
goal (1 subgoal):
 1. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; valid_entries pde_range pd; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6\<rbrakk> \<Longrightarrow> pd (UCAST(32 \<rightarrow> 12) (s && mask 14 >> 2)) = InvalidPDE proof (prove)
goal (2 subgoals):
 1. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2) \<noteq> UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2)
 2. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2)) \<inter> pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> pd (UCAST(32 \<rightarrow> 12) (s && mask 14 >> 2)) = InvalidPDE proof (prove)
goal (2 subgoals):
 1. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; \<not> UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2) \<noteq> UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2)\<rbrakk> \<Longrightarrow> False
 2. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2)) \<inter> pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> pd (UCAST(32 \<rightarrow> 12) (s && mask 14 >> 2)) = InvalidPDE proof (prove)
goal (2 subgoals):
 1. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v + word_of_nat slot * 4 && mask pd_bits >> 2) = UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)\<rbrakk> \<Longrightarrow> False
 2. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2)) \<inter> pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> pd (UCAST(32 \<rightarrow> 12) (s && mask 14 >> 2)) = InvalidPDE proof (prove)
goal (2 subgoals):
 1. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v + word_of_nat slot * 4 && mask pd_bits >> 2)) = UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2))\<rbrakk> \<Longrightarrow> False
 2. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2)) \<inter> pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> pd (UCAST(32 \<rightarrow> 12) (s && mask 14 >> 2)) = InvalidPDE proof (prove)
goal (2 subgoals):
 1. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v + word_of_nat slot * 4 && mask pd_bits >> 2)) << 2 = UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) << 2\<rbrakk> \<Longrightarrow> False
 2. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2)) \<inter> pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> pd (UCAST(32 \<rightarrow> 12) (s && mask 14 >> 2)) = InvalidPDE proof (prove)
goal (3 subgoals):
 1. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6\<rbrakk> \<Longrightarrow> lookup_pd_slot (s && ~~ mask 14) v + word_of_nat slot * 4 && mask pd_bits >> 2 < 2 ^ LENGTH(12)
 2. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; lookup_pd_slot (s && ~~ mask 14) v + word_of_nat slot * 4 && mask pd_bits >> 2 << 2 = UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) << 2\<rbrakk> \<Longrightarrow> False
 3. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2)) \<inter> pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> pd (UCAST(32 \<rightarrow> 12) (s && mask 14 >> 2)) = InvalidPDE proof (prove)
goal (3 subgoals):
 1. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6\<rbrakk> \<Longrightarrow> lookup_pd_slot (s && ~~ mask 14) v + word_of_nat slot * 4 && mask pd_bits < 2 ^ (2 + LENGTH(12))
 2. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; lookup_pd_slot (s && ~~ mask 14) v + word_of_nat slot * 4 && mask pd_bits >> 2 << 2 = UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) << 2\<rbrakk> \<Longrightarrow> False
 3. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2)) \<inter> pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> pd (UCAST(32 \<rightarrow> 12) (s && mask 14 >> 2)) = InvalidPDE proof (prove)
goal (4 subgoals):
 1. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6\<rbrakk> \<Longrightarrow> pd_bits < LENGTH(32)
 2. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6\<rbrakk> \<Longrightarrow> 2 ^ pd_bits \<le> 2 ^ (2 + LENGTH(12))
 3. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; lookup_pd_slot (s && ~~ mask 14) v + word_of_nat slot * 4 && mask pd_bits >> 2 << 2 = UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) << 2\<rbrakk> \<Longrightarrow> False
 4. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2)) \<inter> pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> pd (UCAST(32 \<rightarrow> 12) (s && mask 14 >> 2)) = InvalidPDE proof (prove)
goal (3 subgoals):
 1. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6\<rbrakk> \<Longrightarrow> 2 ^ pd_bits \<le> 2 ^ (2 + LENGTH(12))
 2. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; lookup_pd_slot (s && ~~ mask 14) v + word_of_nat slot * 4 && mask pd_bits >> 2 << 2 = UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) << 2\<rbrakk> \<Longrightarrow> False
 3. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2)) \<inter> pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> pd (UCAST(32 \<rightarrow> 12) (s && mask 14 >> 2)) = InvalidPDE proof (prove)
goal (2 subgoals):
 1. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; lookup_pd_slot (s && ~~ mask 14) v + word_of_nat slot * 4 && mask pd_bits >> 2 << 2 = UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) << 2\<rbrakk> \<Longrightarrow> False
 2. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2)) \<inter> pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> pd (UCAST(32 \<rightarrow> 12) (s && mask 14 >> 2)) = InvalidPDE proof (prove)
goal (3 subgoals):
 1. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6\<rbrakk> \<Longrightarrow> lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2 < 2 ^ LENGTH(12)
 2. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; lookup_pd_slot (s && ~~ mask 14) v + word_of_nat slot * 4 && mask pd_bits >> 2 << 2 = lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2 << 2\<rbrakk> \<Longrightarrow> False
 3. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2)) \<inter> pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> pd (UCAST(32 \<rightarrow> 12) (s && mask 14 >> 2)) = InvalidPDE proof (prove)
goal (3 subgoals):
 1. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6\<rbrakk> \<Longrightarrow> lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits < 2 ^ (2 + LENGTH(12))
 2. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; lookup_pd_slot (s && ~~ mask 14) v + word_of_nat slot * 4 && mask pd_bits >> 2 << 2 = lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2 << 2\<rbrakk> \<Longrightarrow> False
 3. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2)) \<inter> pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> pd (UCAST(32 \<rightarrow> 12) (s && mask 14 >> 2)) = InvalidPDE proof (prove)
goal (4 subgoals):
 1. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6\<rbrakk> \<Longrightarrow> pd_bits < LENGTH(32)
 2. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6\<rbrakk> \<Longrightarrow> 2 ^ pd_bits \<le> 2 ^ (2 + LENGTH(12))
 3. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; lookup_pd_slot (s && ~~ mask 14) v + word_of_nat slot * 4 && mask pd_bits >> 2 << 2 = lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2 << 2\<rbrakk> \<Longrightarrow> False
 4. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2)) \<inter> pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> pd (UCAST(32 \<rightarrow> 12) (s && mask 14 >> 2)) = InvalidPDE proof (prove)
goal (3 subgoals):
 1. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6\<rbrakk> \<Longrightarrow> 2 ^ pd_bits \<le> 2 ^ (2 + LENGTH(12))
 2. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; lookup_pd_slot (s && ~~ mask 14) v + word_of_nat slot * 4 && mask pd_bits >> 2 << 2 = lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2 << 2\<rbrakk> \<Longrightarrow> False
 3. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2)) \<inter> pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> pd (UCAST(32 \<rightarrow> 12) (s && mask 14 >> 2)) = InvalidPDE proof (prove)
goal (2 subgoals):
 1. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; lookup_pd_slot (s && ~~ mask 14) v + word_of_nat slot * 4 && mask pd_bits >> 2 << 2 = lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2 << 2\<rbrakk> \<Longrightarrow> False
 2. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2)) \<inter> pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> pd (UCAST(32 \<rightarrow> 12) (s && mask 14 >> 2)) = InvalidPDE proof (prove)
goal (2 subgoals):
 1. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; (lookup_pd_slot (s && ~~ mask 14) v + word_of_nat slot * 4 && mask pd_bits) && ~~ mask 2 = (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits) && ~~ mask 2\<rbrakk> \<Longrightarrow> False
 2. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2)) \<inter> pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> pd (UCAST(32 \<rightarrow> 12) (s && mask 14 >> 2)) = InvalidPDE proof (prove)
goal (3 subgoals):
 1. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6\<rbrakk> \<Longrightarrow> is_aligned (lookup_pd_slot (s && ~~ mask 14) v + word_of_nat slot * 4 && mask pd_bits) 2
 2. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; lookup_pd_slot (s && ~~ mask 14) v + word_of_nat slot * 4 && mask pd_bits = (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits) && ~~ mask 2\<rbrakk> \<Longrightarrow> False
 3. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2)) \<inter> pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> pd (UCAST(32 \<rightarrow> 12) (s && mask 14 >> 2)) = InvalidPDE proof (prove)
goal (4 subgoals):
 1. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd\<rbrakk> \<Longrightarrow> is_aligned (word_of_nat slot * 4) 2
 2. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd\<rbrakk> \<Longrightarrow> 2 \<le> 6
 3. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; lookup_pd_slot (s && ~~ mask 14) v + word_of_nat slot * 4 && mask pd_bits = (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits) && ~~ mask 2\<rbrakk> \<Longrightarrow> False
 4. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2)) \<inter> pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> pd (UCAST(32 \<rightarrow> 12) (s && mask 14 >> 2)) = InvalidPDE proof (prove)
goal (3 subgoals):
 1. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd\<rbrakk> \<Longrightarrow> 2 \<le> 6
 2. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; lookup_pd_slot (s && ~~ mask 14) v + word_of_nat slot * 4 && mask pd_bits = (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits) && ~~ mask 2\<rbrakk> \<Longrightarrow> False
 3. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2)) \<inter> pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> pd (UCAST(32 \<rightarrow> 12) (s && mask 14 >> 2)) = InvalidPDE proof (prove)
goal (2 subgoals):
 1. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; lookup_pd_slot (s && ~~ mask 14) v + word_of_nat slot * 4 && mask pd_bits = (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits) && ~~ mask 2\<rbrakk> \<Longrightarrow> False
 2. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2)) \<inter> pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> pd (UCAST(32 \<rightarrow> 12) (s && mask 14 >> 2)) = InvalidPDE proof (prove)
goal (3 subgoals):
 1. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6\<rbrakk> \<Longrightarrow> is_aligned (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits) 2
 2. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; lookup_pd_slot (s && ~~ mask 14) v + word_of_nat slot * 4 && mask pd_bits = lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits\<rbrakk> \<Longrightarrow> False
 3. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2)) \<inter> pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> pd (UCAST(32 \<rightarrow> 12) (s && mask 14 >> 2)) = InvalidPDE proof (prove)
goal (3 subgoals):
 1. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd\<rbrakk> \<Longrightarrow> 2 \<le> 6
 2. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; lookup_pd_slot (s && ~~ mask 14) v + word_of_nat slot * 4 && mask pd_bits = lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits\<rbrakk> \<Longrightarrow> False
 3. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2)) \<inter> pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> pd (UCAST(32 \<rightarrow> 12) (s && mask 14 >> 2)) = InvalidPDE proof (prove)
goal (2 subgoals):
 1. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; lookup_pd_slot (s && ~~ mask 14) v + word_of_nat slot * 4 && mask pd_bits = lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits\<rbrakk> \<Longrightarrow> False
 2. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2)) \<inter> pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> pd (UCAST(32 \<rightarrow> 12) (s && mask 14 >> 2)) = InvalidPDE proof (prove)
goal (6 subgoals):
 1. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6\<rbrakk> \<Longrightarrow> is_aligned (lookup_pd_slot (s && ~~ mask 14) v) (?m180 sa pd rights attr ref s slot)
 2. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6\<rbrakk> \<Longrightarrow> ?m180 sa pd rights attr ref s slot \<le> pd_bits
 3. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6\<rbrakk> \<Longrightarrow> pd_bits < 32
 4. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6\<rbrakk> \<Longrightarrow> word_of_nat slot * 4 < 2 ^ ?m180 sa pd rights attr ref s slot
 5. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits) + word_of_nat slot * 4 = lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits\<rbrakk> \<Longrightarrow> False
 6. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2)) \<inter> pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> pd (UCAST(32 \<rightarrow> 12) (s && mask 14 >> 2)) = InvalidPDE proof (prove)
goal (5 subgoals):
 1. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6\<rbrakk> \<Longrightarrow> 6 \<le> pd_bits
 2. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6\<rbrakk> \<Longrightarrow> pd_bits < 32
 3. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6\<rbrakk> \<Longrightarrow> word_of_nat slot * 4 < 2 ^ 6
 4. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits) + word_of_nat slot * 4 = lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits\<rbrakk> \<Longrightarrow> False
 5. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2)) \<inter> pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> pd (UCAST(32 \<rightarrow> 12) (s && mask 14 >> 2)) = InvalidPDE proof (prove)
goal (3 subgoals):
 1. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask 14 >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6\<rbrakk> \<Longrightarrow> word_of_nat slot * 4 < 0x40
 2. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits) + word_of_nat slot * 4 = lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits\<rbrakk> \<Longrightarrow> False
 3. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2)) \<inter> pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> pd (UCAST(32 \<rightarrow> 12) (s && mask 14 >> 2)) = InvalidPDE proof (prove)
goal (3 subgoals):
 1. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask 14 >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = (word_of_nat slot << 2) + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6\<rbrakk> \<Longrightarrow> word_of_nat slot << 2 < 0x40
 2. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits) + word_of_nat slot * 4 = lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits\<rbrakk> \<Longrightarrow> False
 3. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2)) \<inter> pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> pd (UCAST(32 \<rightarrow> 12) (s && mask 14 >> 2)) = InvalidPDE proof (prove)
goal (4 subgoals):
 1. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask 14 >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = (word_of_nat slot << 2) + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6\<rbrakk> \<Longrightarrow> word_of_nat slot < 2 ^ (6 - 2)
 2. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask 14 >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = (word_of_nat slot << 2) + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6\<rbrakk> \<Longrightarrow> 6 < LENGTH(32)
 3. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits) + word_of_nat slot * 4 = lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits\<rbrakk> \<Longrightarrow> False
 4. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2)) \<inter> pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> pd (UCAST(32 \<rightarrow> 12) (s && mask 14 >> 2)) = InvalidPDE proof (prove)
goal (3 subgoals):
 1. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask 14 >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = (word_of_nat slot << 2) + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6\<rbrakk> \<Longrightarrow> 6 < LENGTH(32)
 2. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits) + word_of_nat slot * 4 = lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits\<rbrakk> \<Longrightarrow> False
 3. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2)) \<inter> pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> pd (UCAST(32 \<rightarrow> 12) (s && mask 14 >> 2)) = InvalidPDE proof (prove)
goal (2 subgoals):
 1. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits) + word_of_nat slot * 4 = lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits\<rbrakk> \<Longrightarrow> False
 2. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2)) \<inter> pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> pd (UCAST(32 \<rightarrow> 12) (s && mask 14 >> 2)) = InvalidPDE proof (prove)
goal (2 subgoals):
 1. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (s && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned s 6; word_of_nat slot * 4 = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2)) \<inter> pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> pd (UCAST(32 \<rightarrow> 12) (s && mask 14 >> 2)) = InvalidPDE proof (prove)
goal (3 subgoals):
 1. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (s && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned s 6; word_of_nat slot * 4 = 0; 0 < word_of_nat (slot * 4)\<rbrakk> \<Longrightarrow> False
 2. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (s && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned s 6; word_of_nat slot * 4 = 0\<rbrakk> \<Longrightarrow> 0 < word_of_nat (slot * 4)
 3. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2)) \<inter> pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> pd (UCAST(32 \<rightarrow> 12) (s && mask 14 >> 2)) = InvalidPDE proof (prove)
goal (2 subgoals):
 1. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (s && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned s 6; word_of_nat slot * 4 = 0\<rbrakk> \<Longrightarrow> 0 < word_of_nat (slot * 4)
 2. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2)) \<inter> pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> pd (UCAST(32 \<rightarrow> 12) (s && mask 14 >> 2)) = InvalidPDE proof (prove)
goal (4 subgoals):
 1. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (s && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned s 6; word_of_nat slot * 4 = 0\<rbrakk> \<Longrightarrow> 0 \<le> word_of_nat 0
 2. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (s && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned s 6; word_of_nat slot * 4 = 0\<rbrakk> \<Longrightarrow> slot * 4 < 2 ^ LENGTH(32)
 3. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (s && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned s 6; word_of_nat slot * 4 = 0\<rbrakk> \<Longrightarrow> 0 < slot * 4
 4. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2)) \<inter> pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> pd (UCAST(32 \<rightarrow> 12) (s && mask 14 >> 2)) = InvalidPDE proof (prove)
goal (3 subgoals):
 1. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (s && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned s 6; word_of_nat slot * 4 = 0\<rbrakk> \<Longrightarrow> slot * 4 < 2 ^ LENGTH(32)
 2. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (s && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned s 6; word_of_nat slot * 4 = 0\<rbrakk> \<Longrightarrow> 0 < slot * 4
 3. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2)) \<inter> pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> pd (UCAST(32 \<rightarrow> 12) (s && mask 14 >> 2)) = InvalidPDE proof (prove)
goal (2 subgoals):
 1. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (s && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned s 6; word_of_nat slot * 4 = 0\<rbrakk> \<Longrightarrow> 0 < slot * 4
 2. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2)) \<inter> pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> pd (UCAST(32 \<rightarrow> 12) (s && mask 14 >> 2)) = InvalidPDE proof (prove)
goal (1 subgoal):
 1. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2)) \<inter> pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2)) = {}\<rbrakk> \<Longrightarrow> pd (UCAST(32 \<rightarrow> 12) (s && mask 14 >> 2)) = InvalidPDE proof (prove)
goal (1 subgoal):
 1. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2)) \<inter> pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2)) = {}; pd (UCAST(32 \<rightarrow> 12) (s && mask 14 >> 2)) \<noteq> InvalidPDE\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pd (UCAST(32 \<rightarrow> 12) (s && mask 14 >> 2)) \<noteq> InvalidPDE\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2) \<in> pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2))
 2. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pd (UCAST(32 \<rightarrow> 12) (s && mask 14 >> 2)) \<noteq> InvalidPDE\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2) \<in> pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2)) proof (prove)
goal (2 subgoals):
 1. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pd (UCAST(32 \<rightarrow> 12) (s && mask 14 >> 2)) \<noteq> InvalidPDE\<rbrakk> \<Longrightarrow> pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2)) \<noteq> InvalidPDE
 2. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pd (UCAST(32 \<rightarrow> 12) (s && mask 14 >> 2)) \<noteq> InvalidPDE\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2) \<in> pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2)) proof (prove)
goal (1 subgoal):
 1. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pd (UCAST(32 \<rightarrow> 12) (s && mask 14 >> 2)) \<noteq> InvalidPDE\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v + word_of_nat slot * 4 && mask pd_bits >> 2) \<in> pde_range (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2))) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot ptr v && mask pd_bits >> 2)) proof (prove)
goal (1 subgoal):
 1. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pd (UCAST(32 \<rightarrow> 12) (s && mask 14 >> 2)) \<noteq> InvalidPDE\<rbrakk> \<Longrightarrow> (is_aligned (lookup_pd_slot (s && ~~ mask 14) v >> 2) 4 \<longrightarrow> UCAST(32 \<rightarrow> 12) ((lookup_pd_slot (s && ~~ mask 14) v + word_of_nat slot * 4 && mask pd_bits >> 2) && ~~ mask 4) = UCAST(32 \<rightarrow> 12) ((lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2) && ~~ mask 4)) \<and> (\<not> is_aligned (lookup_pd_slot (s && ~~ mask 14) v >> 2) 4 \<longrightarrow> UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v + word_of_nat slot * 4 && mask pd_bits >> 2) = UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) proof (prove)
goal (1 subgoal):
 1. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pd (UCAST(32 \<rightarrow> 12) (s && mask 14 >> 2)) \<noteq> InvalidPDE\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) ((lookup_pd_slot (s && ~~ mask 14) v + word_of_nat slot * 4 && mask pd_bits >> 2) && ~~ mask 4) = UCAST(32 \<rightarrow> 12) ((lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2) && ~~ mask 4) proof (prove)
goal (1 subgoal):
 1. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pd (UCAST(32 \<rightarrow> 12) (s && mask 14 >> 2)) \<noteq> InvalidPDE\<rbrakk> \<Longrightarrow> (lookup_pd_slot (s && ~~ mask 14) v + word_of_nat slot * 4 && mask pd_bits >> 2) && ~~ mask 4 = (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2) && ~~ mask 4 proof (prove)
goal (1 subgoal):
 1. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2)) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pd (UCAST(32 \<rightarrow> 12) (s && mask 14 >> 2)) \<noteq> InvalidPDE\<rbrakk> \<Longrightarrow> lookup_pd_slot (s && ~~ mask 14) v + word_of_nat slot * 4 && mask pd_bits >> 2 >> 4 = lookup_pd_slot (s && ~~ mask 14) v && mask pd_bits >> 2 >> 4 proof (prove)
goal (1 subgoal):
 1. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) ((lookup_pd_slot (s && ~~ mask 14) v >> 2) && (mask pd_bits >> 2))) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pd (UCAST(32 \<rightarrow> 12) ((s >> 2) && (mask 14 >> 2))) \<noteq> InvalidPDE\<rbrakk> \<Longrightarrow> (lookup_pd_slot (s && ~~ mask 14) v + word_of_nat slot * 4 >> 6) && (mask pd_bits >> 6) = (lookup_pd_slot (s && ~~ mask 14) v >> 6) && (mask pd_bits >> 6) proof (prove)
goal (4 subgoals):
 1. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) ((lookup_pd_slot (s && ~~ mask 14) v >> 2) && (mask pd_bits >> 2))) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pd (UCAST(32 \<rightarrow> 12) ((s >> 2) && (mask 14 >> 2))) \<noteq> InvalidPDE\<rbrakk> \<Longrightarrow> word_of_nat slot * 4 < 2 ^ 6
 2. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) ((lookup_pd_slot (s && ~~ mask 14) v >> 2) && (mask pd_bits >> 2))) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pd (UCAST(32 \<rightarrow> 12) ((s >> 2) && (mask 14 >> 2))) \<noteq> InvalidPDE\<rbrakk> \<Longrightarrow> is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6
 3. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) ((lookup_pd_slot (s && ~~ mask 14) v >> 2) && (mask pd_bits >> 2))) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pd (UCAST(32 \<rightarrow> 12) ((s >> 2) && (mask 14 >> 2))) \<noteq> InvalidPDE\<rbrakk> \<Longrightarrow> 6 \<le> LENGTH(32)
 4. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) ((lookup_pd_slot (s && ~~ mask 14) v >> 2) && (mask pd_bits >> 2))) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pd (UCAST(32 \<rightarrow> 12) ((s >> 2) && (mask 14 >> 2))) \<noteq> InvalidPDE\<rbrakk> \<Longrightarrow> (lookup_pd_slot (s && ~~ mask 14) v >> 6) && (mask pd_bits >> 6) = (lookup_pd_slot (s && ~~ mask 14) v >> 6) && (mask pd_bits >> 6) proof (prove)
goal (4 subgoals):
 1. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) ((lookup_pd_slot (s && ~~ mask 14) v >> 2) && (mask pd_bits >> 2))) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = (word_of_nat slot << 2) + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pd (UCAST(32 \<rightarrow> 12) ((s >> 2) && (mask 14 >> 2))) \<noteq> InvalidPDE\<rbrakk> \<Longrightarrow> word_of_nat slot << 2 < 0x40
 2. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) ((lookup_pd_slot (s && ~~ mask 14) v >> 2) && (mask pd_bits >> 2))) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pd (UCAST(32 \<rightarrow> 12) ((s >> 2) && (mask 14 >> 2))) \<noteq> InvalidPDE\<rbrakk> \<Longrightarrow> is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6
 3. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) ((lookup_pd_slot (s && ~~ mask 14) v >> 2) && (mask pd_bits >> 2))) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pd (UCAST(32 \<rightarrow> 12) ((s >> 2) && (mask 14 >> 2))) \<noteq> InvalidPDE\<rbrakk> \<Longrightarrow> 6 \<le> LENGTH(32)
 4. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) ((lookup_pd_slot (s && ~~ mask 14) v >> 2) && (mask pd_bits >> 2))) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pd (UCAST(32 \<rightarrow> 12) ((s >> 2) && (mask 14 >> 2))) \<noteq> InvalidPDE\<rbrakk> \<Longrightarrow> (lookup_pd_slot (s && ~~ mask 14) v >> 6) && (mask pd_bits >> 6) = (lookup_pd_slot (s && ~~ mask 14) v >> 6) && (mask pd_bits >> 6) proof (prove)
goal (5 subgoals):
 1. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) ((lookup_pd_slot (s && ~~ mask 14) v >> 2) && (mask pd_bits >> 2))) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = (word_of_nat slot << 2) + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pd (UCAST(32 \<rightarrow> 12) ((s >> 2) && (mask 14 >> 2))) \<noteq> InvalidPDE\<rbrakk> \<Longrightarrow> word_of_nat slot < 2 ^ (6 - 2)
 2. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) ((lookup_pd_slot (s && ~~ mask 14) v >> 2) && (mask pd_bits >> 2))) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = (word_of_nat slot << 2) + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pd (UCAST(32 \<rightarrow> 12) ((s >> 2) && (mask 14 >> 2))) \<noteq> InvalidPDE\<rbrakk> \<Longrightarrow> 6 < LENGTH(32)
 3. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) ((lookup_pd_slot (s && ~~ mask 14) v >> 2) && (mask pd_bits >> 2))) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pd (UCAST(32 \<rightarrow> 12) ((s >> 2) && (mask 14 >> 2))) \<noteq> InvalidPDE\<rbrakk> \<Longrightarrow> is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6
 4. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) ((lookup_pd_slot (s && ~~ mask 14) v >> 2) && (mask pd_bits >> 2))) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pd (UCAST(32 \<rightarrow> 12) ((s >> 2) && (mask 14 >> 2))) \<noteq> InvalidPDE\<rbrakk> \<Longrightarrow> 6 \<le> LENGTH(32)
 5. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) ((lookup_pd_slot (s && ~~ mask 14) v >> 2) && (mask pd_bits >> 2))) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pd (UCAST(32 \<rightarrow> 12) ((s >> 2) && (mask 14 >> 2))) \<noteq> InvalidPDE\<rbrakk> \<Longrightarrow> (lookup_pd_slot (s && ~~ mask 14) v >> 6) && (mask pd_bits >> 6) = (lookup_pd_slot (s && ~~ mask 14) v >> 6) && (mask pd_bits >> 6) proof (prove)
goal (4 subgoals):
 1. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) ((lookup_pd_slot (s && ~~ mask 14) v >> 2) && (mask pd_bits >> 2))) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = (word_of_nat slot << 2) + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pd (UCAST(32 \<rightarrow> 12) ((s >> 2) && (mask 14 >> 2))) \<noteq> InvalidPDE\<rbrakk> \<Longrightarrow> 6 < LENGTH(32)
 2. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) ((lookup_pd_slot (s && ~~ mask 14) v >> 2) && (mask pd_bits >> 2))) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pd (UCAST(32 \<rightarrow> 12) ((s >> 2) && (mask 14 >> 2))) \<noteq> InvalidPDE\<rbrakk> \<Longrightarrow> is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6
 3. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) ((lookup_pd_slot (s && ~~ mask 14) v >> 2) && (mask pd_bits >> 2))) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pd (UCAST(32 \<rightarrow> 12) ((s >> 2) && (mask 14 >> 2))) \<noteq> InvalidPDE\<rbrakk> \<Longrightarrow> 6 \<le> LENGTH(32)
 4. \<And>sa pd rights attr ref s slot. \<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned (s && ~~ mask 14) 14; v < kernel_base; invs sa; kheap sa (s && ~~ mask 14) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) ((lookup_pd_slot (s && ~~ mask 14) v >> 2) && (mask pd_bits >> 2))) = SuperSectionPDE ref rights attr; pg_id = ptrFromPAddr ref; ptr = s && ~~ mask 14; s = word_of_nat slot * 4 + lookup_pd_slot (s && ~~ mask 14) v; Suc 0 \<le> slot; slot < 16; entries_align pde_range_sz pd; is_aligned (lookup_pd_slot (s && ~~ mask 14) v) 6; pd (UCAST(32 \<rightarrow> 12) ((s >> 2) && (mask 14 >> 2))) \<noteq> InvalidPDE\<rbrakk> \<Longrightarrow> (lookup_pd_slot (s && ~~ mask 14) v >> 6) && (mask pd_bits >> 6) = (lookup_pd_slot (s && ~~ mask 14) v >> 6) && (mask pd_bits >> 6) proof (prove)
goal:
No subgoals!