theory ArchArch_IF

lemma arch_perform_invocation_reads_respects:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows "reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs
                                               and authorised_arch_inv aag ai
                                               and valid_arch_inv ai and is_subject aag \<circ> cur_thread)
                        (arch_perform_invocation ai)" unfolding arch_perform_invocation_def fun_app_def apply (rule equiv_valid_guard_imp) apply (wpsimp wp: perform_page_table_invocation_reads_respects
                     perform_page_directory_invocation_reads_respects
                     perform_page_invocation_reads_respects
                     perform_asid_control_invocation_reads_respects
                     perform_asid_pool_invocation_reads_respects) by (auto simp: authorised_arch_inv_def valid_arch_inv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and authorised_arch_inv aag ai and valid_arch_inv ai and is_subject aag \<circ> cur_thread) (arch_perform_invocation ai) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and authorised_arch_inv aag ai and valid_arch_inv ai and is_subject aag \<circ> cur_thread) (liftE (case ai of InvokePageTable oper \<Rightarrow> do perform_page_table_invocation oper;
return []
od | InvokePageDirectory oper \<Rightarrow> do perform_page_directory_invocation oper;
return []
od | InvokePage x \<Rightarrow> perform_page_invocation x | InvokeASIDControl oper \<Rightarrow> do perform_asid_control_invocation oper;
return []
od | InvokeASIDPool oper \<Rightarrow> do perform_asid_pool_invocation oper;
return []
od)) proof (prove)
goal (2 subgoals):
 1. reads_respects aag l ?Q (liftE (case ai of InvokePageTable oper \<Rightarrow> do perform_page_table_invocation oper;
return []
od | InvokePageDirectory oper \<Rightarrow> do perform_page_directory_invocation oper;
return []
od | InvokePage x \<Rightarrow> perform_page_invocation x | InvokeASIDControl oper \<Rightarrow> do perform_asid_control_invocation oper;
return []
od | InvokeASIDPool oper \<Rightarrow> do perform_asid_pool_invocation oper;
return []
od))
 2. \<And>s. (pas_refined aag and pspace_aligned and valid_vspace_objs and authorised_arch_inv aag ai and valid_arch_inv ai and is_subject aag \<circ> cur_thread) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (pas_refined aag and pspace_aligned and valid_vspace_objs and authorised_arch_inv aag ai and valid_arch_inv ai and is_subject aag \<circ> cur_thread) s \<Longrightarrow> (\<forall>x. ai = InvokePageTable x \<longrightarrow> (pas_refined aag and pspace_aligned and valid_vspace_objs and K (authorised_page_table_inv aag x)) s \<and> True) \<and> (\<forall>x. ai = InvokePageDirectory x \<longrightarrow> (is_subject aag \<circ> cur_thread) s \<and> True) \<and> (\<forall>x. ai = InvokePage x \<longrightarrow> (pas_refined aag and K (authorised_page_inv aag x) and valid_page_inv x and valid_vspace_objs and pspace_aligned and is_subject aag \<circ> cur_thread) s) \<and> (\<forall>x. ai = InvokeASIDControl x \<longrightarrow> K (authorised_asid_control_inv aag x) s \<and> True) \<and> (\<forall>x. ai = InvokeASIDPool x \<longrightarrow> (pas_refined aag and K (authorised_asid_pool_inv aag x)) s \<and> True)