theory Interrupt_AC

lemma decode_irq_handler_invocation_authorised [wp]:
  "\<lbrace>K (is_subject_irq aag irq \<and> (\<forall>cap_slot \<in> set caps. pas_cap_cur_auth aag (fst cap_slot)
                              \<and> is_subject aag (fst (snd cap_slot))))\<rbrace>
   decode_irq_handler_invocation info_label irq caps
   \<lbrace>\<lambda>x s. authorised_irq_hdl_inv aag x\<rbrace>, -" unfolding decode_irq_handler_invocation_def authorised_irq_hdl_inv_def apply (rule hoare_pre) apply (simp add: Let_def split_def split del: if_split cong: if_cong) apply wp apply (auto dest!: hd_in_set) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (is_subject_irq aag irq \<and> (\<forall>cap_slot\<in>set caps. pas_cap_cur_auth aag (fst cap_slot) \<and> is_subject aag (fst (snd cap_slot))))\<rbrace> decode_irq_handler_invocation info_label irq caps \<lbrace>\<lambda>x s. authorised_irq_hdl_inv aag x\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (is_subject_irq aag irq \<and> (\<forall>cap_slot\<in>set caps. pas_cap_cur_auth aag (fst cap_slot) \<and> is_subject aag (fst (snd cap_slot))))\<rbrace> if gen_invocation_type info_label = IRQAckIRQ then returnOk $ ACKIrq irq else if gen_invocation_type info_label = IRQSetIRQHandler then if caps \<noteq> [] then let (cap, slot) = hd caps in if is_ntfn_cap cap \<and> AllowSend \<in> cap_rights cap then returnOk $ SetIRQHandler irq cap slot else throwError $ InvalidCapability 0 else throwError TruncatedMessage else if gen_invocation_type info_label = IRQClearIRQHandler then returnOk $ ClearIRQHandler irq else throwError IllegalOperation \<lbrace>\<lambda>x s. case x of ACKIrq worda \<Rightarrow> True | SetIRQHandler word cap x \<Rightarrow> is_subject aag (fst x) \<and> pas_cap_cur_auth aag cap \<and> is_subject_irq aag word | ClearIRQHandler word \<Rightarrow> is_subject_irq aag word\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> if gen_invocation_type info_label = IRQAckIRQ then returnOk $ ACKIrq irq else if gen_invocation_type info_label = IRQSetIRQHandler then if caps \<noteq> [] then let (cap, slot) = hd caps in if is_ntfn_cap cap \<and> AllowSend \<in> cap_rights cap then returnOk $ SetIRQHandler irq cap slot else throwError $ InvalidCapability 0 else throwError TruncatedMessage else if gen_invocation_type info_label = IRQClearIRQHandler then returnOk $ ClearIRQHandler irq else throwError IllegalOperation \<lbrace>\<lambda>x s. case x of ACKIrq worda \<Rightarrow> True | SetIRQHandler word cap x \<Rightarrow> is_subject aag (fst x) \<and> pas_cap_cur_auth aag cap \<and> is_subject_irq aag word | ClearIRQHandler word \<Rightarrow> is_subject_irq aag word\<rbrace>, -
 2. \<And>s. K (is_subject_irq aag irq \<and> (\<forall>cap_slot\<in>set caps. pas_cap_cur_auth aag (fst cap_slot) \<and> is_subject aag (fst (snd cap_slot)))) s \<Longrightarrow> ?P' s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> if gen_invocation_type info_label = IRQAckIRQ then returnOk (ACKIrq irq) else if gen_invocation_type info_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 info_label = IRQClearIRQHandler then returnOk (ClearIRQHandler irq) else throwError IllegalOperation \<lbrace>\<lambda>x s. case x of ACKIrq worda \<Rightarrow> True | SetIRQHandler word cap x \<Rightarrow> is_subject aag (fst x) \<and> pas_cap_cur_auth aag cap \<and> is_subject_irq aag word | ClearIRQHandler word \<Rightarrow> is_subject_irq aag word\<rbrace>, -
 2. \<And>s. K (is_subject_irq aag irq \<and> (\<forall>cap_slot\<in>set caps. pas_cap_cur_auth aag (fst cap_slot) \<and> is_subject aag (fst (snd cap_slot)))) s \<Longrightarrow> ?P' s proof (prove)
goal (1 subgoal):
 1. \<And>s. K (is_subject_irq aag irq \<and> (\<forall>cap_slot\<in>set caps. pas_cap_cur_auth aag (fst cap_slot) \<and> is_subject aag (fst (snd cap_slot)))) s \<Longrightarrow> (gen_invocation_type info_label = IRQAckIRQ \<longrightarrow> (case ACKIrq irq of ACKIrq worda \<Rightarrow> True | SetIRQHandler word cap x \<Rightarrow> is_subject aag (fst x) \<and> pas_cap_cur_auth aag cap \<and> is_subject_irq aag word | ClearIRQHandler word \<Rightarrow> is_subject_irq aag word)) \<and> (gen_invocation_type info_label \<noteq> IRQAckIRQ \<longrightarrow> (gen_invocation_type info_label = IRQSetIRQHandler \<longrightarrow> (caps \<noteq> [] \<longrightarrow> (is_ntfn_cap (fst (hd caps)) \<and> AllowSend \<in> cap_rights (fst (hd caps)) \<longrightarrow> (case SetIRQHandler irq (fst (hd caps)) (snd (hd caps)) of ACKIrq worda \<Rightarrow> True | SetIRQHandler word cap x \<Rightarrow> is_subject aag (fst x) \<and> pas_cap_cur_auth aag cap \<and> is_subject_irq aag word | ClearIRQHandler word \<Rightarrow> is_subject_irq aag word)) \<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 info_label \<noteq> IRQSetIRQHandler \<longrightarrow> (gen_invocation_type info_label = IRQClearIRQHandler \<longrightarrow> (case ClearIRQHandler irq of ACKIrq worda \<Rightarrow> True | SetIRQHandler word cap x \<Rightarrow> is_subject aag (fst x) \<and> pas_cap_cur_auth aag cap \<and> is_subject_irq aag word | ClearIRQHandler word \<Rightarrow> is_subject_irq aag word)) \<and> (gen_invocation_type info_label \<noteq> IRQClearIRQHandler \<longrightarrow> True))) proof (prove)
goal:
No subgoals!