theory ArchRetype_AI

lemma init_arch_objects_invs_from_restricted:
  "\<lbrace>post_retype_invs new_type refs
         and (\<lambda>s. global_refs s \<inter> set refs = {})
         and K (\<forall>ref \<in> set refs. is_aligned ref (obj_bits_api new_type obj_sz))\<rbrace>
     init_arch_objects new_type ptr bits obj_sz refs
   \<lbrace>\<lambda>_. invs\<rbrace>" apply (simp add: init_arch_objects_def split del: if_split) apply (rule hoare_pre) apply (wp mapM_copy_global_invs_mappings_restricted
             hoare_vcg_const_Ball_lift
             valid_irq_node_typ
                  | wpc)+ apply (auto simp: post_retype_invs_def default_arch_object_def
                    pd_bits_def pageBits_def obj_bits_api_def
                    global_refs_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>post_retype_invs new_type refs and (\<lambda>s. global_refs s \<inter> set refs = {}) and K (\<forall>ref\<in>set refs. is_aligned ref (obj_bits_api new_type obj_sz))\<rbrace> init_arch_objects new_type ptr bits obj_sz refs \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>post_retype_invs new_type refs and (\<lambda>s. global_refs s \<inter> set refs = {}) and (\<lambda>y. \<forall>ref\<in>set refs. is_aligned ref (obj_bits_api new_type obj_sz))\<rbrace> if new_type = ArchObject PageDirectoryObj then do mapM_x copy_global_mappings refs;
do_machine_op $ mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + (1 << pd_bits) - 1) (addrFromPPtr x)) refs
od else return () \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> if new_type = ArchObject PageDirectoryObj then do mapM_x copy_global_mappings refs;
do_machine_op $ mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + (1 << pd_bits) - 1) (addrFromPPtr x)) refs
od else return () \<lbrace>\<lambda>_. invs\<rbrace>
 2. \<And>s. (post_retype_invs new_type refs and (\<lambda>s. global_refs s \<inter> set refs = {}) and (\<lambda>y. \<forall>ref\<in>set refs. is_aligned ref (obj_bits_api new_type obj_sz))) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (post_retype_invs new_type refs and (\<lambda>s. global_refs s \<inter> set refs = {}) and (\<lambda>y. \<forall>ref\<in>set refs. is_aligned ref (obj_bits_api new_type obj_sz))) s \<Longrightarrow> (new_type = ArchObject PageDirectoryObj \<longrightarrow> ((\<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> set refs \<inter> global_refs s = {} \<and> (\<forall>pd\<in>set refs. is_aligned pd pd_bits)) \<and> (new_type \<noteq> ArchObject PageDirectoryObj \<longrightarrow> invs s) proof (prove)
goal:
No subgoals!