theory ArchRetype_AC

lemma init_arch_objects_pas_refined[Retype_AC_assms]:
  "\<lbrace>pas_refined aag and post_retype_invs tp refs and (\<lambda>s. \<forall> x\<in>set refs. x \<notin> global_refs s)
                    and K (\<forall>ref \<in> set refs. is_aligned ref (obj_bits_api tp obj_sz))\<rbrace>
   init_arch_objects tp ptr bits obj_sz refs
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" apply (rule hoare_gen_asm) apply (cases tp) apply (simp_all add: init_arch_objects_def) apply (wp | simp)+ apply (rename_tac aobject_type) apply (case_tac aobject_type, simp_all) apply ((simp | wp)+)[5] apply wp apply (rule_tac Q="\<lambda>rv. pas_refined aag and
                            all_invs_but_equal_kernel_mappings_restricted (set refs) and
                            (\<lambda>s. \<forall>x \<in> set refs. x \<notin> global_refs s)" in hoare_strengthen_post) apply (wp mapM_x_wp[OF _ subset_refl]) apply ((wp copy_global_mappings_pas_refined copy_global_invs_mappings_restricted'
                copy_global_mappings_global_refs_inv copy_global_invs_mappings_restricted'
             | fastforce simp: obj_bits_api_def default_arch_object_def pd_bits_def pageBits_def)+)[2] apply (wp dmo_invs hoare_vcg_const_Ball_lift valid_irq_node_typ
         | fastforce simp: post_retype_invs_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and post_retype_invs tp refs and (\<lambda>s. \<forall>x\<in>set refs. x \<notin> global_refs s) and K (\<forall>ref\<in>set refs. is_aligned ref (obj_bits_api tp obj_sz))\<rbrace> init_arch_objects tp ptr bits obj_sz refs \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<forall>ref\<in>set refs. is_aligned ref (obj_bits_api tp obj_sz) \<Longrightarrow> \<lbrace>pas_refined aag and post_retype_invs tp refs and (\<lambda>s. \<forall>x\<in>set refs. x \<notin> global_refs s)\<rbrace> init_arch_objects tp ptr bits obj_sz refs \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<lbrakk>\<forall>ref\<in>set refs. is_aligned ref (obj_bits_api tp obj_sz); tp = Untyped\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and post_retype_invs tp refs and (\<lambda>s. \<forall>x\<in>set refs. x \<notin> global_refs s)\<rbrace> init_arch_objects tp ptr bits obj_sz refs \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 2. \<lbrakk>\<forall>ref\<in>set refs. is_aligned ref (obj_bits_api tp obj_sz); tp = TCBObject\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and post_retype_invs tp refs and (\<lambda>s. \<forall>x\<in>set refs. x \<notin> global_refs s)\<rbrace> init_arch_objects tp ptr bits obj_sz refs \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 3. \<lbrakk>\<forall>ref\<in>set refs. is_aligned ref (obj_bits_api tp obj_sz); tp = EndpointObject\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and post_retype_invs tp refs and (\<lambda>s. \<forall>x\<in>set refs. x \<notin> global_refs s)\<rbrace> init_arch_objects tp ptr bits obj_sz refs \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 4. \<lbrakk>\<forall>ref\<in>set refs. is_aligned ref (obj_bits_api tp obj_sz); tp = NotificationObject\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and post_retype_invs tp refs and (\<lambda>s. \<forall>x\<in>set refs. x \<notin> global_refs s)\<rbrace> init_arch_objects tp ptr bits obj_sz refs \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 5. \<lbrakk>\<forall>ref\<in>set refs. is_aligned ref (obj_bits_api tp obj_sz); tp = CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and post_retype_invs tp refs and (\<lambda>s. \<forall>x\<in>set refs. x \<notin> global_refs s)\<rbrace> init_arch_objects tp ptr bits obj_sz refs \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 6. \<And>x6. \<lbrakk>\<forall>ref\<in>set refs. is_aligned ref (obj_bits_api tp obj_sz); tp = ArchObject x6\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and post_retype_invs tp refs and (\<lambda>s. \<forall>x\<in>set refs. x \<notin> global_refs s)\<rbrace> init_arch_objects tp ptr bits obj_sz refs \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<lbrakk>\<forall>ref\<in>set refs. is_aligned ref (obj_bits_api Untyped obj_sz); tp = Untyped\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and post_retype_invs Untyped refs and (\<lambda>s. \<forall>x\<in>set refs. x \<notin> global_refs s)\<rbrace> return () \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 2. \<lbrakk>\<forall>ref\<in>set refs. is_aligned ref (obj_bits_api TCBObject obj_sz); tp = TCBObject\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and post_retype_invs TCBObject refs and (\<lambda>s. \<forall>x\<in>set refs. x \<notin> global_refs s)\<rbrace> return () \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 3. \<lbrakk>\<forall>ref\<in>set refs. is_aligned ref (obj_bits_api EndpointObject obj_sz); tp = EndpointObject\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and post_retype_invs EndpointObject refs and (\<lambda>s. \<forall>x\<in>set refs. x \<notin> global_refs s)\<rbrace> return () \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 4. \<lbrakk>\<forall>ref\<in>set refs. is_aligned ref (obj_bits_api NotificationObject obj_sz); tp = NotificationObject\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and post_retype_invs NotificationObject refs and (\<lambda>s. \<forall>x\<in>set refs. x \<notin> global_refs s)\<rbrace> return () \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 5. \<lbrakk>\<forall>ref\<in>set refs. is_aligned ref (obj_bits_api CapTableObject obj_sz); tp = CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and post_retype_invs CapTableObject refs and (\<lambda>s. \<forall>x\<in>set refs. x \<notin> global_refs s)\<rbrace> return () \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 6. \<And>x6. \<lbrakk>\<forall>ref\<in>set refs. is_aligned ref (obj_bits_api (ArchObject x6) obj_sz); tp = ArchObject x6\<rbrakk> \<Longrightarrow> (x6 = PageDirectoryObj \<longrightarrow> \<lbrace>pas_refined aag and post_retype_invs (ArchObject PageDirectoryObj) refs and (\<lambda>s. \<forall>x\<in>set refs. x \<notin> global_refs s)\<rbrace> do y <- mapM_x copy_global_mappings refs;
do_machine_op (mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + 2 ^ pd_bits - 1) (addrFromPPtr x)) refs)
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace>) \<and> (x6 \<noteq> PageDirectoryObj \<longrightarrow> \<lbrace>pas_refined aag and post_retype_invs (ArchObject x6) refs and (\<lambda>s. \<forall>x\<in>set refs. x \<notin> global_refs s)\<rbrace> return () \<lbrace>\<lambda>_. pas_refined aag\<rbrace>) proof (prove)
goal (1 subgoal):
 1. \<And>x6. \<lbrakk>\<forall>ref\<in>set refs. is_aligned ref (obj_bits_api (ArchObject x6) obj_sz); tp = ArchObject x6\<rbrakk> \<Longrightarrow> (x6 = PageDirectoryObj \<longrightarrow> \<lbrace>pas_refined aag and post_retype_invs (ArchObject PageDirectoryObj) refs and (\<lambda>s. \<forall>x\<in>set refs. x \<notin> global_refs s)\<rbrace> do y <- mapM_x copy_global_mappings refs;
do_machine_op (mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + 2 ^ pd_bits - 1) (addrFromPPtr x)) refs)
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace>) \<and> (x6 \<noteq> PageDirectoryObj \<longrightarrow> \<lbrace>pas_refined aag and post_retype_invs (ArchObject x6) refs and (\<lambda>s. \<forall>x\<in>set refs. x \<notin> global_refs s)\<rbrace> return () \<lbrace>\<lambda>_. pas_refined aag\<rbrace>) proof (prove)
goal (1 subgoal):
 1. \<And>aobject_type. \<lbrakk>\<forall>ref\<in>set refs. is_aligned ref (obj_bits_api (ArchObject aobject_type) obj_sz); tp = ArchObject aobject_type\<rbrakk> \<Longrightarrow> (aobject_type = PageDirectoryObj \<longrightarrow> \<lbrace>pas_refined aag and post_retype_invs (ArchObject PageDirectoryObj) refs and (\<lambda>s. \<forall>x\<in>set refs. x \<notin> global_refs s)\<rbrace> do y <- mapM_x copy_global_mappings refs;
do_machine_op (mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + 2 ^ pd_bits - 1) (addrFromPPtr x)) refs)
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace>) \<and> (aobject_type \<noteq> PageDirectoryObj \<longrightarrow> \<lbrace>pas_refined aag and post_retype_invs (ArchObject aobject_type) refs and (\<lambda>s. \<forall>x\<in>set refs. x \<notin> global_refs s)\<rbrace> return () \<lbrace>\<lambda>_. pas_refined aag\<rbrace>) proof (prove)
goal (7 subgoals):
 1. \<And>aobject_type. \<lbrakk>\<forall>ref\<in>set refs. is_aligned ref (obj_bits_api (ArchObject SmallPageObj) obj_sz); tp = ArchObject SmallPageObj; aobject_type = SmallPageObj\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and post_retype_invs (ArchObject SmallPageObj) refs and (\<lambda>s. \<forall>x\<in>set refs. x \<notin> global_refs s)\<rbrace> return () \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 2. \<And>aobject_type. \<lbrakk>\<forall>ref\<in>set refs. is_aligned ref (obj_bits_api (ArchObject LargePageObj) obj_sz); tp = ArchObject LargePageObj; aobject_type = LargePageObj\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and post_retype_invs (ArchObject LargePageObj) refs and (\<lambda>s. \<forall>x\<in>set refs. x \<notin> global_refs s)\<rbrace> return () \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 3. \<And>aobject_type. \<lbrakk>\<forall>ref\<in>set refs. is_aligned ref (obj_bits_api (ArchObject SectionObj) obj_sz); tp = ArchObject SectionObj; aobject_type = SectionObj\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and post_retype_invs (ArchObject SectionObj) refs and (\<lambda>s. \<forall>x\<in>set refs. x \<notin> global_refs s)\<rbrace> return () \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 4. \<And>aobject_type. \<lbrakk>\<forall>ref\<in>set refs. is_aligned ref (obj_bits_api (ArchObject SuperSectionObj) obj_sz); tp = ArchObject SuperSectionObj; aobject_type = SuperSectionObj\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and post_retype_invs (ArchObject SuperSectionObj) refs and (\<lambda>s. \<forall>x\<in>set refs. x \<notin> global_refs s)\<rbrace> return () \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 5. \<And>aobject_type. \<lbrakk>\<forall>ref\<in>set refs. is_aligned ref (obj_bits_api (ArchObject PageTableObj) obj_sz); tp = ArchObject PageTableObj; aobject_type = PageTableObj\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and post_retype_invs (ArchObject PageTableObj) refs and (\<lambda>s. \<forall>x\<in>set refs. x \<notin> global_refs s)\<rbrace> return () \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 6. \<And>aobject_type. \<lbrakk>\<forall>ref\<in>set refs. is_aligned ref (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); tp = ArchObject PageDirectoryObj; aobject_type = PageDirectoryObj\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and post_retype_invs (ArchObject PageDirectoryObj) refs and (\<lambda>s. \<forall>x\<in>set refs. x \<notin> global_refs s)\<rbrace> do y <- mapM_x copy_global_mappings refs;
do_machine_op (mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + 2 ^ pd_bits - 1) (addrFromPPtr x)) refs)
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 7. \<And>aobject_type. \<lbrakk>\<forall>ref\<in>set refs. is_aligned ref (obj_bits_api (ArchObject ASIDPoolObj) obj_sz); tp = ArchObject ASIDPoolObj; aobject_type = ASIDPoolObj\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and post_retype_invs (ArchObject ASIDPoolObj) refs and (\<lambda>s. \<forall>x\<in>set refs. x \<notin> global_refs s)\<rbrace> return () \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>aobject_type. \<lbrakk>\<forall>ref\<in>set refs. is_aligned ref (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); tp = ArchObject PageDirectoryObj; aobject_type = PageDirectoryObj\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and post_retype_invs (ArchObject PageDirectoryObj) refs and (\<lambda>s. \<forall>x\<in>set refs. x \<notin> global_refs s)\<rbrace> do y <- mapM_x copy_global_mappings refs;
do_machine_op (mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + 2 ^ pd_bits - 1) (addrFromPPtr x)) refs)
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 2. \<And>aobject_type. \<lbrakk>\<forall>ref\<in>set refs. is_aligned ref (obj_bits_api (ArchObject ASIDPoolObj) obj_sz); tp = ArchObject ASIDPoolObj; aobject_type = ASIDPoolObj\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and post_retype_invs (ArchObject ASIDPoolObj) refs and (\<lambda>s. \<forall>x\<in>set refs. x \<notin> global_refs s)\<rbrace> return () \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>aobject_type. \<lbrakk>\<forall>ref\<in>set refs. is_aligned ref (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); tp = ArchObject PageDirectoryObj; aobject_type = PageDirectoryObj\<rbrakk> \<Longrightarrow> \<lbrace>?Q53 aobject_type\<rbrace> mapM_x copy_global_mappings refs \<lbrace>\<lambda>y. pas_refined aag\<rbrace>
 2. \<And>aobject_type s. \<lbrakk>\<forall>ref\<in>set refs. is_aligned ref (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); tp = ArchObject PageDirectoryObj; aobject_type = PageDirectoryObj; (pas_refined aag and post_retype_invs (ArchObject PageDirectoryObj) refs and (\<lambda>s. \<forall>x\<in>set refs. x \<notin> global_refs s)) s\<rbrakk> \<Longrightarrow> ?Q53 aobject_type s
 3. \<And>aobject_type. \<lbrakk>\<forall>ref\<in>set refs. is_aligned ref (obj_bits_api (ArchObject ASIDPoolObj) obj_sz); tp = ArchObject ASIDPoolObj; aobject_type = ASIDPoolObj\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and post_retype_invs (ArchObject ASIDPoolObj) refs and (\<lambda>s. \<forall>x\<in>set refs. x \<notin> global_refs s)\<rbrace> return () \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>aobject_type. \<lbrakk>\<forall>ref\<in>set refs. is_aligned ref (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); tp = ArchObject PageDirectoryObj; aobject_type = PageDirectoryObj\<rbrakk> \<Longrightarrow> \<lbrace>?Q53 aobject_type\<rbrace> mapM_x copy_global_mappings refs \<lbrace>\<lambda>rv. pas_refined aag and ((\<lambda>s. equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- set refs)\<rparr>)) and valid_pspace and valid_mdb and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_vspace_objs and valid_irq_states and valid_global_objs and valid_arch_caps and valid_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb and valid_ioc and valid_machine_state and valid_ioports) and (\<lambda>s. \<forall>x\<in>set refs. x \<notin> global_refs s)\<rbrace>
 2. \<And>aobject_type rv s. \<lbrakk>\<forall>ref\<in>set refs. is_aligned ref (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); tp = ArchObject PageDirectoryObj; aobject_type = PageDirectoryObj; (pas_refined aag and ((\<lambda>s. equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- set refs)\<rparr>)) and valid_pspace and valid_mdb and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_vspace_objs and valid_irq_states and valid_global_objs and valid_arch_caps and valid_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb and valid_ioc and valid_machine_state and valid_ioports) and (\<lambda>s. \<forall>x\<in>set refs. x \<notin> global_refs s)) s\<rbrakk> \<Longrightarrow> pas_refined aag s
 3. \<And>aobject_type s. \<lbrakk>\<forall>ref\<in>set refs. is_aligned ref (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); tp = ArchObject PageDirectoryObj; aobject_type = PageDirectoryObj; (pas_refined aag and post_retype_invs (ArchObject PageDirectoryObj) refs and (\<lambda>s. \<forall>x\<in>set refs. x \<notin> global_refs s)) s\<rbrakk> \<Longrightarrow> ?Q53 aobject_type s
 4. \<And>aobject_type. \<lbrakk>\<forall>ref\<in>set refs. is_aligned ref (obj_bits_api (ArchObject ASIDPoolObj) obj_sz); tp = ArchObject ASIDPoolObj; aobject_type = ASIDPoolObj\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and post_retype_invs (ArchObject ASIDPoolObj) refs and (\<lambda>s. \<forall>x\<in>set refs. x \<notin> global_refs s)\<rbrace> return () \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>aobject_type x. \<lbrakk>\<forall>ref\<in>set refs. is_aligned ref (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); tp = ArchObject PageDirectoryObj; aobject_type = PageDirectoryObj; x \<in> set refs\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and ((\<lambda>s. equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- set refs)\<rparr>)) and valid_pspace and valid_mdb and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_vspace_objs and valid_irq_states and valid_global_objs and valid_arch_caps and valid_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb and valid_ioc and valid_machine_state and valid_ioports) and (\<lambda>s. \<forall>x\<in>set refs. x \<notin> global_refs s)\<rbrace> copy_global_mappings x \<lbrace>\<lambda>rv s. pas_refined aag s \<and> ((\<lambda>s. equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- set refs)\<rparr>)) and valid_pspace and valid_mdb and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_vspace_objs and valid_irq_states and valid_global_objs and valid_arch_caps and valid_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb and valid_ioc and valid_machine_state and valid_ioports) s \<and> (\<forall>x\<in>set refs. x \<notin> global_refs s)\<rbrace>
 2. \<And>aobject_type rv s. \<lbrakk>\<forall>ref\<in>set refs. is_aligned ref (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); tp = ArchObject PageDirectoryObj; aobject_type = PageDirectoryObj; (pas_refined aag and ((\<lambda>s. equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- set refs)\<rparr>)) and valid_pspace and valid_mdb and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_vspace_objs and valid_irq_states and valid_global_objs and valid_arch_caps and valid_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb and valid_ioc and valid_machine_state and valid_ioports) and (\<lambda>s. \<forall>x\<in>set refs. x \<notin> global_refs s)) s\<rbrakk> \<Longrightarrow> pas_refined aag s
 3. \<And>aobject_type s. \<lbrakk>\<forall>ref\<in>set refs. is_aligned ref (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); tp = ArchObject PageDirectoryObj; aobject_type = PageDirectoryObj; (pas_refined aag and post_retype_invs (ArchObject PageDirectoryObj) refs and (\<lambda>s. \<forall>x\<in>set refs. x \<notin> global_refs s)) s\<rbrakk> \<Longrightarrow> (pas_refined aag and ((\<lambda>s. equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- set refs)\<rparr>)) and valid_pspace and valid_mdb and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_vspace_objs and valid_irq_states and valid_global_objs and valid_arch_caps and valid_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb and valid_ioc and valid_machine_state and valid_ioports) and (\<lambda>s. \<forall>x\<in>set refs. x \<notin> global_refs s)) s
 4. \<And>aobject_type. \<lbrakk>\<forall>ref\<in>set refs. is_aligned ref (obj_bits_api (ArchObject ASIDPoolObj) obj_sz); tp = ArchObject ASIDPoolObj; aobject_type = ASIDPoolObj\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and post_retype_invs (ArchObject ASIDPoolObj) refs and (\<lambda>s. \<forall>x\<in>set refs. x \<notin> global_refs s)\<rbrace> return () \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>aobject_type s. \<lbrakk>\<forall>ref\<in>set refs. is_aligned ref (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); tp = ArchObject PageDirectoryObj; aobject_type = PageDirectoryObj; (pas_refined aag and post_retype_invs (ArchObject PageDirectoryObj) refs and (\<lambda>s. \<forall>x\<in>set refs. x \<notin> global_refs s)) s\<rbrakk> \<Longrightarrow> (pas_refined aag and ((\<lambda>s. equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- set refs)\<rparr>)) and valid_pspace and valid_mdb and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_vspace_objs and valid_irq_states and valid_global_objs and valid_arch_caps and valid_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb and valid_ioc and valid_machine_state and valid_ioports) and (\<lambda>s. \<forall>x\<in>set refs. x \<notin> global_refs s)) s
 2. \<And>aobject_type. \<lbrakk>\<forall>ref\<in>set refs. is_aligned ref (obj_bits_api (ArchObject ASIDPoolObj) obj_sz); tp = ArchObject ASIDPoolObj; aobject_type = ASIDPoolObj\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and post_retype_invs (ArchObject ASIDPoolObj) refs and (\<lambda>s. \<forall>x\<in>set refs. x \<notin> global_refs s)\<rbrace> return () \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal:
No subgoals!