theory Interrupt_AI

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 ((=) (cap.IRQHandlerCap irq)) ptr' s)
        \<and> (\<forall>cap \<in> set caps. \<forall>r \<in> cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_to r s)
        \<and> (\<forall>cap \<in> set caps. ex_cte_cap_wp_to is_cnode_cap (snd cap) s)
        \<and> (\<forall>cap \<in> set caps. cte_wp_at (interrupt_derived (fst cap)) (snd cap) s)\<rbrace>
     decode_irq_handler_invocation label irq caps
   \<lbrace>irq_handler_inv_valid\<rbrace>,-" apply (simp add: decode_irq_handler_invocation_def Let_def split_def
                  split del: if_split cong: if_cong) apply (rule hoare_pre, wp) apply (clarsimp simp: neq_Nil_conv) apply (fastforce dest: valid_irq_handlersD simp: invs_def valid_state_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. invs s \<and> (\<forall>cap\<in>set caps. s \<turnstile> fst cap) \<and> (\<exists>ptr'. cte_wp_at ((=) (IRQHandlerCap irq)) ptr' s) \<and> (\<forall>cap\<in>set caps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s) \<and> (\<forall>cap\<in>set caps. ex_cte_cap_wp_to is_cnode_cap (snd cap) s) \<and> (\<forall>cap\<in>set caps. cte_wp_at (interrupt_derived (fst cap)) (snd cap) s)\<rbrace> decode_irq_handler_invocation 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. s \<turnstile> fst cap) \<and> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap irq)) (a, b) s) \<and> (\<forall>cap\<in>set caps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s) \<and> (\<forall>cap\<in>set caps. ex_cte_cap_wp_to is_cnode_cap (snd cap) s) \<and> (\<forall>cap\<in>set caps. cte_wp_at (interrupt_derived (fst cap)) (snd cap) s)\<rbrace> if gen_invocation_type label = IRQAckIRQ then returnOk (ACKIrq irq) else if gen_invocation_type label = IRQSetIRQHandler then if caps \<noteq> [] then if is_ntfn_cap (fst (hd caps)) \<and> AllowSend \<in> cap_rights (fst (hd caps)) then returnOk (SetIRQHandler irq (fst (hd caps)) (snd (hd caps))) else throwError (InvalidCapability 0) else throwError TruncatedMessage else if gen_invocation_type label = IRQClearIRQHandler then returnOk (ClearIRQHandler irq) else throwError IllegalOperation \<lbrace>irq_handler_inv_valid\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>s. invs s \<and> (\<forall>cap\<in>set caps. s \<turnstile> fst cap) \<and> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap irq)) (a, b) s) \<and> (\<forall>cap\<in>set caps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s) \<and> (\<forall>cap\<in>set caps. ex_cte_cap_wp_to is_cnode_cap (snd cap) s) \<and> (\<forall>cap\<in>set caps. cte_wp_at (interrupt_derived (fst cap)) (snd cap) s) \<Longrightarrow> (gen_invocation_type label = IRQAckIRQ \<longrightarrow> irq_handler_inv_valid (ACKIrq irq) s) \<and> (gen_invocation_type label \<noteq> IRQAckIRQ \<longrightarrow> (gen_invocation_type label = IRQSetIRQHandler \<longrightarrow> (caps \<noteq> [] \<longrightarrow> (is_ntfn_cap (fst (hd caps)) \<and> AllowSend \<in> cap_rights (fst (hd caps)) \<longrightarrow> irq_handler_inv_valid (SetIRQHandler irq (fst (hd caps)) (snd (hd caps))) s) \<and> (\<not> (is_ntfn_cap (fst (hd caps)) \<and> AllowSend \<in> cap_rights (fst (hd caps))) \<longrightarrow> True)) \<and> (\<not> caps \<noteq> [] \<longrightarrow> True)) \<and> (gen_invocation_type label \<noteq> IRQSetIRQHandler \<longrightarrow> (gen_invocation_type label = IRQClearIRQHandler \<longrightarrow> irq_handler_inv_valid (ClearIRQHandler irq) s) \<and> (gen_invocation_type label \<noteq> IRQClearIRQHandler \<longrightarrow> True))) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>invs s; \<forall>cap\<in>set caps. s \<turnstile> fst cap; cte_wp_at ((=) (IRQHandlerCap irq)) (a, b) s; \<forall>cap\<in>set caps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s; \<forall>cap\<in>set caps. ex_cte_cap_wp_to is_cnode_cap (snd cap) s; \<forall>cap\<in>set caps. cte_wp_at (interrupt_derived (fst cap)) (snd cap) s; gen_invocation_type label = IRQAckIRQ; interrupt_states s irq = IRQInactive\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!