theory IRQMasks_IF

lemma perform_invocation_irq_masks:
  "\<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and
    (\<lambda>s. (\<forall>blah. oper = InvokeIRQHandler blah
                 \<longrightarrow> (\<exists>ptr'. cte_wp_at ((=) (IRQHandlerCap (irq_of_handler_inv blah))) ptr' s))) and
    domain_sep_inv False (st :: 's state) and valid_invocation oper\<rbrace>
   perform_invocation blocking calling oper
   \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>" apply (cases oper) by (wpsimp wp: invoke_tcb_irq_masks invoke_cnode_irq_masks[where st=st]
                 invoke_irq_control_irq_masks[where st=st]
                 invoke_irq_handler_irq_masks[where st=st]
      | fastforce)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and (\<lambda>s. \<forall>blah. oper = InvokeIRQHandler blah \<longrightarrow> (\<exists>ptr'. cte_wp_at ((=) (IRQHandlerCap (irq_of_handler_inv blah))) ptr' s)) and domain_sep_inv False st and valid_invocation oper\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace> proof (prove)
goal (10 subgoals):
 1. \<And>x1. oper = InvokeUntyped x1 \<Longrightarrow> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and (\<lambda>s. \<forall>blah. oper = InvokeIRQHandler blah \<longrightarrow> (\<exists>ptr'. cte_wp_at ((=) (IRQHandlerCap (irq_of_handler_inv blah))) ptr' s)) and domain_sep_inv False st and valid_invocation oper\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 2. \<And>x21 x22 x23 x24. oper = InvokeEndpoint x21 x22 x23 x24 \<Longrightarrow> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and (\<lambda>s. \<forall>blah. oper = InvokeIRQHandler blah \<longrightarrow> (\<exists>ptr'. cte_wp_at ((=) (IRQHandlerCap (irq_of_handler_inv blah))) ptr' s)) and domain_sep_inv False st and valid_invocation oper\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 3. \<And>x31 x32. oper = InvokeNotification x31 x32 \<Longrightarrow> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and (\<lambda>s. \<forall>blah. oper = InvokeIRQHandler blah \<longrightarrow> (\<exists>ptr'. cte_wp_at ((=) (IRQHandlerCap (irq_of_handler_inv blah))) ptr' s)) and domain_sep_inv False st and valid_invocation oper\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 4. \<And>x41 x42 x43. oper = InvokeReply x41 x42 x43 \<Longrightarrow> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and (\<lambda>s. \<forall>blah. oper = InvokeIRQHandler blah \<longrightarrow> (\<exists>ptr'. cte_wp_at ((=) (IRQHandlerCap (irq_of_handler_inv blah))) ptr' s)) and domain_sep_inv False st and valid_invocation oper\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 5. \<And>x5. oper = InvokeTCB x5 \<Longrightarrow> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and (\<lambda>s. \<forall>blah. oper = InvokeIRQHandler blah \<longrightarrow> (\<exists>ptr'. cte_wp_at ((=) (IRQHandlerCap (irq_of_handler_inv blah))) ptr' s)) and domain_sep_inv False st and valid_invocation oper\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 6. \<And>x61 x62. oper = InvokeDomain x61 x62 \<Longrightarrow> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and (\<lambda>s. \<forall>blah. oper = InvokeIRQHandler blah \<longrightarrow> (\<exists>ptr'. cte_wp_at ((=) (IRQHandlerCap (irq_of_handler_inv blah))) ptr' s)) and domain_sep_inv False st and valid_invocation oper\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 7. \<And>x7. oper = InvokeCNode x7 \<Longrightarrow> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and (\<lambda>s. \<forall>blah. oper = InvokeIRQHandler blah \<longrightarrow> (\<exists>ptr'. cte_wp_at ((=) (IRQHandlerCap (irq_of_handler_inv blah))) ptr' s)) and domain_sep_inv False st and valid_invocation oper\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 8. \<And>x8. oper = InvokeIRQControl x8 \<Longrightarrow> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and (\<lambda>s. \<forall>blah. oper = InvokeIRQHandler blah \<longrightarrow> (\<exists>ptr'. cte_wp_at ((=) (IRQHandlerCap (irq_of_handler_inv blah))) ptr' s)) and domain_sep_inv False st and valid_invocation oper\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 9. \<And>x9. oper = InvokeIRQHandler x9 \<Longrightarrow> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and (\<lambda>s. \<forall>blah. oper = InvokeIRQHandler blah \<longrightarrow> (\<exists>ptr'. cte_wp_at ((=) (IRQHandlerCap (irq_of_handler_inv blah))) ptr' s)) and domain_sep_inv False st and valid_invocation oper\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 10. \<And>x10. oper = InvokeArchObject x10 \<Longrightarrow> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and (\<lambda>s. \<forall>blah. oper = InvokeIRQHandler blah \<longrightarrow> (\<exists>ptr'. cte_wp_at ((=) (IRQHandlerCap (irq_of_handler_inv blah))) ptr' s)) and domain_sep_inv False st and valid_invocation oper\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>