theory ArchRetype_IF

lemma init_arch_objects_globals_equiv:
  "\<lbrace>globals_equiv s and (\<lambda>s. arm_global_pd (arch_state s) \<notin> set refs \<and>
                             pspace_aligned s \<and> valid_arch_state s)
                    and K (\<forall>x\<in>set refs. is_aligned x (obj_bits_api new_type obj_sz))\<rbrace>
   init_arch_objects new_type ptr num_objects obj_sz refs
   \<lbrace>\<lambda>_. globals_equiv s\<rbrace>" unfolding init_arch_objects_def fun_app_def apply (rule hoare_gen_asm)+ apply (subst do_machine_op_mapM_x[OF empty_fail_cleanCacheRange_PoU])+ apply (rule hoare_pre) apply (wpc | wp mapM_x_wp[OF dmo_cleanCacheRange_PoU_globals_equiv subset_refl])+ apply (rule_tac Q="\<lambda>_. globals_equiv s and (\<lambda> s. arm_global_pd (arch_state s) \<notin> set refs)"
                 in hoare_strengthen_post) apply (wp mapM_x_wp[OF _ subset_refl] copy_global_mappings_globals_equiv
              dmo_cleanCacheRange_PoU_globals_equiv
            | simp add: obj_bits_api_def default_arch_object_def pd_bits_def pageBits_def
            | blast)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and (\<lambda>s. arm_global_pd (arch_state s) \<notin> set refs \<and> pspace_aligned s \<and> valid_arch_state s) and K (\<forall>x\<in>set refs. is_aligned x (obj_bits_api new_type obj_sz))\<rbrace> init_arch_objects new_type ptr num_objects obj_sz refs \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and (\<lambda>s. arm_global_pd (arch_state s) \<notin> set refs \<and> pspace_aligned s \<and> valid_arch_state s) and K (\<forall>x\<in>set refs. is_aligned x (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>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>set refs. is_aligned x (obj_bits_api new_type obj_sz) \<Longrightarrow> \<lbrace>globals_equiv s and (\<lambda>s. arm_global_pd (arch_state s) \<notin> set refs \<and> pspace_aligned s \<and> valid_arch_state s)\<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>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>set refs. is_aligned x (obj_bits_api new_type obj_sz) \<Longrightarrow> \<lbrace>globals_equiv s and (\<lambda>s. arm_global_pd (arch_state s) \<notin> set refs \<and> pspace_aligned s \<and> valid_arch_state s)\<rbrace> if new_type = ArchObject PageDirectoryObj then do mapM_x copy_global_mappings refs;
mapM_x (\<lambda>x. do_machine_op (cleanCacheRange_PoU x (x + (1 << pd_bits) - 1) (addrFromPPtr x))) refs
od else return () \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<forall>x\<in>set refs. is_aligned x (obj_bits_api new_type obj_sz) \<Longrightarrow> \<lbrace>?Q2\<rbrace> if new_type = ArchObject PageDirectoryObj then do mapM_x copy_global_mappings refs;
mapM_x (\<lambda>x. do_machine_op (cleanCacheRange_PoU x (x + (1 << pd_bits) - 1) (addrFromPPtr x))) refs
od else return () \<lbrace>\<lambda>_. globals_equiv s\<rbrace>
 2. \<And>sa. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api new_type obj_sz); (globals_equiv s and (\<lambda>s. arm_global_pd (arch_state s) \<notin> set refs \<and> pspace_aligned s \<and> valid_arch_state s)) sa\<rbrakk> \<Longrightarrow> ?Q2 sa proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api new_type obj_sz); new_type = ArchObject PageDirectoryObj\<rbrakk> \<Longrightarrow> \<lbrace>?Q6\<rbrace> mapM_x copy_global_mappings refs \<lbrace>\<lambda>x. globals_equiv s\<rbrace>
 2. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api new_type obj_sz); new_type \<noteq> ArchObject PageDirectoryObj\<rbrakk> \<Longrightarrow> \<lbrace>?R6\<rbrace> return () \<lbrace>\<lambda>_. globals_equiv s\<rbrace>
 3. \<And>sa. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api new_type obj_sz); (globals_equiv s and (\<lambda>s. arm_global_pd (arch_state s) \<notin> set refs \<and> pspace_aligned s \<and> valid_arch_state s)) sa\<rbrakk> \<Longrightarrow> (new_type = ArchObject PageDirectoryObj \<longrightarrow> ?Q6 sa) \<and> (new_type \<noteq> ArchObject PageDirectoryObj \<longrightarrow> ?R6 sa) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api new_type obj_sz); new_type = ArchObject PageDirectoryObj\<rbrakk> \<Longrightarrow> \<lbrace>?Q6\<rbrace> mapM_x copy_global_mappings refs \<lbrace>\<lambda>_. globals_equiv s and (\<lambda>s. arm_global_pd (arch_state s) \<notin> set refs)\<rbrace>
 2. \<And>rv sa. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api new_type obj_sz); new_type = ArchObject PageDirectoryObj; (globals_equiv s and (\<lambda>s. arm_global_pd (arch_state s) \<notin> set refs)) sa\<rbrakk> \<Longrightarrow> globals_equiv s sa
 3. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api new_type obj_sz); new_type \<noteq> ArchObject PageDirectoryObj\<rbrakk> \<Longrightarrow> \<lbrace>?R6\<rbrace> return () \<lbrace>\<lambda>_. globals_equiv s\<rbrace>
 4. \<And>sa. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api new_type obj_sz); (globals_equiv s and (\<lambda>s. arm_global_pd (arch_state s) \<notin> set refs \<and> pspace_aligned s \<and> valid_arch_state s)) sa\<rbrakk> \<Longrightarrow> (new_type = ArchObject PageDirectoryObj \<longrightarrow> ?Q6 sa) \<and> (new_type \<noteq> ArchObject PageDirectoryObj \<longrightarrow> ?R6 sa) proof (prove)
goal:
No subgoals!