theory Interrupt_R

lemma decodeIRQControlInvocation_corres:
  "list_all2 cap_relation caps caps' \<Longrightarrow>
   corres (ser \<oplus> 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))
     (decode_irq_control_invocation label args slot caps)
     (decodeIRQControlInvocation label args (cte_map slot) caps')" apply (clarsimp simp: decode_irq_control_invocation_def decodeIRQControlInvocation_def
                        arch_check_irq_def ARM_H.checkIRQ_def
                  split del: if_split cong: if_cong
                  split: ) apply clarsimp apply (rule conjI, clarsimp) apply (rule conjI, clarsimp) apply (cases caps, simp split: list.split) apply (case_tac "\<exists>n. length args = Suc (Suc (Suc n))") apply (clarsimp simp: list_all2_Cons1 Let_def split_def liftE_bindE
                           length_Suc_conv checkIRQ_def ) defer apply (subgoal_tac "length args \<le> 2", clarsimp split: list.split) apply arith apply (simp add: minIRQ_def o_def) apply (auto intro!: corres_guard_imp[OF arch_decodeIRQControlInvocation_corres])[1] apply (auto intro!: corres_guard_imp[OF arch_decodeIRQControlInvocation_corres]
               dest!: not_le_imp_less
               simp: minIRQ_def o_def length_Suc_conv whenE_rangeCheck_eq ucast_nat_def
               split: list.splits)[1] apply (simp add: minIRQ_def o_def length_Suc_conv whenE_rangeCheck_eq) apply (rule corres_guard_imp) apply (rule whenE_throwError_corres, clarsimp, clarsimp) 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
               simp: not_less unat_le_helper) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. list_all2 cap_relation caps caps' \<Longrightarrow> corres (ser \<oplus> 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)) (decode_irq_control_invocation label args slot caps) (global.decodeIRQControlInvocation label args (cte_map slot) caps') proof (prove)
goal (1 subgoal):
 1. list_all2 cap_relation caps caps' \<Longrightarrow> corres (ser \<oplus> 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)) (if gen_invocation_type label = IRQIssueIRQHandler then if 3 \<le> length args \<and> Suc 0 \<le> length caps then let irq_word = args ! 0; irq = UCAST(32 \<rightarrow> 10) irq_word in doE y <- whenE (UCAST(10 \<rightarrow> 32) maxIRQ < irq_word) (throwError (ExceptionTypes_A.syscall_error.RangeError 0 (UCAST(10 \<rightarrow> 32) maxIRQ)));
irq_active <- liftE (is_irq_active irq);
y <- whenE irq_active (throwError ExceptionTypes_A.syscall_error.RevokeFirst);
dest_slot <- lookup_slot_for_cnode_op False (caps ! 0) (to_bl (args ! Suc 0)) (unat (args ! 2));
y <- ensure_empty dest_slot;
returnOk (IRQControl irq dest_slot slot)
odE else throwError ExceptionTypes_A.syscall_error.TruncatedMessage else liftME irq_control_invocation.ArchIRQControl (arch_decode_irq_control_invocation label args slot caps)) (case gen_invocation_type label of IRQIssueIRQHandler \<Rightarrow> case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, index] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | irqW # index # depth # x \<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 $ Invocations_H.irqcontrol_invocation.IssueIRQHandler irq destSlot (cte_map slot)
odE | _ \<Rightarrow> liftME irqcontrol_invocation.ArchIRQControl $ Arch.decodeIRQControlInvocation label args (cte_map slot) caps') proof (prove)
goal (1 subgoal):
 1. list_all2 cap_relation caps caps' \<Longrightarrow> (3 \<le> length args \<and> Suc 0 \<le> length caps \<longrightarrow> (gen_invocation_type label = IRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> 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)) (let irq_word = args ! 0; irq = UCAST(32 \<rightarrow> 10) irq_word in doE y <- whenE (UCAST(10 \<rightarrow> 32) maxIRQ < irq_word) (throwError (ExceptionTypes_A.syscall_error.RangeError 0 (UCAST(10 \<rightarrow> 32) maxIRQ)));
irq_active <- liftE (is_irq_active irq);
y <- whenE irq_active (throwError ExceptionTypes_A.syscall_error.RevokeFirst);
dest_slot <- lookup_slot_for_cnode_op False (caps ! 0) (to_bl (args ! Suc 0)) (unat (args ! 2));
y <- ensure_empty dest_slot;
returnOk (IRQControl irq dest_slot slot)
odE) (case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, index] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | irqW # index # depth # x \<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 $ Invocations_H.irqcontrol_invocation.IssueIRQHandler irq destSlot (cte_map slot)
odE)) \<and> (gen_invocation_type label \<noteq> IRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> ((\<lambda>x. irq_control_inv_relation x \<circ> irqcontrol_invocation.ArchIRQControl) \<circ> irq_control_invocation.ArchIRQControl)) (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'))) \<and> ((3 \<le> length args \<longrightarrow> \<not> Suc 0 \<le> length caps) \<longrightarrow> (gen_invocation_type label = IRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> 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, index] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | irqW # index # depth # x \<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 $ Invocations_H.irqcontrol_invocation.IssueIRQHandler irq destSlot (cte_map slot)
odE)) \<and> (gen_invocation_type label \<noteq> IRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> ((\<lambda>x. irq_control_inv_relation x \<circ> irqcontrol_invocation.ArchIRQControl) \<circ> irq_control_invocation.ArchIRQControl)) (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 (2 subgoals):
 1. \<lbrakk>list_all2 cap_relation caps caps'; 3 \<le> length args; Suc 0 \<le> length caps\<rbrakk> \<Longrightarrow> (gen_invocation_type label = IRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> 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)) (let irq_word = args ! 0; irq = UCAST(32 \<rightarrow> 10) irq_word in doE y <- whenE (UCAST(10 \<rightarrow> 32) maxIRQ < irq_word) (throwError (ExceptionTypes_A.syscall_error.RangeError 0 (UCAST(10 \<rightarrow> 32) maxIRQ)));
irq_active <- liftE (is_irq_active irq);
y <- whenE irq_active (throwError ExceptionTypes_A.syscall_error.RevokeFirst);
dest_slot <- lookup_slot_for_cnode_op False (caps ! 0) (to_bl (args ! Suc 0)) (unat (args ! 2));
y <- ensure_empty dest_slot;
returnOk (IRQControl irq dest_slot slot)
odE) (case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, index] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | irqW # index # depth # x \<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 $ Invocations_H.irqcontrol_invocation.IssueIRQHandler irq destSlot (cte_map slot)
odE)) \<and> (gen_invocation_type label \<noteq> IRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> ((\<lambda>x. irq_control_inv_relation x \<circ> irqcontrol_invocation.ArchIRQControl) \<circ> irq_control_invocation.ArchIRQControl)) (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'))
 2. list_all2 cap_relation caps caps' \<Longrightarrow> (3 \<le> length args \<longrightarrow> \<not> Suc 0 \<le> length caps) \<longrightarrow> (gen_invocation_type label = IRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> 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, index] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | irqW # index # depth # x \<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 $ Invocations_H.irqcontrol_invocation.IssueIRQHandler irq destSlot (cte_map slot)
odE)) \<and> (gen_invocation_type label \<noteq> IRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> ((\<lambda>x. irq_control_inv_relation x \<circ> irqcontrol_invocation.ArchIRQControl) \<circ> irq_control_invocation.ArchIRQControl)) (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 (3 subgoals):
 1. \<lbrakk>list_all2 cap_relation caps caps'; 3 \<le> length args; Suc 0 \<le> length caps; gen_invocation_type label = IRQIssueIRQHandler\<rbrakk> \<Longrightarrow> corres (ser \<oplus> 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)) (let irq_word = args ! 0; irq = UCAST(32 \<rightarrow> 10) irq_word in doE y <- whenE (UCAST(10 \<rightarrow> 32) maxIRQ < irq_word) (throwError (ExceptionTypes_A.syscall_error.RangeError 0 (UCAST(10 \<rightarrow> 32) maxIRQ)));
irq_active <- liftE (is_irq_active irq);
y <- whenE irq_active (throwError ExceptionTypes_A.syscall_error.RevokeFirst);
dest_slot <- lookup_slot_for_cnode_op False (caps ! 0) (to_bl (args ! Suc 0)) (unat (args ! 2));
y <- ensure_empty dest_slot;
returnOk (IRQControl irq dest_slot slot)
odE) (case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, index] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | irqW # index # depth # x \<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 $ Invocations_H.irqcontrol_invocation.IssueIRQHandler irq destSlot (cte_map slot)
odE)
 2. \<lbrakk>list_all2 cap_relation caps caps'; 3 \<le> length args; Suc 0 \<le> length caps\<rbrakk> \<Longrightarrow> gen_invocation_type label \<noteq> IRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> ((\<lambda>x. irq_control_inv_relation x \<circ> irqcontrol_invocation.ArchIRQControl) \<circ> irq_control_invocation.ArchIRQControl)) (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')
 3. list_all2 cap_relation caps caps' \<Longrightarrow> (3 \<le> length args \<longrightarrow> \<not> Suc 0 \<le> length caps) \<longrightarrow> (gen_invocation_type label = IRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> 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, index] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | irqW # index # depth # x \<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 $ Invocations_H.irqcontrol_invocation.IssueIRQHandler irq destSlot (cte_map slot)
odE)) \<and> (gen_invocation_type label \<noteq> IRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> ((\<lambda>x. irq_control_inv_relation x \<circ> irqcontrol_invocation.ArchIRQControl) \<circ> irq_control_invocation.ArchIRQControl)) (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 (3 subgoals):
 1. \<And>a list. \<lbrakk>list_all2 cap_relation caps caps'; 3 \<le> length args; Suc 0 \<le> length caps; gen_invocation_type label = IRQIssueIRQHandler; caps = a # list\<rbrakk> \<Longrightarrow> corres (ser \<oplus> 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)) (let irq_word = args ! 0; irq = UCAST(32 \<rightarrow> 10) irq_word in doE y <- whenE (UCAST(10 \<rightarrow> 32) maxIRQ < irq_word) (throwError (ExceptionTypes_A.syscall_error.RangeError 0 (UCAST(10 \<rightarrow> 32) maxIRQ)));
irq_active <- liftE (is_irq_active irq);
y <- whenE irq_active (throwError ExceptionTypes_A.syscall_error.RevokeFirst);
dest_slot <- lookup_slot_for_cnode_op False (caps ! 0) (to_bl (args ! Suc 0)) (unat (args ! 2));
y <- ensure_empty dest_slot;
returnOk (IRQControl irq dest_slot slot)
odE) (case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, index] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | irqW # index # depth # x \<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 $ Invocations_H.irqcontrol_invocation.IssueIRQHandler irq destSlot (cte_map slot)
odE)
 2. \<lbrakk>list_all2 cap_relation caps caps'; 3 \<le> length args; Suc 0 \<le> length caps\<rbrakk> \<Longrightarrow> gen_invocation_type label \<noteq> IRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> ((\<lambda>x. irq_control_inv_relation x \<circ> irqcontrol_invocation.ArchIRQControl) \<circ> irq_control_invocation.ArchIRQControl)) (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')
 3. list_all2 cap_relation caps caps' \<Longrightarrow> (3 \<le> length args \<longrightarrow> \<not> Suc 0 \<le> length caps) \<longrightarrow> (gen_invocation_type label = IRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> 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, index] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | irqW # index # depth # x \<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 $ Invocations_H.irqcontrol_invocation.IssueIRQHandler irq destSlot (cte_map slot)
odE)) \<and> (gen_invocation_type label \<noteq> IRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> ((\<lambda>x. irq_control_inv_relation x \<circ> irqcontrol_invocation.ArchIRQControl) \<circ> irq_control_invocation.ArchIRQControl)) (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 (4 subgoals):
 1. \<And>a list. \<lbrakk>list_all2 cap_relation caps caps'; 3 \<le> length args; Suc 0 \<le> length caps; gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; \<exists>n. length args = Suc (Suc (Suc n))\<rbrakk> \<Longrightarrow> corres (ser \<oplus> 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)) (let irq_word = args ! 0; irq = UCAST(32 \<rightarrow> 10) irq_word in doE y <- whenE (UCAST(10 \<rightarrow> 32) maxIRQ < irq_word) (throwError (ExceptionTypes_A.syscall_error.RangeError 0 (UCAST(10 \<rightarrow> 32) maxIRQ)));
irq_active <- liftE (is_irq_active irq);
y <- whenE irq_active (throwError ExceptionTypes_A.syscall_error.RevokeFirst);
dest_slot <- lookup_slot_for_cnode_op False (caps ! 0) (to_bl (args ! Suc 0)) (unat (args ! 2));
y <- ensure_empty dest_slot;
returnOk (IRQControl irq dest_slot slot)
odE) (case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, index] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | irqW # index # depth # x \<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 $ Invocations_H.irqcontrol_invocation.IssueIRQHandler irq destSlot (cte_map slot)
odE)
 2. \<And>a list. \<lbrakk>list_all2 cap_relation caps caps'; 3 \<le> length args; Suc 0 \<le> length caps; gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; \<nexists>n. length args = Suc (Suc (Suc n))\<rbrakk> \<Longrightarrow> corres (ser \<oplus> 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)) (let irq_word = args ! 0; irq = UCAST(32 \<rightarrow> 10) irq_word in doE y <- whenE (UCAST(10 \<rightarrow> 32) maxIRQ < irq_word) (throwError (ExceptionTypes_A.syscall_error.RangeError 0 (UCAST(10 \<rightarrow> 32) maxIRQ)));
irq_active <- liftE (is_irq_active irq);
y <- whenE irq_active (throwError ExceptionTypes_A.syscall_error.RevokeFirst);
dest_slot <- lookup_slot_for_cnode_op False (caps ! 0) (to_bl (args ! Suc 0)) (unat (args ! 2));
y <- ensure_empty dest_slot;
returnOk (IRQControl irq dest_slot slot)
odE) (case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, index] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | irqW # index # depth # x \<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 $ Invocations_H.irqcontrol_invocation.IssueIRQHandler irq destSlot (cte_map slot)
odE)
 3. \<lbrakk>list_all2 cap_relation caps caps'; 3 \<le> length args; Suc 0 \<le> length caps\<rbrakk> \<Longrightarrow> gen_invocation_type label \<noteq> IRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> ((\<lambda>x. irq_control_inv_relation x \<circ> irqcontrol_invocation.ArchIRQControl) \<circ> irq_control_invocation.ArchIRQControl)) (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')
 4. list_all2 cap_relation caps caps' \<Longrightarrow> (3 \<le> length args \<longrightarrow> \<not> Suc 0 \<le> length caps) \<longrightarrow> (gen_invocation_type label = IRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> 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, index] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | irqW # index # depth # x \<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 $ Invocations_H.irqcontrol_invocation.IssueIRQHandler irq destSlot (cte_map slot)
odE)) \<and> (gen_invocation_type label \<noteq> IRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> ((\<lambda>x. irq_control_inv_relation x \<circ> irqcontrol_invocation.ArchIRQControl) \<circ> irq_control_invocation.ArchIRQControl)) (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 (4 subgoals):
 1. \<And>a list z zs y ya yb ysb. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs\<rbrakk> \<Longrightarrow> corres (ser \<oplus> 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 yc <- whenE (UCAST(10 \<rightarrow> 32) maxIRQ < y) (throwError (ExceptionTypes_A.syscall_error.RangeError 0 (UCAST(10 \<rightarrow> 32) maxIRQ)));
do irq_active <- is_irq_active (UCAST(32 \<rightarrow> 10) y);
doE yc <- whenE irq_active (throwError ExceptionTypes_A.syscall_error.RevokeFirst);
dest_slot <- lookup_slot_for_cnode_op False a (to_bl ya) (unat yb);
ya <- ensure_empty dest_slot;
returnOk (IRQControl (UCAST(32 \<rightarrow> 10) y) dest_slot slot)
odE
od
odE) (doE yc <- rangeCheck y (unat minIRQ) (unat maxIRQ);
do irqActive <- isIRQActive (toEnum (unat y));
doE yc <- whenE irqActive (throwError Fault_H.syscall_error.RevokeFirst);
destSlot <- lookupSlotForCNodeOp False z ya (unat yb);
ya <- ensureEmptySlot destSlot;
returnOk (Invocations_H.irqcontrol_invocation.IssueIRQHandler (toEnum (unat y)) destSlot (cte_map slot))
odE
od
odE)
 2. \<And>a list. \<lbrakk>list_all2 cap_relation caps caps'; 3 \<le> length args; Suc 0 \<le> length caps; gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; \<nexists>n. length args = Suc (Suc (Suc n))\<rbrakk> \<Longrightarrow> corres (ser \<oplus> 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)) (let irq_word = args ! 0; irq = UCAST(32 \<rightarrow> 10) irq_word in doE y <- whenE (UCAST(10 \<rightarrow> 32) maxIRQ < irq_word) (throwError (ExceptionTypes_A.syscall_error.RangeError 0 (UCAST(10 \<rightarrow> 32) maxIRQ)));
irq_active <- liftE (is_irq_active irq);
y <- whenE irq_active (throwError ExceptionTypes_A.syscall_error.RevokeFirst);
dest_slot <- lookup_slot_for_cnode_op False (caps ! 0) (to_bl (args ! Suc 0)) (unat (args ! 2));
y <- ensure_empty dest_slot;
returnOk (IRQControl irq dest_slot slot)
odE) (case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, index] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | irqW # index # depth # x \<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 $ Invocations_H.irqcontrol_invocation.IssueIRQHandler irq destSlot (cte_map slot)
odE)
 3. \<lbrakk>list_all2 cap_relation caps caps'; 3 \<le> length args; Suc 0 \<le> length caps\<rbrakk> \<Longrightarrow> gen_invocation_type label \<noteq> IRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> ((\<lambda>x. irq_control_inv_relation x \<circ> irqcontrol_invocation.ArchIRQControl) \<circ> irq_control_invocation.ArchIRQControl)) (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')
 4. list_all2 cap_relation caps caps' \<Longrightarrow> (3 \<le> length args \<longrightarrow> \<not> Suc 0 \<le> length caps) \<longrightarrow> (gen_invocation_type label = IRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> 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, index] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | irqW # index # depth # x \<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 $ Invocations_H.irqcontrol_invocation.IssueIRQHandler irq destSlot (cte_map slot)
odE)) \<and> (gen_invocation_type label \<noteq> IRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> ((\<lambda>x. irq_control_inv_relation x \<circ> irqcontrol_invocation.ArchIRQControl) \<circ> irq_control_invocation.ArchIRQControl)) (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 (4 subgoals):
 1. \<And>a list. \<lbrakk>list_all2 cap_relation caps caps'; 3 \<le> length args; Suc 0 \<le> length caps; gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; \<nexists>n. length args = Suc (Suc (Suc n))\<rbrakk> \<Longrightarrow> corres (ser \<oplus> 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)) (let irq_word = args ! 0; irq = UCAST(32 \<rightarrow> 10) irq_word in doE y <- whenE (UCAST(10 \<rightarrow> 32) maxIRQ < irq_word) (throwError (ExceptionTypes_A.syscall_error.RangeError 0 (UCAST(10 \<rightarrow> 32) maxIRQ)));
irq_active <- liftE (is_irq_active irq);
y <- whenE irq_active (throwError ExceptionTypes_A.syscall_error.RevokeFirst);
dest_slot <- lookup_slot_for_cnode_op False (caps ! 0) (to_bl (args ! Suc 0)) (unat (args ! 2));
y <- ensure_empty dest_slot;
returnOk (IRQControl irq dest_slot slot)
odE) (case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [irqW, index] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | irqW # index # depth # x \<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 $ Invocations_H.irqcontrol_invocation.IssueIRQHandler irq destSlot (cte_map slot)
odE)
 2. \<lbrakk>list_all2 cap_relation caps caps'; 3 \<le> length args; Suc 0 \<le> length caps\<rbrakk> \<Longrightarrow> gen_invocation_type label \<noteq> IRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> ((\<lambda>x. irq_control_inv_relation x \<circ> irqcontrol_invocation.ArchIRQControl) \<circ> irq_control_invocation.ArchIRQControl)) (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')
 3. list_all2 cap_relation caps caps' \<Longrightarrow> (3 \<le> length args \<longrightarrow> \<not> Suc 0 \<le> length caps) \<longrightarrow> (gen_invocation_type label = IRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> 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, index] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | irqW # index # depth # x \<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 $ Invocations_H.irqcontrol_invocation.IssueIRQHandler irq destSlot (cte_map slot)
odE)) \<and> (gen_invocation_type label \<noteq> IRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> ((\<lambda>x. irq_control_inv_relation x \<circ> irqcontrol_invocation.ArchIRQControl) \<circ> irq_control_invocation.ArchIRQControl)) (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'))
 4. \<And>a list z zs y ya yb ysb. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs\<rbrakk> \<Longrightarrow> corres (ser \<oplus> 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 yc <- whenE (UCAST(10 \<rightarrow> 32) maxIRQ < y) (throwError (ExceptionTypes_A.syscall_error.RangeError 0 (UCAST(10 \<rightarrow> 32) maxIRQ)));
do irq_active <- is_irq_active (UCAST(32 \<rightarrow> 10) y);
doE yc <- whenE irq_active (throwError ExceptionTypes_A.syscall_error.RevokeFirst);
dest_slot <- lookup_slot_for_cnode_op False a (to_bl ya) (unat yb);
ya <- ensure_empty dest_slot;
returnOk (IRQControl (UCAST(32 \<rightarrow> 10) y) dest_slot slot)
odE
od
odE) (doE yc <- rangeCheck y (unat minIRQ) (unat maxIRQ);
do irqActive <- isIRQActive (toEnum (unat y));
doE yc <- whenE irqActive (throwError Fault_H.syscall_error.RevokeFirst);
destSlot <- lookupSlotForCNodeOp False z ya (unat yb);
ya <- ensureEmptySlot destSlot;
returnOk (Invocations_H.irqcontrol_invocation.IssueIRQHandler (toEnum (unat y)) destSlot (cte_map slot))
odE
od
odE) proof (prove)
goal (4 subgoals):
 1. \<And>a list. \<lbrakk>list_all2 cap_relation caps caps'; 3 \<le> length args; Suc 0 \<le> length caps; gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; \<nexists>n. length args = Suc (Suc (Suc n))\<rbrakk> \<Longrightarrow> length args \<le> 2
 2. \<lbrakk>list_all2 cap_relation caps caps'; 3 \<le> length args; Suc 0 \<le> length caps\<rbrakk> \<Longrightarrow> gen_invocation_type label \<noteq> IRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> ((\<lambda>x. irq_control_inv_relation x \<circ> irqcontrol_invocation.ArchIRQControl) \<circ> irq_control_invocation.ArchIRQControl)) (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')
 3. list_all2 cap_relation caps caps' \<Longrightarrow> (3 \<le> length args \<longrightarrow> \<not> Suc 0 \<le> length caps) \<longrightarrow> (gen_invocation_type label = IRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> 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, index] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | irqW # index # depth # x \<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 $ Invocations_H.irqcontrol_invocation.IssueIRQHandler irq destSlot (cte_map slot)
odE)) \<and> (gen_invocation_type label \<noteq> IRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> ((\<lambda>x. irq_control_inv_relation x \<circ> irqcontrol_invocation.ArchIRQControl) \<circ> irq_control_invocation.ArchIRQControl)) (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'))
 4. \<And>a list z zs y ya yb ysb. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs\<rbrakk> \<Longrightarrow> corres (ser \<oplus> 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 yc <- whenE (UCAST(10 \<rightarrow> 32) maxIRQ < y) (throwError (ExceptionTypes_A.syscall_error.RangeError 0 (UCAST(10 \<rightarrow> 32) maxIRQ)));
do irq_active <- is_irq_active (UCAST(32 \<rightarrow> 10) y);
doE yc <- whenE irq_active (throwError ExceptionTypes_A.syscall_error.RevokeFirst);
dest_slot <- lookup_slot_for_cnode_op False a (to_bl ya) (unat yb);
ya <- ensure_empty dest_slot;
returnOk (IRQControl (UCAST(32 \<rightarrow> 10) y) dest_slot slot)
odE
od
odE) (doE yc <- rangeCheck y (unat minIRQ) (unat maxIRQ);
do irqActive <- isIRQActive (toEnum (unat y));
doE yc <- whenE irqActive (throwError Fault_H.syscall_error.RevokeFirst);
destSlot <- lookupSlotForCNodeOp False z ya (unat yb);
ya <- ensureEmptySlot destSlot;
returnOk (Invocations_H.irqcontrol_invocation.IssueIRQHandler (toEnum (unat y)) destSlot (cte_map slot))
odE
od
odE) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>list_all2 cap_relation caps caps'; 3 \<le> length args; Suc 0 \<le> length caps\<rbrakk> \<Longrightarrow> gen_invocation_type label \<noteq> IRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> ((\<lambda>x. irq_control_inv_relation x \<circ> irqcontrol_invocation.ArchIRQControl) \<circ> irq_control_invocation.ArchIRQControl)) (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')
 2. list_all2 cap_relation caps caps' \<Longrightarrow> (3 \<le> length args \<longrightarrow> \<not> Suc 0 \<le> length caps) \<longrightarrow> (gen_invocation_type label = IRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> 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, index] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | irqW # index # depth # x \<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 $ Invocations_H.irqcontrol_invocation.IssueIRQHandler irq destSlot (cte_map slot)
odE)) \<and> (gen_invocation_type label \<noteq> IRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> ((\<lambda>x. irq_control_inv_relation x \<circ> irqcontrol_invocation.ArchIRQControl) \<circ> irq_control_invocation.ArchIRQControl)) (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'))
 3. \<And>a list z zs y ya yb ysb. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs\<rbrakk> \<Longrightarrow> corres (ser \<oplus> 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 yc <- whenE (UCAST(10 \<rightarrow> 32) maxIRQ < y) (throwError (ExceptionTypes_A.syscall_error.RangeError 0 (UCAST(10 \<rightarrow> 32) maxIRQ)));
do irq_active <- is_irq_active (UCAST(32 \<rightarrow> 10) y);
doE yc <- whenE irq_active (throwError ExceptionTypes_A.syscall_error.RevokeFirst);
dest_slot <- lookup_slot_for_cnode_op False a (to_bl ya) (unat yb);
ya <- ensure_empty dest_slot;
returnOk (IRQControl (UCAST(32 \<rightarrow> 10) y) dest_slot slot)
odE
od
odE) (doE yc <- rangeCheck y (unat minIRQ) (unat maxIRQ);
do irqActive <- isIRQActive (toEnum (unat y));
doE yc <- whenE irqActive (throwError Fault_H.syscall_error.RevokeFirst);
destSlot <- lookupSlotForCNodeOp False z ya (unat yb);
ya <- ensureEmptySlot destSlot;
returnOk (Invocations_H.irqcontrol_invocation.IssueIRQHandler (toEnum (unat y)) destSlot (cte_map slot))
odE
od
odE) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>list_all2 cap_relation caps caps'; 3 \<le> length args; Suc 0 \<le> length caps\<rbrakk> \<Longrightarrow> gen_invocation_type label \<noteq> IRQIssueIRQHandler \<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')
 2. list_all2 cap_relation caps caps' \<Longrightarrow> (3 \<le> length args \<longrightarrow> \<not> Suc 0 \<le> length caps) \<longrightarrow> (gen_invocation_type label = IRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> 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, index] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | irqW # index # depth # x \<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 $ Invocations_H.irqcontrol_invocation.IssueIRQHandler irq destSlot (cte_map slot)
odE)) \<and> (gen_invocation_type label \<noteq> IRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> ((\<lambda>x. irq_control_inv_relation x \<circ> irqcontrol_invocation.ArchIRQControl) \<circ> irq_control_invocation.ArchIRQControl)) (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'))
 3. \<And>a list z zs y ya yb ysb. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs\<rbrakk> \<Longrightarrow> corres (ser \<oplus> 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 yc <- whenE (UCAST(10 \<rightarrow> 32) maxIRQ < y) (throwError (ExceptionTypes_A.syscall_error.RangeError 0 (UCAST(10 \<rightarrow> 32) maxIRQ)));
do irq_active <- is_irq_active (UCAST(32 \<rightarrow> 10) y);
doE yc <- whenE irq_active (throwError ExceptionTypes_A.syscall_error.RevokeFirst);
dest_slot <- lookup_slot_for_cnode_op False a (to_bl ya) (unat yb);
ya <- ensure_empty dest_slot;
returnOk (IRQControl (UCAST(32 \<rightarrow> 10) y) dest_slot slot)
odE
od
odE) (doE yc <- rangeCheck y (unat minIRQ) (unat maxIRQ);
do irqActive <- isIRQActive (toEnum (unat y));
doE yc <- whenE irqActive (throwError Fault_H.syscall_error.RevokeFirst);
destSlot <- lookupSlotForCNodeOp False z ya (unat yb);
ya <- ensureEmptySlot destSlot;
returnOk (Invocations_H.irqcontrol_invocation.IssueIRQHandler (toEnum (unat y)) destSlot (cte_map slot))
odE
od
odE) proof (prove)
goal (2 subgoals):
 1. list_all2 cap_relation caps caps' \<Longrightarrow> (3 \<le> length args \<longrightarrow> \<not> Suc 0 \<le> length caps) \<longrightarrow> (gen_invocation_type label = IRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> 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, index] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | irqW # index # depth # x \<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 $ Invocations_H.irqcontrol_invocation.IssueIRQHandler irq destSlot (cte_map slot)
odE)) \<and> (gen_invocation_type label \<noteq> IRQIssueIRQHandler \<longrightarrow> corres (ser \<oplus> ((\<lambda>x. irq_control_inv_relation x \<circ> irqcontrol_invocation.ArchIRQControl) \<circ> irq_control_invocation.ArchIRQControl)) (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'))
 2. \<And>a list z zs y ya yb ysb. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs\<rbrakk> \<Longrightarrow> corres (ser \<oplus> 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 yc <- whenE (UCAST(10 \<rightarrow> 32) maxIRQ < y) (throwError (ExceptionTypes_A.syscall_error.RangeError 0 (UCAST(10 \<rightarrow> 32) maxIRQ)));
do irq_active <- is_irq_active (UCAST(32 \<rightarrow> 10) y);
doE yc <- whenE irq_active (throwError ExceptionTypes_A.syscall_error.RevokeFirst);
dest_slot <- lookup_slot_for_cnode_op False a (to_bl ya) (unat yb);
ya <- ensure_empty dest_slot;
returnOk (IRQControl (UCAST(32 \<rightarrow> 10) y) dest_slot slot)
odE
od
odE) (doE yc <- rangeCheck y (unat minIRQ) (unat maxIRQ);
do irqActive <- isIRQActive (toEnum (unat y));
doE yc <- whenE irqActive (throwError Fault_H.syscall_error.RevokeFirst);
destSlot <- lookupSlotForCNodeOp False z ya (unat yb);
ya <- ensureEmptySlot destSlot;
returnOk (Invocations_H.irqcontrol_invocation.IssueIRQHandler (toEnum (unat y)) destSlot (cte_map slot))
odE
od
odE) proof (prove)
goal (1 subgoal):
 1. \<And>a list z zs y ya yb ysb. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs\<rbrakk> \<Longrightarrow> corres (ser \<oplus> 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 yc <- whenE (UCAST(10 \<rightarrow> 32) maxIRQ < y) (throwError (ExceptionTypes_A.syscall_error.RangeError 0 (UCAST(10 \<rightarrow> 32) maxIRQ)));
do irq_active <- is_irq_active (UCAST(32 \<rightarrow> 10) y);
doE yc <- whenE irq_active (throwError ExceptionTypes_A.syscall_error.RevokeFirst);
dest_slot <- lookup_slot_for_cnode_op False a (to_bl ya) (unat yb);
ya <- ensure_empty dest_slot;
returnOk (IRQControl (UCAST(32 \<rightarrow> 10) y) dest_slot slot)
odE
od
odE) (doE yc <- rangeCheck y (unat minIRQ) (unat maxIRQ);
do irqActive <- isIRQActive (toEnum (unat y));
doE yc <- whenE irqActive (throwError Fault_H.syscall_error.RevokeFirst);
destSlot <- lookupSlotForCNodeOp False z ya (unat yb);
ya <- ensureEmptySlot destSlot;
returnOk (Invocations_H.irqcontrol_invocation.IssueIRQHandler (toEnum (unat y)) destSlot (cte_map slot))
odE
od
odE) proof (prove)
goal (1 subgoal):
 1. \<And>a list z zs y ya yb ysb. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs\<rbrakk> \<Longrightarrow> corres (ser \<oplus> 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 yc <- whenE (UCAST(10 \<rightarrow> 32) maxIRQ < y) (throwError (ExceptionTypes_A.syscall_error.RangeError 0 (UCAST(10 \<rightarrow> 32) maxIRQ)));
do irq_active <- is_irq_active (UCAST(32 \<rightarrow> 10) y);
doE yc <- whenE irq_active (throwError ExceptionTypes_A.syscall_error.RevokeFirst);
dest_slot <- lookup_slot_for_cnode_op False a (to_bl ya) (unat yb);
ya <- ensure_empty dest_slot;
returnOk (IRQControl (UCAST(32 \<rightarrow> 10) y) dest_slot slot)
odE
od
odE) (doE yc <- whenE (UCAST(10 \<rightarrow> 32) maxIRQ < y) (throwError (Fault_H.syscall_error.RangeError 0 (UCAST(10 \<rightarrow> 32) maxIRQ)));
do irqActive <- isIRQActive (toEnum (unat y));
doE yc <- whenE irqActive (throwError Fault_H.syscall_error.RevokeFirst);
destSlot <- lookupSlotForCNodeOp False z ya (unat yb);
ya <- ensureEmptySlot destSlot;
returnOk (Invocations_H.irqcontrol_invocation.IssueIRQHandler (toEnum (unat y)) destSlot (cte_map slot))
odE
od
odE) proof (prove)
goal (3 subgoals):
 1. \<And>a list z zs y ya yb ysb. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs\<rbrakk> \<Longrightarrow> corres (ser \<oplus> irq_control_inv_relation) (?Q180 a list z zs y ya yb ysb) (?Q'180 a list z zs y ya yb ysb) (doE yc <- whenE (UCAST(10 \<rightarrow> 32) maxIRQ < y) (throwError (ExceptionTypes_A.syscall_error.RangeError 0 (UCAST(10 \<rightarrow> 32) maxIRQ)));
do irq_active <- is_irq_active (UCAST(32 \<rightarrow> 10) y);
doE yc <- whenE irq_active (throwError ExceptionTypes_A.syscall_error.RevokeFirst);
dest_slot <- lookup_slot_for_cnode_op False a (to_bl ya) (unat yb);
ya <- ensure_empty dest_slot;
returnOk (IRQControl (UCAST(32 \<rightarrow> 10) y) dest_slot slot)
odE
od
odE) (doE yc <- whenE (UCAST(10 \<rightarrow> 32) maxIRQ < y) (throwError (Fault_H.syscall_error.RangeError 0 (UCAST(10 \<rightarrow> 32) maxIRQ)));
do irqActive <- isIRQActive (toEnum (unat y));
doE yc <- whenE irqActive (throwError Fault_H.syscall_error.RevokeFirst);
destSlot <- lookupSlotForCNodeOp False z ya (unat yb);
ya <- ensureEmptySlot destSlot;
returnOk (Invocations_H.irqcontrol_invocation.IssueIRQHandler (toEnum (unat y)) destSlot (cte_map slot))
odE
od
odE)
 2. \<And>a list z zs y ya yb ysb s. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; (invs and (\<lambda>s. s \<turnstile> a \<and> (\<forall>cp\<in>set list. s \<turnstile> cp))) s\<rbrakk> \<Longrightarrow> ?Q180 a list z zs y ya yb ysb s
 3. \<And>a list z zs y ya yb ysb s. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; (invs' and (\<lambda>s. valid_cap' z s \<and> (\<forall>cp\<in>set zs. valid_cap' cp s))) s\<rbrakk> \<Longrightarrow> ?Q'180 a list z zs y ya yb ysb s proof (prove)
goal (3 subgoals):
 1. \<And>a list z zs y ya yb ysb. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; \<not> UCAST(10 \<rightarrow> 32) maxIRQ < y\<rbrakk> \<Longrightarrow> corres (ser \<oplus> irq_control_inv_relation) (?Q184 a list z zs y ya yb ysb) (?Q'184 a list z zs y ya yb ysb) (do irq_active <- is_irq_active (UCAST(32 \<rightarrow> 10) y);
doE yc <- whenE irq_active (throwError ExceptionTypes_A.syscall_error.RevokeFirst);
dest_slot <- lookup_slot_for_cnode_op False a (to_bl ya) (unat yb);
ya <- ensure_empty dest_slot;
returnOk (IRQControl (UCAST(32 \<rightarrow> 10) y) dest_slot slot)
odE
od) (do irqActive <- isIRQActive (toEnum (unat y));
doE yc <- whenE irqActive (throwError Fault_H.syscall_error.RevokeFirst);
destSlot <- lookupSlotForCNodeOp False z ya (unat yb);
ya <- ensureEmptySlot destSlot;
returnOk (Invocations_H.irqcontrol_invocation.IssueIRQHandler (toEnum (unat y)) destSlot (cte_map slot))
odE
od)
 2. \<And>a list z zs y ya yb ysb s. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; (invs and (\<lambda>s. s \<turnstile> a \<and> (\<forall>cp\<in>set list. s \<turnstile> cp))) s\<rbrakk> \<Longrightarrow> \<not> UCAST(10 \<rightarrow> 32) maxIRQ < y \<longrightarrow> ?Q184 a list z zs y ya yb ysb s
 3. \<And>a list z zs y ya yb ysb s. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; (invs' and (\<lambda>s. valid_cap' z s \<and> (\<forall>cp\<in>set zs. valid_cap' cp s))) s\<rbrakk> \<Longrightarrow> \<not> UCAST(10 \<rightarrow> 32) maxIRQ < y \<longrightarrow> ?Q'184 a list z zs y ya yb ysb s proof (prove)
goal (3 subgoals):
 1. \<And>a list z zs y ya yb ysb. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; \<not> UCAST(10 \<rightarrow> 32) maxIRQ < y; unat y \<le> unat maxIRQ\<rbrakk> \<Longrightarrow> corres (ser \<oplus> irq_control_inv_relation) (?P188 a list z zs y ya yb ysb) (?Q'184 a list z zs y ya yb ysb) (do irq_active <- is_irq_active (UCAST(32 \<rightarrow> 10) y);
doE yc <- whenE irq_active (throwError ExceptionTypes_A.syscall_error.RevokeFirst);
dest_slot <- lookup_slot_for_cnode_op False a (to_bl ya) (unat yb);
ya <- ensure_empty dest_slot;
returnOk (IRQControl (UCAST(32 \<rightarrow> 10) y) dest_slot slot)
odE
od) (do irqActive <- isIRQActive (toEnum (unat y));
doE yc <- whenE irqActive (throwError Fault_H.syscall_error.RevokeFirst);
destSlot <- lookupSlotForCNodeOp False z ya (unat yb);
ya <- ensureEmptySlot destSlot;
returnOk (Invocations_H.irqcontrol_invocation.IssueIRQHandler (toEnum (unat y)) destSlot (cte_map slot))
odE
od)
 2. \<And>a list z zs y ya yb ysb s. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; (invs and (\<lambda>s. s \<turnstile> a \<and> (\<forall>cp\<in>set list. s \<turnstile> cp))) s\<rbrakk> \<Longrightarrow> \<not> UCAST(10 \<rightarrow> 32) maxIRQ < y \<longrightarrow> (?P188 a list z zs y ya yb ysb and (\<lambda>s. unat y \<le> unat maxIRQ)) s
 3. \<And>a list z zs y ya yb ysb s. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; (invs' and (\<lambda>s. valid_cap' z s \<and> (\<forall>cp\<in>set zs. valid_cap' cp s))) s\<rbrakk> \<Longrightarrow> \<not> UCAST(10 \<rightarrow> 32) maxIRQ < y \<longrightarrow> ?Q'184 a list z zs y ya yb ysb s proof (prove)
goal (3 subgoals):
 1. \<And>a list z zs y ya yb ysb. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; \<not> 0x9F < y; unat y \<le> 159\<rbrakk> \<Longrightarrow> corres (ser \<oplus> irq_control_inv_relation) (?P188 a list z zs y ya yb ysb) (?Q'184 a list z zs y ya yb ysb) (do irq_active <- is_irq_active (UCAST(32 \<rightarrow> 10) y);
doE yc <- whenE irq_active (throwError ExceptionTypes_A.syscall_error.RevokeFirst);
dest_slot <- lookup_slot_for_cnode_op False a (to_bl ya) (unat yb);
ya <- ensure_empty dest_slot;
returnOk (IRQControl (UCAST(32 \<rightarrow> 10) y) dest_slot slot)
odE
od) (do irqActive <- isIRQActive (UCAST(32 \<rightarrow> 10) y);
doE yc <- whenE irqActive (throwError Fault_H.syscall_error.RevokeFirst);
destSlot <- lookupSlotForCNodeOp False z ya (unat yb);
ya <- ensureEmptySlot destSlot;
returnOk (Invocations_H.irqcontrol_invocation.IssueIRQHandler (UCAST(32 \<rightarrow> 10) y) destSlot (cte_map slot))
odE
od)
 2. \<And>a list z zs y ya yb ysb s. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; (invs and (\<lambda>s. s \<turnstile> a \<and> (\<forall>cp\<in>set list. s \<turnstile> cp))) s\<rbrakk> \<Longrightarrow> \<not> UCAST(10 \<rightarrow> 32) maxIRQ < y \<longrightarrow> (?P188 a list z zs y ya yb ysb and (\<lambda>s. unat y \<le> unat maxIRQ)) s
 3. \<And>a list z zs y ya yb ysb s. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; (invs' and (\<lambda>s. valid_cap' z s \<and> (\<forall>cp\<in>set zs. valid_cap' cp s))) s\<rbrakk> \<Longrightarrow> \<not> UCAST(10 \<rightarrow> 32) maxIRQ < y \<longrightarrow> ?Q'184 a list z zs y ya yb ysb s proof (prove)
goal (5 subgoals):
 1. \<And>a list z zs y ya yb ysb irq_active. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; \<not> 0x9F < y; unat y \<le> 159\<rbrakk> \<Longrightarrow> corres (ser \<oplus> irq_control_inv_relation) (?R223 a list z zs y ya yb ysb irq_active) (?R'223 a list z zs y ya yb ysb irq_active) (doE yc <- whenE irq_active (throwError ExceptionTypes_A.syscall_error.RevokeFirst);
dest_slot <- lookup_slot_for_cnode_op False a (to_bl ya) (unat yb);
ya <- ensure_empty dest_slot;
returnOk (IRQControl (UCAST(32 \<rightarrow> 10) y) dest_slot slot)
odE) (doE yc <- whenE irq_active (throwError Fault_H.syscall_error.RevokeFirst);
destSlot <- lookupSlotForCNodeOp False z ya (unat yb);
ya <- ensureEmptySlot destSlot;
returnOk (Invocations_H.irqcontrol_invocation.IssueIRQHandler (UCAST(32 \<rightarrow> 10) y) destSlot (cte_map slot))
odE)
 2. \<And>a list z zs y ya yb ysb. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; \<not> 0x9F < y; unat y \<le> 159\<rbrakk> \<Longrightarrow> \<lbrace>?Q223 a list z zs y ya yb ysb\<rbrace> is_irq_active (UCAST(32 \<rightarrow> 10) y) \<lbrace>?R223 a list z zs y ya yb ysb\<rbrace>
 3. \<And>a list z zs y ya yb ysb. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; \<not> 0x9F < y; unat y \<le> 159\<rbrakk> \<Longrightarrow> \<lbrace>?Q'223 a list z zs y ya yb ysb\<rbrace> isIRQActive (UCAST(32 \<rightarrow> 10) y) \<lbrace>?R'223 a list z zs y ya yb ysb\<rbrace>
 4. \<And>a list z zs y ya yb ysb s. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; (invs and (\<lambda>s. s \<turnstile> a \<and> (\<forall>cp\<in>set list. s \<turnstile> cp))) s\<rbrakk> \<Longrightarrow> \<not> UCAST(10 \<rightarrow> 32) maxIRQ < y \<longrightarrow> ((\<lambda>_. True) and ?Q223 a list z zs y ya yb ysb and (\<lambda>s. unat y \<le> unat maxIRQ)) s
 5. \<And>a list z zs y ya yb ysb s. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; (invs' and (\<lambda>s. valid_cap' z s \<and> (\<forall>cp\<in>set zs. valid_cap' cp s))) s\<rbrakk> \<Longrightarrow> \<not> UCAST(10 \<rightarrow> 32) maxIRQ < y \<longrightarrow> ((\<lambda>_. True) and ?Q'223 a list z zs y ya yb ysb) s proof (prove)
goal (5 subgoals):
 1. \<And>a list z zs y ya yb ysb irq_active. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; \<not> 0x9F < y; unat y \<le> 159; \<not> irq_active\<rbrakk> \<Longrightarrow> corres (ser \<oplus> irq_control_inv_relation) (?Q228 a list z zs y ya yb ysb irq_active) (?Q'228 a list z zs y ya yb ysb irq_active) (doE dest_slot <- lookup_slot_for_cnode_op False a (to_bl ya) (unat yb);
ya <- ensure_empty dest_slot;
returnOk (IRQControl (UCAST(32 \<rightarrow> 10) y) dest_slot slot)
odE) (doE destSlot <- lookupSlotForCNodeOp False z ya (unat yb);
ya <- ensureEmptySlot destSlot;
returnOk (Invocations_H.irqcontrol_invocation.IssueIRQHandler (UCAST(32 \<rightarrow> 10) y) destSlot (cte_map slot))
odE)
 2. \<And>a list z zs y ya yb ysb. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; \<not> 0x9F < y; unat y \<le> 159\<rbrakk> \<Longrightarrow> \<lbrace>?Q223 a list z zs y ya yb ysb\<rbrace> is_irq_active (UCAST(32 \<rightarrow> 10) y) \<lbrace>\<lambda>irq_active s. \<not> irq_active \<longrightarrow> ?Q228 a list z zs y ya yb ysb irq_active s\<rbrace>
 3. \<And>a list z zs y ya yb ysb. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; \<not> 0x9F < y; unat y \<le> 159\<rbrakk> \<Longrightarrow> \<lbrace>?Q'223 a list z zs y ya yb ysb\<rbrace> isIRQActive (UCAST(32 \<rightarrow> 10) y) \<lbrace>\<lambda>irq_active s. \<not> irq_active \<longrightarrow> ?Q'228 a list z zs y ya yb ysb irq_active s\<rbrace>
 4. \<And>a list z zs y ya yb ysb s. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; (invs and (\<lambda>s. s \<turnstile> a \<and> (\<forall>cp\<in>set list. s \<turnstile> cp))) s\<rbrakk> \<Longrightarrow> \<not> UCAST(10 \<rightarrow> 32) maxIRQ < y \<longrightarrow> ((\<lambda>_. True) and ?Q223 a list z zs y ya yb ysb and (\<lambda>s. unat y \<le> unat maxIRQ)) s
 5. \<And>a list z zs y ya yb ysb s. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; (invs' and (\<lambda>s. valid_cap' z s \<and> (\<forall>cp\<in>set zs. valid_cap' cp s))) s\<rbrakk> \<Longrightarrow> \<not> UCAST(10 \<rightarrow> 32) maxIRQ < y \<longrightarrow> ((\<lambda>_. True) and ?Q'223 a list z zs y ya yb ysb) s proof (prove)
goal (8 subgoals):
 1. \<And>a list z zs y ya yb ysb irq_active. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; \<not> 0x9F < y; unat y \<le> 159; \<not> irq_active\<rbrakk> \<Longrightarrow> corres (ser \<oplus> ?r'232 a list z zs y ya yb ysb irq_active) (?P232 a list z zs y ya yb ysb irq_active) (?P'232 a list z zs y ya yb ysb irq_active) (lookup_slot_for_cnode_op False a (to_bl ya) (unat yb)) (lookupSlotForCNodeOp False z ya (unat yb))
 2. \<And>a list z zs y ya yb ysb irq_active dest_slot destSlot. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; \<not> 0x9F < y; unat y \<le> 159; \<not> irq_active; ?r'232 a list z zs y ya yb ysb irq_active dest_slot destSlot\<rbrakk> \<Longrightarrow> corres (ser \<oplus> irq_control_inv_relation) (?R232 a list z zs y ya yb ysb irq_active dest_slot) (?R'232 a list z zs y ya yb ysb irq_active destSlot) (doE ya <- ensure_empty dest_slot;
returnOk (IRQControl (UCAST(32 \<rightarrow> 10) y) dest_slot slot)
odE) (doE ya <- ensureEmptySlot destSlot;
returnOk (Invocations_H.irqcontrol_invocation.IssueIRQHandler (UCAST(32 \<rightarrow> 10) y) destSlot (cte_map slot))
odE)
 3. \<And>a list z zs y ya yb ysb irq_active. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; \<not> 0x9F < y; unat y \<le> 159; \<not> irq_active\<rbrakk> \<Longrightarrow> \<lbrace>?Q232 a list z zs y ya yb ysb irq_active\<rbrace> lookup_slot_for_cnode_op False a (to_bl ya) (unat yb) \<lbrace>?R232 a list z zs y ya yb ysb irq_active\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>a list z zs y ya yb ysb irq_active. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; \<not> 0x9F < y; unat y \<le> 159; \<not> irq_active\<rbrakk> \<Longrightarrow> \<lbrace>?Q'232 a list z zs y ya yb ysb irq_active\<rbrace> lookupSlotForCNodeOp False z ya (unat yb) \<lbrace>?R'232 a list z zs y ya yb ysb irq_active\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>a list z zs y ya yb ysb. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; \<not> 0x9F < y; unat y \<le> 159\<rbrakk> \<Longrightarrow> \<lbrace>?Q223 a list z zs y ya yb ysb\<rbrace> is_irq_active (UCAST(32 \<rightarrow> 10) y) \<lbrace>\<lambda>irq_active s. \<not> irq_active \<longrightarrow> (?P232 a list z zs y ya yb ysb irq_active and ?Q232 a list z zs y ya yb ysb irq_active) s\<rbrace>
 6. \<And>a list z zs y ya yb ysb. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; \<not> 0x9F < y; unat y \<le> 159\<rbrakk> \<Longrightarrow> \<lbrace>?Q'223 a list z zs y ya yb ysb\<rbrace> isIRQActive (UCAST(32 \<rightarrow> 10) y) \<lbrace>\<lambda>irq_active s. \<not> irq_active \<longrightarrow> (?P'232 a list z zs y ya yb ysb irq_active and ?Q'232 a list z zs y ya yb ysb irq_active) s\<rbrace>
 7. \<And>a list z zs y ya yb ysb s. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; (invs and (\<lambda>s. s \<turnstile> a \<and> (\<forall>cp\<in>set list. s \<turnstile> cp))) s\<rbrakk> \<Longrightarrow> \<not> UCAST(10 \<rightarrow> 32) maxIRQ < y \<longrightarrow> ((\<lambda>_. True) and ?Q223 a list z zs y ya yb ysb and (\<lambda>s. unat y \<le> unat maxIRQ)) s
 8. \<And>a list z zs y ya yb ysb s. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; (invs' and (\<lambda>s. valid_cap' z s \<and> (\<forall>cp\<in>set zs. valid_cap' cp s))) s\<rbrakk> \<Longrightarrow> \<not> UCAST(10 \<rightarrow> 32) maxIRQ < y \<longrightarrow> ((\<lambda>_. True) and ?Q'223 a list z zs y ya yb ysb) s proof (prove)
goal (7 subgoals):
 1. \<And>a list z zs y ya yb ysb irq_active dest_slot destSlot. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; \<not> 0x9F < y; unat y \<le> 159; \<not> irq_active; destSlot = cte_map dest_slot\<rbrakk> \<Longrightarrow> corres (ser \<oplus> irq_control_inv_relation) (?R232 a list z zs y ya yb ysb irq_active dest_slot) (?R'232 a list z zs y ya yb ysb irq_active destSlot) (doE ya <- ensure_empty dest_slot;
returnOk (IRQControl (UCAST(32 \<rightarrow> 10) y) dest_slot slot)
odE) (doE ya <- ensureEmptySlot destSlot;
returnOk (Invocations_H.irqcontrol_invocation.IssueIRQHandler (UCAST(32 \<rightarrow> 10) y) destSlot (cte_map slot))
odE)
 2. \<And>a list z zs y ya yb ysb irq_active. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; \<not> 0x9F < y; unat y \<le> 159; \<not> irq_active\<rbrakk> \<Longrightarrow> \<lbrace>?Q232 a list z zs y ya yb ysb irq_active\<rbrace> lookup_slot_for_cnode_op False a (to_bl ya) (unat yb) \<lbrace>?R232 a list z zs y ya yb ysb irq_active\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>a list z zs y ya yb ysb irq_active. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; \<not> 0x9F < y; unat y \<le> 159; \<not> irq_active\<rbrakk> \<Longrightarrow> \<lbrace>?Q'232 a list z zs y ya yb ysb irq_active\<rbrace> lookupSlotForCNodeOp False z ya (unat yb) \<lbrace>?R'232 a list z zs y ya yb ysb irq_active\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>a list z zs y ya yb ysb. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; \<not> 0x9F < y; unat y \<le> 159\<rbrakk> \<Longrightarrow> \<lbrace>?Q223 a list z zs y ya yb ysb\<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 ?Q232 a list z zs y ya yb ysb irq_active) s\<rbrace>
 5. \<And>a list z zs y ya yb ysb. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; \<not> 0x9F < y; unat y \<le> 159\<rbrakk> \<Longrightarrow> \<lbrace>?Q'223 a list z zs y ya yb ysb\<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'232 a list z zs y ya yb ysb irq_active) s\<rbrace>
 6. \<And>a list z zs y ya yb ysb s. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; (invs and (\<lambda>s. s \<turnstile> a \<and> (\<forall>cp\<in>set list. s \<turnstile> cp))) s\<rbrakk> \<Longrightarrow> \<not> UCAST(10 \<rightarrow> 32) maxIRQ < y \<longrightarrow> ((\<lambda>_. True) and ?Q223 a list z zs y ya yb ysb and (\<lambda>s. unat y \<le> unat maxIRQ)) s
 7. \<And>a list z zs y ya yb ysb s. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; (invs' and (\<lambda>s. valid_cap' z s \<and> (\<forall>cp\<in>set zs. valid_cap' cp s))) s\<rbrakk> \<Longrightarrow> \<not> UCAST(10 \<rightarrow> 32) maxIRQ < y \<longrightarrow> ((\<lambda>_. True) and ?Q'223 a list z zs y ya yb ysb) s proof (prove)
goal (10 subgoals):
 1. \<And>a list z zs y ya yb ysb irq_active dest_slot destSlot. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; \<not> 0x9F < y; unat y \<le> 159; \<not> irq_active; destSlot = cte_map dest_slot\<rbrakk> \<Longrightarrow> corres (ser \<oplus> ?r'246 a list z zs y ya yb ysb irq_active dest_slot destSlot) (?P247 a list z zs y ya yb ysb irq_active dest_slot) (?P'249 a list z zs y ya yb ysb irq_active destSlot) (ensure_empty dest_slot) (ensureEmptySlot destSlot)
 2. \<And>a list z zs y ya yb ysb irq_active dest_slot destSlot yc yd. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; \<not> 0x9F < y; unat y \<le> 159; \<not> irq_active; destSlot = cte_map dest_slot; ?r'246 a list z zs y ya yb ysb irq_active dest_slot destSlot yc yd\<rbrakk> \<Longrightarrow> corres (ser \<oplus> irq_control_inv_relation) (?R246 a list z zs y ya yb ysb irq_active dest_slot destSlot yc) (?R'246 a list z zs y ya yb ysb irq_active dest_slot destSlot yd) (returnOk (IRQControl (UCAST(32 \<rightarrow> 10) y) dest_slot slot)) (returnOk (Invocations_H.irqcontrol_invocation.IssueIRQHandler (UCAST(32 \<rightarrow> 10) y) destSlot (cte_map slot)))
 3. \<And>a list z zs y ya yb ysb irq_active dest_slot destSlot. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; \<not> 0x9F < y; unat y \<le> 159; \<not> irq_active; destSlot = cte_map dest_slot\<rbrakk> \<Longrightarrow> \<lbrace>?Q248 a list z zs y ya yb ysb irq_active dest_slot\<rbrace> ensure_empty dest_slot \<lbrace>?R246 a list z zs y ya yb ysb irq_active dest_slot destSlot\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>a list z zs y ya yb ysb irq_active dest_slot destSlot. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; \<not> 0x9F < y; unat y \<le> 159; \<not> irq_active; destSlot = cte_map dest_slot\<rbrakk> \<Longrightarrow> \<lbrace>?Q'250 a list z zs y ya yb ysb irq_active destSlot\<rbrace> ensureEmptySlot destSlot \<lbrace>?R'246 a list z zs y ya yb ysb irq_active dest_slot destSlot\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>a list z zs y ya yb ysb irq_active. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; \<not> 0x9F < y; unat y \<le> 159; \<not> irq_active\<rbrakk> \<Longrightarrow> \<lbrace>?Q232 a list z zs y ya yb ysb irq_active\<rbrace> lookup_slot_for_cnode_op False a (to_bl ya) (unat yb) \<lbrace>\<lambda>dest_slot. ?P247 a list z zs y ya yb ysb irq_active dest_slot and ?Q248 a list z zs y ya yb ysb irq_active dest_slot\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>a list z zs y ya yb ysb irq_active. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; \<not> 0x9F < y; unat y \<le> 159; \<not> irq_active\<rbrakk> \<Longrightarrow> \<lbrace>?Q'232 a list z zs y ya yb ysb irq_active\<rbrace> lookupSlotForCNodeOp False z ya (unat yb) \<lbrace>\<lambda>destSlot. ?P'249 a list z zs y ya yb ysb irq_active destSlot and ?Q'250 a list z zs y ya yb ysb irq_active destSlot\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>a list z zs y ya yb ysb. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; \<not> 0x9F < y; unat y \<le> 159\<rbrakk> \<Longrightarrow> \<lbrace>?Q223 a list z zs y ya yb ysb\<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 ?Q232 a list z zs y ya yb ysb irq_active) s\<rbrace>
 8. \<And>a list z zs y ya yb ysb. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; \<not> 0x9F < y; unat y \<le> 159\<rbrakk> \<Longrightarrow> \<lbrace>?Q'223 a list z zs y ya yb ysb\<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'232 a list z zs y ya yb ysb irq_active) s\<rbrace>
 9. \<And>a list z zs y ya yb ysb s. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; (invs and (\<lambda>s. s \<turnstile> a \<and> (\<forall>cp\<in>set list. s \<turnstile> cp))) s\<rbrakk> \<Longrightarrow> \<not> UCAST(10 \<rightarrow> 32) maxIRQ < y \<longrightarrow> ((\<lambda>_. True) and ?Q223 a list z zs y ya yb ysb and (\<lambda>s. unat y \<le> unat maxIRQ)) s
 10. \<And>a list z zs y ya yb ysb s. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; (invs' and (\<lambda>s. valid_cap' z s \<and> (\<forall>cp\<in>set zs. valid_cap' cp s))) s\<rbrakk> \<Longrightarrow> \<not> UCAST(10 \<rightarrow> 32) maxIRQ < y \<longrightarrow> ((\<lambda>_. True) and ?Q'223 a list z zs y ya yb ysb) s proof (prove)
goal (9 subgoals):
 1. \<And>a list z zs y ya yb ysb irq_active dest_slot destSlot yc yd. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; \<not> 0x9F < y; unat y \<le> 159; \<not> irq_active; destSlot = cte_map dest_slot; dc yc yd\<rbrakk> \<Longrightarrow> corres (ser \<oplus> irq_control_inv_relation) (?R246 a list z zs y ya yb ysb irq_active dest_slot destSlot yc) (?R'246 a list z zs y ya yb ysb irq_active dest_slot destSlot yd) (returnOk (IRQControl (UCAST(32 \<rightarrow> 10) y) dest_slot slot)) (returnOk (Invocations_H.irqcontrol_invocation.IssueIRQHandler (UCAST(32 \<rightarrow> 10) y) destSlot (cte_map slot)))
 2. \<And>a list z zs y ya yb ysb irq_active dest_slot destSlot. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; \<not> 0x9F < y; unat y \<le> 159; \<not> irq_active; destSlot = cte_map dest_slot\<rbrakk> \<Longrightarrow> \<lbrace>?Q248 a list z zs y ya yb ysb irq_active dest_slot\<rbrace> ensure_empty dest_slot \<lbrace>?R246 a list z zs y ya yb ysb irq_active dest_slot destSlot\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>a list z zs y ya yb ysb irq_active dest_slot destSlot. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; \<not> 0x9F < y; unat y \<le> 159; \<not> irq_active; destSlot = cte_map dest_slot\<rbrakk> \<Longrightarrow> \<lbrace>?Q'250 a list z zs y ya yb ysb irq_active destSlot\<rbrace> ensureEmptySlot destSlot \<lbrace>?R'246 a list z zs y ya yb ysb irq_active dest_slot destSlot\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>a list z zs y ya yb ysb irq_active. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; \<not> 0x9F < y; unat y \<le> 159; \<not> irq_active\<rbrakk> \<Longrightarrow> \<lbrace>?Q232 a list z zs y ya yb ysb irq_active\<rbrace> lookup_slot_for_cnode_op False a (to_bl ya) (unat yb) \<lbrace>\<lambda>dest_slot. invs and cte_wp_at (\<lambda>_. True) dest_slot and ?Q248 a list z zs y ya yb ysb irq_active dest_slot\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>a list z zs y ya yb ysb irq_active. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; \<not> 0x9F < y; unat y \<le> 159; \<not> irq_active\<rbrakk> \<Longrightarrow> \<lbrace>?Q'232 a list z zs y ya yb ysb irq_active\<rbrace> lookupSlotForCNodeOp False z ya (unat yb) \<lbrace>\<lambda>destSlot. invs' and ?Q'250 a list z zs y ya yb ysb irq_active destSlot\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>a list z zs y ya yb ysb. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; \<not> 0x9F < y; unat y \<le> 159\<rbrakk> \<Longrightarrow> \<lbrace>?Q223 a list z zs y ya yb ysb\<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 ?Q232 a list z zs y ya yb ysb irq_active) s\<rbrace>
 7. \<And>a list z zs y ya yb ysb. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; \<not> 0x9F < y; unat y \<le> 159\<rbrakk> \<Longrightarrow> \<lbrace>?Q'223 a list z zs y ya yb ysb\<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'232 a list z zs y ya yb ysb irq_active) s\<rbrace>
 8. \<And>a list z zs y ya yb ysb s. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; (invs and (\<lambda>s. s \<turnstile> a \<and> (\<forall>cp\<in>set list. s \<turnstile> cp))) s\<rbrakk> \<Longrightarrow> \<not> UCAST(10 \<rightarrow> 32) maxIRQ < y \<longrightarrow> ((\<lambda>_. True) and ?Q223 a list z zs y ya yb ysb and (\<lambda>s. unat y \<le> unat maxIRQ)) s
 9. \<And>a list z zs y ya yb ysb s. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; (invs' and (\<lambda>s. valid_cap' z s \<and> (\<forall>cp\<in>set zs. valid_cap' cp s))) s\<rbrakk> \<Longrightarrow> \<not> UCAST(10 \<rightarrow> 32) maxIRQ < y \<longrightarrow> ((\<lambda>_. True) and ?Q'223 a list z zs y ya yb ysb) s proof (prove)
goal (9 subgoals):
 1. \<And>a list z zs y ya yb ysb irq_active dest_slot destSlot yc yd. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; \<not> 0x9F < y; unat y \<le> 159; \<not> irq_active; destSlot = cte_map dest_slot; dc yc yd\<rbrakk> \<Longrightarrow> irq_control_inv_relation (IRQControl (UCAST(32 \<rightarrow> 10) y) dest_slot slot) (Invocations_H.irqcontrol_invocation.IssueIRQHandler (UCAST(32 \<rightarrow> 10) y) destSlot (cte_map slot))
 2. \<And>a list z zs y ya yb ysb irq_active dest_slot destSlot. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; \<not> 0x9F < y; unat y \<le> 159; \<not> irq_active; destSlot = cte_map dest_slot\<rbrakk> \<Longrightarrow> \<lbrace>?Q248 a list z zs y ya yb ysb irq_active dest_slot\<rbrace> ensure_empty dest_slot \<lbrace>\<lambda>yc _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>a list z zs y ya yb ysb irq_active dest_slot destSlot. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; \<not> 0x9F < y; unat y \<le> 159; \<not> irq_active; destSlot = cte_map dest_slot\<rbrakk> \<Longrightarrow> \<lbrace>?Q'250 a list z zs y ya yb ysb irq_active destSlot\<rbrace> ensureEmptySlot destSlot \<lbrace>\<lambda>yd _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>a list z zs y ya yb ysb irq_active. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; \<not> 0x9F < y; unat y \<le> 159; \<not> irq_active\<rbrakk> \<Longrightarrow> \<lbrace>?Q232 a list z zs y ya yb ysb irq_active\<rbrace> lookup_slot_for_cnode_op False a (to_bl ya) (unat yb) \<lbrace>\<lambda>dest_slot. invs and cte_wp_at (\<lambda>_. True) dest_slot and ?Q248 a list z zs y ya yb ysb irq_active dest_slot\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>a list z zs y ya yb ysb irq_active. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; \<not> 0x9F < y; unat y \<le> 159; \<not> irq_active\<rbrakk> \<Longrightarrow> \<lbrace>?Q'232 a list z zs y ya yb ysb irq_active\<rbrace> lookupSlotForCNodeOp False z ya (unat yb) \<lbrace>\<lambda>destSlot. invs' and ?Q'250 a list z zs y ya yb ysb irq_active destSlot\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>a list z zs y ya yb ysb. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; \<not> 0x9F < y; unat y \<le> 159\<rbrakk> \<Longrightarrow> \<lbrace>?Q223 a list z zs y ya yb ysb\<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 ?Q232 a list z zs y ya yb ysb irq_active) s\<rbrace>
 7. \<And>a list z zs y ya yb ysb. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; \<not> 0x9F < y; unat y \<le> 159\<rbrakk> \<Longrightarrow> \<lbrace>?Q'223 a list z zs y ya yb ysb\<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'232 a list z zs y ya yb ysb irq_active) s\<rbrace>
 8. \<And>a list z zs y ya yb ysb s. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; (invs and (\<lambda>s. s \<turnstile> a \<and> (\<forall>cp\<in>set list. s \<turnstile> cp))) s\<rbrakk> \<Longrightarrow> \<not> UCAST(10 \<rightarrow> 32) maxIRQ < y \<longrightarrow> ((\<lambda>_. True) and ?Q223 a list z zs y ya yb ysb and (\<lambda>s. unat y \<le> unat maxIRQ)) s
 9. \<And>a list z zs y ya yb ysb s. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; (invs' and (\<lambda>s. valid_cap' z s \<and> (\<forall>cp\<in>set zs. valid_cap' cp s))) s\<rbrakk> \<Longrightarrow> \<not> UCAST(10 \<rightarrow> 32) maxIRQ < y \<longrightarrow> ((\<lambda>_. True) and ?Q'223 a list z zs y ya yb ysb) s proof (prove)
goal (8 subgoals):
 1. \<And>a list z zs y ya yb ysb irq_active dest_slot destSlot. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; \<not> 0x9F < y; unat y \<le> 159; \<not> irq_active; destSlot = cte_map dest_slot\<rbrakk> \<Longrightarrow> \<lbrace>?Q248 a list z zs y ya yb ysb irq_active dest_slot\<rbrace> ensure_empty dest_slot \<lbrace>\<lambda>yc _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>a list z zs y ya yb ysb irq_active dest_slot destSlot. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; \<not> 0x9F < y; unat y \<le> 159; \<not> irq_active; destSlot = cte_map dest_slot\<rbrakk> \<Longrightarrow> \<lbrace>?Q'250 a list z zs y ya yb ysb irq_active destSlot\<rbrace> ensureEmptySlot destSlot \<lbrace>\<lambda>yd _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>a list z zs y ya yb ysb irq_active. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; \<not> 0x9F < y; unat y \<le> 159; \<not> irq_active\<rbrakk> \<Longrightarrow> \<lbrace>?Q232 a list z zs y ya yb ysb irq_active\<rbrace> lookup_slot_for_cnode_op False a (to_bl ya) (unat yb) \<lbrace>\<lambda>dest_slot. invs and cte_wp_at (\<lambda>_. True) dest_slot and ?Q248 a list z zs y ya yb ysb irq_active dest_slot\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>a list z zs y ya yb ysb irq_active. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; \<not> 0x9F < y; unat y \<le> 159; \<not> irq_active\<rbrakk> \<Longrightarrow> \<lbrace>?Q'232 a list z zs y ya yb ysb irq_active\<rbrace> lookupSlotForCNodeOp False z ya (unat yb) \<lbrace>\<lambda>destSlot. invs' and ?Q'250 a list z zs y ya yb ysb irq_active destSlot\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>a list z zs y ya yb ysb. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; \<not> 0x9F < y; unat y \<le> 159\<rbrakk> \<Longrightarrow> \<lbrace>?Q223 a list z zs y ya yb ysb\<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 ?Q232 a list z zs y ya yb ysb irq_active) s\<rbrace>
 6. \<And>a list z zs y ya yb ysb. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; \<not> 0x9F < y; unat y \<le> 159\<rbrakk> \<Longrightarrow> \<lbrace>?Q'223 a list z zs y ya yb ysb\<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'232 a list z zs y ya yb ysb irq_active) s\<rbrace>
 7. \<And>a list z zs y ya yb ysb s. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; (invs and (\<lambda>s. s \<turnstile> a \<and> (\<forall>cp\<in>set list. s \<turnstile> cp))) s\<rbrakk> \<Longrightarrow> \<not> UCAST(10 \<rightarrow> 32) maxIRQ < y \<longrightarrow> ((\<lambda>_. True) and ?Q223 a list z zs y ya yb ysb and (\<lambda>s. unat y \<le> unat maxIRQ)) s
 8. \<And>a list z zs y ya yb ysb s. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; (invs' and (\<lambda>s. valid_cap' z s \<and> (\<forall>cp\<in>set zs. valid_cap' cp s))) s\<rbrakk> \<Longrightarrow> \<not> UCAST(10 \<rightarrow> 32) maxIRQ < y \<longrightarrow> ((\<lambda>_. True) and ?Q'223 a list z zs y ya yb ysb) s proof (prove)
goal (2 subgoals):
 1. \<And>a list z zs y ya yb ysb s. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; invs s; s \<turnstile> a; \<forall>cp\<in>set list. s \<turnstile> cp; \<not> UCAST(10 \<rightarrow> 32) maxIRQ < y\<rbrakk> \<Longrightarrow> unat y \<le> unat maxIRQ
 2. \<And>a list z zs y ya yb ysb s. \<lbrakk>gen_invocation_type label = IRQIssueIRQHandler; caps = a # list; caps' = z # zs; args = y # ya # yb # ysb; cap_relation a z; list_all2 cap_relation list zs; (invs' and (\<lambda>s. valid_cap' z s \<and> (\<forall>cp\<in>set zs. valid_cap' cp s))) s\<rbrakk> \<Longrightarrow> \<not> UCAST(10 \<rightarrow> 32) maxIRQ < y \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_cap' z s \<and> invs' s)) s proof (prove)
goal:
No subgoals!