theory DomainSepInv

lemma invoke_control_domain_sep_inv:
  "\<lbrace>domain_sep_inv irqs st and irq_control_inv_valid i\<rbrace>
    invoke_irq_control i
   \<lbrace>\<lambda>_ s. domain_sep_inv irqs (st :: 'state_ext state) (s :: det_ext state)\<rbrace>" including no_pre apply (case_tac i) apply (case_tac irqs) apply (wp cap_insert_domain_sep_inv' | simp )+ apply (simp add: set_irq_state_def, wp, simp) apply (fastforce simp: domain_sep_inv_def domain_sep_inv_cap_def) apply (fastforce simp: valid_def domain_sep_inv_def) apply simp apply (wp arch_invoke_irq_control_domain_sep_inv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st and irq_control_inv_valid i\<rbrace> invoke_irq_control i \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st and irq_control_inv_valid i\<rbrace> invoke_irq_control i \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x11 x12 x13. i = IRQControl x11 x12 x13 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and irq_control_inv_valid i\<rbrace> invoke_irq_control i \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 2. \<And>x2. i = ArchIRQControl x2 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and irq_control_inv_valid i\<rbrace> invoke_irq_control i \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x11 x12 x13. \<lbrakk>i = IRQControl x11 x12 x13; irqs\<rbrakk> \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and irq_control_inv_valid i\<rbrace> invoke_irq_control i \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 2. \<And>x11 x12 x13. \<lbrakk>i = IRQControl x11 x12 x13; \<not> irqs\<rbrakk> \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and irq_control_inv_valid i\<rbrace> invoke_irq_control i \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 3. \<And>x2. i = ArchIRQControl x2 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and irq_control_inv_valid i\<rbrace> invoke_irq_control i \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x11 x12 x13. \<lbrakk>i = IRQControl x11 x12 x13; irqs\<rbrakk> \<Longrightarrow> \<lbrace>domain_sep_inv True st and (cte_wp_at ((=) NullCap) x12 and cte_wp_at ((=) IRQControlCap) x13 and ex_cte_cap_wp_to is_cnode_cap x12 and real_cte_at x12 and (\<lambda>y. x11 \<le> maxIRQ))\<rbrace> set_irq_state IRQSignal x11 \<lbrace>\<lambda>y s. domain_sep_inv True st s \<and> domain_sep_inv_cap True (IRQHandlerCap x11)\<rbrace>
 2. \<And>x11 x12 x13. \<lbrakk>i = IRQControl x11 x12 x13; \<not> irqs\<rbrakk> \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and irq_control_inv_valid i\<rbrace> invoke_irq_control i \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 3. \<And>x2. i = ArchIRQControl x2 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and irq_control_inv_valid i\<rbrace> invoke_irq_control i \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x11 x12 x13 s. \<lbrakk>i = IRQControl x11 x12 x13; irqs; domain_sep_inv True st s \<and> cte_wp_at ((=) NullCap) x12 s \<and> cte_wp_at ((=) IRQControlCap) x13 s \<and> ex_cte_cap_wp_to is_cnode_cap x12 s \<and> real_cte_at x12 s \<and> x11 \<le> maxIRQ\<rbrakk> \<Longrightarrow> domain_sep_inv True st (s\<lparr>interrupt_states := \<lambda>a. if a = x11 then IRQSignal else interrupt_states s a\<rparr>) \<and> domain_sep_inv_cap True (IRQHandlerCap x11)
 2. \<And>x11 x12 x13. \<lbrakk>i = IRQControl x11 x12 x13; \<not> irqs\<rbrakk> \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and irq_control_inv_valid i\<rbrace> invoke_irq_control i \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 3. \<And>x2. i = ArchIRQControl x2 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and irq_control_inv_valid i\<rbrace> invoke_irq_control i \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x11 x12 x13. \<lbrakk>i = IRQControl x11 x12 x13; \<not> irqs\<rbrakk> \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and irq_control_inv_valid i\<rbrace> invoke_irq_control i \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 2. \<And>x2. i = ArchIRQControl x2 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and irq_control_inv_valid i\<rbrace> invoke_irq_control i \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x2. i = ArchIRQControl x2 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and irq_control_inv_valid i\<rbrace> invoke_irq_control i \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x2. i = ArchIRQControl x2 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and arch_irq_control_inv_valid x2\<rbrace> arch_invoke_irq_control x2 \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal:
No subgoals!