theory Interrupt_R

lemma decode_irq_handler_valid'[wp]:
  "\<lbrace>\<lambda>s. invs' s \<and> (\<forall>cap \<in> set caps. s \<turnstile>' fst cap)
        \<and> (\<exists>ptr'. cte_wp_at' (\<lambda>cte. cteCap cte = IRQHandlerCap irq) ptr' s)
        \<and> (\<forall>cap \<in> set caps. \<forall>r \<in> cte_refs' (fst cap) (irq_node' s). ex_cte_cap_to' r s)
        \<and> (\<forall>cap \<in> set caps. ex_cte_cap_wp_to' isCNodeCap (snd cap) s)
        \<and> (\<forall>cap \<in> set caps. cte_wp_at' (badge_derived' (fst cap) \<circ> cteCap) (snd cap) s)
        \<and> s \<turnstile>' IRQHandlerCap irq\<rbrace>
     decodeIRQHandlerInvocation label irq caps
   \<lbrace>irq_handler_inv_valid'\<rbrace>,-" apply (simp add: decodeIRQHandlerInvocation_def Let_def split_def
               split del: if_split) apply (rule hoare_pre) apply (wp | wpc | simp)+ apply (clarsimp simp: neq_Nil_conv isCap_simps) apply (rule conjI) apply (clarsimp simp: cte_wp_at_ctes_of) apply (drule (1) valid_irq_handlers_ctes_ofD) apply (simp add: invs'_def valid_state'_def) apply (simp add: irq_issued'_def) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. invs' s \<and> (\<forall>cap\<in>set caps. valid_cap' (fst cap) s) \<and> (\<exists>ptr'. cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap irq) ptr' s) \<and> (\<forall>cap\<in>set caps. \<forall>r\<in>cte_refs' (fst cap) (irq_node' s). ex_cte_cap_wp_to' (\<lambda>_. True) r s) \<and> (\<forall>cap\<in>set caps. ex_cte_cap_wp_to' isCNodeCap (snd cap) s) \<and> (\<forall>cap\<in>set caps. cte_wp_at' (badge_derived' (fst cap) \<circ> cteCap) (snd cap) s) \<and> valid_cap' (capability.IRQHandlerCap irq) s\<rbrace> decodeIRQHandlerInvocation label irq caps \<lbrace>irq_handler_inv_valid'\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. invs' s \<and> (\<forall>cap\<in>set caps. valid_cap' (fst cap) s) \<and> (\<exists>ptr'. cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap irq) ptr' s) \<and> (\<forall>cap\<in>set caps. \<forall>r\<in>cte_refs' (fst cap) (irq_node' s). ex_cte_cap_wp_to' (\<lambda>_. True) r s) \<and> (\<forall>cap\<in>set caps. ex_cte_cap_wp_to' isCNodeCap (snd cap) s) \<and> (\<forall>cap\<in>set caps. cte_wp_at' (badge_derived' (fst cap) \<circ> cteCap) (snd cap) s) \<and> valid_cap' (capability.IRQHandlerCap irq) s\<rbrace> case gen_invocation_type label of IRQAckIRQ \<Rightarrow> returnOk $ AckIRQ irq | IRQSetIRQHandler \<Rightarrow> case snd (gen_invocation_type label, caps) of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (cap, slot) # x \<Rightarrow> case cap of capability.NotificationCap x xa True xb \<Rightarrow> returnOk $ irqhandler_invocation.SetIRQHandler irq cap slot | capability.NotificationCap x xa False xb \<Rightarrow> throw $ Fault_H.syscall_error.InvalidCapability 0 | _ \<Rightarrow> throw $ Fault_H.syscall_error.InvalidCapability 0 | IRQClearIRQHandler \<Rightarrow> returnOk $ irqhandler_invocation.ClearIRQHandler irq | _ \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation \<lbrace>irq_handler_inv_valid'\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'2\<rbrace> case gen_invocation_type label of IRQAckIRQ \<Rightarrow> returnOk $ AckIRQ irq | IRQSetIRQHandler \<Rightarrow> case snd (gen_invocation_type label, caps) of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (cap, slot) # x \<Rightarrow> case cap of capability.NotificationCap x xa True xb \<Rightarrow> returnOk $ irqhandler_invocation.SetIRQHandler irq cap slot | capability.NotificationCap x xa False xb \<Rightarrow> throw $ Fault_H.syscall_error.InvalidCapability 0 | _ \<Rightarrow> throw $ Fault_H.syscall_error.InvalidCapability 0 | IRQClearIRQHandler \<Rightarrow> returnOk $ irqhandler_invocation.ClearIRQHandler irq | _ \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation \<lbrace>irq_handler_inv_valid'\<rbrace>, -
 2. \<And>s. invs' s \<and> (\<forall>cap\<in>set caps. valid_cap' (fst cap) s) \<and> (\<exists>ptr'. cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap irq) ptr' s) \<and> (\<forall>cap\<in>set caps. \<forall>r\<in>cte_refs' (fst cap) (irq_node' s). ex_cte_cap_wp_to' (\<lambda>_. True) r s) \<and> (\<forall>cap\<in>set caps. ex_cte_cap_wp_to' isCNodeCap (snd cap) s) \<and> (\<forall>cap\<in>set caps. cte_wp_at' (badge_derived' (fst cap) \<circ> cteCap) (snd cap) s) \<and> valid_cap' (capability.IRQHandlerCap irq) s \<Longrightarrow> ?P'2 s proof (prove)
goal (1 subgoal):
 1. \<And>s. invs' s \<and> (\<forall>cap\<in>set caps. valid_cap' (fst cap) s) \<and> (\<exists>ptr'. cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap irq) ptr' s) \<and> (\<forall>cap\<in>set caps. \<forall>r\<in>cte_refs' (fst cap) (irq_node' s). ex_cte_cap_wp_to' (\<lambda>_. True) r s) \<and> (\<forall>cap\<in>set caps. ex_cte_cap_wp_to' isCNodeCap (snd cap) s) \<and> (\<forall>cap\<in>set caps. cte_wp_at' (badge_derived' (fst cap) \<circ> cteCap) (snd cap) s) \<and> valid_cap' (capability.IRQHandlerCap irq) s \<Longrightarrow> (gen_invocation_type label = IRQAckIRQ \<longrightarrow> intStateIRQTable (ksInterruptState s) irq \<noteq> irqstate.IRQInactive) \<and> (gen_invocation_type label = IRQSetIRQHandler \<longrightarrow> (\<forall>a b. (\<exists>x. caps = (a, b) # x) \<longrightarrow> (\<forall>x xa xb xc. a = capability.NotificationCap x xa xb xc \<longrightarrow> xb \<longrightarrow> valid_cap' (capability.NotificationCap x xa True xc) s \<and> isNotificationCap (capability.NotificationCap x xa True xc) \<and> cte_wp_at' (badge_derived' (capability.NotificationCap x xa True xc) \<circ> cteCap) b s \<and> ex_cte_cap_wp_to' isCNodeCap b s))) proof (prove)
goal (1 subgoal):
 1. \<And>s ptr'. \<lbrakk>invs' s; \<forall>cap\<in>set caps. valid_cap' (fst cap) s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap irq) ptr' s; \<forall>cap\<in>set caps. \<forall>r\<in>cte_refs' (fst cap) (irq_node' s). ex_cte_cap_wp_to' (\<lambda>_. True) r s; \<forall>cap\<in>set caps. ex_cte_cap_wp_to' isCNodeCap (snd cap) s; \<forall>cap\<in>set caps. cte_wp_at' (badge_derived' (fst cap) \<circ> cteCap) (snd cap) s; valid_cap' (capability.IRQHandlerCap irq) s\<rbrakk> \<Longrightarrow> (gen_invocation_type label = IRQAckIRQ \<longrightarrow> intStateIRQTable (ksInterruptState s) irq \<noteq> irqstate.IRQInactive) \<and> (gen_invocation_type label = IRQSetIRQHandler \<longrightarrow> (\<forall>a b. (\<exists>x. caps = (a, b) # x) \<longrightarrow> (\<forall>x xa xb xc. a = capability.NotificationCap x xa xb xc \<longrightarrow> xb \<longrightarrow> valid_cap' (capability.NotificationCap x xa True xc) s \<and> cte_wp_at' (badge_derived' (capability.NotificationCap x xa True xc) \<circ> cteCap) b s \<and> ex_cte_cap_wp_to' isCNodeCap b s))) proof (prove)
goal (2 subgoals):
 1. \<And>s ptr'. \<lbrakk>invs' s; \<forall>cap\<in>set caps. valid_cap' (fst cap) s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap irq) ptr' s; \<forall>cap\<in>set caps. \<forall>r\<in>cte_refs' (fst cap) (irq_node' s). ex_cte_cap_wp_to' (\<lambda>_. True) r s; \<forall>cap\<in>set caps. ex_cte_cap_wp_to' isCNodeCap (snd cap) s; \<forall>cap\<in>set caps. cte_wp_at' (badge_derived' (fst cap) \<circ> cteCap) (snd cap) s; valid_cap' (capability.IRQHandlerCap irq) s\<rbrakk> \<Longrightarrow> gen_invocation_type label = IRQAckIRQ \<longrightarrow> intStateIRQTable (ksInterruptState s) irq \<noteq> irqstate.IRQInactive
 2. \<And>s ptr'. \<lbrakk>invs' s; \<forall>cap\<in>set caps. valid_cap' (fst cap) s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap irq) ptr' s; \<forall>cap\<in>set caps. \<forall>r\<in>cte_refs' (fst cap) (irq_node' s). ex_cte_cap_wp_to' (\<lambda>_. True) r s; \<forall>cap\<in>set caps. ex_cte_cap_wp_to' isCNodeCap (snd cap) s; \<forall>cap\<in>set caps. cte_wp_at' (badge_derived' (fst cap) \<circ> cteCap) (snd cap) s; valid_cap' (capability.IRQHandlerCap irq) s\<rbrakk> \<Longrightarrow> gen_invocation_type label = IRQSetIRQHandler \<longrightarrow> (\<forall>a b. (\<exists>x. caps = (a, b) # x) \<longrightarrow> (\<forall>x xa xb xc. a = capability.NotificationCap x xa xb xc \<longrightarrow> xb \<longrightarrow> valid_cap' (capability.NotificationCap x xa True xc) s \<and> cte_wp_at' (badge_derived' (capability.NotificationCap x xa True xc) \<circ> cteCap) b s \<and> ex_cte_cap_wp_to' isCNodeCap b s)) proof (prove)
goal (2 subgoals):
 1. \<And>s ptr' cte. \<lbrakk>invs' s; \<forall>cap\<in>set caps. valid_cap' (fst cap) s; \<forall>cap\<in>set caps. \<forall>r\<in>cte_refs' (fst cap) (irq_node' s). ex_cte_cap_wp_to' (\<lambda>_. True) r s; \<forall>cap\<in>set caps. ex_cte_cap_wp_to' isCNodeCap (snd cap) s; \<forall>cap\<in>set caps. \<exists>cte. ctes_of s (snd cap) = Some cte \<and> badge_derived' (fst cap) (cteCap cte); valid_cap' (capability.IRQHandlerCap irq) s; ctes_of s ptr' = Some cte; cteCap cte = capability.IRQHandlerCap irq; gen_invocation_type label = IRQAckIRQ; intStateIRQTable (ksInterruptState s) irq = irqstate.IRQInactive\<rbrakk> \<Longrightarrow> False
 2. \<And>s ptr'. \<lbrakk>invs' s; \<forall>cap\<in>set caps. valid_cap' (fst cap) s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap irq) ptr' s; \<forall>cap\<in>set caps. \<forall>r\<in>cte_refs' (fst cap) (irq_node' s). ex_cte_cap_wp_to' (\<lambda>_. True) r s; \<forall>cap\<in>set caps. ex_cte_cap_wp_to' isCNodeCap (snd cap) s; \<forall>cap\<in>set caps. cte_wp_at' (badge_derived' (fst cap) \<circ> cteCap) (snd cap) s; valid_cap' (capability.IRQHandlerCap irq) s\<rbrakk> \<Longrightarrow> gen_invocation_type label = IRQSetIRQHandler \<longrightarrow> (\<forall>a b. (\<exists>x. caps = (a, b) # x) \<longrightarrow> (\<forall>x xa xb xc. a = capability.NotificationCap x xa xb xc \<longrightarrow> xb \<longrightarrow> valid_cap' (capability.NotificationCap x xa True xc) s \<and> cte_wp_at' (badge_derived' (capability.NotificationCap x xa True xc) \<circ> cteCap) b s \<and> ex_cte_cap_wp_to' isCNodeCap b s)) proof (prove)
goal (3 subgoals):
 1. \<And>s ptr' cte. \<lbrakk>invs' s; \<forall>cap\<in>set caps. valid_cap' (fst cap) s; \<forall>cap\<in>set caps. \<forall>r\<in>cte_refs' (fst cap) (irq_node' s). ex_cte_cap_wp_to' (\<lambda>_. True) r s; \<forall>cap\<in>set caps. ex_cte_cap_wp_to' isCNodeCap (snd cap) s; \<forall>cap\<in>set caps. \<exists>cte. ctes_of s (snd cap) = Some cte \<and> badge_derived' (fst cap) (cteCap cte); valid_cap' (capability.IRQHandlerCap irq) s; cteCap cte = capability.IRQHandlerCap irq; gen_invocation_type label = IRQAckIRQ; intStateIRQTable (ksInterruptState s) irq = irqstate.IRQInactive\<rbrakk> \<Longrightarrow> valid_irq_handlers' s
 2. \<And>s ptr' cte. \<lbrakk>invs' s; \<forall>cap\<in>set caps. valid_cap' (fst cap) s; \<forall>cap\<in>set caps. \<forall>r\<in>cte_refs' (fst cap) (irq_node' s). ex_cte_cap_wp_to' (\<lambda>_. True) r s; \<forall>cap\<in>set caps. ex_cte_cap_wp_to' isCNodeCap (snd cap) s; \<forall>cap\<in>set caps. \<exists>cte. ctes_of s (snd cap) = Some cte \<and> badge_derived' (fst cap) (cteCap cte); valid_cap' (capability.IRQHandlerCap irq) s; cteCap cte = capability.IRQHandlerCap irq; gen_invocation_type label = IRQAckIRQ; intStateIRQTable (ksInterruptState s) irq = irqstate.IRQInactive; irq_issued' irq s\<rbrakk> \<Longrightarrow> False
 3. \<And>s ptr'. \<lbrakk>invs' s; \<forall>cap\<in>set caps. valid_cap' (fst cap) s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap irq) ptr' s; \<forall>cap\<in>set caps. \<forall>r\<in>cte_refs' (fst cap) (irq_node' s). ex_cte_cap_wp_to' (\<lambda>_. True) r s; \<forall>cap\<in>set caps. ex_cte_cap_wp_to' isCNodeCap (snd cap) s; \<forall>cap\<in>set caps. cte_wp_at' (badge_derived' (fst cap) \<circ> cteCap) (snd cap) s; valid_cap' (capability.IRQHandlerCap irq) s\<rbrakk> \<Longrightarrow> gen_invocation_type label = IRQSetIRQHandler \<longrightarrow> (\<forall>a b. (\<exists>x. caps = (a, b) # x) \<longrightarrow> (\<forall>x xa xb xc. a = capability.NotificationCap x xa xb xc \<longrightarrow> xb \<longrightarrow> valid_cap' (capability.NotificationCap x xa True xc) s \<and> cte_wp_at' (badge_derived' (capability.NotificationCap x xa True xc) \<circ> cteCap) b s \<and> ex_cte_cap_wp_to' isCNodeCap b s)) proof (prove)
goal (2 subgoals):
 1. \<And>s ptr' cte. \<lbrakk>invs' s; \<forall>cap\<in>set caps. valid_cap' (fst cap) s; \<forall>cap\<in>set caps. \<forall>r\<in>cte_refs' (fst cap) (irq_node' s). ex_cte_cap_wp_to' (\<lambda>_. True) r s; \<forall>cap\<in>set caps. ex_cte_cap_wp_to' isCNodeCap (snd cap) s; \<forall>cap\<in>set caps. \<exists>cte. ctes_of s (snd cap) = Some cte \<and> badge_derived' (fst cap) (cteCap cte); valid_cap' (capability.IRQHandlerCap irq) s; cteCap cte = capability.IRQHandlerCap irq; gen_invocation_type label = IRQAckIRQ; intStateIRQTable (ksInterruptState s) irq = irqstate.IRQInactive; irq_issued' irq s\<rbrakk> \<Longrightarrow> False
 2. \<And>s ptr'. \<lbrakk>invs' s; \<forall>cap\<in>set caps. valid_cap' (fst cap) s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap irq) ptr' s; \<forall>cap\<in>set caps. \<forall>r\<in>cte_refs' (fst cap) (irq_node' s). ex_cte_cap_wp_to' (\<lambda>_. True) r s; \<forall>cap\<in>set caps. ex_cte_cap_wp_to' isCNodeCap (snd cap) s; \<forall>cap\<in>set caps. cte_wp_at' (badge_derived' (fst cap) \<circ> cteCap) (snd cap) s; valid_cap' (capability.IRQHandlerCap irq) s\<rbrakk> \<Longrightarrow> gen_invocation_type label = IRQSetIRQHandler \<longrightarrow> (\<forall>a b. (\<exists>x. caps = (a, b) # x) \<longrightarrow> (\<forall>x xa xb xc. a = capability.NotificationCap x xa xb xc \<longrightarrow> xb \<longrightarrow> valid_cap' (capability.NotificationCap x xa True xc) s \<and> cte_wp_at' (badge_derived' (capability.NotificationCap x xa True xc) \<circ> cteCap) b s \<and> ex_cte_cap_wp_to' isCNodeCap b s)) proof (prove)
goal (1 subgoal):
 1. \<And>s ptr'. \<lbrakk>invs' s; \<forall>cap\<in>set caps. valid_cap' (fst cap) s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap irq) ptr' s; \<forall>cap\<in>set caps. \<forall>r\<in>cte_refs' (fst cap) (irq_node' s). ex_cte_cap_wp_to' (\<lambda>_. True) r s; \<forall>cap\<in>set caps. ex_cte_cap_wp_to' isCNodeCap (snd cap) s; \<forall>cap\<in>set caps. cte_wp_at' (badge_derived' (fst cap) \<circ> cteCap) (snd cap) s; valid_cap' (capability.IRQHandlerCap irq) s\<rbrakk> \<Longrightarrow> gen_invocation_type label = IRQSetIRQHandler \<longrightarrow> (\<forall>a b. (\<exists>x. caps = (a, b) # x) \<longrightarrow> (\<forall>x xa xb xc. a = capability.NotificationCap x xa xb xc \<longrightarrow> xb \<longrightarrow> valid_cap' (capability.NotificationCap x xa True xc) s \<and> cte_wp_at' (badge_derived' (capability.NotificationCap x xa True xc) \<circ> cteCap) b s \<and> ex_cte_cap_wp_to' isCNodeCap b s)) proof (prove)
goal:
No subgoals!