theory Interrupt_R

lemma arch_performIRQControl_corres:
  "arch_irq_control_inv_relation x2 ivk' \<Longrightarrow> corres (dc \<oplus> dc)
          (einvs and arch_irq_control_inv_valid x2)
          (invs' and arch_irq_control_inv_valid' ivk')
          (arch_invoke_irq_control x2)
          (Arch.performIRQControl ivk')" apply (cases x2; simp add: ARM_H.performIRQControl_def invoke_irq_control.cases IRQ_def) apply (rule corres_guard_imp) apply (rule corres_split_nor) apply (rule setIRQTrigger_corres) apply (rule corres_split_nor) apply (rule setIRQState_corres) apply (simp add: irq_state_relation_def) apply (rule cteInsert_simple_corres; simp) apply (wp | simp add: irq_state_relation_def IRQHandler_valid IRQHandler_valid')+ apply (clarsimp simp: invs_def valid_state_def valid_pspace_def cte_wp_at_caps_of_state
                         is_simple_cap_def is_cap_simps arch_irq_control_inv_valid_def
                         safe_parent_for_def) apply (clarsimp simp: invs'_def valid_state'_def valid_pspace'_def IRQHandler_valid
                        IRQHandler_valid' is_simple_cap'_def isCap_simps IRQ_def) apply (clarsimp simp: safe_parent_for'_def cte_wp_at_ctes_of) apply (case_tac ctea) apply (clarsimp simp: isCap_simps sameRegionAs_def3) apply (auto dest: valid_irq_handlers_ctes_ofD)[1] done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. arch_irq_control_inv_relation x2 ivk' \<Longrightarrow> corres (dc \<oplus> dc) (einvs and arch_irq_control_inv_valid x2) (invs' and arch_irq_control_inv_valid' ivk') (arch_invoke_irq_control x2) (Arch.performIRQControl ivk') proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2a x3 x4. \<lbrakk>ivk' = local.irqcontrol_invocation.IssueIRQHandler x1 (cte_map x2a) (cte_map x3) x4; x2 = ArchIRQControlIssue x1 x2a x3 x4\<rbrakk> \<Longrightarrow> corres dc (einvs and arch_irq_control_inv_valid (ArchIRQControlIssue x1 x2a x3 x4)) (invs' and (cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (cte_map x2a) and cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQControlCap) (cte_map x3) and ex_cte_cap_wp_to' (\<lambda>_. True) (cte_map x2a) and real_cte_at' (cte_map x2a) and Not \<circ> irq_issued' x1 and (\<lambda>y. x1 \<le> maxIRQ))) (do y <- do_machine_op (setIRQTrigger x1 x4);
y <- set_irq_state irq_state.IRQSignal x1;
cap_insert (cap.IRQHandlerCap x1) x3 x2a
od) (do y <- doMachineOp (setIRQTrigger x1 x4);
y <- setIRQState irqstate.IRQSignal x1;
cteInsert (capability.IRQHandlerCap x1) (cte_map x3) (cte_map x2a)
od) proof (prove)
goal (3 subgoals):
 1. \<And>x1 x2a x3 x4. \<lbrakk>ivk' = local.irqcontrol_invocation.IssueIRQHandler x1 (cte_map x2a) (cte_map x3) x4; x2 = ArchIRQControlIssue x1 x2a x3 x4\<rbrakk> \<Longrightarrow> corres dc (?Q5 x1 x2a x3 x4) (?Q'5 x1 x2a x3 x4) (do y <- do_machine_op (setIRQTrigger x1 x4);
y <- set_irq_state irq_state.IRQSignal x1;
cap_insert (cap.IRQHandlerCap x1) x3 x2a
od) (do y <- doMachineOp (setIRQTrigger x1 x4);
y <- setIRQState irqstate.IRQSignal x1;
cteInsert (capability.IRQHandlerCap x1) (cte_map x3) (cte_map x2a)
od)
 2. \<And>x1 x2a x3 x4 s. \<lbrakk>ivk' = local.irqcontrol_invocation.IssueIRQHandler x1 (cte_map x2a) (cte_map x3) x4; x2 = ArchIRQControlIssue x1 x2a x3 x4; (einvs and arch_irq_control_inv_valid (ArchIRQControlIssue x1 x2a x3 x4)) s\<rbrakk> \<Longrightarrow> ?Q5 x1 x2a x3 x4 s
 3. \<And>x1 x2a x3 x4 s. \<lbrakk>ivk' = local.irqcontrol_invocation.IssueIRQHandler x1 (cte_map x2a) (cte_map x3) x4; x2 = ArchIRQControlIssue x1 x2a x3 x4; (invs' and (cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (cte_map x2a) and cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQControlCap) (cte_map x3) and ex_cte_cap_wp_to' (\<lambda>_. True) (cte_map x2a) and real_cte_at' (cte_map x2a) and Not \<circ> irq_issued' x1 and (\<lambda>y. x1 \<le> maxIRQ))) s\<rbrakk> \<Longrightarrow> ?Q'5 x1 x2a x3 x4 s proof (prove)
goal (6 subgoals):
 1. \<And>x1 x2a x3 x4. \<lbrakk>ivk' = local.irqcontrol_invocation.IssueIRQHandler x1 (cte_map x2a) (cte_map x3) x4; x2 = ArchIRQControlIssue x1 x2a x3 x4\<rbrakk> \<Longrightarrow> corres dc (?P9 x1 x2a x3 x4) (?P'9 x1 x2a x3 x4) (do_machine_op (setIRQTrigger x1 x4)) (doMachineOp (setIRQTrigger x1 x4))
 2. \<And>x1 x2a x3 x4. \<lbrakk>ivk' = local.irqcontrol_invocation.IssueIRQHandler x1 (cte_map x2a) (cte_map x3) x4; x2 = ArchIRQControlIssue x1 x2a x3 x4\<rbrakk> \<Longrightarrow> corres dc (?R9 x1 x2a x3 x4) (?R'9 x1 x2a x3 x4) (do y <- set_irq_state irq_state.IRQSignal x1;
cap_insert (cap.IRQHandlerCap x1) x3 x2a
od) (do y <- setIRQState irqstate.IRQSignal x1;
cteInsert (capability.IRQHandlerCap x1) (cte_map x3) (cte_map x2a)
od)
 3. \<And>x1 x2a x3 x4. \<lbrakk>ivk' = local.irqcontrol_invocation.IssueIRQHandler x1 (cte_map x2a) (cte_map x3) x4; x2 = ArchIRQControlIssue x1 x2a x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>?Q9 x1 x2a x3 x4\<rbrace> do_machine_op (setIRQTrigger x1 x4) \<lbrace>\<lambda>x. ?R9 x1 x2a x3 x4\<rbrace>
 4. \<And>x1 x2a x3 x4. \<lbrakk>ivk' = local.irqcontrol_invocation.IssueIRQHandler x1 (cte_map x2a) (cte_map x3) x4; x2 = ArchIRQControlIssue x1 x2a x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>?Q'9 x1 x2a x3 x4\<rbrace> doMachineOp (setIRQTrigger x1 x4) \<lbrace>\<lambda>x. ?R'9 x1 x2a x3 x4\<rbrace>
 5. \<And>x1 x2a x3 x4 s. \<lbrakk>ivk' = local.irqcontrol_invocation.IssueIRQHandler x1 (cte_map x2a) (cte_map x3) x4; x2 = ArchIRQControlIssue x1 x2a x3 x4; (einvs and arch_irq_control_inv_valid (ArchIRQControlIssue x1 x2a x3 x4)) s\<rbrakk> \<Longrightarrow> (?P9 x1 x2a x3 x4 and ?Q9 x1 x2a x3 x4) s
 6. \<And>x1 x2a x3 x4 s. \<lbrakk>ivk' = local.irqcontrol_invocation.IssueIRQHandler x1 (cte_map x2a) (cte_map x3) x4; x2 = ArchIRQControlIssue x1 x2a x3 x4; (invs' and (cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (cte_map x2a) and cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQControlCap) (cte_map x3) and ex_cte_cap_wp_to' (\<lambda>_. True) (cte_map x2a) and real_cte_at' (cte_map x2a) and Not \<circ> irq_issued' x1 and (\<lambda>y. x1 \<le> maxIRQ))) s\<rbrakk> \<Longrightarrow> (?P'9 x1 x2a x3 x4 and ?Q'9 x1 x2a x3 x4) s proof (prove)
goal (5 subgoals):
 1. \<And>x1 x2a x3 x4. \<lbrakk>ivk' = local.irqcontrol_invocation.IssueIRQHandler x1 (cte_map x2a) (cte_map x3) x4; x2 = ArchIRQControlIssue x1 x2a x3 x4\<rbrakk> \<Longrightarrow> corres dc (?R9 x1 x2a x3 x4) (?R'9 x1 x2a x3 x4) (do y <- set_irq_state irq_state.IRQSignal x1;
cap_insert (cap.IRQHandlerCap x1) x3 x2a
od) (do y <- setIRQState irqstate.IRQSignal x1;
cteInsert (capability.IRQHandlerCap x1) (cte_map x3) (cte_map x2a)
od)
 2. \<And>x1 x2a x3 x4. \<lbrakk>ivk' = local.irqcontrol_invocation.IssueIRQHandler x1 (cte_map x2a) (cte_map x3) x4; x2 = ArchIRQControlIssue x1 x2a x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>?Q9 x1 x2a x3 x4\<rbrace> do_machine_op (setIRQTrigger x1 x4) \<lbrace>\<lambda>x. ?R9 x1 x2a x3 x4\<rbrace>
 3. \<And>x1 x2a x3 x4. \<lbrakk>ivk' = local.irqcontrol_invocation.IssueIRQHandler x1 (cte_map x2a) (cte_map x3) x4; x2 = ArchIRQControlIssue x1 x2a x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>?Q'9 x1 x2a x3 x4\<rbrace> doMachineOp (setIRQTrigger x1 x4) \<lbrace>\<lambda>x. ?R'9 x1 x2a x3 x4\<rbrace>
 4. \<And>x1 x2a x3 x4 s. \<lbrakk>ivk' = local.irqcontrol_invocation.IssueIRQHandler x1 (cte_map x2a) (cte_map x3) x4; x2 = ArchIRQControlIssue x1 x2a x3 x4; (einvs and arch_irq_control_inv_valid (ArchIRQControlIssue x1 x2a x3 x4)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q9 x1 x2a x3 x4) s
 5. \<And>x1 x2a x3 x4 s. \<lbrakk>ivk' = local.irqcontrol_invocation.IssueIRQHandler x1 (cte_map x2a) (cte_map x3) x4; x2 = ArchIRQControlIssue x1 x2a x3 x4; (invs' and (cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (cte_map x2a) and cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQControlCap) (cte_map x3) and ex_cte_cap_wp_to' (\<lambda>_. True) (cte_map x2a) and real_cte_at' (cte_map x2a) and Not \<circ> irq_issued' x1 and (\<lambda>y. x1 \<le> maxIRQ))) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'9 x1 x2a x3 x4) s proof (prove)
goal (8 subgoals):
 1. \<And>x1 x2a x3 x4. \<lbrakk>ivk' = local.irqcontrol_invocation.IssueIRQHandler x1 (cte_map x2a) (cte_map x3) x4; x2 = ArchIRQControlIssue x1 x2a x3 x4\<rbrakk> \<Longrightarrow> corres dc (?P15 x1 x2a x3 x4) (?P'15 x1 x2a x3 x4) (set_irq_state irq_state.IRQSignal x1) (setIRQState irqstate.IRQSignal x1)
 2. \<And>x1 x2a x3 x4. \<lbrakk>ivk' = local.irqcontrol_invocation.IssueIRQHandler x1 (cte_map x2a) (cte_map x3) x4; x2 = ArchIRQControlIssue x1 x2a x3 x4\<rbrakk> \<Longrightarrow> corres dc (?R15 x1 x2a x3 x4) (?R'15 x1 x2a x3 x4) (cap_insert (cap.IRQHandlerCap x1) x3 x2a) (cteInsert (capability.IRQHandlerCap x1) (cte_map x3) (cte_map x2a))
 3. \<And>x1 x2a x3 x4. \<lbrakk>ivk' = local.irqcontrol_invocation.IssueIRQHandler x1 (cte_map x2a) (cte_map x3) x4; x2 = ArchIRQControlIssue x1 x2a x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>?Q15 x1 x2a x3 x4\<rbrace> set_irq_state irq_state.IRQSignal x1 \<lbrace>\<lambda>x. ?R15 x1 x2a x3 x4\<rbrace>
 4. \<And>x1 x2a x3 x4. \<lbrakk>ivk' = local.irqcontrol_invocation.IssueIRQHandler x1 (cte_map x2a) (cte_map x3) x4; x2 = ArchIRQControlIssue x1 x2a x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15 x1 x2a x3 x4\<rbrace> setIRQState irqstate.IRQSignal x1 \<lbrace>\<lambda>x. ?R'15 x1 x2a x3 x4\<rbrace>
 5. \<And>x1 x2a x3 x4. \<lbrakk>ivk' = local.irqcontrol_invocation.IssueIRQHandler x1 (cte_map x2a) (cte_map x3) x4; x2 = ArchIRQControlIssue x1 x2a x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>?Q9 x1 x2a x3 x4\<rbrace> do_machine_op (setIRQTrigger x1 x4) \<lbrace>\<lambda>x. ?P15 x1 x2a x3 x4 and ?Q15 x1 x2a x3 x4\<rbrace>
 6. \<And>x1 x2a x3 x4. \<lbrakk>ivk' = local.irqcontrol_invocation.IssueIRQHandler x1 (cte_map x2a) (cte_map x3) x4; x2 = ArchIRQControlIssue x1 x2a x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>?Q'9 x1 x2a x3 x4\<rbrace> doMachineOp (setIRQTrigger x1 x4) \<lbrace>\<lambda>x. ?P'15 x1 x2a x3 x4 and ?Q'15 x1 x2a x3 x4\<rbrace>
 7. \<And>x1 x2a x3 x4 s. \<lbrakk>ivk' = local.irqcontrol_invocation.IssueIRQHandler x1 (cte_map x2a) (cte_map x3) x4; x2 = ArchIRQControlIssue x1 x2a x3 x4; (einvs and arch_irq_control_inv_valid (ArchIRQControlIssue x1 x2a x3 x4)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q9 x1 x2a x3 x4) s
 8. \<And>x1 x2a x3 x4 s. \<lbrakk>ivk' = local.irqcontrol_invocation.IssueIRQHandler x1 (cte_map x2a) (cte_map x3) x4; x2 = ArchIRQControlIssue x1 x2a x3 x4; (invs' and (cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (cte_map x2a) and cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQControlCap) (cte_map x3) and ex_cte_cap_wp_to' (\<lambda>_. True) (cte_map x2a) and real_cte_at' (cte_map x2a) and Not \<circ> irq_issued' x1 and (\<lambda>y. x1 \<le> maxIRQ))) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'9 x1 x2a x3 x4) s proof (prove)
goal (8 subgoals):
 1. \<And>x1 x2a x3 x4. \<lbrakk>ivk' = local.irqcontrol_invocation.IssueIRQHandler x1 (cte_map x2a) (cte_map x3) x4; x2 = ArchIRQControlIssue x1 x2a x3 x4\<rbrakk> \<Longrightarrow> irq_state_relation irq_state.IRQSignal irqstate.IRQSignal
 2. \<And>x1 x2a x3 x4. \<lbrakk>ivk' = local.irqcontrol_invocation.IssueIRQHandler x1 (cte_map x2a) (cte_map x3) x4; x2 = ArchIRQControlIssue x1 x2a x3 x4\<rbrakk> \<Longrightarrow> corres dc (?R15 x1 x2a x3 x4) (?R'15 x1 x2a x3 x4) (cap_insert (cap.IRQHandlerCap x1) x3 x2a) (cteInsert (capability.IRQHandlerCap x1) (cte_map x3) (cte_map x2a))
 3. \<And>x1 x2a x3 x4. \<lbrakk>ivk' = local.irqcontrol_invocation.IssueIRQHandler x1 (cte_map x2a) (cte_map x3) x4; x2 = ArchIRQControlIssue x1 x2a x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>?Q15 x1 x2a x3 x4\<rbrace> set_irq_state irq_state.IRQSignal x1 \<lbrace>\<lambda>x. ?R15 x1 x2a x3 x4\<rbrace>
 4. \<And>x1 x2a x3 x4. \<lbrakk>ivk' = local.irqcontrol_invocation.IssueIRQHandler x1 (cte_map x2a) (cte_map x3) x4; x2 = ArchIRQControlIssue x1 x2a x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15 x1 x2a x3 x4\<rbrace> setIRQState irqstate.IRQSignal x1 \<lbrace>\<lambda>x. ?R'15 x1 x2a x3 x4\<rbrace>
 5. \<And>x1 x2a x3 x4. \<lbrakk>ivk' = local.irqcontrol_invocation.IssueIRQHandler x1 (cte_map x2a) (cte_map x3) x4; x2 = ArchIRQControlIssue x1 x2a x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>?Q9 x1 x2a x3 x4\<rbrace> do_machine_op (setIRQTrigger x1 x4) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q15 x1 x2a x3 x4\<rbrace>
 6. \<And>x1 x2a x3 x4. \<lbrakk>ivk' = local.irqcontrol_invocation.IssueIRQHandler x1 (cte_map x2a) (cte_map x3) x4; x2 = ArchIRQControlIssue x1 x2a x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>?Q'9 x1 x2a x3 x4\<rbrace> doMachineOp (setIRQTrigger x1 x4) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q'15 x1 x2a x3 x4\<rbrace>
 7. \<And>x1 x2a x3 x4 s. \<lbrakk>ivk' = local.irqcontrol_invocation.IssueIRQHandler x1 (cte_map x2a) (cte_map x3) x4; x2 = ArchIRQControlIssue x1 x2a x3 x4; (einvs and arch_irq_control_inv_valid (ArchIRQControlIssue x1 x2a x3 x4)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q9 x1 x2a x3 x4) s
 8. \<And>x1 x2a x3 x4 s. \<lbrakk>ivk' = local.irqcontrol_invocation.IssueIRQHandler x1 (cte_map x2a) (cte_map x3) x4; x2 = ArchIRQControlIssue x1 x2a x3 x4; (invs' and (cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (cte_map x2a) and cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQControlCap) (cte_map x3) and ex_cte_cap_wp_to' (\<lambda>_. True) (cte_map x2a) and real_cte_at' (cte_map x2a) and Not \<circ> irq_issued' x1 and (\<lambda>y. x1 \<le> maxIRQ))) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'9 x1 x2a x3 x4) s proof (prove)
goal (7 subgoals):
 1. \<And>x1 x2a x3 x4. \<lbrakk>ivk' = local.irqcontrol_invocation.IssueIRQHandler x1 (cte_map x2a) (cte_map x3) x4; x2 = ArchIRQControlIssue x1 x2a x3 x4\<rbrakk> \<Longrightarrow> corres dc (?R15 x1 x2a x3 x4) (?R'15 x1 x2a x3 x4) (cap_insert (cap.IRQHandlerCap x1) x3 x2a) (cteInsert (capability.IRQHandlerCap x1) (cte_map x3) (cte_map x2a))
 2. \<And>x1 x2a x3 x4. \<lbrakk>ivk' = local.irqcontrol_invocation.IssueIRQHandler x1 (cte_map x2a) (cte_map x3) x4; x2 = ArchIRQControlIssue x1 x2a x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>?Q15 x1 x2a x3 x4\<rbrace> set_irq_state irq_state.IRQSignal x1 \<lbrace>\<lambda>x. ?R15 x1 x2a x3 x4\<rbrace>
 3. \<And>x1 x2a x3 x4. \<lbrakk>ivk' = local.irqcontrol_invocation.IssueIRQHandler x1 (cte_map x2a) (cte_map x3) x4; x2 = ArchIRQControlIssue x1 x2a x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15 x1 x2a x3 x4\<rbrace> setIRQState irqstate.IRQSignal x1 \<lbrace>\<lambda>x. ?R'15 x1 x2a x3 x4\<rbrace>
 4. \<And>x1 x2a x3 x4. \<lbrakk>ivk' = local.irqcontrol_invocation.IssueIRQHandler x1 (cte_map x2a) (cte_map x3) x4; x2 = ArchIRQControlIssue x1 x2a x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>?Q9 x1 x2a x3 x4\<rbrace> do_machine_op (setIRQTrigger x1 x4) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q15 x1 x2a x3 x4\<rbrace>
 5. \<And>x1 x2a x3 x4. \<lbrakk>ivk' = local.irqcontrol_invocation.IssueIRQHandler x1 (cte_map x2a) (cte_map x3) x4; x2 = ArchIRQControlIssue x1 x2a x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>?Q'9 x1 x2a x3 x4\<rbrace> doMachineOp (setIRQTrigger x1 x4) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q'15 x1 x2a x3 x4\<rbrace>
 6. \<And>x1 x2a x3 x4 s. \<lbrakk>ivk' = local.irqcontrol_invocation.IssueIRQHandler x1 (cte_map x2a) (cte_map x3) x4; x2 = ArchIRQControlIssue x1 x2a x3 x4; (einvs and arch_irq_control_inv_valid (ArchIRQControlIssue x1 x2a x3 x4)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q9 x1 x2a x3 x4) s
 7. \<And>x1 x2a x3 x4 s. \<lbrakk>ivk' = local.irqcontrol_invocation.IssueIRQHandler x1 (cte_map x2a) (cte_map x3) x4; x2 = ArchIRQControlIssue x1 x2a x3 x4; (invs' and (cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (cte_map x2a) and cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQControlCap) (cte_map x3) and ex_cte_cap_wp_to' (\<lambda>_. True) (cte_map x2a) and real_cte_at' (cte_map x2a) and Not \<circ> irq_issued' x1 and (\<lambda>y. x1 \<le> maxIRQ))) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'9 x1 x2a x3 x4) s proof (prove)
goal (6 subgoals):
 1. \<And>x1 x2a x3 x4. \<lbrakk>ivk' = local.irqcontrol_invocation.IssueIRQHandler x1 (cte_map x2a) (cte_map x3) x4; x2 = ArchIRQControlIssue x1 x2a x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>?Q15 x1 x2a x3 x4\<rbrace> set_irq_state irq_state.IRQSignal x1 \<lbrace>\<lambda>x. valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and K (x3 \<noteq> x2a) and cte_wp_at (\<lambda>c. c = cap.NullCap) x2a and K (is_simple_cap (cap.IRQHandlerCap x1)) and (\<lambda>s. cte_wp_at (safe_parent_for (cdt s) x3 (cap.IRQHandlerCap x1)) x3 s)\<rbrace>
 2. \<And>x1 x2a x3 x4. \<lbrakk>ivk' = local.irqcontrol_invocation.IssueIRQHandler x1 (cte_map x2a) (cte_map x3) x4; x2 = ArchIRQControlIssue x1 x2a x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15 x1 x2a x3 x4\<rbrace> setIRQState irqstate.IRQSignal x1 \<lbrace>\<lambda>x. pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' (capability.IRQHandlerCap x1) and K (is_simple_cap' (capability.IRQHandlerCap x1)) and cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map x2a) and (\<lambda>s. safe_parent_for' (ctes_of s) (cte_map x3) (capability.IRQHandlerCap x1))\<rbrace>
 3. \<And>x1 x2a x3 x4. \<lbrakk>ivk' = local.irqcontrol_invocation.IssueIRQHandler x1 (cte_map x2a) (cte_map x3) x4; x2 = ArchIRQControlIssue x1 x2a x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>?Q9 x1 x2a x3 x4\<rbrace> do_machine_op (setIRQTrigger x1 x4) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q15 x1 x2a x3 x4\<rbrace>
 4. \<And>x1 x2a x3 x4. \<lbrakk>ivk' = local.irqcontrol_invocation.IssueIRQHandler x1 (cte_map x2a) (cte_map x3) x4; x2 = ArchIRQControlIssue x1 x2a x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>?Q'9 x1 x2a x3 x4\<rbrace> doMachineOp (setIRQTrigger x1 x4) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q'15 x1 x2a x3 x4\<rbrace>
 5. \<And>x1 x2a x3 x4 s. \<lbrakk>ivk' = local.irqcontrol_invocation.IssueIRQHandler x1 (cte_map x2a) (cte_map x3) x4; x2 = ArchIRQControlIssue x1 x2a x3 x4; (einvs and arch_irq_control_inv_valid (ArchIRQControlIssue x1 x2a x3 x4)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q9 x1 x2a x3 x4) s
 6. \<And>x1 x2a x3 x4 s. \<lbrakk>ivk' = local.irqcontrol_invocation.IssueIRQHandler x1 (cte_map x2a) (cte_map x3) x4; x2 = ArchIRQControlIssue x1 x2a x3 x4; (invs' and (cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (cte_map x2a) and cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQControlCap) (cte_map x3) and ex_cte_cap_wp_to' (\<lambda>_. True) (cte_map x2a) and real_cte_at' (cte_map x2a) and Not \<circ> irq_issued' x1 and (\<lambda>y. x1 \<le> maxIRQ))) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'9 x1 x2a x3 x4) s proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2a x3 x4 s. \<lbrakk>ivk' = local.irqcontrol_invocation.IssueIRQHandler x1 (cte_map x2a) (cte_map x3) x4; x2 = ArchIRQControlIssue x1 x2a x3 x4; invs s \<and> valid_list s \<and> valid_sched s \<and> arch_irq_control_inv_valid (ArchIRQControlIssue x1 x2a x3 x4) s\<rbrakk> \<Longrightarrow> valid_objs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_mdb s \<and> x3 \<noteq> x2a \<and> cte_wp_at (\<lambda>a. a = cap.NullCap) x2a s \<and> is_simple_cap (cap.IRQHandlerCap x1) \<and> cte_wp_at (safe_parent_for (cdt s) x3 (cap.IRQHandlerCap x1)) x3 s
 2. \<And>x1 x2a x3 x4 s. \<lbrakk>ivk' = local.irqcontrol_invocation.IssueIRQHandler x1 (cte_map x2a) (cte_map x3) x4; x2 = ArchIRQControlIssue x1 x2a x3 x4; (invs' and (cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (cte_map x2a) and cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQControlCap) (cte_map x3) and ex_cte_cap_wp_to' (\<lambda>_. True) (cte_map x2a) and real_cte_at' (cte_map x2a) and Not \<circ> irq_issued' x1 and (\<lambda>y. x1 \<le> maxIRQ))) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> pspace_distinct' s \<and> pspace_aligned' s \<and> valid_mdb' s \<and> x1 \<le> maxIRQ \<and> is_simple_cap' (capability.IRQHandlerCap x1) \<and> cte_wp_at' (\<lambda>a. cteCap a = capability.NullCap) (cte_map x2a) s \<and> safe_parent_for' (ctes_of s) (cte_map x3) (capability.IRQHandlerCap x1))) s proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2a x3 x4 s. \<lbrakk>ivk' = local.irqcontrol_invocation.IssueIRQHandler x1 (cte_map x2a) (cte_map x3) x4; x2 = ArchIRQControlIssue x1 x2a x3 x4; (invs' and (cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (cte_map x2a) and cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQControlCap) (cte_map x3) and ex_cte_cap_wp_to' (\<lambda>_. True) (cte_map x2a) and real_cte_at' (cte_map x2a) and Not \<circ> irq_issued' x1 and (\<lambda>y. x1 \<le> maxIRQ))) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> pspace_distinct' s \<and> pspace_aligned' s \<and> valid_mdb' s \<and> x1 \<le> maxIRQ \<and> is_simple_cap' (capability.IRQHandlerCap x1) \<and> cte_wp_at' (\<lambda>a. cteCap a = capability.NullCap) (cte_map x2a) s \<and> safe_parent_for' (ctes_of s) (cte_map x3) (capability.IRQHandlerCap x1))) s proof (prove)
goal (1 subgoal):
 1. \<And>x1 a b aa ba x4 s. \<lbrakk>ivk' = local.irqcontrol_invocation.IssueIRQHandler x1 (cte_map (a, b)) (cte_map (aa, ba)) x4; x2 = ArchIRQControlIssue x1 (a, b) (aa, ba) x4; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (cte_map (a, b)) s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQControlCap) (cte_map (aa, ba)) s; ex_cte_cap_wp_to' (\<lambda>_. True) (cte_map (a, b)) s; real_cte_at' (cte_map (a, b)) s; \<not> irq_issued' x1 s; x1 \<le> maxIRQ\<rbrakk> \<Longrightarrow> safe_parent_for' (ctes_of s) (cte_map (aa, ba)) (capability.IRQHandlerCap x1) proof (prove)
goal (1 subgoal):
 1. \<And>x1 a b aa ba x4 s cte ctea. \<lbrakk>ivk' = local.irqcontrol_invocation.IssueIRQHandler x1 (cte_map (a, b)) (cte_map (aa, ba)) x4; x2 = ArchIRQControlIssue x1 (a, b) (aa, ba) x4; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; ex_cte_cap_wp_to' (\<lambda>_. True) (cte_map (a, b)) s; real_cte_at' (cte_map (a, b)) s; \<not> irq_issued' x1 s; x1 \<le> maxIRQ; ctes_of s (cte_map (a, b)) = Some cte; cteCap cte = capability.NullCap; ctes_of s (cte_map (aa, ba)) = Some ctea; cteCap ctea = capability.IRQControlCap\<rbrakk> \<Longrightarrow> \<exists>parent. (\<exists>node. ctea = CTE parent node) \<and> global.sameRegionAs parent (capability.IRQHandlerCap x1) \<and> (parent = capability.IRQControlCap \<and> (\<forall>p n'. ctes_of s p \<noteq> Some (CTE (capability.IRQHandlerCap x1) n')) \<or> isUntypedCap parent \<and> descendants_of' (cte_map (aa, ba)) (ctes_of s) = {} \<and> capRange (capability.IRQHandlerCap x1) \<noteq> {}) proof (prove)
goal (1 subgoal):
 1. \<And>x1 a b aa ba x4 s cte ctea x1a x2a. \<lbrakk>ivk' = local.irqcontrol_invocation.IssueIRQHandler x1 (cte_map (a, b)) (cte_map (aa, ba)) x4; x2 = ArchIRQControlIssue x1 (a, b) (aa, ba) x4; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; ex_cte_cap_wp_to' (\<lambda>_. True) (cte_map (a, b)) s; real_cte_at' (cte_map (a, b)) s; \<not> irq_issued' x1 s; x1 \<le> maxIRQ; ctes_of s (cte_map (a, b)) = Some cte; cteCap cte = capability.NullCap; ctes_of s (cte_map (aa, ba)) = Some ctea; cteCap ctea = capability.IRQControlCap; ctea = CTE x1a x2a\<rbrakk> \<Longrightarrow> \<exists>parent. (\<exists>node. ctea = CTE parent node) \<and> global.sameRegionAs parent (capability.IRQHandlerCap x1) \<and> (parent = capability.IRQControlCap \<and> (\<forall>p n'. ctes_of s p \<noteq> Some (CTE (capability.IRQHandlerCap x1) n')) \<or> isUntypedCap parent \<and> descendants_of' (cte_map (aa, ba)) (ctes_of s) = {} \<and> capRange (capability.IRQHandlerCap x1) \<noteq> {}) proof (prove)
goal (1 subgoal):
 1. \<And>x1 a b aa ba x4 s cte x2a p n'. \<lbrakk>ivk' = local.irqcontrol_invocation.IssueIRQHandler x1 (cte_map (a, b)) (cte_map (aa, ba)) x4; x2 = ArchIRQControlIssue x1 (a, b) (aa, ba) x4; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; ex_cte_cap_wp_to' (\<lambda>_. True) (cte_map (a, b)) s; real_cte_at' (cte_map (a, b)) s; \<not> irq_issued' x1 s; x1 \<le> maxIRQ; ctes_of s (cte_map (a, b)) = Some cte; cteCap cte = capability.NullCap; ctes_of s (cte_map (aa, ba)) = Some (CTE capability.IRQControlCap x2a); ctes_of s p = Some (CTE (capability.IRQHandlerCap x1) n')\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!