theory ArchRetype_IF

lemma init_arch_objects_reads_respects_g:
  "reads_respects_g aag l ((\<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_subject aag x) and
                           K (\<forall>x\<in>set refs. new_type = ArchObject PageDirectoryObj
                                           \<longrightarrow> is_aligned x pd_bits) and
                           K ((0::obj_ref) < of_nat num_objects))
                    (init_arch_objects new_type ptr num_objects obj_sz refs)" apply (unfold init_arch_objects_def fun_app_def) apply (rule gen_asm_ev)+ apply (subst do_machine_op_mapM_x[OF empty_fail_cleanCacheRange_PoU])+ apply (rule equiv_valid_guard_imp) apply (wp dmo_cleanCacheRange_reads_respects_g mapM_x_ev''
          equiv_valid_guard_imp[OF copy_global_mappings_reads_respects_g]
          copy_global_mappings_valid_arch_state copy_global_mappings_pspace_aligned
          hoare_vcg_ball_lift | wpc | simp)+ apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag ((\<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_subject aag x) and K (\<forall>x\<in>set refs. new_type = ArchObject PageDirectoryObj \<longrightarrow> is_aligned x pd_bits) and K (0 < word_of_nat num_objects)) (init_arch_objects new_type ptr num_objects obj_sz refs) proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag ((\<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_subject aag x) and K (\<forall>x\<in>set refs. new_type = ArchObject PageDirectoryObj \<longrightarrow> is_aligned x pd_bits) and K (0 < word_of_nat num_objects)) (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 ()) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < word_of_nat num_objects; \<forall>x\<in>set refs. new_type = ArchObject PageDirectoryObj \<longrightarrow> is_aligned x pd_bits; \<forall>x\<in>set refs. is_subject aag x\<rbrakk> \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (\<lambda>s. arm_global_pd (arch_state s) \<notin> set refs \<and> pspace_aligned s \<and> valid_arch_state s) (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 ()) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < word_of_nat num_objects; \<forall>x\<in>set refs. new_type = ArchObject PageDirectoryObj \<longrightarrow> is_aligned x pd_bits; \<forall>x\<in>set refs. is_subject aag x\<rbrakk> \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (\<lambda>s. arm_global_pd (arch_state s) \<notin> set refs \<and> pspace_aligned s \<and> valid_arch_state s) (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 ()) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < word_of_nat num_objects; \<forall>x\<in>set refs. new_type = ArchObject PageDirectoryObj \<longrightarrow> is_aligned x pd_bits; \<forall>x\<in>set refs. is_subject aag x\<rbrakk> \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag ?Q6 (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 ())
 2. \<And>s. \<lbrakk>0 < word_of_nat num_objects; \<forall>x\<in>set refs. new_type = ArchObject PageDirectoryObj \<longrightarrow> is_aligned x pd_bits; \<forall>x\<in>set refs. is_subject aag x; arm_global_pd (arch_state s) \<notin> set refs \<and> pspace_aligned s \<and> valid_arch_state s\<rbrakk> \<Longrightarrow> ?Q6 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>0 < word_of_nat num_objects; new_type = ArchObject PageDirectoryObj \<longrightarrow> (\<forall>x\<in>set refs. is_aligned x pd_bits); \<forall>x\<in>set refs. is_subject aag x; arm_global_pd (arch_state s) \<notin> set refs \<and> pspace_aligned s \<and> valid_arch_state s\<rbrakk> \<Longrightarrow> new_type = ArchObject PageDirectoryObj \<longrightarrow> (\<forall>x\<in>set refs. x \<noteq> arm_global_pd (arch_state s)) proof (prove)
goal:
No subgoals!