theory IRQMasks_IF

lemma decode_invocation_IRQHandlerCap:
  "\<lbrace>cte_wp_at ((=) cap) slot\<rbrace>
   decode_invocation label args cap_index slot cap blah
   \<lbrace>\<lambda>rv s. \<forall>x. rv = InvokeIRQHandler x
               \<longrightarrow> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap (irq_of_handler_inv x))) (a, b) s)\<rbrace>, -" apply (simp add: decode_invocation_def split del: if_split) apply (rule hoare_pre) apply (wp | wpc | simp add: o_def)+ apply (rule hoare_post_imp_R[where Q'="\<top>\<top>"]) apply wp apply (clarsimp simp: uncurry_def) apply (wp | wpc | simp add: decode_irq_handler_invocation_def o_def split del: if_split)+ apply (safe | simp add: op_equal | rule exI[where x="fst slot"] exI[where x="snd slot"])+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at ((=) cap) slot\<rbrace> decode_invocation label args cap_index slot cap blah \<lbrace>\<lambda>rv s. \<forall>x. rv = InvokeIRQHandler x \<longrightarrow> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap (irq_of_handler_inv x))) (a, b) s)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at ((=) cap) slot\<rbrace> case cap of UntypedCap dev ptr sz fi \<Rightarrow> liftME InvokeUntyped $ decode_untyped_invocation label args slot cap (map fst blah) | EndpointCap ptr badge rights \<Rightarrow> if AllowSend \<in> rights then returnOk $ InvokeEndpoint ptr badge (AllowGrant \<in> rights) (AllowGrantReply \<in> rights) else throwError $ InvalidCapability 0 | NotificationCap ptr badge rights \<Rightarrow> if AllowSend \<in> rights then returnOk $ InvokeNotification ptr badge else throwError $ InvalidCapability 0 | ReplyCap thread True rights \<Rightarrow> throwError $ InvalidCapability 0 | ReplyCap thread False rights \<Rightarrow> returnOk $ InvokeReply thread slot (AllowGrant \<in> rights) | CNodeCap ptr bits x \<Rightarrow> liftME InvokeCNode $ decode_cnode_invocation label args cap (map fst blah) | ThreadCap ptr \<Rightarrow> liftME InvokeTCB $ decode_tcb_invocation label args cap slot blah | DomainCap \<Rightarrow> liftME (\<lambda>(x, y). InvokeDomain x y) $ decode_domain_invocation label args blah | IRQControlCap \<Rightarrow> liftME InvokeIRQControl $ decode_irq_control_invocation label args slot (map fst blah) | IRQHandlerCap irq \<Rightarrow> liftME InvokeIRQHandler $ decode_irq_handler_invocation label irq blah | ArchObjectCap arch_cap \<Rightarrow> liftME InvokeArchObject $ arch_decode_invocation label args cap_index slot arch_cap blah | _ \<Rightarrow> throwError $ InvalidCapability 0 \<lbrace>\<lambda>rv s. \<forall>x. rv = InvokeIRQHandler x \<longrightarrow> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap (irq_of_handler_inv x))) (a, b) s)\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> case cap of UntypedCap dev ptr sz fi \<Rightarrow> liftME InvokeUntyped $ decode_untyped_invocation label args slot cap (map fst blah) | EndpointCap ptr badge rights \<Rightarrow> if AllowSend \<in> rights then returnOk $ InvokeEndpoint ptr badge (AllowGrant \<in> rights) (AllowGrantReply \<in> rights) else throwError $ InvalidCapability 0 | NotificationCap ptr badge rights \<Rightarrow> if AllowSend \<in> rights then returnOk $ InvokeNotification ptr badge else throwError $ InvalidCapability 0 | ReplyCap thread True rights \<Rightarrow> throwError $ InvalidCapability 0 | ReplyCap thread False rights \<Rightarrow> returnOk $ InvokeReply thread slot (AllowGrant \<in> rights) | CNodeCap ptr bits x \<Rightarrow> liftME InvokeCNode $ decode_cnode_invocation label args cap (map fst blah) | ThreadCap ptr \<Rightarrow> liftME InvokeTCB $ decode_tcb_invocation label args cap slot blah | DomainCap \<Rightarrow> liftME (\<lambda>(x, y). InvokeDomain x y) $ decode_domain_invocation label args blah | IRQControlCap \<Rightarrow> liftME InvokeIRQControl $ decode_irq_control_invocation label args slot (map fst blah) | IRQHandlerCap irq \<Rightarrow> liftME InvokeIRQHandler $ decode_irq_handler_invocation label irq blah | ArchObjectCap arch_cap \<Rightarrow> liftME InvokeArchObject $ arch_decode_invocation label args cap_index slot arch_cap blah | _ \<Rightarrow> throwError $ InvalidCapability 0 \<lbrace>\<lambda>rv s. \<forall>x. rv = InvokeIRQHandler x \<longrightarrow> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap (irq_of_handler_inv x))) (a, b) s)\<rbrace>, -
 2. \<And>s. cte_wp_at ((=) cap) slot s \<Longrightarrow> ?P' s proof (prove)
goal (6 subgoals):
 1. cap = DomainCap \<Longrightarrow> \<lbrace>?R59\<rbrace> decode_domain_invocation label args blah \<lbrace>\<lambda>x s. \<forall>xa. (case x of (x, xa) \<Rightarrow> InvokeDomain x xa) = InvokeIRQHandler xa \<longrightarrow> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap (irq_of_handler_inv xa))) (a, b) s)\<rbrace>, -
 2. cap = IRQControlCap \<Longrightarrow> \<lbrace>?R60\<rbrace> liftME InvokeIRQControl $ decode_irq_control_invocation label args slot (map fst blah) \<lbrace>\<lambda>rv s. \<forall>x. rv = InvokeIRQHandler x \<longrightarrow> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap (irq_of_handler_inv x))) (a, b) s)\<rbrace>, -
 3. \<And>x10. cap = IRQHandlerCap x10 \<Longrightarrow> \<lbrace>?R61 x10\<rbrace> liftME InvokeIRQHandler $ decode_irq_handler_invocation label x10 blah \<lbrace>\<lambda>rv s. \<forall>x. rv = InvokeIRQHandler x \<longrightarrow> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap (irq_of_handler_inv x))) (a, b) s)\<rbrace>, -
 4. \<And>x111 x112 x113. cap = Zombie x111 x112 x113 \<Longrightarrow> \<lbrace>?R62 x111 x112 x113\<rbrace> throwError $ InvalidCapability 0 \<lbrace>\<lambda>rv s. \<forall>x. rv = InvokeIRQHandler x \<longrightarrow> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap (irq_of_handler_inv x))) (a, b) s)\<rbrace>, -
 5. \<And>x12. cap = ArchObjectCap x12 \<Longrightarrow> \<lbrace>?R63 x12\<rbrace> liftME InvokeArchObject $ arch_decode_invocation label args cap_index slot x12 blah \<lbrace>\<lambda>rv s. \<forall>x. rv = InvokeIRQHandler x \<longrightarrow> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap (irq_of_handler_inv x))) (a, b) s)\<rbrace>, -
 6. \<And>s. cte_wp_at ((=) cap) slot s \<Longrightarrow> (cap = NullCap \<longrightarrow> True) \<and> (\<forall>x xa xb xc. cap = UntypedCap x xa xb xc \<longrightarrow> ?R53 x xa xb xc s) \<and> (\<forall>x xa xb. cap = EndpointCap x xa xb \<longrightarrow> (AllowSend \<in> xb \<longrightarrow> (\<forall>xc. InvokeEndpoint x xa (AllowGrant \<in> xb) (AllowGrantReply \<in> xb) = InvokeIRQHandler xc \<longrightarrow> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap (irq_of_handler_inv xc))) (a, b) s))) \<and> (AllowSend \<notin> xb \<longrightarrow> True)) \<and> (\<forall>x xa xb. cap = NotificationCap x xa xb \<longrightarrow> (AllowSend \<in> xb \<longrightarrow> (\<forall>xb. InvokeNotification x xa = InvokeIRQHandler xb \<longrightarrow> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap (irq_of_handler_inv xb))) (a, b) s))) \<and> (AllowSend \<notin> xb \<longrightarrow> True)) \<and> (\<forall>x xa xb. cap = ReplyCap x xa xb \<longrightarrow> (xa = True \<longrightarrow> True) \<and> (xa = False \<longrightarrow> (\<forall>xa. InvokeReply x slot (AllowGrant \<in> xb) = InvokeIRQHandler xa \<longrightarrow> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap (irq_of_handler_inv xa))) (a, b) s)))) \<and> (\<forall>x xa xb. cap = CNodeCap x xa xb \<longrightarrow> ?R57 x xa xb s) \<and> (\<forall>x. cap = ThreadCap x \<longrightarrow> ?R58 x s) \<and> (cap = DomainCap \<longrightarrow> ?R59 s) \<and> (cap = IRQControlCap \<longrightarrow> ?R60 s) \<and> (\<forall>x. cap = IRQHandlerCap x \<longrightarrow> ?R61 x s) \<and> (\<forall>x xa xb. cap = Zombie x xa xb \<longrightarrow> ?R62 x xa xb s) \<and> (\<forall>x. cap = ArchObjectCap x \<longrightarrow> ?R63 x s) proof (prove)
goal (7 subgoals):
 1. cap = DomainCap \<Longrightarrow> \<lbrace>?R59\<rbrace> decode_domain_invocation label args blah \<lbrace>\<lambda>_ _. True\<rbrace>, -
 2. \<And>rv s. \<lbrakk>cap = DomainCap; True\<rbrakk> \<Longrightarrow> \<forall>x. (case rv of (x, xa) \<Rightarrow> InvokeDomain x xa) = InvokeIRQHandler x \<longrightarrow> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap (irq_of_handler_inv x))) (a, b) s)
 3. cap = IRQControlCap \<Longrightarrow> \<lbrace>?R60\<rbrace> liftME InvokeIRQControl $ decode_irq_control_invocation label args slot (map fst blah) \<lbrace>\<lambda>rv s. \<forall>x. rv = InvokeIRQHandler x \<longrightarrow> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap (irq_of_handler_inv x))) (a, b) s)\<rbrace>, -
 4. \<And>x10. cap = IRQHandlerCap x10 \<Longrightarrow> \<lbrace>?R61 x10\<rbrace> liftME InvokeIRQHandler $ decode_irq_handler_invocation label x10 blah \<lbrace>\<lambda>rv s. \<forall>x. rv = InvokeIRQHandler x \<longrightarrow> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap (irq_of_handler_inv x))) (a, b) s)\<rbrace>, -
 5. \<And>x111 x112 x113. cap = Zombie x111 x112 x113 \<Longrightarrow> \<lbrace>?R62 x111 x112 x113\<rbrace> throwError $ InvalidCapability 0 \<lbrace>\<lambda>rv s. \<forall>x. rv = InvokeIRQHandler x \<longrightarrow> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap (irq_of_handler_inv x))) (a, b) s)\<rbrace>, -
 6. \<And>x12. cap = ArchObjectCap x12 \<Longrightarrow> \<lbrace>?R63 x12\<rbrace> liftME InvokeArchObject $ arch_decode_invocation label args cap_index slot x12 blah \<lbrace>\<lambda>rv s. \<forall>x. rv = InvokeIRQHandler x \<longrightarrow> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap (irq_of_handler_inv x))) (a, b) s)\<rbrace>, -
 7. \<And>s. cte_wp_at ((=) cap) slot s \<Longrightarrow> (cap = NullCap \<longrightarrow> True) \<and> (\<forall>x xa xb xc. cap = UntypedCap x xa xb xc \<longrightarrow> ?R53 x xa xb xc s) \<and> (\<forall>x xa xb. cap = EndpointCap x xa xb \<longrightarrow> (AllowSend \<in> xb \<longrightarrow> (\<forall>xc. InvokeEndpoint x xa (AllowGrant \<in> xb) (AllowGrantReply \<in> xb) = InvokeIRQHandler xc \<longrightarrow> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap (irq_of_handler_inv xc))) (a, b) s))) \<and> (AllowSend \<notin> xb \<longrightarrow> True)) \<and> (\<forall>x xa xb. cap = NotificationCap x xa xb \<longrightarrow> (AllowSend \<in> xb \<longrightarrow> (\<forall>xb. InvokeNotification x xa = InvokeIRQHandler xb \<longrightarrow> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap (irq_of_handler_inv xb))) (a, b) s))) \<and> (AllowSend \<notin> xb \<longrightarrow> True)) \<and> (\<forall>x xa xb. cap = ReplyCap x xa xb \<longrightarrow> (xa = True \<longrightarrow> True) \<and> (xa = False \<longrightarrow> (\<forall>xa. InvokeReply x slot (AllowGrant \<in> xb) = InvokeIRQHandler xa \<longrightarrow> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap (irq_of_handler_inv xa))) (a, b) s)))) \<and> (\<forall>x xa xb. cap = CNodeCap x xa xb \<longrightarrow> ?R57 x xa xb s) \<and> (\<forall>x. cap = ThreadCap x \<longrightarrow> ?R58 x s) \<and> (cap = DomainCap \<longrightarrow> ?R59 s) \<and> (cap = IRQControlCap \<longrightarrow> ?R60 s) \<and> (\<forall>x. cap = IRQHandlerCap x \<longrightarrow> ?R61 x s) \<and> (\<forall>x xa xb. cap = Zombie x xa xb \<longrightarrow> ?R62 x xa xb s) \<and> (\<forall>x. cap = ArchObjectCap x \<longrightarrow> ?R63 x s) proof (prove)
goal (6 subgoals):
 1. \<And>rv s. \<lbrakk>cap = DomainCap; True\<rbrakk> \<Longrightarrow> \<forall>x. (case rv of (x, xa) \<Rightarrow> InvokeDomain x xa) = InvokeIRQHandler x \<longrightarrow> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap (irq_of_handler_inv x))) (a, b) s)
 2. cap = IRQControlCap \<Longrightarrow> \<lbrace>?R60\<rbrace> liftME InvokeIRQControl $ decode_irq_control_invocation label args slot (map fst blah) \<lbrace>\<lambda>rv s. \<forall>x. rv = InvokeIRQHandler x \<longrightarrow> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap (irq_of_handler_inv x))) (a, b) s)\<rbrace>, -
 3. \<And>x10. cap = IRQHandlerCap x10 \<Longrightarrow> \<lbrace>?R61 x10\<rbrace> liftME InvokeIRQHandler $ decode_irq_handler_invocation label x10 blah \<lbrace>\<lambda>rv s. \<forall>x. rv = InvokeIRQHandler x \<longrightarrow> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap (irq_of_handler_inv x))) (a, b) s)\<rbrace>, -
 4. \<And>x111 x112 x113. cap = Zombie x111 x112 x113 \<Longrightarrow> \<lbrace>?R62 x111 x112 x113\<rbrace> throwError $ InvalidCapability 0 \<lbrace>\<lambda>rv s. \<forall>x. rv = InvokeIRQHandler x \<longrightarrow> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap (irq_of_handler_inv x))) (a, b) s)\<rbrace>, -
 5. \<And>x12. cap = ArchObjectCap x12 \<Longrightarrow> \<lbrace>?R63 x12\<rbrace> liftME InvokeArchObject $ arch_decode_invocation label args cap_index slot x12 blah \<lbrace>\<lambda>rv s. \<forall>x. rv = InvokeIRQHandler x \<longrightarrow> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap (irq_of_handler_inv x))) (a, b) s)\<rbrace>, -
 6. \<And>s. cte_wp_at ((=) cap) slot s \<Longrightarrow> (cap = NullCap \<longrightarrow> True) \<and> (\<forall>x xa xb xc. cap = UntypedCap x xa xb xc \<longrightarrow> ?R53 x xa xb xc s) \<and> (\<forall>x xa xb. cap = EndpointCap x xa xb \<longrightarrow> (AllowSend \<in> xb \<longrightarrow> (\<forall>xc. InvokeEndpoint x xa (AllowGrant \<in> xb) (AllowGrantReply \<in> xb) = InvokeIRQHandler xc \<longrightarrow> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap (irq_of_handler_inv xc))) (a, b) s))) \<and> (AllowSend \<notin> xb \<longrightarrow> True)) \<and> (\<forall>x xa xb. cap = NotificationCap x xa xb \<longrightarrow> (AllowSend \<in> xb \<longrightarrow> (\<forall>xb. InvokeNotification x xa = InvokeIRQHandler xb \<longrightarrow> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap (irq_of_handler_inv xb))) (a, b) s))) \<and> (AllowSend \<notin> xb \<longrightarrow> True)) \<and> (\<forall>x xa xb. cap = ReplyCap x xa xb \<longrightarrow> (xa = True \<longrightarrow> True) \<and> (xa = False \<longrightarrow> (\<forall>xa. InvokeReply x slot (AllowGrant \<in> xb) = InvokeIRQHandler xa \<longrightarrow> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap (irq_of_handler_inv xa))) (a, b) s)))) \<and> (\<forall>x xa xb. cap = CNodeCap x xa xb \<longrightarrow> ?R57 x xa xb s) \<and> (\<forall>x. cap = ThreadCap x \<longrightarrow> ?R58 x s) \<and> (cap = DomainCap \<longrightarrow> True) \<and> (cap = IRQControlCap \<longrightarrow> ?R60 s) \<and> (\<forall>x. cap = IRQHandlerCap x \<longrightarrow> ?R61 x s) \<and> (\<forall>x xa xb. cap = Zombie x xa xb \<longrightarrow> ?R62 x xa xb s) \<and> (\<forall>x. cap = ArchObjectCap x \<longrightarrow> ?R63 x s) proof (prove)
goal (5 subgoals):
 1. cap = IRQControlCap \<Longrightarrow> \<lbrace>?R60\<rbrace> liftME InvokeIRQControl $ decode_irq_control_invocation label args slot (map fst blah) \<lbrace>\<lambda>rv s. \<forall>x. rv = InvokeIRQHandler x \<longrightarrow> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap (irq_of_handler_inv x))) (a, b) s)\<rbrace>, -
 2. \<And>x10. cap = IRQHandlerCap x10 \<Longrightarrow> \<lbrace>?R61 x10\<rbrace> liftME InvokeIRQHandler $ decode_irq_handler_invocation label x10 blah \<lbrace>\<lambda>rv s. \<forall>x. rv = InvokeIRQHandler x \<longrightarrow> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap (irq_of_handler_inv x))) (a, b) s)\<rbrace>, -
 3. \<And>x111 x112 x113. cap = Zombie x111 x112 x113 \<Longrightarrow> \<lbrace>?R62 x111 x112 x113\<rbrace> throwError $ InvalidCapability 0 \<lbrace>\<lambda>rv s. \<forall>x. rv = InvokeIRQHandler x \<longrightarrow> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap (irq_of_handler_inv x))) (a, b) s)\<rbrace>, -
 4. \<And>x12. cap = ArchObjectCap x12 \<Longrightarrow> \<lbrace>?R63 x12\<rbrace> liftME InvokeArchObject $ arch_decode_invocation label args cap_index slot x12 blah \<lbrace>\<lambda>rv s. \<forall>x. rv = InvokeIRQHandler x \<longrightarrow> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap (irq_of_handler_inv x))) (a, b) s)\<rbrace>, -
 5. \<And>s. cte_wp_at ((=) cap) slot s \<Longrightarrow> (cap = NullCap \<longrightarrow> True) \<and> (\<forall>x xa xb xc. cap = UntypedCap x xa xb xc \<longrightarrow> ?R53 x xa xb xc s) \<and> (\<forall>x xa xb. cap = EndpointCap x xa xb \<longrightarrow> (AllowSend \<in> xb \<longrightarrow> (\<forall>xc. InvokeEndpoint x xa (AllowGrant \<in> xb) (AllowGrantReply \<in> xb) = InvokeIRQHandler xc \<longrightarrow> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap (irq_of_handler_inv xc))) (a, b) s))) \<and> (AllowSend \<notin> xb \<longrightarrow> True)) \<and> (\<forall>x xa xb. cap = NotificationCap x xa xb \<longrightarrow> (AllowSend \<in> xb \<longrightarrow> (\<forall>xb. InvokeNotification x xa = InvokeIRQHandler xb \<longrightarrow> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap (irq_of_handler_inv xb))) (a, b) s))) \<and> (AllowSend \<notin> xb \<longrightarrow> True)) \<and> (\<forall>x xa xb. cap = ReplyCap x xa xb \<longrightarrow> (xa = True \<longrightarrow> True) \<and> (xa = False \<longrightarrow> (\<forall>xa. InvokeReply x slot (AllowGrant \<in> xb) = InvokeIRQHandler xa \<longrightarrow> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap (irq_of_handler_inv xa))) (a, b) s)))) \<and> (\<forall>x xa xb. cap = CNodeCap x xa xb \<longrightarrow> ?R57 x xa xb s) \<and> (\<forall>x. cap = ThreadCap x \<longrightarrow> ?R58 x s) \<and> (cap = DomainCap \<longrightarrow> True) \<and> (cap = IRQControlCap \<longrightarrow> ?R60 s) \<and> (\<forall>x. cap = IRQHandlerCap x \<longrightarrow> ?R61 x s) \<and> (\<forall>x xa xb. cap = Zombie x xa xb \<longrightarrow> ?R62 x xa xb s) \<and> (\<forall>x. cap = ArchObjectCap x \<longrightarrow> ?R63 x s) proof (prove)
goal (1 subgoal):
 1. \<And>s. cte_wp_at ((=) cap) slot s \<Longrightarrow> (\<forall>x xa xb xc. cap = UntypedCap x xa xb xc \<longrightarrow> ?R53 x xa xb xc s) \<and> (\<forall>x xa xb. cap = CNodeCap x xa xb \<longrightarrow> ?R57 x xa xb s) \<and> (\<forall>x. cap = ThreadCap x \<longrightarrow> ?R58 x s) \<and> (cap = IRQControlCap \<longrightarrow> ?R60 s) \<and> (\<forall>x. cap = IRQHandlerCap x \<longrightarrow> (gen_invocation_type label = IRQAckIRQ \<longrightarrow> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap x)) (a, b) s)) \<and> (gen_invocation_type label \<noteq> IRQAckIRQ \<longrightarrow> (gen_invocation_type label = IRQSetIRQHandler \<longrightarrow> blah \<noteq> [] \<longrightarrow> (\<forall>xa. (\<exists>a b. hd blah = (xa, a, b)) \<longrightarrow> is_ntfn_cap xa \<and> AllowSend \<in> cap_rights xa \<longrightarrow> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap x)) (a, b) s))) \<and> (gen_invocation_type label \<noteq> IRQSetIRQHandler \<longrightarrow> gen_invocation_type label = IRQClearIRQHandler \<longrightarrow> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap x)) (a, b) s)))) \<and> (\<forall>x. cap = ArchObjectCap x \<longrightarrow> ?R63 x s) proof (prove)
goal:
No subgoals!