theory ArchDomainSepInv

lemma arch_invoke_irq_control_domain_sep_inv[DomainSepInv_assms]:
  "\<lbrace>domain_sep_inv irqs st and arch_irq_control_inv_valid ivk\<rbrace>
   arch_invoke_irq_control ivk
   \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>" apply (cases ivk) apply (wpsimp wp: cap_insert_domain_sep_inv' simp: set_irq_state_def) apply (rule_tac Q="\<lambda>_. domain_sep_inv irqs st and arch_irq_control_inv_valid ivk"
                in hoare_strengthen_post[rotated]) apply (fastforce simp: domain_sep_inv_def domain_sep_inv_cap_def arch_irq_control_inv_valid_def) apply (wpsimp wp: do_machine_op_domain_sep_inv simp: arch_irq_control_inv_valid_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st and arch_irq_control_inv_valid ivk\<rbrace> arch_invoke_irq_control ivk \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4. ivk = ArchIRQControlIssue x1 x2 x3 x4 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and arch_irq_control_inv_valid ivk\<rbrace> arch_invoke_irq_control ivk \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x1 a b aa ba x4. ivk = ArchIRQControlIssue x1 (a, b) (aa, ba) x4 \<Longrightarrow> \<lbrace>?Q12 x1 a b aa ba (a, b) (aa, ba) x4\<rbrace> do_machine_op (setIRQTrigger x1 x4) \<lbrace>\<lambda>y s. domain_sep_inv irqs st (s\<lparr>interrupt_states := \<lambda>a. if a = x1 then IRQSignal else interrupt_states s a\<rparr>) \<and> domain_sep_inv_cap irqs (IRQHandlerCap x1)\<rbrace>
 2. \<And>x1 x2 x3 x4 s. \<lbrakk>ivk = ArchIRQControlIssue x1 x2 x3 x4; (domain_sep_inv irqs st and arch_irq_control_inv_valid ivk) s\<rbrakk> \<Longrightarrow> ?Q12 x1 (fst x2) (snd x2) (fst x3) (snd x3) x2 x3 x4 s proof (prove)
goal (3 subgoals):
 1. \<And>x1 a b aa ba x4 rv s. \<lbrakk>ivk = ArchIRQControlIssue x1 (a, b) (aa, ba) x4; (domain_sep_inv irqs st and arch_irq_control_inv_valid ivk) s\<rbrakk> \<Longrightarrow> domain_sep_inv irqs st (s\<lparr>interrupt_states := \<lambda>a. if a = x1 then IRQSignal else interrupt_states s a\<rparr>) \<and> domain_sep_inv_cap irqs (IRQHandlerCap x1)
 2. \<And>x1 a b aa ba x4. ivk = ArchIRQControlIssue x1 (a, b) (aa, ba) x4 \<Longrightarrow> \<lbrace>?Q12 x1 a b aa ba (a, b) (aa, ba) x4\<rbrace> do_machine_op (setIRQTrigger x1 x4) \<lbrace>\<lambda>_. domain_sep_inv irqs st and arch_irq_control_inv_valid ivk\<rbrace>
 3. \<And>x1 x2 x3 x4 s. \<lbrakk>ivk = ArchIRQControlIssue x1 x2 x3 x4; (domain_sep_inv irqs st and arch_irq_control_inv_valid ivk) s\<rbrakk> \<Longrightarrow> ?Q12 x1 (fst x2) (snd x2) (fst x3) (snd x3) x2 x3 x4 s proof (prove)
goal (2 subgoals):
 1. \<And>x1 a b aa ba x4. ivk = ArchIRQControlIssue x1 (a, b) (aa, ba) x4 \<Longrightarrow> \<lbrace>?Q12 x1 a b aa ba (a, b) (aa, ba) x4\<rbrace> do_machine_op (setIRQTrigger x1 x4) \<lbrace>\<lambda>_. domain_sep_inv irqs st and arch_irq_control_inv_valid ivk\<rbrace>
 2. \<And>x1 x2 x3 x4 s. \<lbrakk>ivk = ArchIRQControlIssue x1 x2 x3 x4; (domain_sep_inv irqs st and arch_irq_control_inv_valid ivk) s\<rbrakk> \<Longrightarrow> ?Q12 x1 (fst x2) (snd x2) (fst x3) (snd x3) x2 x3 x4 s proof (prove)
goal:
No subgoals!