theory ArchVSpaceEntries_AI

lemma init_arch_objects_valid_pdpt:
  "\<lbrace>valid_pdpt_objs and pspace_aligned and valid_arch_state
           and K (\<exists>us sz. orefs = retype_addrs ptr type n us
               \<and> range_cover ptr sz (obj_bits_api type us) n)\<rbrace>
     init_arch_objects type ptr n obj_sz orefs
   \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>" apply (rule hoare_gen_asm)+ apply (clarsimp simp: init_arch_objects_def
             split del: if_split) apply (rule hoare_pre) apply (wp | wpc)+ apply (rule_tac Q="\<lambda>rv. valid_pdpt_objs and pspace_aligned and valid_arch_state"
                  in hoare_post_imp, simp) apply (rule mapM_x_wp') apply (rule hoare_pre, wp copy_global_mappings_valid_pdpt_objs) apply clarsimp apply (drule_tac sz=sz in retype_addrs_aligned) apply (simp add:range_cover_def) apply (drule range_cover.sz,simp add:word_bits_def) apply (simp add:range_cover_def) apply (clarsimp simp:obj_bits_api_def pd_bits_def pageBits_def
       arch_kobj_size_def default_arch_object_def range_cover_def)+ apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and pspace_aligned and valid_arch_state and K (\<exists>us sz. orefs = retype_addrs ptr type n us \<and> range_cover ptr sz (obj_bits_api type us) n)\<rbrace> init_arch_objects type ptr n obj_sz orefs \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<exists>us sz. orefs = retype_addrs ptr type n us \<and> range_cover ptr sz (obj_bits_api type us) n \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and pspace_aligned and valid_arch_state\<rbrace> init_arch_objects type ptr n obj_sz orefs \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>us sz. \<lbrakk>orefs = retype_addrs ptr type n us; range_cover ptr sz (obj_bits_api type us) n\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and pspace_aligned and valid_arch_state\<rbrace> if type = ArchObject PageDirectoryObj then do y <- mapM_x copy_global_mappings (retype_addrs ptr (ArchObject PageDirectoryObj) n us);
do_machine_op (mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + 2 ^ pd_bits - 1) (addrFromPPtr x)) (retype_addrs ptr (ArchObject PageDirectoryObj) n us))
od else return () \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>us sz. \<lbrakk>orefs = retype_addrs ptr type n us; range_cover ptr sz (obj_bits_api type us) n\<rbrakk> \<Longrightarrow> \<lbrace>?Q9 us sz\<rbrace> if type = ArchObject PageDirectoryObj then do y <- mapM_x copy_global_mappings (retype_addrs ptr (ArchObject PageDirectoryObj) n us);
do_machine_op (mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + 2 ^ pd_bits - 1) (addrFromPPtr x)) (retype_addrs ptr (ArchObject PageDirectoryObj) n us))
od else return () \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace>
 2. \<And>us sz s. \<lbrakk>orefs = retype_addrs ptr type n us; range_cover ptr sz (obj_bits_api type us) n; ((\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and pspace_aligned and valid_arch_state) s\<rbrakk> \<Longrightarrow> ?Q9 us sz s proof (prove)
goal (3 subgoals):
 1. \<And>us sz. \<lbrakk>orefs = retype_addrs ptr type n us; range_cover ptr sz (obj_bits_api type us) n; type = ArchObject PageDirectoryObj\<rbrakk> \<Longrightarrow> \<lbrace>?Q13 us sz\<rbrace> mapM_x copy_global_mappings (retype_addrs ptr (ArchObject PageDirectoryObj) n us) \<lbrace>\<lambda>y s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace>
 2. \<And>us sz. \<lbrakk>orefs = retype_addrs ptr type n us; range_cover ptr sz (obj_bits_api type us) n; type \<noteq> ArchObject PageDirectoryObj\<rbrakk> \<Longrightarrow> \<lbrace>?R13 us sz\<rbrace> return () \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace>
 3. \<And>us sz s. \<lbrakk>orefs = retype_addrs ptr type n us; range_cover ptr sz (obj_bits_api type us) n; ((\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and pspace_aligned and valid_arch_state) s\<rbrakk> \<Longrightarrow> (type = ArchObject PageDirectoryObj \<longrightarrow> ?Q13 us sz s) \<and> (type \<noteq> ArchObject PageDirectoryObj \<longrightarrow> ?R13 us sz s) proof (prove)
goal (3 subgoals):
 1. \<And>us sz. \<lbrakk>orefs = retype_addrs ptr type n us; range_cover ptr sz (obj_bits_api type us) n; type = ArchObject PageDirectoryObj\<rbrakk> \<Longrightarrow> \<lbrace>?Q13 us sz\<rbrace> mapM_x copy_global_mappings (retype_addrs ptr (ArchObject PageDirectoryObj) n us) \<lbrace>\<lambda>rv. (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and pspace_aligned and valid_arch_state\<rbrace>
 2. \<And>us sz. \<lbrakk>orefs = retype_addrs ptr type n us; range_cover ptr sz (obj_bits_api type us) n; type \<noteq> ArchObject PageDirectoryObj\<rbrakk> \<Longrightarrow> \<lbrace>?R13 us sz\<rbrace> return () \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace>
 3. \<And>us sz s. \<lbrakk>orefs = retype_addrs ptr type n us; range_cover ptr sz (obj_bits_api type us) n; ((\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and pspace_aligned and valid_arch_state) s\<rbrakk> \<Longrightarrow> (type = ArchObject PageDirectoryObj \<longrightarrow> ?Q13 us sz s) \<and> (type \<noteq> ArchObject PageDirectoryObj \<longrightarrow> ?R13 us sz s) proof (prove)
goal (3 subgoals):
 1. \<And>us sz x. \<lbrakk>orefs = retype_addrs ptr type n us; range_cover ptr sz (obj_bits_api type us) n; type = ArchObject PageDirectoryObj; x \<in> set (retype_addrs ptr (ArchObject PageDirectoryObj) n us)\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and pspace_aligned and valid_arch_state\<rbrace> copy_global_mappings x \<lbrace>\<lambda>rv. (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and pspace_aligned and valid_arch_state\<rbrace>
 2. \<And>us sz. \<lbrakk>orefs = retype_addrs ptr type n us; range_cover ptr sz (obj_bits_api type us) n; type \<noteq> ArchObject PageDirectoryObj\<rbrakk> \<Longrightarrow> \<lbrace>?R13 us sz\<rbrace> return () \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace>
 3. \<And>us sz s. \<lbrakk>orefs = retype_addrs ptr type n us; range_cover ptr sz (obj_bits_api type us) n; ((\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and pspace_aligned and valid_arch_state) s\<rbrakk> \<Longrightarrow> (type = ArchObject PageDirectoryObj \<longrightarrow> ((\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and pspace_aligned and valid_arch_state) s) \<and> (type \<noteq> ArchObject PageDirectoryObj \<longrightarrow> ?R13 us sz s) proof (prove)
goal (3 subgoals):
 1. \<And>us sz x s. \<lbrakk>orefs = retype_addrs ptr type n us; range_cover ptr sz (obj_bits_api type us) n; type = ArchObject PageDirectoryObj; x \<in> set (retype_addrs ptr (ArchObject PageDirectoryObj) n us); ((\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and pspace_aligned and valid_arch_state) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_arch_state and pspace_aligned and K (is_aligned x pd_bits)) s \<and> pspace_aligned s \<and> valid_arch_state s
 2. \<And>us sz. \<lbrakk>orefs = retype_addrs ptr type n us; range_cover ptr sz (obj_bits_api type us) n; type \<noteq> ArchObject PageDirectoryObj\<rbrakk> \<Longrightarrow> \<lbrace>?R13 us sz\<rbrace> return () \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace>
 3. \<And>us sz s. \<lbrakk>orefs = retype_addrs ptr type n us; range_cover ptr sz (obj_bits_api type us) n; ((\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and pspace_aligned and valid_arch_state) s\<rbrakk> \<Longrightarrow> (type = ArchObject PageDirectoryObj \<longrightarrow> ((\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and pspace_aligned and valid_arch_state) s) \<and> (type \<noteq> ArchObject PageDirectoryObj \<longrightarrow> ?R13 us sz s) proof (prove)
goal (3 subgoals):
 1. \<And>us sz x s. \<lbrakk>orefs = retype_addrs ptr (ArchObject PageDirectoryObj) n us; range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) us) n; type = ArchObject PageDirectoryObj; x \<in> set (retype_addrs ptr (ArchObject PageDirectoryObj) n us); \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pspace_aligned s; valid_arch_state s\<rbrakk> \<Longrightarrow> is_aligned x pd_bits
 2. \<And>us sz. \<lbrakk>orefs = retype_addrs ptr type n us; range_cover ptr sz (obj_bits_api type us) n; type \<noteq> ArchObject PageDirectoryObj\<rbrakk> \<Longrightarrow> \<lbrace>?R13 us sz\<rbrace> return () \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace>
 3. \<And>us sz s. \<lbrakk>orefs = retype_addrs ptr type n us; range_cover ptr sz (obj_bits_api type us) n; ((\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and pspace_aligned and valid_arch_state) s\<rbrakk> \<Longrightarrow> (type = ArchObject PageDirectoryObj \<longrightarrow> ((\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and pspace_aligned and valid_arch_state) s) \<and> (type \<noteq> ArchObject PageDirectoryObj \<longrightarrow> ?R13 us sz s) proof (prove)
goal (6 subgoals):
 1. \<And>us sz x s. \<lbrakk>orefs = retype_addrs ptr (ArchObject PageDirectoryObj) n us; range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) us) n; type = ArchObject PageDirectoryObj; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pspace_aligned s; valid_arch_state s\<rbrakk> \<Longrightarrow> is_aligned ptr (obj_bits_api (ArchObject PageDirectoryObj) us)
 2. \<And>us sz x s. \<lbrakk>orefs = retype_addrs ptr (ArchObject PageDirectoryObj) n us; range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) us) n; type = ArchObject PageDirectoryObj; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pspace_aligned s; valid_arch_state s\<rbrakk> \<Longrightarrow> sz < word_bits
 3. \<And>us sz x s. \<lbrakk>orefs = retype_addrs ptr (ArchObject PageDirectoryObj) n us; range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) us) n; type = ArchObject PageDirectoryObj; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pspace_aligned s; valid_arch_state s\<rbrakk> \<Longrightarrow> obj_bits_api (ArchObject PageDirectoryObj) us \<le> sz
 4. \<And>us sz x s. \<lbrakk>orefs = retype_addrs ptr (ArchObject PageDirectoryObj) n us; range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) us) n; type = ArchObject PageDirectoryObj; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pspace_aligned s; valid_arch_state s; is_aligned x (obj_bits_api (ArchObject PageDirectoryObj) us)\<rbrakk> \<Longrightarrow> is_aligned x pd_bits
 5. \<And>us sz. \<lbrakk>orefs = retype_addrs ptr type n us; range_cover ptr sz (obj_bits_api type us) n; type \<noteq> ArchObject PageDirectoryObj\<rbrakk> \<Longrightarrow> \<lbrace>?R13 us sz\<rbrace> return () \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace>
 6. \<And>us sz s. \<lbrakk>orefs = retype_addrs ptr type n us; range_cover ptr sz (obj_bits_api type us) n; ((\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and pspace_aligned and valid_arch_state) s\<rbrakk> \<Longrightarrow> (type = ArchObject PageDirectoryObj \<longrightarrow> ((\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and pspace_aligned and valid_arch_state) s) \<and> (type \<noteq> ArchObject PageDirectoryObj \<longrightarrow> ?R13 us sz s) proof (prove)
goal (5 subgoals):
 1. \<And>us sz x s. \<lbrakk>orefs = retype_addrs ptr (ArchObject PageDirectoryObj) n us; range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) us) n; type = ArchObject PageDirectoryObj; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pspace_aligned s; valid_arch_state s\<rbrakk> \<Longrightarrow> sz < word_bits
 2. \<And>us sz x s. \<lbrakk>orefs = retype_addrs ptr (ArchObject PageDirectoryObj) n us; range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) us) n; type = ArchObject PageDirectoryObj; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pspace_aligned s; valid_arch_state s\<rbrakk> \<Longrightarrow> obj_bits_api (ArchObject PageDirectoryObj) us \<le> sz
 3. \<And>us sz x s. \<lbrakk>orefs = retype_addrs ptr (ArchObject PageDirectoryObj) n us; range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) us) n; type = ArchObject PageDirectoryObj; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pspace_aligned s; valid_arch_state s; is_aligned x (obj_bits_api (ArchObject PageDirectoryObj) us)\<rbrakk> \<Longrightarrow> is_aligned x pd_bits
 4. \<And>us sz. \<lbrakk>orefs = retype_addrs ptr type n us; range_cover ptr sz (obj_bits_api type us) n; type \<noteq> ArchObject PageDirectoryObj\<rbrakk> \<Longrightarrow> \<lbrace>?R13 us sz\<rbrace> return () \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace>
 5. \<And>us sz s. \<lbrakk>orefs = retype_addrs ptr type n us; range_cover ptr sz (obj_bits_api type us) n; ((\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and pspace_aligned and valid_arch_state) s\<rbrakk> \<Longrightarrow> (type = ArchObject PageDirectoryObj \<longrightarrow> ((\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and pspace_aligned and valid_arch_state) s) \<and> (type \<noteq> ArchObject PageDirectoryObj \<longrightarrow> ?R13 us sz s) proof (prove)
goal (4 subgoals):
 1. \<And>us sz x s. \<lbrakk>orefs = retype_addrs ptr (ArchObject PageDirectoryObj) n us; range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) us) n; type = ArchObject PageDirectoryObj; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pspace_aligned s; valid_arch_state s\<rbrakk> \<Longrightarrow> obj_bits_api (ArchObject PageDirectoryObj) us \<le> sz
 2. \<And>us sz x s. \<lbrakk>orefs = retype_addrs ptr (ArchObject PageDirectoryObj) n us; range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) us) n; type = ArchObject PageDirectoryObj; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pspace_aligned s; valid_arch_state s; is_aligned x (obj_bits_api (ArchObject PageDirectoryObj) us)\<rbrakk> \<Longrightarrow> is_aligned x pd_bits
 3. \<And>us sz. \<lbrakk>orefs = retype_addrs ptr type n us; range_cover ptr sz (obj_bits_api type us) n; type \<noteq> ArchObject PageDirectoryObj\<rbrakk> \<Longrightarrow> \<lbrace>?R13 us sz\<rbrace> return () \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace>
 4. \<And>us sz s. \<lbrakk>orefs = retype_addrs ptr type n us; range_cover ptr sz (obj_bits_api type us) n; ((\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and pspace_aligned and valid_arch_state) s\<rbrakk> \<Longrightarrow> (type = ArchObject PageDirectoryObj \<longrightarrow> ((\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and pspace_aligned and valid_arch_state) s) \<and> (type \<noteq> ArchObject PageDirectoryObj \<longrightarrow> ?R13 us sz s) proof (prove)
goal (3 subgoals):
 1. \<And>us sz x s. \<lbrakk>orefs = retype_addrs ptr (ArchObject PageDirectoryObj) n us; range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) us) n; type = ArchObject PageDirectoryObj; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pspace_aligned s; valid_arch_state s; is_aligned x (obj_bits_api (ArchObject PageDirectoryObj) us)\<rbrakk> \<Longrightarrow> is_aligned x pd_bits
 2. \<And>us sz. \<lbrakk>orefs = retype_addrs ptr type n us; range_cover ptr sz (obj_bits_api type us) n; type \<noteq> ArchObject PageDirectoryObj\<rbrakk> \<Longrightarrow> \<lbrace>?R13 us sz\<rbrace> return () \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace>
 3. \<And>us sz s. \<lbrakk>orefs = retype_addrs ptr type n us; range_cover ptr sz (obj_bits_api type us) n; ((\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and pspace_aligned and valid_arch_state) s\<rbrakk> \<Longrightarrow> (type = ArchObject PageDirectoryObj \<longrightarrow> ((\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and pspace_aligned and valid_arch_state) s) \<and> (type \<noteq> ArchObject PageDirectoryObj \<longrightarrow> ?R13 us sz s) proof (prove)
goal (2 subgoals):
 1. \<And>us sz. \<lbrakk>orefs = retype_addrs ptr type n us; type \<noteq> ArchObject PageDirectoryObj; is_aligned ptr (case type of Untyped \<Rightarrow> us | TCBObject \<Rightarrow> obj_bits (TCB default_tcb) | EndpointObject \<Rightarrow> obj_bits (Endpoint undefined) | NotificationObject \<Rightarrow> obj_bits (Notification undefined) | CapTableObject \<Rightarrow> us + slot_bits | ArchObject aobj \<Rightarrow> obj_bits $ ArchObj $ default_arch_object aobj False us); sz < 32; (case type of Untyped \<Rightarrow> us | TCBObject \<Rightarrow> obj_bits (TCB default_tcb) | EndpointObject \<Rightarrow> obj_bits (Endpoint undefined) | NotificationObject \<Rightarrow> obj_bits (Notification undefined) | CapTableObject \<Rightarrow> us + slot_bits | ArchObject aobj \<Rightarrow> obj_bits $ ArchObj $ default_arch_object aobj False us) \<le> sz; n + unat (ptr && mask sz >> (case type of Untyped \<Rightarrow> us | TCBObject \<Rightarrow> obj_bits (TCB default_tcb) | EndpointObject \<Rightarrow> obj_bits (Endpoint undefined) | NotificationObject \<Rightarrow> obj_bits (Notification undefined) | CapTableObject \<Rightarrow> us + slot_bits | ArchObject aobj \<Rightarrow> obj_bits $ ArchObj $ default_arch_object aobj False us)) \<le> 2 ^ (sz - (case type of Untyped \<Rightarrow> us | TCBObject \<Rightarrow> obj_bits (TCB default_tcb) | EndpointObject \<Rightarrow> obj_bits (Endpoint undefined) | NotificationObject \<Rightarrow> obj_bits (Notification undefined) | CapTableObject \<Rightarrow> us + slot_bits | ArchObject aobj \<Rightarrow> obj_bits $ ArchObj $ default_arch_object aobj False us))\<rbrakk> \<Longrightarrow> \<lbrace>?R13 us sz\<rbrace> return () \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace>
 2. \<And>us sz s. \<lbrakk>orefs = retype_addrs ptr type n us; range_cover ptr sz (obj_bits_api type us) n; ((\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and pspace_aligned and valid_arch_state) s\<rbrakk> \<Longrightarrow> (type = ArchObject PageDirectoryObj \<longrightarrow> ((\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and pspace_aligned and valid_arch_state) s) \<and> (type \<noteq> ArchObject PageDirectoryObj \<longrightarrow> ?R13 us sz s) proof (prove)
goal (1 subgoal):
 1. \<And>us sz s. \<lbrakk>orefs = retype_addrs ptr type n us; range_cover ptr sz (obj_bits_api type us) n; ((\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and pspace_aligned and valid_arch_state) s\<rbrakk> \<Longrightarrow> (type = ArchObject PageDirectoryObj \<longrightarrow> ((\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and pspace_aligned and valid_arch_state) s) \<and> (type \<noteq> ArchObject PageDirectoryObj \<longrightarrow> (\<forall>x\<in>ran (kheap s). obj_valid_pdpt x)) proof (prove)
goal:
No subgoals!