theory ArchArch_AC

lemma invoke_arch_pas_refined:
  "\<lbrace>pas_refined aag and pas_cur_domain aag and invs and ct_active
                    and valid_arch_inv ai and authorised_arch_inv aag ai\<rbrace>
   arch_perform_invocation ai
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" apply (simp add: arch_perform_invocation_def valid_arch_inv_def) apply (rule hoare_pre) apply (wp | wpc)+ apply (fastforce simp add: authorised_arch_inv_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and pas_cur_domain aag and invs and ct_active and valid_arch_inv ai and authorised_arch_inv aag ai\<rbrace> arch_perform_invocation ai \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and pas_cur_domain aag and invs and ct_active and (case ai of InvokePageTable pti \<Rightarrow> valid_pti pti | InvokePageDirectory pdi \<Rightarrow> valid_pdi pdi | InvokePage pgi \<Rightarrow> valid_page_inv pgi | InvokeASIDControl aci \<Rightarrow> valid_aci aci | InvokeASIDPool ap \<Rightarrow> valid_apinv ap) and authorised_arch_inv aag ai\<rbrace> 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) \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> 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) \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 2. \<And>s. (pas_refined aag and pas_cur_domain aag and invs and ct_active and (case ai of InvokePageTable pti \<Rightarrow> valid_pti pti | InvokePageDirectory pdi \<Rightarrow> valid_pdi pdi | InvokePage pgi \<Rightarrow> valid_page_inv pgi | InvokeASIDControl aci \<Rightarrow> valid_aci aci | InvokeASIDPool ap \<Rightarrow> valid_apinv ap) and authorised_arch_inv aag ai) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (pas_refined aag and pas_cur_domain aag and invs and ct_active and (case ai of InvokePageTable pti \<Rightarrow> valid_pti pti | InvokePageDirectory pdi \<Rightarrow> valid_pdi pdi | InvokePage pgi \<Rightarrow> valid_page_inv pgi | InvokeASIDControl aci \<Rightarrow> valid_aci aci | InvokeASIDPool ap \<Rightarrow> valid_apinv ap) and authorised_arch_inv aag ai) s \<Longrightarrow> (\<forall>x. ai = InvokePageTable x \<longrightarrow> (pas_refined aag and invs and valid_pti x and K (authorised_page_table_inv aag x)) s) \<and> (\<forall>x. ai = InvokePageDirectory x \<longrightarrow> pas_refined aag s) \<and> (\<forall>x. ai = InvokePage x \<longrightarrow> (pas_refined aag and invs and K (authorised_page_inv aag x) and valid_page_inv x) s) \<and> (\<forall>x. ai = InvokeASIDControl x \<longrightarrow> (pas_refined aag and pas_cur_domain aag and invs and valid_aci x and ct_active and K (authorised_asid_control_inv aag x)) s) \<and> (\<forall>x. ai = InvokeASIDPool x \<longrightarrow> (pas_refined aag and invs and valid_apinv x and K (authorised_asid_pool_inv aag x)) s) proof (prove)
goal:
No subgoals!