theory Interrupt_R

lemma invoke_irq_control_invs'[wp]:
  "\<lbrace>invs' and irq_control_inv_valid' i\<rbrace> performIRQControl i \<lbrace>\<lambda>rv. invs'\<rbrace>" apply (cases i, simp_all add: performIRQControl_def) apply (rule hoare_pre) apply (wp cteInsert_simple_invs | simp add: cte_wp_at_ctes_of)+ apply (clarsimp simp: cte_wp_at_ctes_of IRQHandler_valid'
                        is_simple_cap'_def isCap_simps
                        safe_parent_for'_def sameRegionAs_def3) apply (case_tac ctea) apply (auto dest: valid_irq_handlers_ctes_ofD
              simp: invs'_def valid_state'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and irq_control_inv_valid' i\<rbrace> global.performIRQControl i \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x1. i = irqcontrol_invocation.ArchIRQControl x1 \<Longrightarrow> \<lbrace>invs' and arch_irq_control_inv_valid' x1\<rbrace> Arch.performIRQControl x1 \<lbrace>\<lambda>rv. invs'\<rbrace>
 2. \<And>x21 x22 x23. i = Invocations_H.irqcontrol_invocation.IssueIRQHandler x21 x22 x23 \<Longrightarrow> \<lbrace>invs' and (cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x22 and cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQControlCap) x23 and ex_cte_cap_wp_to' (\<lambda>_. True) x22 and real_cte_at' x22 and Not \<circ> irq_issued' x21 and (\<lambda>y. x21 \<le> maxIRQ))\<rbrace> liftE (do y <- setIRQState irqstate.IRQSignal x21;
cteInsert (capability.IRQHandlerCap x21) x23 x22
od) \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x1. i = irqcontrol_invocation.ArchIRQControl x1 \<Longrightarrow> \<lbrace>?Q2 x1\<rbrace> Arch.performIRQControl x1 \<lbrace>\<lambda>rv. invs'\<rbrace>
 2. \<And>x1 s. \<lbrakk>i = irqcontrol_invocation.ArchIRQControl x1; (invs' and arch_irq_control_inv_valid' x1) s\<rbrakk> \<Longrightarrow> ?Q2 x1 s
 3. \<And>x21 x22 x23. i = Invocations_H.irqcontrol_invocation.IssueIRQHandler x21 x22 x23 \<Longrightarrow> \<lbrace>invs' and (cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x22 and cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQControlCap) x23 and ex_cte_cap_wp_to' (\<lambda>_. True) x22 and real_cte_at' x22 and Not \<circ> irq_issued' x21 and (\<lambda>y. x21 \<le> maxIRQ))\<rbrace> liftE (do y <- setIRQState irqstate.IRQSignal x21;
cteInsert (capability.IRQHandlerCap x21) x23 x22
od) \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x21 x22 x23 s. \<lbrakk>i = Invocations_H.irqcontrol_invocation.IssueIRQHandler x21 x22 x23; invs' s \<and> (\<exists>cte. ctes_of s x22 = Some cte \<and> cteCap cte = capability.NullCap) \<and> (\<exists>cte. ctes_of s x23 = Some cte \<and> cteCap cte = capability.IRQControlCap) \<and> ex_cte_cap_wp_to' (\<lambda>_. True) x22 s \<and> real_cte_at' x22 s \<and> \<not> irq_issued' x21 s \<and> x21 \<le> maxIRQ\<rbrakk> \<Longrightarrow> valid_cap' (capability.IRQHandlerCap x21) s \<and> x23 \<noteq> x22 \<and> safe_parent_for' (ctes_of s) x23 (capability.IRQHandlerCap x21) \<and> (\<exists>cte. ctes_of s x23 = Some cte) \<and> is_simple_cap' (capability.IRQHandlerCap x21) proof (prove)
goal (1 subgoal):
 1. \<And>x21 x22 x23 s cte ctea. \<lbrakk>i = Invocations_H.irqcontrol_invocation.IssueIRQHandler x21 x22 x23; invs' s; ctes_of s x22 = Some cte; cteCap cte = capability.NullCap; ex_cte_cap_wp_to' (\<lambda>_. True) x22 s; ctes_of s x23 = Some ctea; cteCap ctea = capability.IRQControlCap; real_cte_at' x22 s; \<not> irq_issued' x21 s; x21 \<le> maxIRQ\<rbrakk> \<Longrightarrow> x23 \<noteq> x22 \<and> (\<exists>parent. (\<exists>node. ctea = CTE parent node) \<and> (capMasterCap parent = capability.IRQHandlerCap x21 \<and> parent \<noteq> capability.NullCap \<and> (\<forall>v0 v1 v2. parent \<noteq> capability.Zombie v0 v1 v2) \<and> (\<forall>d v0 v1 f. parent \<noteq> capability.UntypedCap d v0 v1 f) \<and> (\<forall>d ref rghts sz data. parent \<noteq> capability.ArchObjectCap (arch_capability.PageCap d ref rghts sz data)) \<or> capRange (capability.IRQHandlerCap x21) \<noteq> {} \<and> capRange (capability.IRQHandlerCap x21) \<subseteq> capRange parent \<and> (\<exists>d v0 v1 f. parent = capability.UntypedCap d v0 v1 f) \<or> parent = capability.IRQControlCap) \<and> (parent = capability.IRQControlCap \<and> (\<forall>p n'. ctes_of s p \<noteq> Some (CTE (capability.IRQHandlerCap x21) n')) \<or> (\<exists>d v0 v1 f. parent = capability.UntypedCap d v0 v1 f) \<and> descendants_of' x23 (ctes_of s) = {} \<and> capRange (capability.IRQHandlerCap x21) \<noteq> {})) proof (prove)
goal (1 subgoal):
 1. \<And>x21 x22 x23 s cte ctea x1 x2. \<lbrakk>i = Invocations_H.irqcontrol_invocation.IssueIRQHandler x21 x22 x23; invs' s; ctes_of s x22 = Some cte; cteCap cte = capability.NullCap; ex_cte_cap_wp_to' (\<lambda>_. True) x22 s; ctes_of s x23 = Some ctea; cteCap ctea = capability.IRQControlCap; real_cte_at' x22 s; \<not> irq_issued' x21 s; x21 \<le> maxIRQ; ctea = CTE x1 x2\<rbrakk> \<Longrightarrow> x23 \<noteq> x22 \<and> (\<exists>parent. (\<exists>node. ctea = CTE parent node) \<and> (capMasterCap parent = capability.IRQHandlerCap x21 \<and> parent \<noteq> capability.NullCap \<and> (\<forall>v0 v1 v2. parent \<noteq> capability.Zombie v0 v1 v2) \<and> (\<forall>d v0 v1 f. parent \<noteq> capability.UntypedCap d v0 v1 f) \<and> (\<forall>d ref rghts sz data. parent \<noteq> capability.ArchObjectCap (arch_capability.PageCap d ref rghts sz data)) \<or> capRange (capability.IRQHandlerCap x21) \<noteq> {} \<and> capRange (capability.IRQHandlerCap x21) \<subseteq> capRange parent \<and> (\<exists>d v0 v1 f. parent = capability.UntypedCap d v0 v1 f) \<or> parent = capability.IRQControlCap) \<and> (parent = capability.IRQControlCap \<and> (\<forall>p n'. ctes_of s p \<noteq> Some (CTE (capability.IRQHandlerCap x21) n')) \<or> (\<exists>d v0 v1 f. parent = capability.UntypedCap d v0 v1 f) \<and> descendants_of' x23 (ctes_of s) = {} \<and> capRange (capability.IRQHandlerCap x21) \<noteq> {})) proof (prove)
goal:
No subgoals!