theory Interrupt_R

lemma decode_irq_control_valid'[wp]:
  "\<lbrace>\<lambda>s. invs' s \<and> (\<forall>cap \<in> set caps. s \<turnstile>' cap)
        \<and> (\<forall>cap \<in> set caps. \<forall>r \<in> cte_refs' cap (irq_node' s). ex_cte_cap_to' r s)
        \<and> cte_wp_at' (\<lambda>cte. cteCap cte = IRQControlCap) slot s\<rbrace>
     decodeIRQControlInvocation label args slot caps
   \<lbrace>irq_control_inv_valid'\<rbrace>,-" apply (simp add: decodeIRQControlInvocation_def Let_def split_def checkIRQ_def
                   rangeCheck_def unlessE_whenE
                split del: if_split cong: if_cong list.case_cong
                                          gen_invocation_labels.case_cong) apply (wpsimp wp: ensureEmptySlot_stronger isIRQActive_wp whenE_throwError_wp
                simp: o_def
         | wp (once) hoare_drop_imps)+ apply (clarsimp simp: invs_valid_objs' irq_const_defs unat_word_ariths word_le_nat_alt
                        not_less unat_le_helper unat_of_nat) apply (rule order.trans, rule unat_ucast_le, assumption) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. invs' s \<and> (\<forall>cap\<in>set caps. valid_cap' cap s) \<and> (\<forall>cap\<in>set caps. \<forall>r\<in>cte_refs' cap (irq_node' s). ex_cte_cap_wp_to' (\<lambda>_. True) r s) \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQControlCap) slot s\<rbrace> global.decodeIRQControlInvocation label args slot caps \<lbrace>irq_control_inv_valid'\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. invs' s \<and> (\<forall>cap\<in>set caps. valid_cap' cap s) \<and> (\<forall>cap\<in>set caps. \<forall>r\<in>cte_refs' cap (irq_node' s). ex_cte_cap_wp_to' (\<lambda>_. True) r s) \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQControlCap) slot s\<rbrace> case gen_invocation_type label of IRQIssueIRQHandler \<Rightarrow> case args of [] \<Rightarrow> throwError Fault_H.syscall_error.TruncatedMessage | [irqW] \<Rightarrow> throwError Fault_H.syscall_error.TruncatedMessage | [irqW, index] \<Rightarrow> throwError Fault_H.syscall_error.TruncatedMessage | irqW # index # depth # x \<Rightarrow> case caps of [] \<Rightarrow> throwError Fault_H.syscall_error.TruncatedMessage | cnode # xa \<Rightarrow> doE y <- whenE (UCAST(10 \<rightarrow> 32) minIRQ \<le> irqW \<longrightarrow> \<not> irqW \<le> UCAST(10 \<rightarrow> 32) maxIRQ) (throwError (Fault_H.syscall_error.RangeError (UCAST(10 \<rightarrow> 32) minIRQ) (UCAST(10 \<rightarrow> 32) maxIRQ)));
irqActive <- liftE (isIRQActive (toEnum (unat irqW)));
y <- whenE irqActive (throwError Fault_H.syscall_error.RevokeFirst);
destSlot <- lookupSlotForCNodeOp False cnode index (unat depth);
y <- ensureEmptySlot destSlot;
returnOk (Invocations_H.irqcontrol_invocation.IssueIRQHandler (toEnum (unat irqW)) destSlot slot)
odE | _ \<Rightarrow> liftME irqcontrol_invocation.ArchIRQControl (Arch.decodeIRQControlInvocation label args slot caps) \<lbrace>irq_control_inv_valid'\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>s x xb xd xe xf xg rv. \<lbrakk>invs' s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQControlCap) slot s; gen_invocation_type label = IRQIssueIRQHandler; args = x # xb # xd # xe; caps = xf # xg; UCAST(10 \<rightarrow> 32) minIRQ \<le> x; x \<le> UCAST(10 \<rightarrow> 32) maxIRQ; \<not> rv; \<not> irq_issued' (toEnum (unat x)) s; valid_cap' xf s; \<forall>cap\<in>set xg. valid_cap' cap s; \<forall>r\<in>cte_refs' xf (irq_node' s). ex_cte_cap_wp_to' (\<lambda>_. True) r s; \<forall>cap\<in>set xg. \<forall>r\<in>cte_refs' cap (irq_node' s). ex_cte_cap_wp_to' (\<lambda>_. True) r s\<rbrakk> \<Longrightarrow> valid_objs' s \<and> toEnum (unat x) \<le> maxIRQ proof (prove)
goal (1 subgoal):
 1. \<And>s x xb xd xe xf xg rv. \<lbrakk>invs' s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQControlCap) slot s; gen_invocation_type label = IRQIssueIRQHandler; args = x # xb # xd # xe; caps = xf # xg; unat x \<le> 159; \<not> rv; \<not> irq_issued' (UCAST(32 \<rightarrow> 10) x) s; valid_cap' xf s; \<forall>cap\<in>set xg. valid_cap' cap s; \<forall>r\<in>cte_refs' xf (irq_node' s). ex_cte_cap_wp_to' (\<lambda>_. True) r s; \<forall>cap\<in>set xg. \<forall>r\<in>cte_refs' cap (irq_node' s). ex_cte_cap_wp_to' (\<lambda>_. True) r s\<rbrakk> \<Longrightarrow> unat (UCAST(32 \<rightarrow> 10) x) \<le> 159 proof (prove)
goal:
No subgoals!