theory ADT_IF

lemma perform_invocation_irq_state_inv:
   "\<lbrace>irq_state_inv st and domain_sep_inv False (sta :: det_state)
                      and valid_invocation op and K (irq_is_recurring irq st)
                      and (\<lambda>s. \<forall>i. op = InvokeIRQHandler i \<longrightarrow>
                                   (\<exists>p. cte_wp_at ((=) (IRQHandlerCap (irq_of_handler_inv i))) p s))\<rbrace>
    perform_invocation x y op
    \<lbrace>\<lambda>_. irq_state_inv st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>" apply (case_tac op; simp;
         (solves \<open>(wp invoke_untyped_irq_state_inv[where irq=irq] irq_state_inv_triv
                      invoke_tcb_irq_state_inv invoke_cnode_irq_state_inv[simplified validE_R_def]
                   | clarsimp | simp add: invoke_domain_def)+\<close>)?) apply wp apply (wp irq_state_inv_triv' invoke_irq_control_irq_masks) apply clarsimp apply assumption apply auto[1] apply wp apply (wp irq_state_inv_triv' invoke_irq_handler_irq_masks | clarsimp)+ apply assumption apply auto[1] done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>irq_state_inv st and domain_sep_inv False sta and valid_invocation op and K (irq_is_recurring irq st) and (\<lambda>s. \<forall>i. op = InvokeIRQHandler i \<longrightarrow> (\<exists>p. cte_wp_at ((=) (IRQHandlerCap (irq_of_handler_inv i))) p s))\<rbrace> perform_invocation x y op \<lbrace>\<lambda>_. irq_state_inv st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x8. op = InvokeIRQControl x8 \<Longrightarrow> \<lbrace>irq_state_inv st and domain_sep_inv False sta and irq_control_inv_valid x8 and (\<lambda>y. irq_is_recurring irq st)\<rbrace> doE y <- invoke_irq_control x8;
returnOk []
odE \<lbrace>\<lambda>_. irq_state_inv st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 2. \<And>x9. op = InvokeIRQHandler x9 \<Longrightarrow> \<lbrace>irq_state_inv st and domain_sep_inv False sta and irq_handler_inv_valid x9 and (\<lambda>y. irq_is_recurring irq st) and (\<lambda>s. \<exists>a b. cte_wp_at ((=) (IRQHandlerCap (irq_of_handler_inv x9))) (a, b) s)\<rbrace> doE y <- liftE (invoke_irq_handler x9);
returnOk []
odE \<lbrace>\<lambda>_. irq_state_inv st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x8. op = InvokeIRQControl x8 \<Longrightarrow> \<lbrace>?P'142 x8\<rbrace> invoke_irq_control x8 \<lbrace>\<lambda>y. irq_state_inv st\<rbrace>, -
 2. \<And>x8 s. \<lbrakk>op = InvokeIRQControl x8; (irq_state_inv st and domain_sep_inv False sta and irq_control_inv_valid x8 and (\<lambda>y. irq_is_recurring irq st)) s\<rbrakk> \<Longrightarrow> True \<and> ?P'142 x8 s
 3. \<And>x9. op = InvokeIRQHandler x9 \<Longrightarrow> \<lbrace>irq_state_inv st and domain_sep_inv False sta and irq_handler_inv_valid x9 and (\<lambda>y. irq_is_recurring irq st) and (\<lambda>s. \<exists>a b. cte_wp_at ((=) (IRQHandlerCap (irq_of_handler_inv x9))) (a, b) s)\<rbrace> doE y <- liftE (invoke_irq_handler x9);
returnOk []
odE \<lbrace>\<lambda>_. irq_state_inv st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x8 P s. \<lbrakk>op = InvokeIRQControl x8; ((\<lambda>s. P (irq_masks_of_state s)) and ?Q147 x8) s\<rbrakk> \<Longrightarrow> (domain_sep_inv False (?st151 x8 P) and irq_control_inv_valid x8) s
 2. \<And>x8 s. \<lbrakk>op = InvokeIRQControl x8; (irq_state_inv st and domain_sep_inv False sta and irq_control_inv_valid x8 and (\<lambda>y. irq_is_recurring irq st)) s\<rbrakk> \<Longrightarrow> True \<and> (irq_state_inv st and ?Q147 x8) s
 3. \<And>x9. op = InvokeIRQHandler x9 \<Longrightarrow> \<lbrace>irq_state_inv st and domain_sep_inv False sta and irq_handler_inv_valid x9 and (\<lambda>y. irq_is_recurring irq st) and (\<lambda>s. \<exists>a b. cte_wp_at ((=) (IRQHandlerCap (irq_of_handler_inv x9))) (a, b) s)\<rbrace> doE y <- liftE (invoke_irq_handler x9);
returnOk []
odE \<lbrace>\<lambda>_. irq_state_inv st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x8 P s. \<lbrakk>op = InvokeIRQControl x8; P (irq_masks_of_state s); ?Q147 x8 s\<rbrakk> \<Longrightarrow> domain_sep_inv False (?st151 x8 P) s \<and> irq_control_inv_valid x8 s
 2. \<And>x8 s. \<lbrakk>op = InvokeIRQControl x8; (irq_state_inv st and domain_sep_inv False sta and irq_control_inv_valid x8 and (\<lambda>y. irq_is_recurring irq st)) s\<rbrakk> \<Longrightarrow> True \<and> (irq_state_inv st and ?Q147 x8) s
 3. \<And>x9. op = InvokeIRQHandler x9 \<Longrightarrow> \<lbrace>irq_state_inv st and domain_sep_inv False sta and irq_handler_inv_valid x9 and (\<lambda>y. irq_is_recurring irq st) and (\<lambda>s. \<exists>a b. cte_wp_at ((=) (IRQHandlerCap (irq_of_handler_inv x9))) (a, b) s)\<rbrace> doE y <- liftE (invoke_irq_handler x9);
returnOk []
odE \<lbrace>\<lambda>_. irq_state_inv st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x8 s. \<lbrakk>op = InvokeIRQControl x8; (irq_state_inv st and domain_sep_inv False sta and irq_control_inv_valid x8 and (\<lambda>y. irq_is_recurring irq st)) s\<rbrakk> \<Longrightarrow> True \<and> (irq_state_inv st and (\<lambda>s. domain_sep_inv False (?st158 x8) s \<and> irq_control_inv_valid x8 s)) s
 2. \<And>x9. op = InvokeIRQHandler x9 \<Longrightarrow> \<lbrace>irq_state_inv st and domain_sep_inv False sta and irq_handler_inv_valid x9 and (\<lambda>y. irq_is_recurring irq st) and (\<lambda>s. \<exists>a b. cte_wp_at ((=) (IRQHandlerCap (irq_of_handler_inv x9))) (a, b) s)\<rbrace> doE y <- liftE (invoke_irq_handler x9);
returnOk []
odE \<lbrace>\<lambda>_. irq_state_inv st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x9. op = InvokeIRQHandler x9 \<Longrightarrow> \<lbrace>irq_state_inv st and domain_sep_inv False sta and irq_handler_inv_valid x9 and (\<lambda>y. irq_is_recurring irq st) and (\<lambda>s. \<exists>a b. cte_wp_at ((=) (IRQHandlerCap (irq_of_handler_inv x9))) (a, b) s)\<rbrace> doE y <- liftE (invoke_irq_handler x9);
returnOk []
odE \<lbrace>\<lambda>_. irq_state_inv st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x9. op = InvokeIRQHandler x9 \<Longrightarrow> \<lbrace>?Q164 x9\<rbrace> invoke_irq_handler x9 \<lbrace>\<lambda>y. irq_state_inv st\<rbrace>
 2. \<And>x9 s. \<lbrakk>op = InvokeIRQHandler x9; (irq_state_inv st and domain_sep_inv False sta and irq_handler_inv_valid x9 and (\<lambda>y. irq_is_recurring irq st) and (\<lambda>s. \<exists>a b. cte_wp_at ((=) (IRQHandlerCap (irq_of_handler_inv x9))) (a, b) s)) s\<rbrakk> \<Longrightarrow> ?Q164 x9 s proof (prove)
goal (2 subgoals):
 1. \<And>x9 P s. \<lbrakk>op = InvokeIRQHandler x9; P (irq_masks_of_state s); ?Q169 x9 s\<rbrakk> \<Longrightarrow> domain_sep_inv False (?st173 x9 P) s \<and> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap (?irq173 x9 P))) (a, b) s)
 2. \<And>x9 s. \<lbrakk>op = InvokeIRQHandler x9; (irq_state_inv st and domain_sep_inv False sta and irq_handler_inv_valid x9 and (\<lambda>y. irq_is_recurring irq st) and (\<lambda>s. \<exists>a b. cte_wp_at ((=) (IRQHandlerCap (irq_of_handler_inv x9))) (a, b) s)) s\<rbrakk> \<Longrightarrow> (irq_state_inv st and ?Q169 x9) s proof (prove)
goal (1 subgoal):
 1. \<And>x9 s. \<lbrakk>op = InvokeIRQHandler x9; (irq_state_inv st and domain_sep_inv False sta and irq_handler_inv_valid x9 and (\<lambda>y. irq_is_recurring irq st) and (\<lambda>s. \<exists>a b. cte_wp_at ((=) (IRQHandlerCap (irq_of_handler_inv x9))) (a, b) s)) s\<rbrakk> \<Longrightarrow> (irq_state_inv st and (\<lambda>s. domain_sep_inv False (?st180 x9) s \<and> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap (?irq181 x9))) (a, b) s))) s proof (prove)
goal:
No subgoals!