theory Interrupt_R

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and arch_irq_control_inv_valid' i\<rbrace> Arch.performIRQControl i \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and arch_irq_control_inv_valid' i\<rbrace> case i of local.irqcontrol_invocation.IssueIRQHandler irq destSlot srcSlot trigger \<Rightarrow> withoutPreemption $ do doMachineOp $ setIRQTrigger irq trigger;
setIRQState irqstate.IRQSignal (IRQ irq);
cteInsert (capability.IRQHandlerCap (IRQ irq)) srcSlot destSlot;
return ()
od \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> case i of local.irqcontrol_invocation.IssueIRQHandler irq destSlot srcSlot trigger \<Rightarrow> withoutPreemption $ do doMachineOp $ setIRQTrigger irq trigger;
setIRQState irqstate.IRQSignal (IRQ irq);
cteInsert (capability.IRQHandlerCap (IRQ irq)) srcSlot destSlot;
return ()
od \<lbrace>\<lambda>rv. invs'\<rbrace>
 2. \<And>s. (invs' and arch_irq_control_inv_valid' i) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. invs' s \<and> arch_irq_control_inv_valid' i s \<Longrightarrow> \<forall>x xa xb. (\<exists>xc. i = local.irqcontrol_invocation.IssueIRQHandler x xa xb xc) \<longrightarrow> x \<le> maxIRQ \<and> (\<exists>cte. ctes_of s xa = Some cte \<and> cteCap cte = capability.NullCap) \<and> valid_cap' (capability.IRQHandlerCap x) s \<and> xb \<noteq> xa \<and> safe_parent_for' (ctes_of s) xb (capability.IRQHandlerCap x) \<and> (\<exists>cte. ctes_of s xb = Some cte) \<and> ex_cte_cap_wp_to' (\<lambda>_. True) xa s \<and> is_simple_cap' (capability.IRQHandlerCap x) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa xb xc cte ctea. \<lbrakk>invs' s; i = local.irqcontrol_invocation.IssueIRQHandler x xa xb xc; ctes_of s xa = Some cte; cteCap cte = capability.NullCap; ex_cte_cap_wp_to' (\<lambda>_. True) xa s; ctes_of s xb = Some ctea; cteCap ctea = capability.IRQControlCap; real_cte_at' xa s; \<not> irq_issued' x s; x \<le> maxIRQ\<rbrakk> \<Longrightarrow> xb \<noteq> xa \<and> (\<exists>parent. (\<exists>node. ctea = CTE parent node) \<and> (capMasterCap parent = capability.IRQHandlerCap x \<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 x) \<noteq> {} \<and> capRange (capability.IRQHandlerCap x) \<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 x) n')) \<or> (\<exists>d v0 v1 f. parent = capability.UntypedCap d v0 v1 f) \<and> descendants_of' xb (ctes_of s) = {} \<and> capRange (capability.IRQHandlerCap x) \<noteq> {})) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa xb xc cte ctea. \<lbrakk>invs' s; i = local.irqcontrol_invocation.IssueIRQHandler x xa xb xc; ctes_of s xa = Some cte; cteCap cte = capability.NullCap; ex_cte_cap_wp_to' (\<lambda>_. True) xa s; ctes_of s xb = Some ctea; cteCap ctea = capability.IRQControlCap; real_cte_at' xa s; \<not> irq_issued' x s; x \<le> maxIRQ\<rbrakk> \<Longrightarrow> \<exists>parent. (\<exists>node. ctea = CTE parent node) \<and> (capMasterCap parent = capability.IRQHandlerCap x \<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 x) \<noteq> {} \<and> capRange (capability.IRQHandlerCap x) \<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 x) n')) \<or> (\<exists>d v0 v1 f. parent = capability.UntypedCap d v0 v1 f) \<and> descendants_of' xb (ctes_of s) = {} \<and> capRange (capability.IRQHandlerCap x) \<noteq> {}) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa xb xc cte ctea x1 x2. \<lbrakk>invs' s; i = local.irqcontrol_invocation.IssueIRQHandler x xa xb xc; ctes_of s xa = Some cte; cteCap cte = capability.NullCap; ex_cte_cap_wp_to' (\<lambda>_. True) xa s; ctes_of s xb = Some ctea; cteCap ctea = capability.IRQControlCap; real_cte_at' xa s; \<not> irq_issued' x s; x \<le> maxIRQ; ctea = CTE x1 x2\<rbrakk> \<Longrightarrow> \<exists>parent. (\<exists>node. ctea = CTE parent node) \<and> (capMasterCap parent = capability.IRQHandlerCap x \<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 x) \<noteq> {} \<and> capRange (capability.IRQHandlerCap x) \<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 x) n')) \<or> (\<exists>d v0 v1 f. parent = capability.UntypedCap d v0 v1 f) \<and> descendants_of' xb (ctes_of s) = {} \<and> capRange (capability.IRQHandlerCap x) \<noteq> {}) proof (prove)
goal:
No subgoals!