theory ArchInterrupt_AI

lemma (* invoke_irq_control_invs *) [Interrupt_AI_asms]:
  "\<lbrace>invs and irq_control_inv_valid i\<rbrace> invoke_irq_control i \<lbrace>\<lambda>rv. invs\<rbrace>" apply (cases i, simp_all) apply (wp cap_insert_simple_invs
          | simp add: IRQHandler_valid is_cap_simps  no_cap_to_obj_with_diff_IRQHandler_ARCH
          | strengthen real_cte_tcb_valid)+ apply (clarsimp simp: cte_wp_at_caps_of_state
                         is_simple_cap_def is_cap_simps is_pt_cap_def
                         safe_parent_for_def
                         ex_cte_cap_to_cnode_always_appropriate_strg) apply (case_tac x2) apply (simp add: arch_irq_control_inv_valid_def) apply (wp cap_insert_simple_invs
         | simp add: IRQHandler_valid is_cap_simps  no_cap_to_obj_with_diff_IRQHandler_ARCH
         | strengthen real_cte_tcb_valid)+ apply (clarsimp simp: cte_wp_at_caps_of_state
                        is_simple_cap_def is_cap_simps is_pt_cap_def
                        safe_parent_for_def
                        ex_cte_cap_to_cnode_always_appropriate_strg) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and irq_control_inv_valid i\<rbrace> invoke_irq_control i \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x11 x12 x13. i = IRQControl x11 x12 x13 \<Longrightarrow> \<lbrace>invs 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> liftE (do y <- set_irq_state IRQSignal x11;
cap_insert (IRQHandlerCap x11) x13 x12
od) \<lbrace>\<lambda>rv. invs\<rbrace>
 2. \<And>x2. i = ArchIRQControl x2 \<Longrightarrow> \<lbrace>invs and arch_irq_control_inv_valid x2\<rbrace> arch_invoke_irq_control x2 \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x11 x12 x13 s. \<lbrakk>i = IRQControl x11 x12 x13; invs 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> ex_cte_cap_wp_to (appropriate_cte_cap (IRQHandlerCap x11)) x12 s \<and> cte_wp_at (\<lambda>a. (\<exists>dev r bits f. a = UntypedCap dev r bits f) \<longrightarrow> usable_untyped_range a = {}) x13 s \<and> cte_wp_at (\<lambda>a. a = NullCap) x12 s \<and> cte_wp_at (safe_parent_for (cdt s) x13 (IRQHandlerCap x11)) x13 s \<and> is_simple_cap (IRQHandlerCap x11)
 2. \<And>x2. i = ArchIRQControl x2 \<Longrightarrow> \<lbrace>invs and arch_irq_control_inv_valid x2\<rbrace> arch_invoke_irq_control x2 \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x2. i = ArchIRQControl x2 \<Longrightarrow> \<lbrace>invs and arch_irq_control_inv_valid x2\<rbrace> arch_invoke_irq_control x2 \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x2 x1 x2a x3 x4. \<lbrakk>i = ArchIRQControl x2; x2 = ArchIRQControlIssue x1 x2a x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>invs and arch_irq_control_inv_valid x2\<rbrace> arch_invoke_irq_control x2 \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x2 x1 x2a x3 x4. \<lbrakk>i = ArchIRQControl (ArchIRQControlIssue x1 x2a x3 x4); x2 = ArchIRQControlIssue x1 x2a x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>invs and (cte_wp_at ((=) NullCap) x2a and cte_wp_at ((=) IRQControlCap) x3 and ex_cte_cap_wp_to is_cnode_cap x2a and real_cte_at x2a and (\<lambda>y. x1 \<le> maxIRQ))\<rbrace> liftE (do y <- do_machine_op (setIRQTrigger x1 x4);
y <- set_irq_state IRQSignal x1;
cap_insert (IRQHandlerCap x1) x3 x2a
od) \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x2 x1 x2a x3 x4 s. \<lbrakk>i = ArchIRQControl (ArchIRQControlIssue x1 x2a x3 x4); x2 = ArchIRQControlIssue x1 x2a x3 x4; invs s \<and> cte_wp_at ((=) NullCap) x2a s \<and> cte_wp_at ((=) IRQControlCap) x3 s \<and> ex_cte_cap_wp_to is_cnode_cap x2a s \<and> real_cte_at x2a s \<and> x1 \<le> maxIRQ\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap (IRQHandlerCap x1)) x2a s \<and> cte_wp_at (\<lambda>a. (\<exists>dev r bits f. a = UntypedCap dev r bits f) \<longrightarrow> usable_untyped_range a = {}) x3 s \<and> cte_wp_at (\<lambda>a. a = NullCap) x2a s \<and> cte_wp_at (safe_parent_for (cdt s) x3 (IRQHandlerCap x1)) x3 s \<and> is_simple_cap (IRQHandlerCap x1) proof (prove)
goal:
No subgoals!