theory Interrupt_R

lemma arch_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>
     ARM_H.decodeIRQControlInvocation label args slot caps
   \<lbrace>arch_irq_control_inv_valid'\<rbrace>,-" apply (clarsimp simp add: ARM_H.decodeIRQControlInvocation_def Let_def split_def
                            rangeCheck_def unlessE_whenE
                  split del: if_split
                  cong: if_cong list.case_cong prod.case_cong arch_invocation_label.case_cong) apply (rule hoare_pre) apply (simp add: rangeCheck_def unlessE_whenE checkIRQ_def
               cong: list.case_cong prod.case_cong
          | wp whenE_throwError_wp isIRQActive_wp ensureEmptySlot_stronger
          | wpc
          | wp (once) hoare_drop_imps)+ apply (clarsimp simp add: 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> Arch.decodeIRQControlInvocation label args slot caps \<lbrace>arch_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 invocation_type label of GenInvocationLabel gen_invocation_labels \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation | ArchInvocationLabel ARMIRQIssueIRQHandler \<Rightarrow> case snd (fst (invocation_type label, args, caps), fst (snd (invocation_type label, args, caps)), snd (snd (invocation_type label, args, caps))) of ([], xa) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | ([irqW], xa) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | ([irqW, triggerW], xa) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | ([irqW, triggerW, index], xa) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (irqW # triggerW # index # depth # x, []) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (irqW # triggerW # index # depth # x, cnode # xaa) \<Rightarrow> doE checkIRQ irqW;
irq <- returnOk (toEnum (fromIntegral irqW));
irqActive <- withoutFailure $ isIRQActive irq;
whenE irqActive $ throw Fault_H.syscall_error.RevokeFirst;
destSlot <- lookupTargetSlot cnode (CPtr index) (fromIntegral depth);
ensureEmptySlot destSlot;
returnOk $ local.irqcontrol_invocation.IssueIRQHandler irq destSlot slot (triggerW \<noteq> 0)
odE | ArchInvocationLabel _ \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation \<lbrace>arch_irq_control_inv_valid'\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'3\<rbrace> case invocation_type label of GenInvocationLabel gen_invocation_labels \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation | ArchInvocationLabel ARMIRQIssueIRQHandler \<Rightarrow> case snd (fst (invocation_type label, args, caps), fst (snd (invocation_type label, args, caps)), snd (snd (invocation_type label, args, caps))) of ([], xa) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | ([irqW], xa) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | ([irqW, triggerW], xa) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | ([irqW, triggerW, index], xa) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (irqW # triggerW # index # depth # x, []) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (irqW # triggerW # index # depth # x, cnode # xaa) \<Rightarrow> doE checkIRQ irqW;
irq <- returnOk (toEnum (fromIntegral irqW));
irqActive <- withoutFailure $ isIRQActive irq;
whenE irqActive $ throw Fault_H.syscall_error.RevokeFirst;
destSlot <- lookupTargetSlot cnode (CPtr index) (fromIntegral depth);
ensureEmptySlot destSlot;
returnOk $ local.irqcontrol_invocation.IssueIRQHandler irq destSlot slot (triggerW \<noteq> 0)
odE | ArchInvocationLabel _ \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation \<lbrace>arch_irq_control_inv_valid'\<rbrace>, -
 2. \<And>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 \<Longrightarrow> ?P'3 s proof (prove)
goal (1 subgoal):
 1. \<And>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 \<Longrightarrow> invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler \<longrightarrow> (\<forall>x xa. args = x # xa \<longrightarrow> (\<forall>xb xc. xa = xb # xc \<longrightarrow> (\<forall>xa xb. xc = xa # xb \<longrightarrow> (\<exists>x xa. xb = x # xa) \<longrightarrow> (\<forall>xa. (\<exists>x. caps = xa # x) \<longrightarrow> UCAST(10 \<rightarrow> 32) minIRQ \<le> x \<and> x \<le> UCAST(10 \<rightarrow> 32) maxIRQ \<longrightarrow> (\<forall>rv. (irq_issued' (toEnum (unat x)) s \<longrightarrow> rv) \<longrightarrow> \<not> rv \<longrightarrow> (\<forall>r\<in>cte_refs' xa (irq_node' s). ex_cte_cap_wp_to' (\<lambda>_. True) r s) \<and> valid_objs' s \<and> \<not> irq_issued' (toEnum (unat x)) s \<and> toEnum (unat x) \<le> maxIRQ))))) proof (prove)
goal (1 subgoal):
 1. \<And>s x xb xd xf xg xh xi rv. \<lbrakk>invs' s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQControlCap) slot s; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; args = x # xb # xd # xf # xg; caps = xh # xi; unat x \<le> 159; \<not> rv; \<not> irq_issued' (UCAST(32 \<rightarrow> 10) x) s; valid_cap' xh s; \<forall>cap\<in>set xi. valid_cap' cap s; \<forall>r\<in>cte_refs' xh (irq_node' s). ex_cte_cap_wp_to' (\<lambda>_. True) r s; \<forall>cap\<in>set xi. \<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!