theory Interrupt_R

lemma arch_decodeIRQControlInvocation_corres:
  "list_all2 cap_relation caps caps' \<Longrightarrow>
   corres (ser \<oplus> arch_irq_control_inv_relation)
     (invs and (\<lambda>s. \<forall>cp \<in> set caps. s \<turnstile> cp))
     (invs' and (\<lambda>s. \<forall>cp \<in> set caps'. s \<turnstile>' cp))
     (arch_decode_irq_control_invocation label args slot caps)
     (ARM_H.decodeIRQControlInvocation label args (cte_map slot) caps')" apply (clarsimp simp: arch_decode_irq_control_invocation_def ARM_H.decodeIRQControlInvocation_def Let_def) apply (rule conjI, clarsimp) prefer 2 apply clarsimp apply (cases caps, simp) apply (auto split: arch_invocation_label.splits list.splits invocation_label.splits
                 simp: length_Suc_conv list_all2_Cons1 whenE_rangeCheck_eq liftE_bindE split_def)[2] apply (cases caps, simp split: list.split) apply (case_tac "\<exists>n. length args = Suc (Suc (Suc (Suc n)))",
              clarsimp simp: length_Suc_conv list_all2_Cons1 whenE_rangeCheck_eq
                             liftE_bindE split_def) prefer 2 apply (auto split: list.split)[1]
  \<comment>\<open>ARMIRQIssueIRQHandler\<close> apply (rule conjI, clarsimp) apply (rule corres_guard_imp) apply (rule corres_splitEE[OF checkIRQ_corres]) apply (rule_tac F="unat y \<le> unat maxIRQ" in corres_gen_asm) apply (clarsimp simp add: minIRQ_def maxIRQ_def ucast_nat_def) apply (rule corres_split_eqr[OF is_irq_active_corres]) apply (rule whenE_throwError_corres, clarsimp, clarsimp) apply (rule corres_splitEE) apply (rule lookupSlotForCNodeOp_corres; simp) apply (rule corres_splitEE) apply (rule ensureEmptySlot_corres; simp) apply (rule corres_returnOkTT) apply (clarsimp simp: arch_irq_control_inv_relation_def ) apply ((wpsimp wp: isIRQActive_inv arch_check_irq_maxIRQ_valid' checkIRQ_inv
                           simp: invs_valid_objs invs_psp_aligned invs_valid_objs'
                                 invs_pspace_aligned' invs_pspace_distinct'
                   | strengthen invs_valid_objs invs_psp_aligned
                   | wp (once) hoare_drop_imps arch_check_irq_inv)+) apply (auto split: arch_invocation_label.splits invocation_label.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. list_all2 cap_relation caps caps' \<Longrightarrow> corres (ser \<oplus> arch_irq_control_inv_relation) (invs and (\<lambda>s. \<forall>cp\<in>set caps. s \<turnstile> cp)) (invs' and (\<lambda>s. \<forall>cp\<in>set caps'. valid_cap' cp s)) (arch_decode_irq_control_invocation label args slot caps) (Arch.decodeIRQControlInvocation label args (cte_map slot) caps') proof (prove)
goal (1 subgoal):
 1. list_all2 cap_relation caps caps' \<Longrightarrow> (4 \<le> length args \<and> Suc 0 \<le> length caps \<longrightarrow> (invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> arch_irq_control_inv_relation) (invs and (\<lambda>s. \<forall>cp\<in>set caps. s \<turnstile> cp)) (invs' and (\<lambda>s. \<forall>cp\<in>set caps'. valid_cap' cp s)) (doE y <- arch_check_irq (args ! 0);
irq_active <- liftE (is_irq_active (UCAST(32 \<rightarrow> 10) (args ! 0)));
y <- whenE irq_active (throwError ExceptionTypes_A.syscall_error.RevokeFirst);
dest_slot <- lookup_slot_for_cnode_op False (caps ! 0) (to_bl (args ! 2)) (unat (args ! 3));
y <- ensure_empty dest_slot;
returnOk (ArchIRQControlIssue (UCAST(32 \<rightarrow> 10) (args ! 0)) dest_slot slot (args ! Suc 0 \<noteq> 0))
odE) (case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW, index] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | irqW # triggerW # index # depth # xa \<Rightarrow> case caps' of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | cnode # xa \<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 (cte_map slot) (triggerW \<noteq> 0)
odE)) \<and> (invocation_type label \<noteq> ArchInvocationLabel ARMIRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> arch_irq_control_inv_relation) (invs and (\<lambda>s. \<forall>cp\<in>set caps. s \<turnstile> cp)) (invs' and (\<lambda>s. \<forall>cp\<in>set caps'. valid_cap' cp s)) (throwError ExceptionTypes_A.syscall_error.IllegalOperation) (case invocation_type label of GenInvocationLabel gen_invocation_labels \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation | ArchInvocationLabel ARMIRQIssueIRQHandler \<Rightarrow> case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW, index] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | irqW # triggerW # index # depth # xa \<Rightarrow> case caps' of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | cnode # xa \<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 (cte_map slot) (triggerW \<noteq> 0)
odE | ArchInvocationLabel _ \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation))) \<and> ((4 \<le> length args \<longrightarrow> \<not> Suc 0 \<le> length caps) \<longrightarrow> (invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> arch_irq_control_inv_relation) (invs and (\<lambda>s. \<forall>cp\<in>set caps. s \<turnstile> cp)) (invs' and (\<lambda>s. \<forall>cp\<in>set caps'. valid_cap' cp s)) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage) (case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW, index] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | irqW # triggerW # index # depth # xa \<Rightarrow> case caps' of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | cnode # xa \<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 (cte_map slot) (triggerW \<noteq> 0)
odE)) \<and> (invocation_type label \<noteq> ArchInvocationLabel ARMIRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> arch_irq_control_inv_relation) (invs and (\<lambda>s. \<forall>cp\<in>set caps. s \<turnstile> cp)) (invs' and (\<lambda>s. \<forall>cp\<in>set caps'. valid_cap' cp s)) (throwError ExceptionTypes_A.syscall_error.IllegalOperation) (case invocation_type label of GenInvocationLabel gen_invocation_labels \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation | ArchInvocationLabel ARMIRQIssueIRQHandler \<Rightarrow> case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW, index] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | irqW # triggerW # index # depth # xa \<Rightarrow> case caps' of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | cnode # xa \<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 (cte_map slot) (triggerW \<noteq> 0)
odE | ArchInvocationLabel _ \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>list_all2 cap_relation caps caps'; 4 \<le> length args; Suc 0 \<le> length caps\<rbrakk> \<Longrightarrow> (invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> arch_irq_control_inv_relation) (invs and (\<lambda>s. \<forall>cp\<in>set caps. s \<turnstile> cp)) (invs' and (\<lambda>s. \<forall>cp\<in>set caps'. valid_cap' cp s)) (doE y <- arch_check_irq (args ! 0);
irq_active <- liftE (is_irq_active (UCAST(32 \<rightarrow> 10) (args ! 0)));
y <- whenE irq_active (throwError ExceptionTypes_A.syscall_error.RevokeFirst);
dest_slot <- lookup_slot_for_cnode_op False (caps ! 0) (to_bl (args ! 2)) (unat (args ! 3));
y <- ensure_empty dest_slot;
returnOk (ArchIRQControlIssue (UCAST(32 \<rightarrow> 10) (args ! 0)) dest_slot slot (args ! Suc 0 \<noteq> 0))
odE) (case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW, index] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | irqW # triggerW # index # depth # xa \<Rightarrow> case caps' of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | cnode # xa \<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 (cte_map slot) (triggerW \<noteq> 0)
odE)) \<and> (invocation_type label \<noteq> ArchInvocationLabel ARMIRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> arch_irq_control_inv_relation) (invs and (\<lambda>s. \<forall>cp\<in>set caps. s \<turnstile> cp)) (invs' and (\<lambda>s. \<forall>cp\<in>set caps'. valid_cap' cp s)) (throwError ExceptionTypes_A.syscall_error.IllegalOperation) (case invocation_type label of GenInvocationLabel gen_invocation_labels \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation | ArchInvocationLabel ARMIRQIssueIRQHandler \<Rightarrow> case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW, index] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | irqW # triggerW # index # depth # xa \<Rightarrow> case caps' of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | cnode # xa \<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 (cte_map slot) (triggerW \<noteq> 0)
odE | ArchInvocationLabel _ \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation))
 2. list_all2 cap_relation caps caps' \<Longrightarrow> (4 \<le> length args \<longrightarrow> \<not> Suc 0 \<le> length caps) \<longrightarrow> (invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> arch_irq_control_inv_relation) (invs and (\<lambda>s. \<forall>cp\<in>set caps. s \<turnstile> cp)) (invs' and (\<lambda>s. \<forall>cp\<in>set caps'. valid_cap' cp s)) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage) (case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW, index] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | irqW # triggerW # index # depth # xa \<Rightarrow> case caps' of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | cnode # xa \<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 (cte_map slot) (triggerW \<noteq> 0)
odE)) \<and> (invocation_type label \<noteq> ArchInvocationLabel ARMIRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> arch_irq_control_inv_relation) (invs and (\<lambda>s. \<forall>cp\<in>set caps. s \<turnstile> cp)) (invs' and (\<lambda>s. \<forall>cp\<in>set caps'. valid_cap' cp s)) (throwError ExceptionTypes_A.syscall_error.IllegalOperation) (case invocation_type label of GenInvocationLabel gen_invocation_labels \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation | ArchInvocationLabel ARMIRQIssueIRQHandler \<Rightarrow> case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW, index] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | irqW # triggerW # index # depth # xa \<Rightarrow> case caps' of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | cnode # xa \<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 (cte_map slot) (triggerW \<noteq> 0)
odE | ArchInvocationLabel _ \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation)) proof (prove)
goal (2 subgoals):
 1. list_all2 cap_relation caps caps' \<Longrightarrow> (4 \<le> length args \<longrightarrow> \<not> Suc 0 \<le> length caps) \<longrightarrow> (invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> arch_irq_control_inv_relation) (invs and (\<lambda>s. \<forall>cp\<in>set caps. s \<turnstile> cp)) (invs' and (\<lambda>s. \<forall>cp\<in>set caps'. valid_cap' cp s)) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage) (case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW, index] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | irqW # triggerW # index # depth # xa \<Rightarrow> case caps' of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | cnode # xa \<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 (cte_map slot) (triggerW \<noteq> 0)
odE)) \<and> (invocation_type label \<noteq> ArchInvocationLabel ARMIRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> arch_irq_control_inv_relation) (invs and (\<lambda>s. \<forall>cp\<in>set caps. s \<turnstile> cp)) (invs' and (\<lambda>s. \<forall>cp\<in>set caps'. valid_cap' cp s)) (throwError ExceptionTypes_A.syscall_error.IllegalOperation) (case invocation_type label of GenInvocationLabel gen_invocation_labels \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation | ArchInvocationLabel ARMIRQIssueIRQHandler \<Rightarrow> case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW, index] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | irqW # triggerW # index # depth # xa \<Rightarrow> case caps' of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | cnode # xa \<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 (cte_map slot) (triggerW \<noteq> 0)
odE | ArchInvocationLabel _ \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation))
 2. \<lbrakk>list_all2 cap_relation caps caps'; 4 \<le> length args; Suc 0 \<le> length caps\<rbrakk> \<Longrightarrow> (invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> arch_irq_control_inv_relation) (invs and (\<lambda>s. \<forall>cp\<in>set caps. s \<turnstile> cp)) (invs' and (\<lambda>s. \<forall>cp\<in>set caps'. valid_cap' cp s)) (doE y <- arch_check_irq (args ! 0);
irq_active <- liftE (is_irq_active (UCAST(32 \<rightarrow> 10) (args ! 0)));
y <- whenE irq_active (throwError ExceptionTypes_A.syscall_error.RevokeFirst);
dest_slot <- lookup_slot_for_cnode_op False (caps ! 0) (to_bl (args ! 2)) (unat (args ! 3));
y <- ensure_empty dest_slot;
returnOk (ArchIRQControlIssue (UCAST(32 \<rightarrow> 10) (args ! 0)) dest_slot slot (args ! Suc 0 \<noteq> 0))
odE) (case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW, index] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | irqW # triggerW # index # depth # xa \<Rightarrow> case caps' of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | cnode # xa \<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 (cte_map slot) (triggerW \<noteq> 0)
odE)) \<and> (invocation_type label \<noteq> ArchInvocationLabel ARMIRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> arch_irq_control_inv_relation) (invs and (\<lambda>s. \<forall>cp\<in>set caps. s \<turnstile> cp)) (invs' and (\<lambda>s. \<forall>cp\<in>set caps'. valid_cap' cp s)) (throwError ExceptionTypes_A.syscall_error.IllegalOperation) (case invocation_type label of GenInvocationLabel gen_invocation_labels \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation | ArchInvocationLabel ARMIRQIssueIRQHandler \<Rightarrow> case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW, index] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | irqW # triggerW # index # depth # xa \<Rightarrow> case caps' of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | cnode # xa \<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 (cte_map slot) (triggerW \<noteq> 0)
odE | ArchInvocationLabel _ \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>list_all2 cap_relation caps caps'; 4 \<le> length args \<longrightarrow> \<not> Suc 0 \<le> length caps\<rbrakk> \<Longrightarrow> (invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> arch_irq_control_inv_relation) (invs and (\<lambda>s. \<forall>cp\<in>set caps. s \<turnstile> cp)) (invs' and (\<lambda>s. \<forall>cp\<in>set caps'. valid_cap' cp s)) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage) (case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW, index] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | irqW # triggerW # index # depth # xa \<Rightarrow> case caps' of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | cnode # xa \<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 (cte_map slot) (triggerW \<noteq> 0)
odE)) \<and> (invocation_type label \<noteq> ArchInvocationLabel ARMIRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> arch_irq_control_inv_relation) (invs and (\<lambda>s. \<forall>cp\<in>set caps. s \<turnstile> cp)) (invs' and (\<lambda>s. \<forall>cp\<in>set caps'. valid_cap' cp s)) (throwError ExceptionTypes_A.syscall_error.IllegalOperation) (case invocation_type label of GenInvocationLabel gen_invocation_labels \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation | ArchInvocationLabel ARMIRQIssueIRQHandler \<Rightarrow> case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW, index] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | irqW # triggerW # index # depth # xa \<Rightarrow> case caps' of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | cnode # xa \<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 (cte_map slot) (triggerW \<noteq> 0)
odE | ArchInvocationLabel _ \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation))
 2. \<lbrakk>list_all2 cap_relation caps caps'; 4 \<le> length args; Suc 0 \<le> length caps\<rbrakk> \<Longrightarrow> (invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> arch_irq_control_inv_relation) (invs and (\<lambda>s. \<forall>cp\<in>set caps. s \<turnstile> cp)) (invs' and (\<lambda>s. \<forall>cp\<in>set caps'. valid_cap' cp s)) (doE y <- arch_check_irq (args ! 0);
irq_active <- liftE (is_irq_active (UCAST(32 \<rightarrow> 10) (args ! 0)));
y <- whenE irq_active (throwError ExceptionTypes_A.syscall_error.RevokeFirst);
dest_slot <- lookup_slot_for_cnode_op False (caps ! 0) (to_bl (args ! 2)) (unat (args ! 3));
y <- ensure_empty dest_slot;
returnOk (ArchIRQControlIssue (UCAST(32 \<rightarrow> 10) (args ! 0)) dest_slot slot (args ! Suc 0 \<noteq> 0))
odE) (case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW, index] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | irqW # triggerW # index # depth # xa \<Rightarrow> case caps' of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | cnode # xa \<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 (cte_map slot) (triggerW \<noteq> 0)
odE)) \<and> (invocation_type label \<noteq> ArchInvocationLabel ARMIRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> arch_irq_control_inv_relation) (invs and (\<lambda>s. \<forall>cp\<in>set caps. s \<turnstile> cp)) (invs' and (\<lambda>s. \<forall>cp\<in>set caps'. valid_cap' cp s)) (throwError ExceptionTypes_A.syscall_error.IllegalOperation) (case invocation_type label of GenInvocationLabel gen_invocation_labels \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation | ArchInvocationLabel ARMIRQIssueIRQHandler \<Rightarrow> case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW, index] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | irqW # triggerW # index # depth # xa \<Rightarrow> case caps' of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | cnode # xa \<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 (cte_map slot) (triggerW \<noteq> 0)
odE | ArchInvocationLabel _ \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation)) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>caps' = []; caps = []\<rbrakk> \<Longrightarrow> (invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> arch_irq_control_inv_relation) invs invs' (throwError ExceptionTypes_A.syscall_error.TruncatedMessage) (case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW, index] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | irqW # triggerW # index # depth # xa \<Rightarrow> case caps' of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | cnode # xa \<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 (cte_map slot) (triggerW \<noteq> 0)
odE)) \<and> (invocation_type label \<noteq> ArchInvocationLabel ARMIRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> arch_irq_control_inv_relation) invs invs' (throwError ExceptionTypes_A.syscall_error.IllegalOperation) (case invocation_type label of GenInvocationLabel gen_invocation_labels \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation | ArchInvocationLabel ARMIRQIssueIRQHandler \<Rightarrow> case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW, index] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | irqW # triggerW # index # depth # xa \<Rightarrow> case caps' of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | cnode # xa \<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 (cte_map slot) (triggerW \<noteq> 0)
odE | ArchInvocationLabel _ \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation))
 2. \<And>a list. \<lbrakk>list_all2 cap_relation caps caps'; 4 \<le> length args \<longrightarrow> \<not> Suc 0 \<le> length caps; caps = a # list\<rbrakk> \<Longrightarrow> (invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> arch_irq_control_inv_relation) (invs and (\<lambda>s. \<forall>cp\<in>set caps. s \<turnstile> cp)) (invs' and (\<lambda>s. \<forall>cp\<in>set caps'. valid_cap' cp s)) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage) (case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW, index] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | irqW # triggerW # index # depth # xa \<Rightarrow> case caps' of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | cnode # xa \<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 (cte_map slot) (triggerW \<noteq> 0)
odE)) \<and> (invocation_type label \<noteq> ArchInvocationLabel ARMIRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> arch_irq_control_inv_relation) (invs and (\<lambda>s. \<forall>cp\<in>set caps. s \<turnstile> cp)) (invs' and (\<lambda>s. \<forall>cp\<in>set caps'. valid_cap' cp s)) (throwError ExceptionTypes_A.syscall_error.IllegalOperation) (case invocation_type label of GenInvocationLabel gen_invocation_labels \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation | ArchInvocationLabel ARMIRQIssueIRQHandler \<Rightarrow> case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW, index] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | irqW # triggerW # index # depth # xa \<Rightarrow> case caps' of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | cnode # xa \<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 (cte_map slot) (triggerW \<noteq> 0)
odE | ArchInvocationLabel _ \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation))
 3. \<lbrakk>list_all2 cap_relation caps caps'; 4 \<le> length args; Suc 0 \<le> length caps\<rbrakk> \<Longrightarrow> (invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> arch_irq_control_inv_relation) (invs and (\<lambda>s. \<forall>cp\<in>set caps. s \<turnstile> cp)) (invs' and (\<lambda>s. \<forall>cp\<in>set caps'. valid_cap' cp s)) (doE y <- arch_check_irq (args ! 0);
irq_active <- liftE (is_irq_active (UCAST(32 \<rightarrow> 10) (args ! 0)));
y <- whenE irq_active (throwError ExceptionTypes_A.syscall_error.RevokeFirst);
dest_slot <- lookup_slot_for_cnode_op False (caps ! 0) (to_bl (args ! 2)) (unat (args ! 3));
y <- ensure_empty dest_slot;
returnOk (ArchIRQControlIssue (UCAST(32 \<rightarrow> 10) (args ! 0)) dest_slot slot (args ! Suc 0 \<noteq> 0))
odE) (case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW, index] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | irqW # triggerW # index # depth # xa \<Rightarrow> case caps' of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | cnode # xa \<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 (cte_map slot) (triggerW \<noteq> 0)
odE)) \<and> (invocation_type label \<noteq> ArchInvocationLabel ARMIRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> arch_irq_control_inv_relation) (invs and (\<lambda>s. \<forall>cp\<in>set caps. s \<turnstile> cp)) (invs' and (\<lambda>s. \<forall>cp\<in>set caps'. valid_cap' cp s)) (throwError ExceptionTypes_A.syscall_error.IllegalOperation) (case invocation_type label of GenInvocationLabel gen_invocation_labels \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation | ArchInvocationLabel ARMIRQIssueIRQHandler \<Rightarrow> case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW, index] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | irqW # triggerW # index # depth # xa \<Rightarrow> case caps' of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | cnode # xa \<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 (cte_map slot) (triggerW \<noteq> 0)
odE | ArchInvocationLabel _ \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>list_all2 cap_relation caps caps'; 4 \<le> length args; Suc 0 \<le> length caps\<rbrakk> \<Longrightarrow> (invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> arch_irq_control_inv_relation) (invs and (\<lambda>s. \<forall>cp\<in>set caps. s \<turnstile> cp)) (invs' and (\<lambda>s. \<forall>cp\<in>set caps'. valid_cap' cp s)) (doE y <- arch_check_irq (args ! 0);
irq_active <- liftE (is_irq_active (UCAST(32 \<rightarrow> 10) (args ! 0)));
y <- whenE irq_active (throwError ExceptionTypes_A.syscall_error.RevokeFirst);
dest_slot <- lookup_slot_for_cnode_op False (caps ! 0) (to_bl (args ! 2)) (unat (args ! 3));
y <- ensure_empty dest_slot;
returnOk (ArchIRQControlIssue (UCAST(32 \<rightarrow> 10) (args ! 0)) dest_slot slot (args ! Suc 0 \<noteq> 0))
odE) (case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW, index] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | irqW # triggerW # index # depth # xa \<Rightarrow> case caps' of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | cnode # xa \<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 (cte_map slot) (triggerW \<noteq> 0)
odE)) \<and> (invocation_type label \<noteq> ArchInvocationLabel ARMIRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> arch_irq_control_inv_relation) (invs and (\<lambda>s. \<forall>cp\<in>set caps. s \<turnstile> cp)) (invs' and (\<lambda>s. \<forall>cp\<in>set caps'. valid_cap' cp s)) (throwError ExceptionTypes_A.syscall_error.IllegalOperation) (case invocation_type label of GenInvocationLabel gen_invocation_labels \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation | ArchInvocationLabel ARMIRQIssueIRQHandler \<Rightarrow> case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW, index] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | irqW # triggerW # index # depth # xa \<Rightarrow> case caps' of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | cnode # xa \<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 (cte_map slot) (triggerW \<noteq> 0)
odE | ArchInvocationLabel _ \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation)) proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>list_all2 cap_relation caps caps'; 4 \<le> length args; Suc 0 \<le> length caps; caps = a # list\<rbrakk> \<Longrightarrow> (invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> arch_irq_control_inv_relation) (invs and (\<lambda>s. \<forall>cp\<in>set caps. s \<turnstile> cp)) (invs' and (\<lambda>s. \<forall>cp\<in>set caps'. valid_cap' cp s)) (doE y <- arch_check_irq (args ! 0);
irq_active <- liftE (is_irq_active (UCAST(32 \<rightarrow> 10) (args ! 0)));
y <- whenE irq_active (throwError ExceptionTypes_A.syscall_error.RevokeFirst);
dest_slot <- lookup_slot_for_cnode_op False (caps ! 0) (to_bl (args ! 2)) (unat (args ! 3));
y <- ensure_empty dest_slot;
returnOk (ArchIRQControlIssue (UCAST(32 \<rightarrow> 10) (args ! 0)) dest_slot slot (args ! Suc 0 \<noteq> 0))
odE) (case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW, index] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | irqW # triggerW # index # depth # xa \<Rightarrow> case caps' of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | cnode # xa \<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 (cte_map slot) (triggerW \<noteq> 0)
odE)) \<and> (invocation_type label \<noteq> ArchInvocationLabel ARMIRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> arch_irq_control_inv_relation) (invs and (\<lambda>s. \<forall>cp\<in>set caps. s \<turnstile> cp)) (invs' and (\<lambda>s. \<forall>cp\<in>set caps'. valid_cap' cp s)) (throwError ExceptionTypes_A.syscall_error.IllegalOperation) (case invocation_type label of GenInvocationLabel gen_invocation_labels \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation | ArchInvocationLabel ARMIRQIssueIRQHandler \<Rightarrow> case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW, index] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | irqW # triggerW # index # depth # xa \<Rightarrow> case caps' of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | cnode # xa \<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 (cte_map slot) (triggerW \<noteq> 0)
odE | ArchInvocationLabel _ \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation)) proof (prove)
goal (2 subgoals):
 1. \<And>a list z zs y ya yb yc ysc. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs\<rbrakk> \<Longrightarrow> (invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> arch_irq_control_inv_relation) (invs and (\<lambda>s. s \<turnstile> a \<and> (\<forall>cp\<in>set list. s \<turnstile> cp))) (invs' and (\<lambda>s. valid_cap' z s \<and> (\<forall>cp\<in>set zs. valid_cap' cp s))) (doE yd <- arch_check_irq y;
do irq_active <- is_irq_active (UCAST(32 \<rightarrow> 10) y);
doE yd <- whenE irq_active (throwError ExceptionTypes_A.syscall_error.RevokeFirst);
dest_slot <- lookup_slot_for_cnode_op False a (to_bl yb) (unat yc);
yb <- ensure_empty dest_slot;
returnOk (ArchIRQControlIssue (UCAST(32 \<rightarrow> 10) y) dest_slot slot (ya \<noteq> 0))
odE
od
odE) (doE yd <- checkIRQ y;
do irqActive <- isIRQActive (toEnum (unat y));
doE yd <- whenE irqActive (throwError Fault_H.syscall_error.RevokeFirst);
destSlot <- lookupSlotForCNodeOp False z yb (unat yc);
yb <- ensureEmptySlot destSlot;
returnOk (local.irqcontrol_invocation.IssueIRQHandler (toEnum (unat y)) destSlot (cte_map slot) (ya \<noteq> 0))
odE
od
odE)) \<and> (invocation_type label \<noteq> ArchInvocationLabel ARMIRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> arch_irq_control_inv_relation) (invs and (\<lambda>s. s \<turnstile> a \<and> (\<forall>cp\<in>set list. s \<turnstile> cp))) (invs' and (\<lambda>s. valid_cap' z s \<and> (\<forall>cp\<in>set zs. valid_cap' cp s))) (throwError ExceptionTypes_A.syscall_error.IllegalOperation) (case invocation_type label of GenInvocationLabel gen_invocation_labels \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation | ArchInvocationLabel ARMIRQIssueIRQHandler \<Rightarrow> case y # ya # yb # yc # ysc of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW, index] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | irqW # triggerW # index # depth # xa \<Rightarrow> case z # zs of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | cnode # xa \<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 (cte_map slot) (triggerW \<noteq> 0)
odE | ArchInvocationLabel _ \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation))
 2. \<And>a list. \<lbrakk>list_all2 cap_relation caps caps'; 4 \<le> length args; Suc 0 \<le> length caps; caps = a # list; \<nexists>n. length args = Suc (Suc (Suc (Suc n)))\<rbrakk> \<Longrightarrow> (invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> arch_irq_control_inv_relation) (invs and (\<lambda>s. \<forall>cp\<in>set caps. s \<turnstile> cp)) (invs' and (\<lambda>s. \<forall>cp\<in>set caps'. valid_cap' cp s)) (doE y <- arch_check_irq (args ! 0);
irq_active <- liftE (is_irq_active (UCAST(32 \<rightarrow> 10) (args ! 0)));
y <- whenE irq_active (throwError ExceptionTypes_A.syscall_error.RevokeFirst);
dest_slot <- lookup_slot_for_cnode_op False (caps ! 0) (to_bl (args ! 2)) (unat (args ! 3));
y <- ensure_empty dest_slot;
returnOk (ArchIRQControlIssue (UCAST(32 \<rightarrow> 10) (args ! 0)) dest_slot slot (args ! Suc 0 \<noteq> 0))
odE) (case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW, index] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | irqW # triggerW # index # depth # xa \<Rightarrow> case caps' of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | cnode # xa \<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 (cte_map slot) (triggerW \<noteq> 0)
odE)) \<and> (invocation_type label \<noteq> ArchInvocationLabel ARMIRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> arch_irq_control_inv_relation) (invs and (\<lambda>s. \<forall>cp\<in>set caps. s \<turnstile> cp)) (invs' and (\<lambda>s. \<forall>cp\<in>set caps'. valid_cap' cp s)) (throwError ExceptionTypes_A.syscall_error.IllegalOperation) (case invocation_type label of GenInvocationLabel gen_invocation_labels \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation | ArchInvocationLabel ARMIRQIssueIRQHandler \<Rightarrow> case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW, index] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | irqW # triggerW # index # depth # xa \<Rightarrow> case caps' of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | cnode # xa \<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 (cte_map slot) (triggerW \<noteq> 0)
odE | ArchInvocationLabel _ \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation)) proof (prove)
goal (2 subgoals):
 1. \<And>a list. \<lbrakk>list_all2 cap_relation caps caps'; 4 \<le> length args; Suc 0 \<le> length caps; caps = a # list; \<nexists>n. length args = Suc (Suc (Suc (Suc n)))\<rbrakk> \<Longrightarrow> (invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> arch_irq_control_inv_relation) (invs and (\<lambda>s. \<forall>cp\<in>set caps. s \<turnstile> cp)) (invs' and (\<lambda>s. \<forall>cp\<in>set caps'. valid_cap' cp s)) (doE y <- arch_check_irq (args ! 0);
irq_active <- liftE (is_irq_active (UCAST(32 \<rightarrow> 10) (args ! 0)));
y <- whenE irq_active (throwError ExceptionTypes_A.syscall_error.RevokeFirst);
dest_slot <- lookup_slot_for_cnode_op False (caps ! 0) (to_bl (args ! 2)) (unat (args ! 3));
y <- ensure_empty dest_slot;
returnOk (ArchIRQControlIssue (UCAST(32 \<rightarrow> 10) (args ! 0)) dest_slot slot (args ! Suc 0 \<noteq> 0))
odE) (case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW, index] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | irqW # triggerW # index # depth # xa \<Rightarrow> case caps' of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | cnode # xa \<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 (cte_map slot) (triggerW \<noteq> 0)
odE)) \<and> (invocation_type label \<noteq> ArchInvocationLabel ARMIRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> arch_irq_control_inv_relation) (invs and (\<lambda>s. \<forall>cp\<in>set caps. s \<turnstile> cp)) (invs' and (\<lambda>s. \<forall>cp\<in>set caps'. valid_cap' cp s)) (throwError ExceptionTypes_A.syscall_error.IllegalOperation) (case invocation_type label of GenInvocationLabel gen_invocation_labels \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation | ArchInvocationLabel ARMIRQIssueIRQHandler \<Rightarrow> case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW, index] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | irqW # triggerW # index # depth # xa \<Rightarrow> case caps' of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | cnode # xa \<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 (cte_map slot) (triggerW \<noteq> 0)
odE | ArchInvocationLabel _ \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation))
 2. \<And>a list z zs y ya yb yc ysc. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs\<rbrakk> \<Longrightarrow> (invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> arch_irq_control_inv_relation) (invs and (\<lambda>s. s \<turnstile> a \<and> (\<forall>cp\<in>set list. s \<turnstile> cp))) (invs' and (\<lambda>s. valid_cap' z s \<and> (\<forall>cp\<in>set zs. valid_cap' cp s))) (doE yd <- arch_check_irq y;
do irq_active <- is_irq_active (UCAST(32 \<rightarrow> 10) y);
doE yd <- whenE irq_active (throwError ExceptionTypes_A.syscall_error.RevokeFirst);
dest_slot <- lookup_slot_for_cnode_op False a (to_bl yb) (unat yc);
yb <- ensure_empty dest_slot;
returnOk (ArchIRQControlIssue (UCAST(32 \<rightarrow> 10) y) dest_slot slot (ya \<noteq> 0))
odE
od
odE) (doE yd <- checkIRQ y;
do irqActive <- isIRQActive (toEnum (unat y));
doE yd <- whenE irqActive (throwError Fault_H.syscall_error.RevokeFirst);
destSlot <- lookupSlotForCNodeOp False z yb (unat yc);
yb <- ensureEmptySlot destSlot;
returnOk (local.irqcontrol_invocation.IssueIRQHandler (toEnum (unat y)) destSlot (cte_map slot) (ya \<noteq> 0))
odE
od
odE)) \<and> (invocation_type label \<noteq> ArchInvocationLabel ARMIRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> arch_irq_control_inv_relation) (invs and (\<lambda>s. s \<turnstile> a \<and> (\<forall>cp\<in>set list. s \<turnstile> cp))) (invs' and (\<lambda>s. valid_cap' z s \<and> (\<forall>cp\<in>set zs. valid_cap' cp s))) (throwError ExceptionTypes_A.syscall_error.IllegalOperation) (case invocation_type label of GenInvocationLabel gen_invocation_labels \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation | ArchInvocationLabel ARMIRQIssueIRQHandler \<Rightarrow> case y # ya # yb # yc # ysc of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW, index] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | irqW # triggerW # index # depth # xa \<Rightarrow> case z # zs of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | cnode # xa \<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 (cte_map slot) (triggerW \<noteq> 0)
odE | ArchInvocationLabel _ \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation)) proof (prove)
goal (1 subgoal):
 1. \<And>a list z zs y ya yb yc ysc. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs\<rbrakk> \<Longrightarrow> (invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> arch_irq_control_inv_relation) (invs and (\<lambda>s. s \<turnstile> a \<and> (\<forall>cp\<in>set list. s \<turnstile> cp))) (invs' and (\<lambda>s. valid_cap' z s \<and> (\<forall>cp\<in>set zs. valid_cap' cp s))) (doE yd <- arch_check_irq y;
do irq_active <- is_irq_active (UCAST(32 \<rightarrow> 10) y);
doE yd <- whenE irq_active (throwError ExceptionTypes_A.syscall_error.RevokeFirst);
dest_slot <- lookup_slot_for_cnode_op False a (to_bl yb) (unat yc);
yb <- ensure_empty dest_slot;
returnOk (ArchIRQControlIssue (UCAST(32 \<rightarrow> 10) y) dest_slot slot (ya \<noteq> 0))
odE
od
odE) (doE yd <- checkIRQ y;
do irqActive <- isIRQActive (toEnum (unat y));
doE yd <- whenE irqActive (throwError Fault_H.syscall_error.RevokeFirst);
destSlot <- lookupSlotForCNodeOp False z yb (unat yc);
yb <- ensureEmptySlot destSlot;
returnOk (local.irqcontrol_invocation.IssueIRQHandler (toEnum (unat y)) destSlot (cte_map slot) (ya \<noteq> 0))
odE
od
odE)) \<and> (invocation_type label \<noteq> ArchInvocationLabel ARMIRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> arch_irq_control_inv_relation) (invs and (\<lambda>s. s \<turnstile> a \<and> (\<forall>cp\<in>set list. s \<turnstile> cp))) (invs' and (\<lambda>s. valid_cap' z s \<and> (\<forall>cp\<in>set zs. valid_cap' cp s))) (throwError ExceptionTypes_A.syscall_error.IllegalOperation) (case invocation_type label of GenInvocationLabel gen_invocation_labels \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation | ArchInvocationLabel ARMIRQIssueIRQHandler \<Rightarrow> case y # ya # yb # yc # ysc of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW, index] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | irqW # triggerW # index # depth # xa \<Rightarrow> case z # zs of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | cnode # xa \<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 (cte_map slot) (triggerW \<noteq> 0)
odE | ArchInvocationLabel _ \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation)) proof (prove)
goal (2 subgoals):
 1. \<And>a list z zs y ya yb yc ysc. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler\<rbrakk> \<Longrightarrow> corres (ser \<oplus> arch_irq_control_inv_relation) (invs and (\<lambda>s. s \<turnstile> a \<and> (\<forall>cp\<in>set list. s \<turnstile> cp))) (invs' and (\<lambda>s. valid_cap' z s \<and> (\<forall>cp\<in>set zs. valid_cap' cp s))) (doE yd <- arch_check_irq y;
do irq_active <- is_irq_active (UCAST(32 \<rightarrow> 10) y);
doE yd <- whenE irq_active (throwError ExceptionTypes_A.syscall_error.RevokeFirst);
dest_slot <- lookup_slot_for_cnode_op False a (to_bl yb) (unat yc);
yb <- ensure_empty dest_slot;
returnOk (ArchIRQControlIssue (UCAST(32 \<rightarrow> 10) y) dest_slot slot (ya \<noteq> 0))
odE
od
odE) (doE yd <- checkIRQ y;
do irqActive <- isIRQActive (toEnum (unat y));
doE yd <- whenE irqActive (throwError Fault_H.syscall_error.RevokeFirst);
destSlot <- lookupSlotForCNodeOp False z yb (unat yc);
yb <- ensureEmptySlot destSlot;
returnOk (local.irqcontrol_invocation.IssueIRQHandler (toEnum (unat y)) destSlot (cte_map slot) (ya \<noteq> 0))
odE
od
odE)
 2. \<And>a list z zs y ya yb yc ysc. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs\<rbrakk> \<Longrightarrow> invocation_type label \<noteq> ArchInvocationLabel ARMIRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> arch_irq_control_inv_relation) (invs and (\<lambda>s. s \<turnstile> a \<and> (\<forall>cp\<in>set list. s \<turnstile> cp))) (invs' and (\<lambda>s. valid_cap' z s \<and> (\<forall>cp\<in>set zs. valid_cap' cp s))) (throwError ExceptionTypes_A.syscall_error.IllegalOperation) (case invocation_type label of GenInvocationLabel gen_invocation_labels \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation | ArchInvocationLabel ARMIRQIssueIRQHandler \<Rightarrow> case y # ya # yb # yc # ysc of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW, index] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | irqW # triggerW # index # depth # xa \<Rightarrow> case z # zs of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | cnode # xa \<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 (cte_map slot) (triggerW \<noteq> 0)
odE | ArchInvocationLabel _ \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation) proof (prove)
goal (4 subgoals):
 1. \<And>a list z zs y ya yb yc ysc. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler\<rbrakk> \<Longrightarrow> corres (ser \<oplus> arch_irq_control_inv_relation) (?Q337 a list z zs y ya yb yc ysc) (?Q'337 a list z zs y ya yb yc ysc) (doE yd <- arch_check_irq y;
do irq_active <- is_irq_active (UCAST(32 \<rightarrow> 10) y);
doE yd <- whenE irq_active (throwError ExceptionTypes_A.syscall_error.RevokeFirst);
dest_slot <- lookup_slot_for_cnode_op False a (to_bl yb) (unat yc);
yb <- ensure_empty dest_slot;
returnOk (ArchIRQControlIssue (UCAST(32 \<rightarrow> 10) y) dest_slot slot (ya \<noteq> 0))
odE
od
odE) (doE yd <- checkIRQ y;
do irqActive <- isIRQActive (toEnum (unat y));
doE yd <- whenE irqActive (throwError Fault_H.syscall_error.RevokeFirst);
destSlot <- lookupSlotForCNodeOp False z yb (unat yc);
yb <- ensureEmptySlot destSlot;
returnOk (local.irqcontrol_invocation.IssueIRQHandler (toEnum (unat y)) destSlot (cte_map slot) (ya \<noteq> 0))
odE
od
odE)
 2. \<And>a list z zs y ya yb yc ysc s. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; (invs and (\<lambda>s. s \<turnstile> a \<and> (\<forall>cp\<in>set list. s \<turnstile> cp))) s\<rbrakk> \<Longrightarrow> ?Q337 a list z zs y ya yb yc ysc s
 3. \<And>a list z zs y ya yb yc ysc s. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; (invs' and (\<lambda>s. valid_cap' z s \<and> (\<forall>cp\<in>set zs. valid_cap' cp s))) s\<rbrakk> \<Longrightarrow> ?Q'337 a list z zs y ya yb yc ysc s
 4. \<And>a list z zs y ya yb yc ysc. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs\<rbrakk> \<Longrightarrow> invocation_type label \<noteq> ArchInvocationLabel ARMIRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> arch_irq_control_inv_relation) (invs and (\<lambda>s. s \<turnstile> a \<and> (\<forall>cp\<in>set list. s \<turnstile> cp))) (invs' and (\<lambda>s. valid_cap' z s \<and> (\<forall>cp\<in>set zs. valid_cap' cp s))) (throwError ExceptionTypes_A.syscall_error.IllegalOperation) (case invocation_type label of GenInvocationLabel gen_invocation_labels \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation | ArchInvocationLabel ARMIRQIssueIRQHandler \<Rightarrow> case y # ya # yb # yc # ysc of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW, index] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | irqW # triggerW # index # depth # xa \<Rightarrow> case z # zs of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | cnode # xa \<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 (cte_map slot) (triggerW \<noteq> 0)
odE | ArchInvocationLabel _ \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation) proof (prove)
goal (6 subgoals):
 1. \<And>a list z zs y ya yb yc ysc yd ye. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; dc yd ye\<rbrakk> \<Longrightarrow> corres (ser \<oplus> arch_irq_control_inv_relation) (?R341 a list z zs y ya yb yc ysc yd) (?R'341 a list z zs y ya yb yc ysc ye) (do irq_active <- is_irq_active (UCAST(32 \<rightarrow> 10) y);
doE yd <- whenE irq_active (throwError ExceptionTypes_A.syscall_error.RevokeFirst);
dest_slot <- lookup_slot_for_cnode_op False a (to_bl yb) (unat yc);
yb <- ensure_empty dest_slot;
returnOk (ArchIRQControlIssue (UCAST(32 \<rightarrow> 10) y) dest_slot slot (ya \<noteq> 0))
odE
od) (do irqActive <- isIRQActive (toEnum (unat y));
doE yd <- whenE irqActive (throwError Fault_H.syscall_error.RevokeFirst);
destSlot <- lookupSlotForCNodeOp False z yb (unat yc);
yb <- ensureEmptySlot destSlot;
returnOk (local.irqcontrol_invocation.IssueIRQHandler (toEnum (unat y)) destSlot (cte_map slot) (ya \<noteq> 0))
odE
od)
 2. \<And>a list z zs y ya yb yc ysc. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler\<rbrakk> \<Longrightarrow> \<lbrace>?Q341 a list z zs y ya yb yc ysc\<rbrace> arch_check_irq y \<lbrace>?R341 a list z zs y ya yb yc ysc\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>a list z zs y ya yb yc ysc. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler\<rbrakk> \<Longrightarrow> \<lbrace>?Q'341 a list z zs y ya yb yc ysc\<rbrace> checkIRQ y \<lbrace>?R'341 a list z zs y ya yb yc ysc\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>a list z zs y ya yb yc ysc s. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; (invs and (\<lambda>s. s \<turnstile> a \<and> (\<forall>cp\<in>set list. s \<turnstile> cp))) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q341 a list z zs y ya yb yc ysc) s
 5. \<And>a list z zs y ya yb yc ysc s. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; (invs' and (\<lambda>s. valid_cap' z s \<and> (\<forall>cp\<in>set zs. valid_cap' cp s))) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'341 a list z zs y ya yb yc ysc) s
 6. \<And>a list z zs y ya yb yc ysc. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs\<rbrakk> \<Longrightarrow> invocation_type label \<noteq> ArchInvocationLabel ARMIRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> arch_irq_control_inv_relation) (invs and (\<lambda>s. s \<turnstile> a \<and> (\<forall>cp\<in>set list. s \<turnstile> cp))) (invs' and (\<lambda>s. valid_cap' z s \<and> (\<forall>cp\<in>set zs. valid_cap' cp s))) (throwError ExceptionTypes_A.syscall_error.IllegalOperation) (case invocation_type label of GenInvocationLabel gen_invocation_labels \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation | ArchInvocationLabel ARMIRQIssueIRQHandler \<Rightarrow> case y # ya # yb # yc # ysc of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW, index] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | irqW # triggerW # index # depth # xa \<Rightarrow> case z # zs of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | cnode # xa \<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 (cte_map slot) (triggerW \<noteq> 0)
odE | ArchInvocationLabel _ \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation) proof (prove)
goal (6 subgoals):
 1. \<And>a list z zs y ya yb yc ysc yd ye. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; dc yd ye; unat y \<le> unat maxIRQ\<rbrakk> \<Longrightarrow> corres (ser \<oplus> arch_irq_control_inv_relation) (?P347 a list z zs y ya yb yc ysc yd) (?R'341 a list z zs y ya yb yc ysc ye) (do irq_active <- is_irq_active (UCAST(32 \<rightarrow> 10) y);
doE yd <- whenE irq_active (throwError ExceptionTypes_A.syscall_error.RevokeFirst);
dest_slot <- lookup_slot_for_cnode_op False a (to_bl yb) (unat yc);
yb <- ensure_empty dest_slot;
returnOk (ArchIRQControlIssue (UCAST(32 \<rightarrow> 10) y) dest_slot slot (ya \<noteq> 0))
odE
od) (do irqActive <- isIRQActive (toEnum (unat y));
doE yd <- whenE irqActive (throwError Fault_H.syscall_error.RevokeFirst);
destSlot <- lookupSlotForCNodeOp False z yb (unat yc);
yb <- ensureEmptySlot destSlot;
returnOk (local.irqcontrol_invocation.IssueIRQHandler (toEnum (unat y)) destSlot (cte_map slot) (ya \<noteq> 0))
odE
od)
 2. \<And>a list z zs y ya yb yc ysc. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler\<rbrakk> \<Longrightarrow> \<lbrace>?Q341 a list z zs y ya yb yc ysc\<rbrace> arch_check_irq y \<lbrace>\<lambda>yd. ?P347 a list z zs y ya yb yc ysc yd and (\<lambda>s. unat y \<le> unat maxIRQ)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>a list z zs y ya yb yc ysc. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler\<rbrakk> \<Longrightarrow> \<lbrace>?Q'341 a list z zs y ya yb yc ysc\<rbrace> checkIRQ y \<lbrace>?R'341 a list z zs y ya yb yc ysc\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>a list z zs y ya yb yc ysc s. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; (invs and (\<lambda>s. s \<turnstile> a \<and> (\<forall>cp\<in>set list. s \<turnstile> cp))) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q341 a list z zs y ya yb yc ysc) s
 5. \<And>a list z zs y ya yb yc ysc s. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; (invs' and (\<lambda>s. valid_cap' z s \<and> (\<forall>cp\<in>set zs. valid_cap' cp s))) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'341 a list z zs y ya yb yc ysc) s
 6. \<And>a list z zs y ya yb yc ysc. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs\<rbrakk> \<Longrightarrow> invocation_type label \<noteq> ArchInvocationLabel ARMIRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> arch_irq_control_inv_relation) (invs and (\<lambda>s. s \<turnstile> a \<and> (\<forall>cp\<in>set list. s \<turnstile> cp))) (invs' and (\<lambda>s. valid_cap' z s \<and> (\<forall>cp\<in>set zs. valid_cap' cp s))) (throwError ExceptionTypes_A.syscall_error.IllegalOperation) (case invocation_type label of GenInvocationLabel gen_invocation_labels \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation | ArchInvocationLabel ARMIRQIssueIRQHandler \<Rightarrow> case y # ya # yb # yc # ysc of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW, index] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | irqW # triggerW # index # depth # xa \<Rightarrow> case z # zs of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | cnode # xa \<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 (cte_map slot) (triggerW \<noteq> 0)
odE | ArchInvocationLabel _ \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation) proof (prove)
goal (6 subgoals):
 1. \<And>a list z zs y ya yb yc ysc. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; unat y \<le> 159\<rbrakk> \<Longrightarrow> corres (ser \<oplus> arch_irq_control_inv_relation) (?P347 a list z zs y ya yb yc ysc ()) (?R'341 a list z zs y ya yb yc ysc ()) (do irq_active <- is_irq_active (UCAST(32 \<rightarrow> 10) y);
doE yd <- whenE irq_active (throwError ExceptionTypes_A.syscall_error.RevokeFirst);
dest_slot <- lookup_slot_for_cnode_op False a (to_bl yb) (unat yc);
yb <- ensure_empty dest_slot;
returnOk (ArchIRQControlIssue (UCAST(32 \<rightarrow> 10) y) dest_slot slot (ya \<noteq> 0))
odE
od) (do irqActive <- isIRQActive (UCAST(32 \<rightarrow> 10) y);
doE yd <- whenE irqActive (throwError Fault_H.syscall_error.RevokeFirst);
destSlot <- lookupSlotForCNodeOp False z yb (unat yc);
yb <- ensureEmptySlot destSlot;
returnOk (local.irqcontrol_invocation.IssueIRQHandler (UCAST(32 \<rightarrow> 10) y) destSlot (cte_map slot) (ya \<noteq> 0))
odE
od)
 2. \<And>a list z zs y ya yb yc ysc. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler\<rbrakk> \<Longrightarrow> \<lbrace>?Q341 a list z zs y ya yb yc ysc\<rbrace> arch_check_irq y \<lbrace>\<lambda>yd. ?P347 a list z zs y ya yb yc ysc yd and (\<lambda>s. unat y \<le> unat maxIRQ)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>a list z zs y ya yb yc ysc. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler\<rbrakk> \<Longrightarrow> \<lbrace>?Q'341 a list z zs y ya yb yc ysc\<rbrace> checkIRQ y \<lbrace>?R'341 a list z zs y ya yb yc ysc\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>a list z zs y ya yb yc ysc s. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; (invs and (\<lambda>s. s \<turnstile> a \<and> (\<forall>cp\<in>set list. s \<turnstile> cp))) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q341 a list z zs y ya yb yc ysc) s
 5. \<And>a list z zs y ya yb yc ysc s. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; (invs' and (\<lambda>s. valid_cap' z s \<and> (\<forall>cp\<in>set zs. valid_cap' cp s))) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'341 a list z zs y ya yb yc ysc) s
 6. \<And>a list z zs y ya yb yc ysc. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs\<rbrakk> \<Longrightarrow> invocation_type label \<noteq> ArchInvocationLabel ARMIRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> arch_irq_control_inv_relation) (invs and (\<lambda>s. s \<turnstile> a \<and> (\<forall>cp\<in>set list. s \<turnstile> cp))) (invs' and (\<lambda>s. valid_cap' z s \<and> (\<forall>cp\<in>set zs. valid_cap' cp s))) (throwError ExceptionTypes_A.syscall_error.IllegalOperation) (case invocation_type label of GenInvocationLabel gen_invocation_labels \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation | ArchInvocationLabel ARMIRQIssueIRQHandler \<Rightarrow> case y # ya # yb # yc # ysc of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW, index] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | irqW # triggerW # index # depth # xa \<Rightarrow> case z # zs of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | cnode # xa \<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 (cte_map slot) (triggerW \<noteq> 0)
odE | ArchInvocationLabel _ \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation) proof (prove)
goal (8 subgoals):
 1. \<And>a list z zs y ya yb yc ysc irq_active. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; unat y \<le> 159\<rbrakk> \<Longrightarrow> corres (ser \<oplus> arch_irq_control_inv_relation) (?R382 a list z zs y ya yb yc ysc irq_active) (?R'382 a list z zs y ya yb yc ysc irq_active) (doE yd <- whenE irq_active (throwError ExceptionTypes_A.syscall_error.RevokeFirst);
dest_slot <- lookup_slot_for_cnode_op False a (to_bl yb) (unat yc);
yb <- ensure_empty dest_slot;
returnOk (ArchIRQControlIssue (UCAST(32 \<rightarrow> 10) y) dest_slot slot (ya \<noteq> 0))
odE) (doE yd <- whenE irq_active (throwError Fault_H.syscall_error.RevokeFirst);
destSlot <- lookupSlotForCNodeOp False z yb (unat yc);
yb <- ensureEmptySlot destSlot;
returnOk (local.irqcontrol_invocation.IssueIRQHandler (UCAST(32 \<rightarrow> 10) y) destSlot (cte_map slot) (ya \<noteq> 0))
odE)
 2. \<And>a list z zs y ya yb yc ysc. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; unat y \<le> 159\<rbrakk> \<Longrightarrow> \<lbrace>?Q387 a list z zs y ya yb yc ysc ()\<rbrace> is_irq_active (UCAST(32 \<rightarrow> 10) y) \<lbrace>?R382 a list z zs y ya yb yc ysc\<rbrace>
 3. \<And>a list z zs y ya yb yc ysc. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; unat y \<le> 159\<rbrakk> \<Longrightarrow> \<lbrace>?Q'386 a list z zs y ya yb yc ysc ()\<rbrace> isIRQActive (UCAST(32 \<rightarrow> 10) y) \<lbrace>?R'382 a list z zs y ya yb yc ysc\<rbrace>
 4. \<And>a list z zs y ya yb yc ysc. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler\<rbrakk> \<Longrightarrow> \<lbrace>?Q341 a list z zs y ya yb yc ysc\<rbrace> arch_check_irq y \<lbrace>\<lambda>yd. (\<lambda>_. True) and ?Q387 a list z zs y ya yb yc ysc yd and (\<lambda>s. unat y \<le> unat maxIRQ)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>a list z zs y ya yb yc ysc. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler\<rbrakk> \<Longrightarrow> \<lbrace>?Q'341 a list z zs y ya yb yc ysc\<rbrace> checkIRQ y \<lbrace>\<lambda>b. (\<lambda>_. True) and ?Q'386 a list z zs y ya yb yc ysc b\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>a list z zs y ya yb yc ysc s. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; (invs and (\<lambda>s. s \<turnstile> a \<and> (\<forall>cp\<in>set list. s \<turnstile> cp))) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q341 a list z zs y ya yb yc ysc) s
 7. \<And>a list z zs y ya yb yc ysc s. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; (invs' and (\<lambda>s. valid_cap' z s \<and> (\<forall>cp\<in>set zs. valid_cap' cp s))) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'341 a list z zs y ya yb yc ysc) s
 8. \<And>a list z zs y ya yb yc ysc. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs\<rbrakk> \<Longrightarrow> invocation_type label \<noteq> ArchInvocationLabel ARMIRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> arch_irq_control_inv_relation) (invs and (\<lambda>s. s \<turnstile> a \<and> (\<forall>cp\<in>set list. s \<turnstile> cp))) (invs' and (\<lambda>s. valid_cap' z s \<and> (\<forall>cp\<in>set zs. valid_cap' cp s))) (throwError ExceptionTypes_A.syscall_error.IllegalOperation) (case invocation_type label of GenInvocationLabel gen_invocation_labels \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation | ArchInvocationLabel ARMIRQIssueIRQHandler \<Rightarrow> case y # ya # yb # yc # ysc of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW, index] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | irqW # triggerW # index # depth # xa \<Rightarrow> case z # zs of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | cnode # xa \<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 (cte_map slot) (triggerW \<noteq> 0)
odE | ArchInvocationLabel _ \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation) proof (prove)
goal (8 subgoals):
 1. \<And>a list z zs y ya yb yc ysc irq_active. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; unat y \<le> 159; \<not> irq_active\<rbrakk> \<Longrightarrow> corres (ser \<oplus> arch_irq_control_inv_relation) (?Q391 a list z zs y ya yb yc ysc irq_active) (?Q'391 a list z zs y ya yb yc ysc irq_active) (doE dest_slot <- lookup_slot_for_cnode_op False a (to_bl yb) (unat yc);
yb <- ensure_empty dest_slot;
returnOk (ArchIRQControlIssue (UCAST(32 \<rightarrow> 10) y) dest_slot slot (ya \<noteq> 0))
odE) (doE destSlot <- lookupSlotForCNodeOp False z yb (unat yc);
yb <- ensureEmptySlot destSlot;
returnOk (local.irqcontrol_invocation.IssueIRQHandler (UCAST(32 \<rightarrow> 10) y) destSlot (cte_map slot) (ya \<noteq> 0))
odE)
 2. \<And>a list z zs y ya yb yc ysc. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; unat y \<le> 159\<rbrakk> \<Longrightarrow> \<lbrace>?Q387 a list z zs y ya yb yc ysc ()\<rbrace> is_irq_active (UCAST(32 \<rightarrow> 10) y) \<lbrace>\<lambda>irq_active s. \<not> irq_active \<longrightarrow> ?Q391 a list z zs y ya yb yc ysc irq_active s\<rbrace>
 3. \<And>a list z zs y ya yb yc ysc. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; unat y \<le> 159\<rbrakk> \<Longrightarrow> \<lbrace>?Q'386 a list z zs y ya yb yc ysc ()\<rbrace> isIRQActive (UCAST(32 \<rightarrow> 10) y) \<lbrace>\<lambda>irq_active s. \<not> irq_active \<longrightarrow> ?Q'391 a list z zs y ya yb yc ysc irq_active s\<rbrace>
 4. \<And>a list z zs y ya yb yc ysc. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler\<rbrakk> \<Longrightarrow> \<lbrace>?Q341 a list z zs y ya yb yc ysc\<rbrace> arch_check_irq y \<lbrace>\<lambda>yd. (\<lambda>_. True) and ?Q387 a list z zs y ya yb yc ysc yd and (\<lambda>s. unat y \<le> unat maxIRQ)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>a list z zs y ya yb yc ysc. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler\<rbrakk> \<Longrightarrow> \<lbrace>?Q'341 a list z zs y ya yb yc ysc\<rbrace> checkIRQ y \<lbrace>\<lambda>b. (\<lambda>_. True) and ?Q'386 a list z zs y ya yb yc ysc b\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>a list z zs y ya yb yc ysc s. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; (invs and (\<lambda>s. s \<turnstile> a \<and> (\<forall>cp\<in>set list. s \<turnstile> cp))) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q341 a list z zs y ya yb yc ysc) s
 7. \<And>a list z zs y ya yb yc ysc s. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; (invs' and (\<lambda>s. valid_cap' z s \<and> (\<forall>cp\<in>set zs. valid_cap' cp s))) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'341 a list z zs y ya yb yc ysc) s
 8. \<And>a list z zs y ya yb yc ysc. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs\<rbrakk> \<Longrightarrow> invocation_type label \<noteq> ArchInvocationLabel ARMIRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> arch_irq_control_inv_relation) (invs and (\<lambda>s. s \<turnstile> a \<and> (\<forall>cp\<in>set list. s \<turnstile> cp))) (invs' and (\<lambda>s. valid_cap' z s \<and> (\<forall>cp\<in>set zs. valid_cap' cp s))) (throwError ExceptionTypes_A.syscall_error.IllegalOperation) (case invocation_type label of GenInvocationLabel gen_invocation_labels \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation | ArchInvocationLabel ARMIRQIssueIRQHandler \<Rightarrow> case y # ya # yb # yc # ysc of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW, index] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | irqW # triggerW # index # depth # xa \<Rightarrow> case z # zs of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | cnode # xa \<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 (cte_map slot) (triggerW \<noteq> 0)
odE | ArchInvocationLabel _ \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation) proof (prove)
goal (11 subgoals):
 1. \<And>a list z zs y ya yb yc ysc irq_active. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; unat y \<le> 159; \<not> irq_active\<rbrakk> \<Longrightarrow> corres (ser \<oplus> ?r'395 a list z zs y ya yb yc ysc irq_active) (?P395 a list z zs y ya yb yc ysc irq_active) (?P'395 a list z zs y ya yb yc ysc irq_active) (lookup_slot_for_cnode_op False a (to_bl yb) (unat yc)) (lookupSlotForCNodeOp False z yb (unat yc))
 2. \<And>a list z zs y ya yb yc ysc irq_active rv rv'. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; unat y \<le> 159; \<not> irq_active; ?r'395 a list z zs y ya yb yc ysc irq_active rv rv'\<rbrakk> \<Longrightarrow> corres (ser \<oplus> arch_irq_control_inv_relation) (?R395 a list z zs y ya yb yc ysc irq_active rv) (?R'395 a list z zs y ya yb yc ysc irq_active rv') (doE yb <- ensure_empty rv;
returnOk (ArchIRQControlIssue (UCAST(32 \<rightarrow> 10) y) rv slot (ya \<noteq> 0))
odE) (doE yb <- ensureEmptySlot rv';
returnOk (local.irqcontrol_invocation.IssueIRQHandler (UCAST(32 \<rightarrow> 10) y) rv' (cte_map slot) (ya \<noteq> 0))
odE)
 3. \<And>a list z zs y ya yb yc ysc irq_active. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; unat y \<le> 159; \<not> irq_active\<rbrakk> \<Longrightarrow> \<lbrace>?Q395 a list z zs y ya yb yc ysc irq_active\<rbrace> lookup_slot_for_cnode_op False a (to_bl yb) (unat yc) \<lbrace>?R395 a list z zs y ya yb yc ysc irq_active\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>a list z zs y ya yb yc ysc irq_active. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; unat y \<le> 159; \<not> irq_active\<rbrakk> \<Longrightarrow> \<lbrace>?Q'395 a list z zs y ya yb yc ysc irq_active\<rbrace> lookupSlotForCNodeOp False z yb (unat yc) \<lbrace>?R'395 a list z zs y ya yb yc ysc irq_active\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>a list z zs y ya yb yc ysc. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; unat y \<le> 159\<rbrakk> \<Longrightarrow> \<lbrace>?Q387 a list z zs y ya yb yc ysc ()\<rbrace> is_irq_active (UCAST(32 \<rightarrow> 10) y) \<lbrace>\<lambda>irq_active s. \<not> irq_active \<longrightarrow> (?P395 a list z zs y ya yb yc ysc irq_active and ?Q395 a list z zs y ya yb yc ysc irq_active) s\<rbrace>
 6. \<And>a list z zs y ya yb yc ysc. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; unat y \<le> 159\<rbrakk> \<Longrightarrow> \<lbrace>?Q'386 a list z zs y ya yb yc ysc ()\<rbrace> isIRQActive (UCAST(32 \<rightarrow> 10) y) \<lbrace>\<lambda>irq_active s. \<not> irq_active \<longrightarrow> (?P'395 a list z zs y ya yb yc ysc irq_active and ?Q'395 a list z zs y ya yb yc ysc irq_active) s\<rbrace>
 7. \<And>a list z zs y ya yb yc ysc. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler\<rbrakk> \<Longrightarrow> \<lbrace>?Q341 a list z zs y ya yb yc ysc\<rbrace> arch_check_irq y \<lbrace>\<lambda>yd. (\<lambda>_. True) and ?Q387 a list z zs y ya yb yc ysc yd and (\<lambda>s. unat y \<le> unat maxIRQ)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 8. \<And>a list z zs y ya yb yc ysc. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler\<rbrakk> \<Longrightarrow> \<lbrace>?Q'341 a list z zs y ya yb yc ysc\<rbrace> checkIRQ y \<lbrace>\<lambda>b. (\<lambda>_. True) and ?Q'386 a list z zs y ya yb yc ysc b\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 9. \<And>a list z zs y ya yb yc ysc s. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; (invs and (\<lambda>s. s \<turnstile> a \<and> (\<forall>cp\<in>set list. s \<turnstile> cp))) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q341 a list z zs y ya yb yc ysc) s
 10. \<And>a list z zs y ya yb yc ysc s. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; (invs' and (\<lambda>s. valid_cap' z s \<and> (\<forall>cp\<in>set zs. valid_cap' cp s))) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'341 a list z zs y ya yb yc ysc) s
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>a list z zs y ya yb yc ysc irq_active rv rv'. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; unat y \<le> 159; \<not> irq_active; rv' = cte_map rv\<rbrakk> \<Longrightarrow> corres (ser \<oplus> arch_irq_control_inv_relation) (?R395 a list z zs y ya yb yc ysc irq_active rv) (?R'395 a list z zs y ya yb yc ysc irq_active rv') (doE yb <- ensure_empty rv;
returnOk (ArchIRQControlIssue (UCAST(32 \<rightarrow> 10) y) rv slot (ya \<noteq> 0))
odE) (doE yb <- ensureEmptySlot rv';
returnOk (local.irqcontrol_invocation.IssueIRQHandler (UCAST(32 \<rightarrow> 10) y) rv' (cte_map slot) (ya \<noteq> 0))
odE)
 2. \<And>a list z zs y ya yb yc ysc irq_active. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; unat y \<le> 159; \<not> irq_active\<rbrakk> \<Longrightarrow> \<lbrace>?Q395 a list z zs y ya yb yc ysc irq_active\<rbrace> lookup_slot_for_cnode_op False a (to_bl yb) (unat yc) \<lbrace>?R395 a list z zs y ya yb yc ysc irq_active\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>a list z zs y ya yb yc ysc irq_active. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; unat y \<le> 159; \<not> irq_active\<rbrakk> \<Longrightarrow> \<lbrace>?Q'395 a list z zs y ya yb yc ysc irq_active\<rbrace> lookupSlotForCNodeOp False z yb (unat yc) \<lbrace>?R'395 a list z zs y ya yb yc ysc irq_active\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>a list z zs y ya yb yc ysc. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; unat y \<le> 159\<rbrakk> \<Longrightarrow> \<lbrace>?Q387 a list z zs y ya yb yc ysc ()\<rbrace> is_irq_active (UCAST(32 \<rightarrow> 10) y) \<lbrace>\<lambda>irq_active s. \<not> irq_active \<longrightarrow> (valid_objs and pspace_aligned and valid_cap a and ?Q395 a list z zs y ya yb yc ysc irq_active) s\<rbrace>
 5. \<And>a list z zs y ya yb yc ysc. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; unat y \<le> 159\<rbrakk> \<Longrightarrow> \<lbrace>?Q'386 a list z zs y ya yb yc ysc ()\<rbrace> isIRQActive (UCAST(32 \<rightarrow> 10) y) \<lbrace>\<lambda>irq_active s. \<not> irq_active \<longrightarrow> (valid_objs' and pspace_aligned' and pspace_distinct' and valid_cap' z and ?Q'395 a list z zs y ya yb yc ysc irq_active) s\<rbrace>
 6. \<And>a list z zs y ya yb yc ysc. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler\<rbrakk> \<Longrightarrow> \<lbrace>?Q341 a list z zs y ya yb yc ysc\<rbrace> arch_check_irq y \<lbrace>\<lambda>yd. (\<lambda>_. True) and ?Q387 a list z zs y ya yb yc ysc yd and (\<lambda>s. unat y \<le> unat maxIRQ)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>a list z zs y ya yb yc ysc. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler\<rbrakk> \<Longrightarrow> \<lbrace>?Q'341 a list z zs y ya yb yc ysc\<rbrace> checkIRQ y \<lbrace>\<lambda>b. (\<lambda>_. True) and ?Q'386 a list z zs y ya yb yc ysc b\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 8. \<And>a list z zs y ya yb yc ysc s. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; (invs and (\<lambda>s. s \<turnstile> a \<and> (\<forall>cp\<in>set list. s \<turnstile> cp))) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q341 a list z zs y ya yb yc ysc) s
 9. \<And>a list z zs y ya yb yc ysc s. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; (invs' and (\<lambda>s. valid_cap' z s \<and> (\<forall>cp\<in>set zs. valid_cap' cp s))) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'341 a list z zs y ya yb yc ysc) s
 10. \<And>a list z zs y ya yb yc ysc. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs\<rbrakk> \<Longrightarrow> invocation_type label \<noteq> ArchInvocationLabel ARMIRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> arch_irq_control_inv_relation) (invs and (\<lambda>s. s \<turnstile> a \<and> (\<forall>cp\<in>set list. s \<turnstile> cp))) (invs' and (\<lambda>s. valid_cap' z s \<and> (\<forall>cp\<in>set zs. valid_cap' cp s))) (throwError ExceptionTypes_A.syscall_error.IllegalOperation) (case invocation_type label of GenInvocationLabel gen_invocation_labels \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation | ArchInvocationLabel ARMIRQIssueIRQHandler \<Rightarrow> case y # ya # yb # yc # ysc of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW, index] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | irqW # triggerW # index # depth # xa \<Rightarrow> case z # zs of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | cnode # xa \<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 (cte_map slot) (triggerW \<noteq> 0)
odE | ArchInvocationLabel _ \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation) proof (prove)
goal (13 subgoals):
 1. \<And>a list z zs y ya yb yc ysc irq_active rv rv'. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; unat y \<le> 159; \<not> irq_active; rv' = cte_map rv\<rbrakk> \<Longrightarrow> corres (ser \<oplus> ?r'409 a list z zs y ya yb yc ysc irq_active rv rv') (?P410 a list z zs y ya yb yc ysc irq_active rv) (?P'412 a list z zs y ya yb yc ysc irq_active rv') (ensure_empty rv) (ensureEmptySlot rv')
 2. \<And>a list z zs y ya yb yc ysc irq_active rv rv' rva rv'a. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; unat y \<le> 159; \<not> irq_active; rv' = cte_map rv; ?r'409 a list z zs y ya yb yc ysc irq_active rv rv' rva rv'a\<rbrakk> \<Longrightarrow> corres (ser \<oplus> arch_irq_control_inv_relation) (?R409 a list z zs y ya yb yc ysc irq_active rv rv' rva) (?R'409 a list z zs y ya yb yc ysc irq_active rv rv' rv'a) (returnOk (ArchIRQControlIssue (UCAST(32 \<rightarrow> 10) y) rv slot (ya \<noteq> 0))) (returnOk (local.irqcontrol_invocation.IssueIRQHandler (UCAST(32 \<rightarrow> 10) y) rv' (cte_map slot) (ya \<noteq> 0)))
 3. \<And>a list z zs y ya yb yc ysc irq_active rv rv'. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; unat y \<le> 159; \<not> irq_active; rv' = cte_map rv\<rbrakk> \<Longrightarrow> \<lbrace>?Q411 a list z zs y ya yb yc ysc irq_active rv\<rbrace> ensure_empty rv \<lbrace>?R409 a list z zs y ya yb yc ysc irq_active rv rv'\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>a list z zs y ya yb yc ysc irq_active rv rv'. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; unat y \<le> 159; \<not> irq_active; rv' = cte_map rv\<rbrakk> \<Longrightarrow> \<lbrace>?Q'413 a list z zs y ya yb yc ysc irq_active rv'\<rbrace> ensureEmptySlot rv' \<lbrace>?R'409 a list z zs y ya yb yc ysc irq_active rv rv'\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>a list z zs y ya yb yc ysc irq_active. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; unat y \<le> 159; \<not> irq_active\<rbrakk> \<Longrightarrow> \<lbrace>?Q395 a list z zs y ya yb yc ysc irq_active\<rbrace> lookup_slot_for_cnode_op False a (to_bl yb) (unat yc) \<lbrace>\<lambda>rv. ?P410 a list z zs y ya yb yc ysc irq_active rv and ?Q411 a list z zs y ya yb yc ysc irq_active rv\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>a list z zs y ya yb yc ysc irq_active. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; unat y \<le> 159; \<not> irq_active\<rbrakk> \<Longrightarrow> \<lbrace>?Q'395 a list z zs y ya yb yc ysc irq_active\<rbrace> lookupSlotForCNodeOp False z yb (unat yc) \<lbrace>\<lambda>rv'. ?P'412 a list z zs y ya yb yc ysc irq_active rv' and ?Q'413 a list z zs y ya yb yc ysc irq_active rv'\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>a list z zs y ya yb yc ysc. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; unat y \<le> 159\<rbrakk> \<Longrightarrow> \<lbrace>?Q387 a list z zs y ya yb yc ysc ()\<rbrace> is_irq_active (UCAST(32 \<rightarrow> 10) y) \<lbrace>\<lambda>irq_active s. \<not> irq_active \<longrightarrow> (valid_objs and pspace_aligned and valid_cap a and ?Q395 a list z zs y ya yb yc ysc irq_active) s\<rbrace>
 8. \<And>a list z zs y ya yb yc ysc. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; unat y \<le> 159\<rbrakk> \<Longrightarrow> \<lbrace>?Q'386 a list z zs y ya yb yc ysc ()\<rbrace> isIRQActive (UCAST(32 \<rightarrow> 10) y) \<lbrace>\<lambda>irq_active s. \<not> irq_active \<longrightarrow> (valid_objs' and pspace_aligned' and pspace_distinct' and valid_cap' z and ?Q'395 a list z zs y ya yb yc ysc irq_active) s\<rbrace>
 9. \<And>a list z zs y ya yb yc ysc. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler\<rbrakk> \<Longrightarrow> \<lbrace>?Q341 a list z zs y ya yb yc ysc\<rbrace> arch_check_irq y \<lbrace>\<lambda>yd. (\<lambda>_. True) and ?Q387 a list z zs y ya yb yc ysc yd and (\<lambda>s. unat y \<le> unat maxIRQ)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 10. \<And>a list z zs y ya yb yc ysc. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler\<rbrakk> \<Longrightarrow> \<lbrace>?Q'341 a list z zs y ya yb yc ysc\<rbrace> checkIRQ y \<lbrace>\<lambda>b. (\<lambda>_. True) and ?Q'386 a list z zs y ya yb yc ysc b\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
A total of 13 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>a list z zs y ya yb yc ysc irq_active rv rv' rva rv'a. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; unat y \<le> 159; \<not> irq_active; rv' = cte_map rv; dc rva rv'a\<rbrakk> \<Longrightarrow> corres (ser \<oplus> arch_irq_control_inv_relation) (?R409 a list z zs y ya yb yc ysc irq_active rv rv' rva) (?R'409 a list z zs y ya yb yc ysc irq_active rv rv' rv'a) (returnOk (ArchIRQControlIssue (UCAST(32 \<rightarrow> 10) y) rv slot (ya \<noteq> 0))) (returnOk (local.irqcontrol_invocation.IssueIRQHandler (UCAST(32 \<rightarrow> 10) y) rv' (cte_map slot) (ya \<noteq> 0)))
 2. \<And>a list z zs y ya yb yc ysc irq_active rv rv'. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; unat y \<le> 159; \<not> irq_active; rv' = cte_map rv\<rbrakk> \<Longrightarrow> \<lbrace>?Q411 a list z zs y ya yb yc ysc irq_active rv\<rbrace> ensure_empty rv \<lbrace>?R409 a list z zs y ya yb yc ysc irq_active rv rv'\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>a list z zs y ya yb yc ysc irq_active rv rv'. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; unat y \<le> 159; \<not> irq_active; rv' = cte_map rv\<rbrakk> \<Longrightarrow> \<lbrace>?Q'413 a list z zs y ya yb yc ysc irq_active rv'\<rbrace> ensureEmptySlot rv' \<lbrace>?R'409 a list z zs y ya yb yc ysc irq_active rv rv'\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>a list z zs y ya yb yc ysc irq_active. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; unat y \<le> 159; \<not> irq_active\<rbrakk> \<Longrightarrow> \<lbrace>?Q395 a list z zs y ya yb yc ysc irq_active\<rbrace> lookup_slot_for_cnode_op False a (to_bl yb) (unat yc) \<lbrace>\<lambda>rv. invs and cte_wp_at (\<lambda>_. True) rv and ?Q411 a list z zs y ya yb yc ysc irq_active rv\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>a list z zs y ya yb yc ysc irq_active. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; unat y \<le> 159; \<not> irq_active\<rbrakk> \<Longrightarrow> \<lbrace>?Q'395 a list z zs y ya yb yc ysc irq_active\<rbrace> lookupSlotForCNodeOp False z yb (unat yc) \<lbrace>\<lambda>rv'. invs' and ?Q'413 a list z zs y ya yb yc ysc irq_active rv'\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>a list z zs y ya yb yc ysc. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; unat y \<le> 159\<rbrakk> \<Longrightarrow> \<lbrace>?Q387 a list z zs y ya yb yc ysc ()\<rbrace> is_irq_active (UCAST(32 \<rightarrow> 10) y) \<lbrace>\<lambda>irq_active s. \<not> irq_active \<longrightarrow> (valid_objs and pspace_aligned and valid_cap a and ?Q395 a list z zs y ya yb yc ysc irq_active) s\<rbrace>
 7. \<And>a list z zs y ya yb yc ysc. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; unat y \<le> 159\<rbrakk> \<Longrightarrow> \<lbrace>?Q'386 a list z zs y ya yb yc ysc ()\<rbrace> isIRQActive (UCAST(32 \<rightarrow> 10) y) \<lbrace>\<lambda>irq_active s. \<not> irq_active \<longrightarrow> (valid_objs' and pspace_aligned' and pspace_distinct' and valid_cap' z and ?Q'395 a list z zs y ya yb yc ysc irq_active) s\<rbrace>
 8. \<And>a list z zs y ya yb yc ysc. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler\<rbrakk> \<Longrightarrow> \<lbrace>?Q341 a list z zs y ya yb yc ysc\<rbrace> arch_check_irq y \<lbrace>\<lambda>yd. (\<lambda>_. True) and ?Q387 a list z zs y ya yb yc ysc yd and (\<lambda>s. unat y \<le> unat maxIRQ)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 9. \<And>a list z zs y ya yb yc ysc. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler\<rbrakk> \<Longrightarrow> \<lbrace>?Q'341 a list z zs y ya yb yc ysc\<rbrace> checkIRQ y \<lbrace>\<lambda>b. (\<lambda>_. True) and ?Q'386 a list z zs y ya yb yc ysc b\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 10. \<And>a list z zs y ya yb yc ysc s. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; (invs and (\<lambda>s. s \<turnstile> a \<and> (\<forall>cp\<in>set list. s \<turnstile> cp))) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q341 a list z zs y ya yb yc ysc) s
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>a list z zs y ya yb yc ysc irq_active rv rv' rva rv'a. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; unat y \<le> 159; \<not> irq_active; rv' = cte_map rv; dc rva rv'a\<rbrakk> \<Longrightarrow> arch_irq_control_inv_relation (ArchIRQControlIssue (UCAST(32 \<rightarrow> 10) y) rv slot (ya \<noteq> 0)) (local.irqcontrol_invocation.IssueIRQHandler (UCAST(32 \<rightarrow> 10) y) rv' (cte_map slot) (ya \<noteq> 0))
 2. \<And>a list z zs y ya yb yc ysc irq_active rv rv'. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; unat y \<le> 159; \<not> irq_active; rv' = cte_map rv\<rbrakk> \<Longrightarrow> \<lbrace>?Q411 a list z zs y ya yb yc ysc irq_active rv\<rbrace> ensure_empty rv \<lbrace>\<lambda>rva _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>a list z zs y ya yb yc ysc irq_active rv rv'. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; unat y \<le> 159; \<not> irq_active; rv' = cte_map rv\<rbrakk> \<Longrightarrow> \<lbrace>?Q'413 a list z zs y ya yb yc ysc irq_active rv'\<rbrace> ensureEmptySlot rv' \<lbrace>\<lambda>rv'a _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>a list z zs y ya yb yc ysc irq_active. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; unat y \<le> 159; \<not> irq_active\<rbrakk> \<Longrightarrow> \<lbrace>?Q395 a list z zs y ya yb yc ysc irq_active\<rbrace> lookup_slot_for_cnode_op False a (to_bl yb) (unat yc) \<lbrace>\<lambda>rv. invs and cte_wp_at (\<lambda>_. True) rv and ?Q411 a list z zs y ya yb yc ysc irq_active rv\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>a list z zs y ya yb yc ysc irq_active. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; unat y \<le> 159; \<not> irq_active\<rbrakk> \<Longrightarrow> \<lbrace>?Q'395 a list z zs y ya yb yc ysc irq_active\<rbrace> lookupSlotForCNodeOp False z yb (unat yc) \<lbrace>\<lambda>rv'. invs' and ?Q'413 a list z zs y ya yb yc ysc irq_active rv'\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>a list z zs y ya yb yc ysc. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; unat y \<le> 159\<rbrakk> \<Longrightarrow> \<lbrace>?Q387 a list z zs y ya yb yc ysc ()\<rbrace> is_irq_active (UCAST(32 \<rightarrow> 10) y) \<lbrace>\<lambda>irq_active s. \<not> irq_active \<longrightarrow> (valid_objs and pspace_aligned and valid_cap a and ?Q395 a list z zs y ya yb yc ysc irq_active) s\<rbrace>
 7. \<And>a list z zs y ya yb yc ysc. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; unat y \<le> 159\<rbrakk> \<Longrightarrow> \<lbrace>?Q'386 a list z zs y ya yb yc ysc ()\<rbrace> isIRQActive (UCAST(32 \<rightarrow> 10) y) \<lbrace>\<lambda>irq_active s. \<not> irq_active \<longrightarrow> (valid_objs' and pspace_aligned' and pspace_distinct' and valid_cap' z and ?Q'395 a list z zs y ya yb yc ysc irq_active) s\<rbrace>
 8. \<And>a list z zs y ya yb yc ysc. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler\<rbrakk> \<Longrightarrow> \<lbrace>?Q341 a list z zs y ya yb yc ysc\<rbrace> arch_check_irq y \<lbrace>\<lambda>yd. (\<lambda>_. True) and ?Q387 a list z zs y ya yb yc ysc yd and (\<lambda>s. unat y \<le> unat maxIRQ)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 9. \<And>a list z zs y ya yb yc ysc. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler\<rbrakk> \<Longrightarrow> \<lbrace>?Q'341 a list z zs y ya yb yc ysc\<rbrace> checkIRQ y \<lbrace>\<lambda>b. (\<lambda>_. True) and ?Q'386 a list z zs y ya yb yc ysc b\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 10. \<And>a list z zs y ya yb yc ysc s. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; (invs and (\<lambda>s. s \<turnstile> a \<and> (\<forall>cp\<in>set list. s \<turnstile> cp))) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q341 a list z zs y ya yb yc ysc) s
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>a list z zs y ya yb yc ysc irq_active rv rv'. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; unat y \<le> 159; \<not> irq_active; rv' = cte_map rv\<rbrakk> \<Longrightarrow> \<lbrace>?Q411 a list z zs y ya yb yc ysc irq_active rv\<rbrace> ensure_empty rv \<lbrace>\<lambda>rva _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>a list z zs y ya yb yc ysc irq_active rv rv'. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; unat y \<le> 159; \<not> irq_active; rv' = cte_map rv\<rbrakk> \<Longrightarrow> \<lbrace>?Q'413 a list z zs y ya yb yc ysc irq_active rv'\<rbrace> ensureEmptySlot rv' \<lbrace>\<lambda>rv'a _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>a list z zs y ya yb yc ysc irq_active. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; unat y \<le> 159; \<not> irq_active\<rbrakk> \<Longrightarrow> \<lbrace>?Q395 a list z zs y ya yb yc ysc irq_active\<rbrace> lookup_slot_for_cnode_op False a (to_bl yb) (unat yc) \<lbrace>\<lambda>rv. invs and cte_wp_at (\<lambda>_. True) rv and ?Q411 a list z zs y ya yb yc ysc irq_active rv\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>a list z zs y ya yb yc ysc irq_active. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; unat y \<le> 159; \<not> irq_active\<rbrakk> \<Longrightarrow> \<lbrace>?Q'395 a list z zs y ya yb yc ysc irq_active\<rbrace> lookupSlotForCNodeOp False z yb (unat yc) \<lbrace>\<lambda>rv'. invs' and ?Q'413 a list z zs y ya yb yc ysc irq_active rv'\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>a list z zs y ya yb yc ysc. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; unat y \<le> 159\<rbrakk> \<Longrightarrow> \<lbrace>?Q387 a list z zs y ya yb yc ysc ()\<rbrace> is_irq_active (UCAST(32 \<rightarrow> 10) y) \<lbrace>\<lambda>irq_active s. \<not> irq_active \<longrightarrow> (valid_objs and pspace_aligned and valid_cap a and ?Q395 a list z zs y ya yb yc ysc irq_active) s\<rbrace>
 6. \<And>a list z zs y ya yb yc ysc. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; unat y \<le> 159\<rbrakk> \<Longrightarrow> \<lbrace>?Q'386 a list z zs y ya yb yc ysc ()\<rbrace> isIRQActive (UCAST(32 \<rightarrow> 10) y) \<lbrace>\<lambda>irq_active s. \<not> irq_active \<longrightarrow> (valid_objs' and pspace_aligned' and pspace_distinct' and valid_cap' z and ?Q'395 a list z zs y ya yb yc ysc irq_active) s\<rbrace>
 7. \<And>a list z zs y ya yb yc ysc. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler\<rbrakk> \<Longrightarrow> \<lbrace>?Q341 a list z zs y ya yb yc ysc\<rbrace> arch_check_irq y \<lbrace>\<lambda>yd. (\<lambda>_. True) and ?Q387 a list z zs y ya yb yc ysc yd and (\<lambda>s. unat y \<le> unat maxIRQ)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 8. \<And>a list z zs y ya yb yc ysc. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler\<rbrakk> \<Longrightarrow> \<lbrace>?Q'341 a list z zs y ya yb yc ysc\<rbrace> checkIRQ y \<lbrace>\<lambda>b. (\<lambda>_. True) and ?Q'386 a list z zs y ya yb yc ysc b\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 9. \<And>a list z zs y ya yb yc ysc s. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; (invs and (\<lambda>s. s \<turnstile> a \<and> (\<forall>cp\<in>set list. s \<turnstile> cp))) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q341 a list z zs y ya yb yc ysc) s
 10. \<And>a list z zs y ya yb yc ysc s. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; (invs' and (\<lambda>s. valid_cap' z s \<and> (\<forall>cp\<in>set zs. valid_cap' cp s))) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'341 a list z zs y ya yb yc ysc) s
A total of 11 subgoals... proof (prove)
goal (1 subgoal):
 1. \<And>a list z zs y ya yb yc ysc. \<lbrakk>caps = a # list; caps' = z # zs; args = y # ya # yb # yc # ysc; cap_relation a z; list_all2 cap_relation list zs; invocation_type label \<noteq> ArchInvocationLabel ARMIRQIssueIRQHandler\<rbrakk> \<Longrightarrow> corres (ser \<oplus> arch_irq_control_inv_relation) (invs and (\<lambda>s. s \<turnstile> a \<and> (\<forall>cp\<in>set list. s \<turnstile> cp))) (invs' and (\<lambda>s. valid_cap' z s \<and> (\<forall>cp\<in>set zs. valid_cap' cp s))) (throwError ExceptionTypes_A.syscall_error.IllegalOperation) (case invocation_type label of GenInvocationLabel gen_invocation_labels \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation | ArchInvocationLabel ARMIRQIssueIRQHandler \<Rightarrow> case y # ya # yb # yc # ysc of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, triggerW, index] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | irqW # triggerW # index # depth # xa \<Rightarrow> case z # zs of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | cnode # xa \<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 (cte_map slot) (triggerW \<noteq> 0)
odE | ArchInvocationLabel _ \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation) proof (prove)
goal:
No subgoals!