theory DomainSepInv

lemma perform_invocation_domain_sep_inv':
  "\<lbrace>domain_sep_inv irqs st and valid_invocation iv and valid_objs
                           and valid_mdb and sym_refs \<circ> state_refs_of\<rbrace>
   perform_invocation block call iv
   \<lbrace>\<lambda>_ s. domain_sep_inv irqs (st :: 'state_ext state) (s :: det_ext state)\<rbrace>" apply (case_tac iv) apply (wp send_ipc_domain_sep_inv invoke_tcb_domain_sep_inv
                     invoke_cnode_domain_sep_inv invoke_control_domain_sep_inv
                     invoke_irq_handler_domain_sep_inv arch_perform_invocation_domain_sep_inv
                     invoke_domain_domain_set_inv
                  | simp add: split_def | blast)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st and valid_invocation iv and valid_objs and valid_mdb and sym_refs \<circ> state_refs_of\<rbrace> perform_invocation block call iv \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (10 subgoals):
 1. \<And>x1. iv = InvokeUntyped x1 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and valid_invocation iv and valid_objs and valid_mdb and sym_refs \<circ> state_refs_of\<rbrace> perform_invocation block call iv \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 2. \<And>x21 x22 x23 x24. iv = InvokeEndpoint x21 x22 x23 x24 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and valid_invocation iv and valid_objs and valid_mdb and sym_refs \<circ> state_refs_of\<rbrace> perform_invocation block call iv \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 3. \<And>x31 x32. iv = InvokeNotification x31 x32 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and valid_invocation iv and valid_objs and valid_mdb and sym_refs \<circ> state_refs_of\<rbrace> perform_invocation block call iv \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 4. \<And>x41 x42 x43. iv = InvokeReply x41 x42 x43 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and valid_invocation iv and valid_objs and valid_mdb and sym_refs \<circ> state_refs_of\<rbrace> perform_invocation block call iv \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 5. \<And>x5. iv = InvokeTCB x5 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and valid_invocation iv and valid_objs and valid_mdb and sym_refs \<circ> state_refs_of\<rbrace> perform_invocation block call iv \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 6. \<And>x61 x62. iv = InvokeDomain x61 x62 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and valid_invocation iv and valid_objs and valid_mdb and sym_refs \<circ> state_refs_of\<rbrace> perform_invocation block call iv \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 7. \<And>x7. iv = InvokeCNode x7 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and valid_invocation iv and valid_objs and valid_mdb and sym_refs \<circ> state_refs_of\<rbrace> perform_invocation block call iv \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 8. \<And>x8. iv = InvokeIRQControl x8 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and valid_invocation iv and valid_objs and valid_mdb and sym_refs \<circ> state_refs_of\<rbrace> perform_invocation block call iv \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 9. \<And>x9. iv = InvokeIRQHandler x9 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and valid_invocation iv and valid_objs and valid_mdb and sym_refs \<circ> state_refs_of\<rbrace> perform_invocation block call iv \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 10. \<And>x10. iv = InvokeArchObject x10 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and valid_invocation iv and valid_objs and valid_mdb and sym_refs \<circ> state_refs_of\<rbrace> perform_invocation block call iv \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal:
No subgoals!