theory ArchUntyped_AI

lemma init_arch_objects_nonempty_table[Untyped_AI_assms, wp]:
  "\<lbrace>(\<lambda>s. \<not> (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s)
         \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s) and
    K (\<forall>ref\<in>set refs. is_aligned ref (obj_bits_api tp us))\<rbrace>
        init_arch_objects tp ptr bits us refs
   \<lbrace>\<lambda>rv s. \<not> (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s)\<rbrace>" apply (rule hoare_gen_asm) apply (simp add: init_arch_objects_def split del: if_split) apply (rule hoare_pre) apply (wp unless_wp | wpc | simp add: reserve_region_def second_level_tables_def)+ apply (clarsimp simp: obj_bits_api_def default_arch_object_def pd_bits_def pageBits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s) and K (\<forall>ref\<in>set refs. is_aligned ref (obj_bits_api tp us))\<rbrace> init_arch_objects tp ptr bits us refs \<lbrace>\<lambda>rv s. \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<forall>ref\<in>set refs. is_aligned ref (obj_bits_api tp us) \<Longrightarrow> \<lbrace>\<lambda>s. \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s\<rbrace> init_arch_objects tp ptr bits us refs \<lbrace>\<lambda>rv s. \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<forall>ref\<in>set refs. is_aligned ref (obj_bits_api tp us) \<Longrightarrow> \<lbrace>\<lambda>s. \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s\<rbrace> if tp = 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>rv s. \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<forall>ref\<in>set refs. is_aligned ref (obj_bits_api tp us) \<Longrightarrow> \<lbrace>?Q2\<rbrace> if tp = 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>rv s. \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s\<rbrace>
 2. \<And>s. \<lbrakk>\<forall>ref\<in>set refs. is_aligned ref (obj_bits_api tp us); \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>ref\<in>set refs. is_aligned ref (obj_bits_api tp us); \<not> obj_at (nonempty_table (set (arm_global_pts (arch_state s)))) r s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s\<rbrakk> \<Longrightarrow> tp = ArchObject PageDirectoryObj \<longrightarrow> (\<forall>pd\<in>set refs. is_aligned pd pd_bits) proof (prove)
goal:
No subgoals!