theory Interrupt_DR

lemma decode_irq_handler_corres:
  "\<And> slot. \<lbrakk> Some (IrqHandlerIntent ui) = transform_intent (invocation_type label') args';
     cap = transform_cap (Structures_A.IRQHandlerCap x');
     excaps = transform_cap_list excaps' \<rbrakk> \<Longrightarrow>
   dcorres (dc \<oplus> cdl_irq_handler_invocation_relation) \<top> \<top>
     (Interrupt_D.decode_irq_handler_invocation cap slot excaps ui)
     (Decode_A.decode_irq_handler_invocation label' x' excaps')" apply (unfold Interrupt_D.decode_irq_handler_invocation_def Decode_A.decode_irq_handler_invocation_def) apply (cases "invocation_type label' = GenInvocationLabel IRQAckIRQ") apply (simp add: transform_intent_def cdl_cap_irq_def assert_opt_def
               flip: returnOk_liftE gen_invocation_type_eq) apply (rule corres_alternate1) apply (rule dcorres_returnOk) apply (simp add: cdl_irq_handler_invocation_relation_def
                    translate_irq_handler_invocation_def) apply (cases "invocation_type label' = GenInvocationLabel IRQSetIRQHandler") apply (simp add: transform_intent_def cdl_cap_irq_def flip: gen_invocation_type_eq) apply (rule conjI) prefer 2 \<comment> \<open>excaps' = []\<close> apply (clarsimp intro!: corres_alternate2) apply (clarsimp simp: neq_Nil_conv) apply (rule conjI) prefer 2 apply (clarsimp intro!: corres_alternate2) apply clarsimp apply (rule corres_alternate1) apply (simp add: get_index_def transform_cap_list_def
                    throw_on_none_def assert_opt_def
                    returnOk_liftE[symmetric]) apply (clarsimp simp: is_cap_simps) apply (rule dcorres_returnOk) apply (simp add: cdl_irq_handler_invocation_relation_def
                    translate_irq_handler_invocation_def) apply (cases "invocation_type label' = GenInvocationLabel IRQClearIRQHandler") apply (simp add: transform_intent_def cdl_cap_irq_def assert_opt_def
               flip: gen_invocation_type_eq returnOk_liftE) apply (rule corres_alternate1) apply (rule dcorres_returnOk) apply (simp add: cdl_irq_handler_invocation_relation_def
                    translate_irq_handler_invocation_def) apply (cases ui, auto simp: dcorres_alternative_throw simp flip: gen_invocation_type_eq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>slot. \<lbrakk>Some (IrqHandlerIntent ui) = transform_intent (invocation_type label') args'; cap = transform_cap (IRQHandlerCap x'); excaps = transform_cap_list excaps'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_irq_handler_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (Interrupt_D.decode_irq_handler_invocation cap slot excaps ui) (Decode_A.decode_irq_handler_invocation label' x' excaps') proof (prove)
goal (1 subgoal):
 1. \<And>slot. \<lbrakk>Some (IrqHandlerIntent ui) = transform_intent (invocation_type label') args'; cap = transform_cap (IRQHandlerCap x'); excaps = transform_cap_list excaps'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_irq_handler_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (case ui of IrqHandlerAckIntent \<Rightarrow> doE irq <- liftE $ assert_opt $ cdl_cap_irq cap;
returnOk $ AckIrq irq
odE \<sqinter> throw | IrqHandlerSetEndpointIntent \<Rightarrow> doE endpoint <- throw_on_none $ get_index excaps 0;
endpoint_cap <- returnOk $ fst endpoint;
endpoint_cap_ref <- returnOk $ snd endpoint;
irq <- liftE $ assert_opt $ cdl_cap_irq cap;
case endpoint_cap of cdl_cap.NotificationCap x xa xb \<Rightarrow> returnOk () | _ \<Rightarrow> throw;
returnOk $ SetIrqHandler irq endpoint_cap endpoint_cap_ref
odE \<sqinter> throw | IrqHandlerClearIntent \<Rightarrow> doE irq <- liftE $ assert_opt $ cdl_cap_irq cap;
returnOk $ ClearIrqHandler irq
odE \<sqinter> throw) (if gen_invocation_type label' = IRQAckIRQ then returnOk $ ACKIrq x' else if gen_invocation_type label' = IRQSetIRQHandler then if excaps' \<noteq> [] then let (cap, slot) = hd excaps' in if Structures_A.is_ntfn_cap cap \<and> AllowSend \<in> Structures_A.cap_rights cap then returnOk $ SetIRQHandler x' cap slot else throwError $ InvalidCapability 0 else throwError TruncatedMessage else if gen_invocation_type label' = IRQClearIRQHandler then returnOk $ ClearIRQHandler x' else throwError IllegalOperation) proof (prove)
goal (2 subgoals):
 1. \<And>slot. \<lbrakk>Some (IrqHandlerIntent ui) = transform_intent (invocation_type label') args'; cap = transform_cap (IRQHandlerCap x'); excaps = transform_cap_list excaps'; invocation_type label' = GenInvocationLabel IRQAckIRQ\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_irq_handler_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (case ui of IrqHandlerAckIntent \<Rightarrow> doE irq <- liftE $ assert_opt $ cdl_cap_irq cap;
returnOk $ AckIrq irq
odE \<sqinter> throw | IrqHandlerSetEndpointIntent \<Rightarrow> doE endpoint <- throw_on_none $ get_index excaps 0;
endpoint_cap <- returnOk $ fst endpoint;
endpoint_cap_ref <- returnOk $ snd endpoint;
irq <- liftE $ assert_opt $ cdl_cap_irq cap;
case endpoint_cap of cdl_cap.NotificationCap x xa xb \<Rightarrow> returnOk () | _ \<Rightarrow> throw;
returnOk $ SetIrqHandler irq endpoint_cap endpoint_cap_ref
odE \<sqinter> throw | IrqHandlerClearIntent \<Rightarrow> doE irq <- liftE $ assert_opt $ cdl_cap_irq cap;
returnOk $ ClearIrqHandler irq
odE \<sqinter> throw) (if gen_invocation_type label' = IRQAckIRQ then returnOk $ ACKIrq x' else if gen_invocation_type label' = IRQSetIRQHandler then if excaps' \<noteq> [] then let (cap, slot) = hd excaps' in if Structures_A.is_ntfn_cap cap \<and> AllowSend \<in> Structures_A.cap_rights cap then returnOk $ SetIRQHandler x' cap slot else throwError $ InvalidCapability 0 else throwError TruncatedMessage else if gen_invocation_type label' = IRQClearIRQHandler then returnOk $ ClearIRQHandler x' else throwError IllegalOperation)
 2. \<And>slot. \<lbrakk>Some (IrqHandlerIntent ui) = transform_intent (invocation_type label') args'; cap = transform_cap (IRQHandlerCap x'); excaps = transform_cap_list excaps'; invocation_type label' \<noteq> GenInvocationLabel IRQAckIRQ\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_irq_handler_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (case ui of IrqHandlerAckIntent \<Rightarrow> doE irq <- liftE $ assert_opt $ cdl_cap_irq cap;
returnOk $ AckIrq irq
odE \<sqinter> throw | IrqHandlerSetEndpointIntent \<Rightarrow> doE endpoint <- throw_on_none $ get_index excaps 0;
endpoint_cap <- returnOk $ fst endpoint;
endpoint_cap_ref <- returnOk $ snd endpoint;
irq <- liftE $ assert_opt $ cdl_cap_irq cap;
case endpoint_cap of cdl_cap.NotificationCap x xa xb \<Rightarrow> returnOk () | _ \<Rightarrow> throw;
returnOk $ SetIrqHandler irq endpoint_cap endpoint_cap_ref
odE \<sqinter> throw | IrqHandlerClearIntent \<Rightarrow> doE irq <- liftE $ assert_opt $ cdl_cap_irq cap;
returnOk $ ClearIrqHandler irq
odE \<sqinter> throw) (if gen_invocation_type label' = IRQAckIRQ then returnOk $ ACKIrq x' else if gen_invocation_type label' = IRQSetIRQHandler then if excaps' \<noteq> [] then let (cap, slot) = hd excaps' in if Structures_A.is_ntfn_cap cap \<and> AllowSend \<in> Structures_A.cap_rights cap then returnOk $ SetIRQHandler x' cap slot else throwError $ InvalidCapability 0 else throwError TruncatedMessage else if gen_invocation_type label' = IRQClearIRQHandler then returnOk $ ClearIRQHandler x' else throwError IllegalOperation) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ui = IrqHandlerAckIntent; cap = IrqHandlerCap x'; excaps = transform_cap_list excaps'; invocation_type label' = GenInvocationLabel IRQAckIRQ\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_irq_handler_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (returnOk (AckIrq x') \<sqinter> throw) (returnOk (ACKIrq x'))
 2. \<And>slot. \<lbrakk>Some (IrqHandlerIntent ui) = transform_intent (invocation_type label') args'; cap = transform_cap (IRQHandlerCap x'); excaps = transform_cap_list excaps'; invocation_type label' \<noteq> GenInvocationLabel IRQAckIRQ\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_irq_handler_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (case ui of IrqHandlerAckIntent \<Rightarrow> doE irq <- liftE $ assert_opt $ cdl_cap_irq cap;
returnOk $ AckIrq irq
odE \<sqinter> throw | IrqHandlerSetEndpointIntent \<Rightarrow> doE endpoint <- throw_on_none $ get_index excaps 0;
endpoint_cap <- returnOk $ fst endpoint;
endpoint_cap_ref <- returnOk $ snd endpoint;
irq <- liftE $ assert_opt $ cdl_cap_irq cap;
case endpoint_cap of cdl_cap.NotificationCap x xa xb \<Rightarrow> returnOk () | _ \<Rightarrow> throw;
returnOk $ SetIrqHandler irq endpoint_cap endpoint_cap_ref
odE \<sqinter> throw | IrqHandlerClearIntent \<Rightarrow> doE irq <- liftE $ assert_opt $ cdl_cap_irq cap;
returnOk $ ClearIrqHandler irq
odE \<sqinter> throw) (if gen_invocation_type label' = IRQAckIRQ then returnOk $ ACKIrq x' else if gen_invocation_type label' = IRQSetIRQHandler then if excaps' \<noteq> [] then let (cap, slot) = hd excaps' in if Structures_A.is_ntfn_cap cap \<and> AllowSend \<in> Structures_A.cap_rights cap then returnOk $ SetIRQHandler x' cap slot else throwError $ InvalidCapability 0 else throwError TruncatedMessage else if gen_invocation_type label' = IRQClearIRQHandler then returnOk $ ClearIRQHandler x' else throwError IllegalOperation) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ui = IrqHandlerAckIntent; cap = IrqHandlerCap x'; excaps = transform_cap_list excaps'; invocation_type label' = GenInvocationLabel IRQAckIRQ\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_irq_handler_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (returnOk (AckIrq x')) (returnOk (ACKIrq x'))
 2. \<And>slot. \<lbrakk>Some (IrqHandlerIntent ui) = transform_intent (invocation_type label') args'; cap = transform_cap (IRQHandlerCap x'); excaps = transform_cap_list excaps'; invocation_type label' \<noteq> GenInvocationLabel IRQAckIRQ\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_irq_handler_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (case ui of IrqHandlerAckIntent \<Rightarrow> doE irq <- liftE $ assert_opt $ cdl_cap_irq cap;
returnOk $ AckIrq irq
odE \<sqinter> throw | IrqHandlerSetEndpointIntent \<Rightarrow> doE endpoint <- throw_on_none $ get_index excaps 0;
endpoint_cap <- returnOk $ fst endpoint;
endpoint_cap_ref <- returnOk $ snd endpoint;
irq <- liftE $ assert_opt $ cdl_cap_irq cap;
case endpoint_cap of cdl_cap.NotificationCap x xa xb \<Rightarrow> returnOk () | _ \<Rightarrow> throw;
returnOk $ SetIrqHandler irq endpoint_cap endpoint_cap_ref
odE \<sqinter> throw | IrqHandlerClearIntent \<Rightarrow> doE irq <- liftE $ assert_opt $ cdl_cap_irq cap;
returnOk $ ClearIrqHandler irq
odE \<sqinter> throw) (if gen_invocation_type label' = IRQAckIRQ then returnOk $ ACKIrq x' else if gen_invocation_type label' = IRQSetIRQHandler then if excaps' \<noteq> [] then let (cap, slot) = hd excaps' in if Structures_A.is_ntfn_cap cap \<and> AllowSend \<in> Structures_A.cap_rights cap then returnOk $ SetIRQHandler x' cap slot else throwError $ InvalidCapability 0 else throwError TruncatedMessage else if gen_invocation_type label' = IRQClearIRQHandler then returnOk $ ClearIRQHandler x' else throwError IllegalOperation) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ui = IrqHandlerAckIntent; cap = IrqHandlerCap x'; excaps = transform_cap_list excaps'; invocation_type label' = GenInvocationLabel IRQAckIRQ\<rbrakk> \<Longrightarrow> cdl_irq_handler_invocation_relation (AckIrq x') (ACKIrq x')
 2. \<And>slot. \<lbrakk>Some (IrqHandlerIntent ui) = transform_intent (invocation_type label') args'; cap = transform_cap (IRQHandlerCap x'); excaps = transform_cap_list excaps'; invocation_type label' \<noteq> GenInvocationLabel IRQAckIRQ\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_irq_handler_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (case ui of IrqHandlerAckIntent \<Rightarrow> doE irq <- liftE $ assert_opt $ cdl_cap_irq cap;
returnOk $ AckIrq irq
odE \<sqinter> throw | IrqHandlerSetEndpointIntent \<Rightarrow> doE endpoint <- throw_on_none $ get_index excaps 0;
endpoint_cap <- returnOk $ fst endpoint;
endpoint_cap_ref <- returnOk $ snd endpoint;
irq <- liftE $ assert_opt $ cdl_cap_irq cap;
case endpoint_cap of cdl_cap.NotificationCap x xa xb \<Rightarrow> returnOk () | _ \<Rightarrow> throw;
returnOk $ SetIrqHandler irq endpoint_cap endpoint_cap_ref
odE \<sqinter> throw | IrqHandlerClearIntent \<Rightarrow> doE irq <- liftE $ assert_opt $ cdl_cap_irq cap;
returnOk $ ClearIrqHandler irq
odE \<sqinter> throw) (if gen_invocation_type label' = IRQAckIRQ then returnOk $ ACKIrq x' else if gen_invocation_type label' = IRQSetIRQHandler then if excaps' \<noteq> [] then let (cap, slot) = hd excaps' in if Structures_A.is_ntfn_cap cap \<and> AllowSend \<in> Structures_A.cap_rights cap then returnOk $ SetIRQHandler x' cap slot else throwError $ InvalidCapability 0 else throwError TruncatedMessage else if gen_invocation_type label' = IRQClearIRQHandler then returnOk $ ClearIRQHandler x' else throwError IllegalOperation) proof (prove)
goal (1 subgoal):
 1. \<And>slot. \<lbrakk>Some (IrqHandlerIntent ui) = transform_intent (invocation_type label') args'; cap = transform_cap (IRQHandlerCap x'); excaps = transform_cap_list excaps'; invocation_type label' \<noteq> GenInvocationLabel IRQAckIRQ\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_irq_handler_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (case ui of IrqHandlerAckIntent \<Rightarrow> doE irq <- liftE $ assert_opt $ cdl_cap_irq cap;
returnOk $ AckIrq irq
odE \<sqinter> throw | IrqHandlerSetEndpointIntent \<Rightarrow> doE endpoint <- throw_on_none $ get_index excaps 0;
endpoint_cap <- returnOk $ fst endpoint;
endpoint_cap_ref <- returnOk $ snd endpoint;
irq <- liftE $ assert_opt $ cdl_cap_irq cap;
case endpoint_cap of cdl_cap.NotificationCap x xa xb \<Rightarrow> returnOk () | _ \<Rightarrow> throw;
returnOk $ SetIrqHandler irq endpoint_cap endpoint_cap_ref
odE \<sqinter> throw | IrqHandlerClearIntent \<Rightarrow> doE irq <- liftE $ assert_opt $ cdl_cap_irq cap;
returnOk $ ClearIrqHandler irq
odE \<sqinter> throw) (if gen_invocation_type label' = IRQAckIRQ then returnOk $ ACKIrq x' else if gen_invocation_type label' = IRQSetIRQHandler then if excaps' \<noteq> [] then let (cap, slot) = hd excaps' in if Structures_A.is_ntfn_cap cap \<and> AllowSend \<in> Structures_A.cap_rights cap then returnOk $ SetIRQHandler x' cap slot else throwError $ InvalidCapability 0 else throwError TruncatedMessage else if gen_invocation_type label' = IRQClearIRQHandler then returnOk $ ClearIRQHandler x' else throwError IllegalOperation) proof (prove)
goal (2 subgoals):
 1. \<And>slot. \<lbrakk>Some (IrqHandlerIntent ui) = transform_intent (invocation_type label') args'; cap = transform_cap (IRQHandlerCap x'); excaps = transform_cap_list excaps'; invocation_type label' \<noteq> GenInvocationLabel IRQAckIRQ; invocation_type label' = GenInvocationLabel IRQSetIRQHandler\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_irq_handler_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (case ui of IrqHandlerAckIntent \<Rightarrow> doE irq <- liftE $ assert_opt $ cdl_cap_irq cap;
returnOk $ AckIrq irq
odE \<sqinter> throw | IrqHandlerSetEndpointIntent \<Rightarrow> doE endpoint <- throw_on_none $ get_index excaps 0;
endpoint_cap <- returnOk $ fst endpoint;
endpoint_cap_ref <- returnOk $ snd endpoint;
irq <- liftE $ assert_opt $ cdl_cap_irq cap;
case endpoint_cap of cdl_cap.NotificationCap x xa xb \<Rightarrow> returnOk () | _ \<Rightarrow> throw;
returnOk $ SetIrqHandler irq endpoint_cap endpoint_cap_ref
odE \<sqinter> throw | IrqHandlerClearIntent \<Rightarrow> doE irq <- liftE $ assert_opt $ cdl_cap_irq cap;
returnOk $ ClearIrqHandler irq
odE \<sqinter> throw) (if gen_invocation_type label' = IRQAckIRQ then returnOk $ ACKIrq x' else if gen_invocation_type label' = IRQSetIRQHandler then if excaps' \<noteq> [] then let (cap, slot) = hd excaps' in if Structures_A.is_ntfn_cap cap \<and> AllowSend \<in> Structures_A.cap_rights cap then returnOk $ SetIRQHandler x' cap slot else throwError $ InvalidCapability 0 else throwError TruncatedMessage else if gen_invocation_type label' = IRQClearIRQHandler then returnOk $ ClearIRQHandler x' else throwError IllegalOperation)
 2. \<And>slot. \<lbrakk>Some (IrqHandlerIntent ui) = transform_intent (invocation_type label') args'; cap = transform_cap (IRQHandlerCap x'); excaps = transform_cap_list excaps'; invocation_type label' \<noteq> GenInvocationLabel IRQAckIRQ; invocation_type label' \<noteq> GenInvocationLabel IRQSetIRQHandler\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_irq_handler_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (case ui of IrqHandlerAckIntent \<Rightarrow> doE irq <- liftE $ assert_opt $ cdl_cap_irq cap;
returnOk $ AckIrq irq
odE \<sqinter> throw | IrqHandlerSetEndpointIntent \<Rightarrow> doE endpoint <- throw_on_none $ get_index excaps 0;
endpoint_cap <- returnOk $ fst endpoint;
endpoint_cap_ref <- returnOk $ snd endpoint;
irq <- liftE $ assert_opt $ cdl_cap_irq cap;
case endpoint_cap of cdl_cap.NotificationCap x xa xb \<Rightarrow> returnOk () | _ \<Rightarrow> throw;
returnOk $ SetIrqHandler irq endpoint_cap endpoint_cap_ref
odE \<sqinter> throw | IrqHandlerClearIntent \<Rightarrow> doE irq <- liftE $ assert_opt $ cdl_cap_irq cap;
returnOk $ ClearIrqHandler irq
odE \<sqinter> throw) (if gen_invocation_type label' = IRQAckIRQ then returnOk $ ACKIrq x' else if gen_invocation_type label' = IRQSetIRQHandler then if excaps' \<noteq> [] then let (cap, slot) = hd excaps' in if Structures_A.is_ntfn_cap cap \<and> AllowSend \<in> Structures_A.cap_rights cap then returnOk $ SetIRQHandler x' cap slot else throwError $ InvalidCapability 0 else throwError TruncatedMessage else if gen_invocation_type label' = IRQClearIRQHandler then returnOk $ ClearIRQHandler x' else throwError IllegalOperation) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ui = IrqHandlerSetEndpointIntent; cap = IrqHandlerCap x'; excaps = transform_cap_list excaps'; invocation_type label' = GenInvocationLabel IRQSetIRQHandler\<rbrakk> \<Longrightarrow> (excaps' \<noteq> [] \<longrightarrow> dcorres (dc \<oplus> cdl_irq_handler_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (doE endpoint <- throw_on_none (get_index (transform_cap_list excaps') 0);
irq <- liftE (return x');
y <- case fst endpoint of cdl_cap.NotificationCap x xa xb \<Rightarrow> returnOk () | _ \<Rightarrow> throw;
returnOk (SetIrqHandler irq (fst endpoint) (snd endpoint))
odE \<sqinter> throw) (case hd excaps' of (cap, slot) \<Rightarrow> if Structures_A.is_ntfn_cap cap \<and> AllowWrite \<in> Structures_A.cap_rights cap then returnOk $ SetIRQHandler x' cap slot else throwError $ InvalidCapability 0)) \<and> (excaps' = [] \<longrightarrow> dcorres (dc \<oplus> cdl_irq_handler_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (doE endpoint <- throw_on_none (get_index (transform_cap_list []) 0);
irq <- liftE (return x');
y <- case fst endpoint of cdl_cap.NotificationCap x xa xb \<Rightarrow> returnOk () | _ \<Rightarrow> throw;
returnOk (SetIrqHandler irq (fst endpoint) (snd endpoint))
odE \<sqinter> throw) (throwError TruncatedMessage))
 2. \<And>slot. \<lbrakk>Some (IrqHandlerIntent ui) = transform_intent (invocation_type label') args'; cap = transform_cap (IRQHandlerCap x'); excaps = transform_cap_list excaps'; invocation_type label' \<noteq> GenInvocationLabel IRQAckIRQ; invocation_type label' \<noteq> GenInvocationLabel IRQSetIRQHandler\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_irq_handler_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (case ui of IrqHandlerAckIntent \<Rightarrow> doE irq <- liftE $ assert_opt $ cdl_cap_irq cap;
returnOk $ AckIrq irq
odE \<sqinter> throw | IrqHandlerSetEndpointIntent \<Rightarrow> doE endpoint <- throw_on_none $ get_index excaps 0;
endpoint_cap <- returnOk $ fst endpoint;
endpoint_cap_ref <- returnOk $ snd endpoint;
irq <- liftE $ assert_opt $ cdl_cap_irq cap;
case endpoint_cap of cdl_cap.NotificationCap x xa xb \<Rightarrow> returnOk () | _ \<Rightarrow> throw;
returnOk $ SetIrqHandler irq endpoint_cap endpoint_cap_ref
odE \<sqinter> throw | IrqHandlerClearIntent \<Rightarrow> doE irq <- liftE $ assert_opt $ cdl_cap_irq cap;
returnOk $ ClearIrqHandler irq
odE \<sqinter> throw) (if gen_invocation_type label' = IRQAckIRQ then returnOk $ ACKIrq x' else if gen_invocation_type label' = IRQSetIRQHandler then if excaps' \<noteq> [] then let (cap, slot) = hd excaps' in if Structures_A.is_ntfn_cap cap \<and> AllowSend \<in> Structures_A.cap_rights cap then returnOk $ SetIRQHandler x' cap slot else throwError $ InvalidCapability 0 else throwError TruncatedMessage else if gen_invocation_type label' = IRQClearIRQHandler then returnOk $ ClearIRQHandler x' else throwError IllegalOperation) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>ui = IrqHandlerSetEndpointIntent; cap = IrqHandlerCap x'; excaps = transform_cap_list excaps'; invocation_type label' = GenInvocationLabel IRQSetIRQHandler\<rbrakk> \<Longrightarrow> excaps' \<noteq> [] \<longrightarrow> dcorres (dc \<oplus> cdl_irq_handler_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (doE endpoint <- throw_on_none (get_index (transform_cap_list excaps') 0);
irq <- liftE (return x');
y <- case fst endpoint of cdl_cap.NotificationCap x xa xb \<Rightarrow> returnOk () | _ \<Rightarrow> throw;
returnOk (SetIrqHandler irq (fst endpoint) (snd endpoint))
odE \<sqinter> throw) (case hd excaps' of (cap, slot) \<Rightarrow> if Structures_A.is_ntfn_cap cap \<and> AllowWrite \<in> Structures_A.cap_rights cap then returnOk $ SetIRQHandler x' cap slot else throwError $ InvalidCapability 0)
 2. \<lbrakk>ui = IrqHandlerSetEndpointIntent; cap = IrqHandlerCap x'; excaps = transform_cap_list excaps'; invocation_type label' = GenInvocationLabel IRQSetIRQHandler\<rbrakk> \<Longrightarrow> excaps' = [] \<longrightarrow> dcorres (dc \<oplus> cdl_irq_handler_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (doE endpoint <- throw_on_none (get_index (transform_cap_list []) 0);
irq <- liftE (return x');
y <- case fst endpoint of cdl_cap.NotificationCap x xa xb \<Rightarrow> returnOk () | _ \<Rightarrow> throw;
returnOk (SetIrqHandler irq (fst endpoint) (snd endpoint))
odE \<sqinter> throw) (throwError TruncatedMessage)
 3. \<And>slot. \<lbrakk>Some (IrqHandlerIntent ui) = transform_intent (invocation_type label') args'; cap = transform_cap (IRQHandlerCap x'); excaps = transform_cap_list excaps'; invocation_type label' \<noteq> GenInvocationLabel IRQAckIRQ; invocation_type label' \<noteq> GenInvocationLabel IRQSetIRQHandler\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_irq_handler_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (case ui of IrqHandlerAckIntent \<Rightarrow> doE irq <- liftE $ assert_opt $ cdl_cap_irq cap;
returnOk $ AckIrq irq
odE \<sqinter> throw | IrqHandlerSetEndpointIntent \<Rightarrow> doE endpoint <- throw_on_none $ get_index excaps 0;
endpoint_cap <- returnOk $ fst endpoint;
endpoint_cap_ref <- returnOk $ snd endpoint;
irq <- liftE $ assert_opt $ cdl_cap_irq cap;
case endpoint_cap of cdl_cap.NotificationCap x xa xb \<Rightarrow> returnOk () | _ \<Rightarrow> throw;
returnOk $ SetIrqHandler irq endpoint_cap endpoint_cap_ref
odE \<sqinter> throw | IrqHandlerClearIntent \<Rightarrow> doE irq <- liftE $ assert_opt $ cdl_cap_irq cap;
returnOk $ ClearIrqHandler irq
odE \<sqinter> throw) (if gen_invocation_type label' = IRQAckIRQ then returnOk $ ACKIrq x' else if gen_invocation_type label' = IRQSetIRQHandler then if excaps' \<noteq> [] then let (cap, slot) = hd excaps' in if Structures_A.is_ntfn_cap cap \<and> AllowSend \<in> Structures_A.cap_rights cap then returnOk $ SetIRQHandler x' cap slot else throwError $ InvalidCapability 0 else throwError TruncatedMessage else if gen_invocation_type label' = IRQClearIRQHandler then returnOk $ ClearIRQHandler x' else throwError IllegalOperation) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>ui = IrqHandlerSetEndpointIntent; cap = IrqHandlerCap x'; excaps = transform_cap_list excaps'; invocation_type label' = GenInvocationLabel IRQSetIRQHandler\<rbrakk> \<Longrightarrow> excaps' = [] \<longrightarrow> dcorres (dc \<oplus> cdl_irq_handler_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (doE endpoint <- throw_on_none (get_index (transform_cap_list []) 0);
irq <- liftE (return x');
y <- case fst endpoint of cdl_cap.NotificationCap x xa xb \<Rightarrow> returnOk () | _ \<Rightarrow> throw;
returnOk (SetIrqHandler irq (fst endpoint) (snd endpoint))
odE \<sqinter> throw) (throwError TruncatedMessage)
 2. \<lbrakk>ui = IrqHandlerSetEndpointIntent; cap = IrqHandlerCap x'; excaps = transform_cap_list excaps'; invocation_type label' = GenInvocationLabel IRQSetIRQHandler\<rbrakk> \<Longrightarrow> excaps' \<noteq> [] \<longrightarrow> dcorres (dc \<oplus> cdl_irq_handler_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (doE endpoint <- throw_on_none (get_index (transform_cap_list excaps') 0);
irq <- liftE (return x');
y <- case fst endpoint of cdl_cap.NotificationCap x xa xb \<Rightarrow> returnOk () | _ \<Rightarrow> throw;
returnOk (SetIrqHandler irq (fst endpoint) (snd endpoint))
odE \<sqinter> throw) (case hd excaps' of (cap, slot) \<Rightarrow> if Structures_A.is_ntfn_cap cap \<and> AllowWrite \<in> Structures_A.cap_rights cap then returnOk $ SetIRQHandler x' cap slot else throwError $ InvalidCapability 0)
 3. \<And>slot. \<lbrakk>Some (IrqHandlerIntent ui) = transform_intent (invocation_type label') args'; cap = transform_cap (IRQHandlerCap x'); excaps = transform_cap_list excaps'; invocation_type label' \<noteq> GenInvocationLabel IRQAckIRQ; invocation_type label' \<noteq> GenInvocationLabel IRQSetIRQHandler\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_irq_handler_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (case ui of IrqHandlerAckIntent \<Rightarrow> doE irq <- liftE $ assert_opt $ cdl_cap_irq cap;
returnOk $ AckIrq irq
odE \<sqinter> throw | IrqHandlerSetEndpointIntent \<Rightarrow> doE endpoint <- throw_on_none $ get_index excaps 0;
endpoint_cap <- returnOk $ fst endpoint;
endpoint_cap_ref <- returnOk $ snd endpoint;
irq <- liftE $ assert_opt $ cdl_cap_irq cap;
case endpoint_cap of cdl_cap.NotificationCap x xa xb \<Rightarrow> returnOk () | _ \<Rightarrow> throw;
returnOk $ SetIrqHandler irq endpoint_cap endpoint_cap_ref
odE \<sqinter> throw | IrqHandlerClearIntent \<Rightarrow> doE irq <- liftE $ assert_opt $ cdl_cap_irq cap;
returnOk $ ClearIrqHandler irq
odE \<sqinter> throw) (if gen_invocation_type label' = IRQAckIRQ then returnOk $ ACKIrq x' else if gen_invocation_type label' = IRQSetIRQHandler then if excaps' \<noteq> [] then let (cap, slot) = hd excaps' in if Structures_A.is_ntfn_cap cap \<and> AllowSend \<in> Structures_A.cap_rights cap then returnOk $ SetIRQHandler x' cap slot else throwError $ InvalidCapability 0 else throwError TruncatedMessage else if gen_invocation_type label' = IRQClearIRQHandler then returnOk $ ClearIRQHandler x' else throwError IllegalOperation) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ui = IrqHandlerSetEndpointIntent; cap = IrqHandlerCap x'; excaps = transform_cap_list excaps'; invocation_type label' = GenInvocationLabel IRQSetIRQHandler\<rbrakk> \<Longrightarrow> excaps' \<noteq> [] \<longrightarrow> dcorres (dc \<oplus> cdl_irq_handler_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (doE endpoint <- throw_on_none (get_index (transform_cap_list excaps') 0);
irq <- liftE (return x');
y <- case fst endpoint of cdl_cap.NotificationCap x xa xb \<Rightarrow> returnOk () | _ \<Rightarrow> throw;
returnOk (SetIrqHandler irq (fst endpoint) (snd endpoint))
odE \<sqinter> throw) (case hd excaps' of (cap, slot) \<Rightarrow> if Structures_A.is_ntfn_cap cap \<and> AllowWrite \<in> Structures_A.cap_rights cap then returnOk $ SetIRQHandler x' cap slot else throwError $ InvalidCapability 0)
 2. \<And>slot. \<lbrakk>Some (IrqHandlerIntent ui) = transform_intent (invocation_type label') args'; cap = transform_cap (IRQHandlerCap x'); excaps = transform_cap_list excaps'; invocation_type label' \<noteq> GenInvocationLabel IRQAckIRQ; invocation_type label' \<noteq> GenInvocationLabel IRQSetIRQHandler\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_irq_handler_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (case ui of IrqHandlerAckIntent \<Rightarrow> doE irq <- liftE $ assert_opt $ cdl_cap_irq cap;
returnOk $ AckIrq irq
odE \<sqinter> throw | IrqHandlerSetEndpointIntent \<Rightarrow> doE endpoint <- throw_on_none $ get_index excaps 0;
endpoint_cap <- returnOk $ fst endpoint;
endpoint_cap_ref <- returnOk $ snd endpoint;
irq <- liftE $ assert_opt $ cdl_cap_irq cap;
case endpoint_cap of cdl_cap.NotificationCap x xa xb \<Rightarrow> returnOk () | _ \<Rightarrow> throw;
returnOk $ SetIrqHandler irq endpoint_cap endpoint_cap_ref
odE \<sqinter> throw | IrqHandlerClearIntent \<Rightarrow> doE irq <- liftE $ assert_opt $ cdl_cap_irq cap;
returnOk $ ClearIrqHandler irq
odE \<sqinter> throw) (if gen_invocation_type label' = IRQAckIRQ then returnOk $ ACKIrq x' else if gen_invocation_type label' = IRQSetIRQHandler then if excaps' \<noteq> [] then let (cap, slot) = hd excaps' in if Structures_A.is_ntfn_cap cap \<and> AllowSend \<in> Structures_A.cap_rights cap then returnOk $ SetIRQHandler x' cap slot else throwError $ InvalidCapability 0 else throwError TruncatedMessage else if gen_invocation_type label' = IRQClearIRQHandler then returnOk $ ClearIRQHandler x' else throwError IllegalOperation) proof (prove)
goal (2 subgoals):
 1. \<And>a aa b ys. \<lbrakk>ui = IrqHandlerSetEndpointIntent; cap = IrqHandlerCap x'; excaps = transform_cap_list ((a, aa, b) # ys); invocation_type label' = GenInvocationLabel IRQSetIRQHandler; excaps' = (a, aa, b) # ys\<rbrakk> \<Longrightarrow> (Structures_A.is_ntfn_cap a \<and> AllowWrite \<in> Structures_A.cap_rights a \<longrightarrow> dcorres (dc \<oplus> cdl_irq_handler_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (doE endpoint <- throw_on_none (get_index (transform_cap_list ((a, aa, b) # ys)) 0);
irq <- liftE (return x');
y <- case fst endpoint of cdl_cap.NotificationCap x xa xb \<Rightarrow> returnOk () | _ \<Rightarrow> throw;
returnOk (SetIrqHandler irq (fst endpoint) (snd endpoint))
odE \<sqinter> throw) (returnOk (SetIRQHandler x' a (aa, b)))) \<and> ((Structures_A.is_ntfn_cap a \<longrightarrow> AllowWrite \<notin> Structures_A.cap_rights a) \<longrightarrow> dcorres (dc \<oplus> cdl_irq_handler_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (doE endpoint <- throw_on_none (get_index (transform_cap_list ((a, aa, b) # ys)) 0);
irq <- liftE (return x');
y <- case fst endpoint of cdl_cap.NotificationCap x xa xb \<Rightarrow> returnOk () | _ \<Rightarrow> throw;
returnOk (SetIrqHandler irq (fst endpoint) (snd endpoint))
odE \<sqinter> throw) (throwError (InvalidCapability 0)))
 2. \<And>slot. \<lbrakk>Some (IrqHandlerIntent ui) = transform_intent (invocation_type label') args'; cap = transform_cap (IRQHandlerCap x'); excaps = transform_cap_list excaps'; invocation_type label' \<noteq> GenInvocationLabel IRQAckIRQ; invocation_type label' \<noteq> GenInvocationLabel IRQSetIRQHandler\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_irq_handler_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (case ui of IrqHandlerAckIntent \<Rightarrow> doE irq <- liftE $ assert_opt $ cdl_cap_irq cap;
returnOk $ AckIrq irq
odE \<sqinter> throw | IrqHandlerSetEndpointIntent \<Rightarrow> doE endpoint <- throw_on_none $ get_index excaps 0;
endpoint_cap <- returnOk $ fst endpoint;
endpoint_cap_ref <- returnOk $ snd endpoint;
irq <- liftE $ assert_opt $ cdl_cap_irq cap;
case endpoint_cap of cdl_cap.NotificationCap x xa xb \<Rightarrow> returnOk () | _ \<Rightarrow> throw;
returnOk $ SetIrqHandler irq endpoint_cap endpoint_cap_ref
odE \<sqinter> throw | IrqHandlerClearIntent \<Rightarrow> doE irq <- liftE $ assert_opt $ cdl_cap_irq cap;
returnOk $ ClearIrqHandler irq
odE \<sqinter> throw) (if gen_invocation_type label' = IRQAckIRQ then returnOk $ ACKIrq x' else if gen_invocation_type label' = IRQSetIRQHandler then if excaps' \<noteq> [] then let (cap, slot) = hd excaps' in if Structures_A.is_ntfn_cap cap \<and> AllowSend \<in> Structures_A.cap_rights cap then returnOk $ SetIRQHandler x' cap slot else throwError $ InvalidCapability 0 else throwError TruncatedMessage else if gen_invocation_type label' = IRQClearIRQHandler then returnOk $ ClearIRQHandler x' else throwError IllegalOperation) proof (prove)
goal (3 subgoals):
 1. \<And>a aa b ys. \<lbrakk>ui = IrqHandlerSetEndpointIntent; cap = IrqHandlerCap x'; excaps = transform_cap_list ((a, aa, b) # ys); invocation_type label' = GenInvocationLabel IRQSetIRQHandler; excaps' = (a, aa, b) # ys\<rbrakk> \<Longrightarrow> Structures_A.is_ntfn_cap a \<and> AllowWrite \<in> Structures_A.cap_rights a \<longrightarrow> dcorres (dc \<oplus> cdl_irq_handler_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (doE endpoint <- throw_on_none (get_index (transform_cap_list ((a, aa, b) # ys)) 0);
irq <- liftE (return x');
y <- case fst endpoint of cdl_cap.NotificationCap x xa xb \<Rightarrow> returnOk () | _ \<Rightarrow> throw;
returnOk (SetIrqHandler irq (fst endpoint) (snd endpoint))
odE \<sqinter> throw) (returnOk (SetIRQHandler x' a (aa, b)))
 2. \<And>a aa b ys. \<lbrakk>ui = IrqHandlerSetEndpointIntent; cap = IrqHandlerCap x'; excaps = transform_cap_list ((a, aa, b) # ys); invocation_type label' = GenInvocationLabel IRQSetIRQHandler; excaps' = (a, aa, b) # ys\<rbrakk> \<Longrightarrow> (Structures_A.is_ntfn_cap a \<longrightarrow> AllowWrite \<notin> Structures_A.cap_rights a) \<longrightarrow> dcorres (dc \<oplus> cdl_irq_handler_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (doE endpoint <- throw_on_none (get_index (transform_cap_list ((a, aa, b) # ys)) 0);
irq <- liftE (return x');
y <- case fst endpoint of cdl_cap.NotificationCap x xa xb \<Rightarrow> returnOk () | _ \<Rightarrow> throw;
returnOk (SetIrqHandler irq (fst endpoint) (snd endpoint))
odE \<sqinter> throw) (throwError (InvalidCapability 0))
 3. \<And>slot. \<lbrakk>Some (IrqHandlerIntent ui) = transform_intent (invocation_type label') args'; cap = transform_cap (IRQHandlerCap x'); excaps = transform_cap_list excaps'; invocation_type label' \<noteq> GenInvocationLabel IRQAckIRQ; invocation_type label' \<noteq> GenInvocationLabel IRQSetIRQHandler\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_irq_handler_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (case ui of IrqHandlerAckIntent \<Rightarrow> doE irq <- liftE $ assert_opt $ cdl_cap_irq cap;
returnOk $ AckIrq irq
odE \<sqinter> throw | IrqHandlerSetEndpointIntent \<Rightarrow> doE endpoint <- throw_on_none $ get_index excaps 0;
endpoint_cap <- returnOk $ fst endpoint;
endpoint_cap_ref <- returnOk $ snd endpoint;
irq <- liftE $ assert_opt $ cdl_cap_irq cap;
case endpoint_cap of cdl_cap.NotificationCap x xa xb \<Rightarrow> returnOk () | _ \<Rightarrow> throw;
returnOk $ SetIrqHandler irq endpoint_cap endpoint_cap_ref
odE \<sqinter> throw | IrqHandlerClearIntent \<Rightarrow> doE irq <- liftE $ assert_opt $ cdl_cap_irq cap;
returnOk $ ClearIrqHandler irq
odE \<sqinter> throw) (if gen_invocation_type label' = IRQAckIRQ then returnOk $ ACKIrq x' else if gen_invocation_type label' = IRQSetIRQHandler then if excaps' \<noteq> [] then let (cap, slot) = hd excaps' in if Structures_A.is_ntfn_cap cap \<and> AllowSend \<in> Structures_A.cap_rights cap then returnOk $ SetIRQHandler x' cap slot else throwError $ InvalidCapability 0 else throwError TruncatedMessage else if gen_invocation_type label' = IRQClearIRQHandler then returnOk $ ClearIRQHandler x' else throwError IllegalOperation) proof (prove)
goal (3 subgoals):
 1. \<And>a aa b ys. \<lbrakk>ui = IrqHandlerSetEndpointIntent; cap = IrqHandlerCap x'; excaps = transform_cap_list ((a, aa, b) # ys); invocation_type label' = GenInvocationLabel IRQSetIRQHandler; excaps' = (a, aa, b) # ys\<rbrakk> \<Longrightarrow> (Structures_A.is_ntfn_cap a \<longrightarrow> AllowWrite \<notin> Structures_A.cap_rights a) \<longrightarrow> dcorres (dc \<oplus> cdl_irq_handler_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (doE endpoint <- throw_on_none (get_index (transform_cap_list ((a, aa, b) # ys)) 0);
irq <- liftE (return x');
y <- case fst endpoint of cdl_cap.NotificationCap x xa xb \<Rightarrow> returnOk () | _ \<Rightarrow> throw;
returnOk (SetIrqHandler irq (fst endpoint) (snd endpoint))
odE \<sqinter> throw) (throwError (InvalidCapability 0))
 2. \<And>a aa b ys. \<lbrakk>ui = IrqHandlerSetEndpointIntent; cap = IrqHandlerCap x'; excaps = transform_cap_list ((a, aa, b) # ys); invocation_type label' = GenInvocationLabel IRQSetIRQHandler; excaps' = (a, aa, b) # ys\<rbrakk> \<Longrightarrow> Structures_A.is_ntfn_cap a \<and> AllowWrite \<in> Structures_A.cap_rights a \<longrightarrow> dcorres (dc \<oplus> cdl_irq_handler_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (doE endpoint <- throw_on_none (get_index (transform_cap_list ((a, aa, b) # ys)) 0);
irq <- liftE (return x');
y <- case fst endpoint of cdl_cap.NotificationCap x xa xb \<Rightarrow> returnOk () | _ \<Rightarrow> throw;
returnOk (SetIrqHandler irq (fst endpoint) (snd endpoint))
odE \<sqinter> throw) (returnOk (SetIRQHandler x' a (aa, b)))
 3. \<And>slot. \<lbrakk>Some (IrqHandlerIntent ui) = transform_intent (invocation_type label') args'; cap = transform_cap (IRQHandlerCap x'); excaps = transform_cap_list excaps'; invocation_type label' \<noteq> GenInvocationLabel IRQAckIRQ; invocation_type label' \<noteq> GenInvocationLabel IRQSetIRQHandler\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_irq_handler_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (case ui of IrqHandlerAckIntent \<Rightarrow> doE irq <- liftE $ assert_opt $ cdl_cap_irq cap;
returnOk $ AckIrq irq
odE \<sqinter> throw | IrqHandlerSetEndpointIntent \<Rightarrow> doE endpoint <- throw_on_none $ get_index excaps 0;
endpoint_cap <- returnOk $ fst endpoint;
endpoint_cap_ref <- returnOk $ snd endpoint;
irq <- liftE $ assert_opt $ cdl_cap_irq cap;
case endpoint_cap of cdl_cap.NotificationCap x xa xb \<Rightarrow> returnOk () | _ \<Rightarrow> throw;
returnOk $ SetIrqHandler irq endpoint_cap endpoint_cap_ref
odE \<sqinter> throw | IrqHandlerClearIntent \<Rightarrow> doE irq <- liftE $ assert_opt $ cdl_cap_irq cap;
returnOk $ ClearIrqHandler irq
odE \<sqinter> throw) (if gen_invocation_type label' = IRQAckIRQ then returnOk $ ACKIrq x' else if gen_invocation_type label' = IRQSetIRQHandler then if excaps' \<noteq> [] then let (cap, slot) = hd excaps' in if Structures_A.is_ntfn_cap cap \<and> AllowSend \<in> Structures_A.cap_rights cap then returnOk $ SetIRQHandler x' cap slot else throwError $ InvalidCapability 0 else throwError TruncatedMessage else if gen_invocation_type label' = IRQClearIRQHandler then returnOk $ ClearIRQHandler x' else throwError IllegalOperation) proof (prove)
goal (2 subgoals):
 1. \<And>a aa b ys. \<lbrakk>ui = IrqHandlerSetEndpointIntent; cap = IrqHandlerCap x'; excaps = transform_cap_list ((a, aa, b) # ys); invocation_type label' = GenInvocationLabel IRQSetIRQHandler; excaps' = (a, aa, b) # ys\<rbrakk> \<Longrightarrow> Structures_A.is_ntfn_cap a \<and> AllowWrite \<in> Structures_A.cap_rights a \<longrightarrow> dcorres (dc \<oplus> cdl_irq_handler_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (doE endpoint <- throw_on_none (get_index (transform_cap_list ((a, aa, b) # ys)) 0);
irq <- liftE (return x');
y <- case fst endpoint of cdl_cap.NotificationCap x xa xb \<Rightarrow> returnOk () | _ \<Rightarrow> throw;
returnOk (SetIrqHandler irq (fst endpoint) (snd endpoint))
odE \<sqinter> throw) (returnOk (SetIRQHandler x' a (aa, b)))
 2. \<And>slot. \<lbrakk>Some (IrqHandlerIntent ui) = transform_intent (invocation_type label') args'; cap = transform_cap (IRQHandlerCap x'); excaps = transform_cap_list excaps'; invocation_type label' \<noteq> GenInvocationLabel IRQAckIRQ; invocation_type label' \<noteq> GenInvocationLabel IRQSetIRQHandler\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_irq_handler_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (case ui of IrqHandlerAckIntent \<Rightarrow> doE irq <- liftE $ assert_opt $ cdl_cap_irq cap;
returnOk $ AckIrq irq
odE \<sqinter> throw | IrqHandlerSetEndpointIntent \<Rightarrow> doE endpoint <- throw_on_none $ get_index excaps 0;
endpoint_cap <- returnOk $ fst endpoint;
endpoint_cap_ref <- returnOk $ snd endpoint;
irq <- liftE $ assert_opt $ cdl_cap_irq cap;
case endpoint_cap of cdl_cap.NotificationCap x xa xb \<Rightarrow> returnOk () | _ \<Rightarrow> throw;
returnOk $ SetIrqHandler irq endpoint_cap endpoint_cap_ref
odE \<sqinter> throw | IrqHandlerClearIntent \<Rightarrow> doE irq <- liftE $ assert_opt $ cdl_cap_irq cap;
returnOk $ ClearIrqHandler irq
odE \<sqinter> throw) (if gen_invocation_type label' = IRQAckIRQ then returnOk $ ACKIrq x' else if gen_invocation_type label' = IRQSetIRQHandler then if excaps' \<noteq> [] then let (cap, slot) = hd excaps' in if Structures_A.is_ntfn_cap cap \<and> AllowSend \<in> Structures_A.cap_rights cap then returnOk $ SetIRQHandler x' cap slot else throwError $ InvalidCapability 0 else throwError TruncatedMessage else if gen_invocation_type label' = IRQClearIRQHandler then returnOk $ ClearIRQHandler x' else throwError IllegalOperation) proof (prove)
goal (2 subgoals):
 1. \<And>a aa b ys. \<lbrakk>ui = IrqHandlerSetEndpointIntent; cap = IrqHandlerCap x'; excaps = transform_cap_list ((a, aa, b) # ys); invocation_type label' = GenInvocationLabel IRQSetIRQHandler; excaps' = (a, aa, b) # ys; Structures_A.is_ntfn_cap a; AllowWrite \<in> Structures_A.cap_rights a\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_irq_handler_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (doE endpoint <- throw_on_none (get_index (transform_cap_list ((a, aa, b) # ys)) 0);
irq <- liftE (return x');
y <- case fst endpoint of cdl_cap.NotificationCap x xa xb \<Rightarrow> returnOk () | _ \<Rightarrow> throw;
returnOk (SetIrqHandler irq (fst endpoint) (snd endpoint))
odE \<sqinter> throw) (returnOk (SetIRQHandler x' a (aa, b)))
 2. \<And>slot. \<lbrakk>Some (IrqHandlerIntent ui) = transform_intent (invocation_type label') args'; cap = transform_cap (IRQHandlerCap x'); excaps = transform_cap_list excaps'; invocation_type label' \<noteq> GenInvocationLabel IRQAckIRQ; invocation_type label' \<noteq> GenInvocationLabel IRQSetIRQHandler\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_irq_handler_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (case ui of IrqHandlerAckIntent \<Rightarrow> doE irq <- liftE $ assert_opt $ cdl_cap_irq cap;
returnOk $ AckIrq irq
odE \<sqinter> throw | IrqHandlerSetEndpointIntent \<Rightarrow> doE endpoint <- throw_on_none $ get_index excaps 0;
endpoint_cap <- returnOk $ fst endpoint;
endpoint_cap_ref <- returnOk $ snd endpoint;
irq <- liftE $ assert_opt $ cdl_cap_irq cap;
case endpoint_cap of cdl_cap.NotificationCap x xa xb \<Rightarrow> returnOk () | _ \<Rightarrow> throw;
returnOk $ SetIrqHandler irq endpoint_cap endpoint_cap_ref
odE \<sqinter> throw | IrqHandlerClearIntent \<Rightarrow> doE irq <- liftE $ assert_opt $ cdl_cap_irq cap;
returnOk $ ClearIrqHandler irq
odE \<sqinter> throw) (if gen_invocation_type label' = IRQAckIRQ then returnOk $ ACKIrq x' else if gen_invocation_type label' = IRQSetIRQHandler then if excaps' \<noteq> [] then let (cap, slot) = hd excaps' in if Structures_A.is_ntfn_cap cap \<and> AllowSend \<in> Structures_A.cap_rights cap then returnOk $ SetIRQHandler x' cap slot else throwError $ InvalidCapability 0 else throwError TruncatedMessage else if gen_invocation_type label' = IRQClearIRQHandler then returnOk $ ClearIRQHandler x' else throwError IllegalOperation) proof (prove)
goal (2 subgoals):
 1. \<And>a aa b ys. \<lbrakk>ui = IrqHandlerSetEndpointIntent; cap = IrqHandlerCap x'; excaps = transform_cap_list ((a, aa, b) # ys); invocation_type label' = GenInvocationLabel IRQSetIRQHandler; excaps' = (a, aa, b) # ys; Structures_A.is_ntfn_cap a; AllowWrite \<in> Structures_A.cap_rights a\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_irq_handler_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (doE endpoint <- throw_on_none (get_index (transform_cap_list ((a, aa, b) # ys)) 0);
irq <- liftE (return x');
y <- case fst endpoint of cdl_cap.NotificationCap x xa xb \<Rightarrow> returnOk () | _ \<Rightarrow> throw;
returnOk (SetIrqHandler irq (fst endpoint) (snd endpoint))
odE) (returnOk (SetIRQHandler x' a (aa, b)))
 2. \<And>slot. \<lbrakk>Some (IrqHandlerIntent ui) = transform_intent (invocation_type label') args'; cap = transform_cap (IRQHandlerCap x'); excaps = transform_cap_list excaps'; invocation_type label' \<noteq> GenInvocationLabel IRQAckIRQ; invocation_type label' \<noteq> GenInvocationLabel IRQSetIRQHandler\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_irq_handler_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (case ui of IrqHandlerAckIntent \<Rightarrow> doE irq <- liftE $ assert_opt $ cdl_cap_irq cap;
returnOk $ AckIrq irq
odE \<sqinter> throw | IrqHandlerSetEndpointIntent \<Rightarrow> doE endpoint <- throw_on_none $ get_index excaps 0;
endpoint_cap <- returnOk $ fst endpoint;
endpoint_cap_ref <- returnOk $ snd endpoint;
irq <- liftE $ assert_opt $ cdl_cap_irq cap;
case endpoint_cap of cdl_cap.NotificationCap x xa xb \<Rightarrow> returnOk () | _ \<Rightarrow> throw;
returnOk $ SetIrqHandler irq endpoint_cap endpoint_cap_ref
odE \<sqinter> throw | IrqHandlerClearIntent \<Rightarrow> doE irq <- liftE $ assert_opt $ cdl_cap_irq cap;
returnOk $ ClearIrqHandler irq
odE \<sqinter> throw) (if gen_invocation_type label' = IRQAckIRQ then returnOk $ ACKIrq x' else if gen_invocation_type label' = IRQSetIRQHandler then if excaps' \<noteq> [] then let (cap, slot) = hd excaps' in if Structures_A.is_ntfn_cap cap \<and> AllowSend \<in> Structures_A.cap_rights cap then returnOk $ SetIRQHandler x' cap slot else throwError $ InvalidCapability 0 else throwError TruncatedMessage else if gen_invocation_type label' = IRQClearIRQHandler then returnOk $ ClearIRQHandler x' else throwError IllegalOperation) proof (prove)
goal (2 subgoals):
 1. \<And>a aa b ys. \<lbrakk>ui = IrqHandlerSetEndpointIntent; cap = IrqHandlerCap x'; excaps = (transform_cap a, transform_cslot_ptr (aa, b)) # map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) ys; invocation_type label' = GenInvocationLabel IRQSetIRQHandler; excaps' = (a, aa, b) # ys; Structures_A.is_ntfn_cap a; AllowWrite \<in> Structures_A.cap_rights a\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_irq_handler_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (doE y <- case transform_cap a of cdl_cap.NotificationCap x xa xb \<Rightarrow> returnOk () | _ \<Rightarrow> throw;
returnOk (SetIrqHandler x' (transform_cap a) (transform_cslot_ptr (aa, b)))
odE) (returnOk (SetIRQHandler x' a (aa, b)))
 2. \<And>slot. \<lbrakk>Some (IrqHandlerIntent ui) = transform_intent (invocation_type label') args'; cap = transform_cap (IRQHandlerCap x'); excaps = transform_cap_list excaps'; invocation_type label' \<noteq> GenInvocationLabel IRQAckIRQ; invocation_type label' \<noteq> GenInvocationLabel IRQSetIRQHandler\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_irq_handler_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (case ui of IrqHandlerAckIntent \<Rightarrow> doE irq <- liftE $ assert_opt $ cdl_cap_irq cap;
returnOk $ AckIrq irq
odE \<sqinter> throw | IrqHandlerSetEndpointIntent \<Rightarrow> doE endpoint <- throw_on_none $ get_index excaps 0;
endpoint_cap <- returnOk $ fst endpoint;
endpoint_cap_ref <- returnOk $ snd endpoint;
irq <- liftE $ assert_opt $ cdl_cap_irq cap;
case endpoint_cap of cdl_cap.NotificationCap x xa xb \<Rightarrow> returnOk () | _ \<Rightarrow> throw;
returnOk $ SetIrqHandler irq endpoint_cap endpoint_cap_ref
odE \<sqinter> throw | IrqHandlerClearIntent \<Rightarrow> doE irq <- liftE $ assert_opt $ cdl_cap_irq cap;
returnOk $ ClearIrqHandler irq
odE \<sqinter> throw) (if gen_invocation_type label' = IRQAckIRQ then returnOk $ ACKIrq x' else if gen_invocation_type label' = IRQSetIRQHandler then if excaps' \<noteq> [] then let (cap, slot) = hd excaps' in if Structures_A.is_ntfn_cap cap \<and> AllowSend \<in> Structures_A.cap_rights cap then returnOk $ SetIRQHandler x' cap slot else throwError $ InvalidCapability 0 else throwError TruncatedMessage else if gen_invocation_type label' = IRQClearIRQHandler then returnOk $ ClearIRQHandler x' else throwError IllegalOperation) proof (prove)
goal (2 subgoals):
 1. \<And>aa b ys r ba R. \<lbrakk>ui = IrqHandlerSetEndpointIntent; cap = IrqHandlerCap x'; excaps = (cdl_cap.NotificationCap r ba R, transform_cslot_ptr (aa, b)) # map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) ys; invocation_type label' = GenInvocationLabel IRQSetIRQHandler; excaps' = (cap.NotificationCap r ba R, aa, b) # ys; AllowWrite \<in> R\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_irq_handler_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (returnOk (SetIrqHandler x' (cdl_cap.NotificationCap r ba R) (transform_cslot_ptr (aa, b)))) (returnOk (SetIRQHandler x' (cap.NotificationCap r ba R) (aa, b)))
 2. \<And>slot. \<lbrakk>Some (IrqHandlerIntent ui) = transform_intent (invocation_type label') args'; cap = transform_cap (IRQHandlerCap x'); excaps = transform_cap_list excaps'; invocation_type label' \<noteq> GenInvocationLabel IRQAckIRQ; invocation_type label' \<noteq> GenInvocationLabel IRQSetIRQHandler\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_irq_handler_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (case ui of IrqHandlerAckIntent \<Rightarrow> doE irq <- liftE $ assert_opt $ cdl_cap_irq cap;
returnOk $ AckIrq irq
odE \<sqinter> throw | IrqHandlerSetEndpointIntent \<Rightarrow> doE endpoint <- throw_on_none $ get_index excaps 0;
endpoint_cap <- returnOk $ fst endpoint;
endpoint_cap_ref <- returnOk $ snd endpoint;
irq <- liftE $ assert_opt $ cdl_cap_irq cap;
case endpoint_cap of cdl_cap.NotificationCap x xa xb \<Rightarrow> returnOk () | _ \<Rightarrow> throw;
returnOk $ SetIrqHandler irq endpoint_cap endpoint_cap_ref
odE \<sqinter> throw | IrqHandlerClearIntent \<Rightarrow> doE irq <- liftE $ assert_opt $ cdl_cap_irq cap;
returnOk $ ClearIrqHandler irq
odE \<sqinter> throw) (if gen_invocation_type label' = IRQAckIRQ then returnOk $ ACKIrq x' else if gen_invocation_type label' = IRQSetIRQHandler then if excaps' \<noteq> [] then let (cap, slot) = hd excaps' in if Structures_A.is_ntfn_cap cap \<and> AllowSend \<in> Structures_A.cap_rights cap then returnOk $ SetIRQHandler x' cap slot else throwError $ InvalidCapability 0 else throwError TruncatedMessage else if gen_invocation_type label' = IRQClearIRQHandler then returnOk $ ClearIRQHandler x' else throwError IllegalOperation) proof (prove)
goal (2 subgoals):
 1. \<And>aa b ys r ba R. \<lbrakk>ui = IrqHandlerSetEndpointIntent; cap = IrqHandlerCap x'; excaps = (cdl_cap.NotificationCap r ba R, transform_cslot_ptr (aa, b)) # map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) ys; invocation_type label' = GenInvocationLabel IRQSetIRQHandler; excaps' = (cap.NotificationCap r ba R, aa, b) # ys; AllowWrite \<in> R\<rbrakk> \<Longrightarrow> cdl_irq_handler_invocation_relation (SetIrqHandler x' (cdl_cap.NotificationCap r ba R) (transform_cslot_ptr (aa, b))) (SetIRQHandler x' (cap.NotificationCap r ba R) (aa, b))
 2. \<And>slot. \<lbrakk>Some (IrqHandlerIntent ui) = transform_intent (invocation_type label') args'; cap = transform_cap (IRQHandlerCap x'); excaps = transform_cap_list excaps'; invocation_type label' \<noteq> GenInvocationLabel IRQAckIRQ; invocation_type label' \<noteq> GenInvocationLabel IRQSetIRQHandler\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_irq_handler_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (case ui of IrqHandlerAckIntent \<Rightarrow> doE irq <- liftE $ assert_opt $ cdl_cap_irq cap;
returnOk $ AckIrq irq
odE \<sqinter> throw | IrqHandlerSetEndpointIntent \<Rightarrow> doE endpoint <- throw_on_none $ get_index excaps 0;
endpoint_cap <- returnOk $ fst endpoint;
endpoint_cap_ref <- returnOk $ snd endpoint;
irq <- liftE $ assert_opt $ cdl_cap_irq cap;
case endpoint_cap of cdl_cap.NotificationCap x xa xb \<Rightarrow> returnOk () | _ \<Rightarrow> throw;
returnOk $ SetIrqHandler irq endpoint_cap endpoint_cap_ref
odE \<sqinter> throw | IrqHandlerClearIntent \<Rightarrow> doE irq <- liftE $ assert_opt $ cdl_cap_irq cap;
returnOk $ ClearIrqHandler irq
odE \<sqinter> throw) (if gen_invocation_type label' = IRQAckIRQ then returnOk $ ACKIrq x' else if gen_invocation_type label' = IRQSetIRQHandler then if excaps' \<noteq> [] then let (cap, slot) = hd excaps' in if Structures_A.is_ntfn_cap cap \<and> AllowSend \<in> Structures_A.cap_rights cap then returnOk $ SetIRQHandler x' cap slot else throwError $ InvalidCapability 0 else throwError TruncatedMessage else if gen_invocation_type label' = IRQClearIRQHandler then returnOk $ ClearIRQHandler x' else throwError IllegalOperation) proof (prove)
goal (1 subgoal):
 1. \<And>slot. \<lbrakk>Some (IrqHandlerIntent ui) = transform_intent (invocation_type label') args'; cap = transform_cap (IRQHandlerCap x'); excaps = transform_cap_list excaps'; invocation_type label' \<noteq> GenInvocationLabel IRQAckIRQ; invocation_type label' \<noteq> GenInvocationLabel IRQSetIRQHandler\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_irq_handler_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (case ui of IrqHandlerAckIntent \<Rightarrow> doE irq <- liftE $ assert_opt $ cdl_cap_irq cap;
returnOk $ AckIrq irq
odE \<sqinter> throw | IrqHandlerSetEndpointIntent \<Rightarrow> doE endpoint <- throw_on_none $ get_index excaps 0;
endpoint_cap <- returnOk $ fst endpoint;
endpoint_cap_ref <- returnOk $ snd endpoint;
irq <- liftE $ assert_opt $ cdl_cap_irq cap;
case endpoint_cap of cdl_cap.NotificationCap x xa xb \<Rightarrow> returnOk () | _ \<Rightarrow> throw;
returnOk $ SetIrqHandler irq endpoint_cap endpoint_cap_ref
odE \<sqinter> throw | IrqHandlerClearIntent \<Rightarrow> doE irq <- liftE $ assert_opt $ cdl_cap_irq cap;
returnOk $ ClearIrqHandler irq
odE \<sqinter> throw) (if gen_invocation_type label' = IRQAckIRQ then returnOk $ ACKIrq x' else if gen_invocation_type label' = IRQSetIRQHandler then if excaps' \<noteq> [] then let (cap, slot) = hd excaps' in if Structures_A.is_ntfn_cap cap \<and> AllowSend \<in> Structures_A.cap_rights cap then returnOk $ SetIRQHandler x' cap slot else throwError $ InvalidCapability 0 else throwError TruncatedMessage else if gen_invocation_type label' = IRQClearIRQHandler then returnOk $ ClearIRQHandler x' else throwError IllegalOperation) proof (prove)
goal (2 subgoals):
 1. \<And>slot. \<lbrakk>Some (IrqHandlerIntent ui) = transform_intent (invocation_type label') args'; cap = transform_cap (IRQHandlerCap x'); excaps = transform_cap_list excaps'; invocation_type label' \<noteq> GenInvocationLabel IRQAckIRQ; invocation_type label' \<noteq> GenInvocationLabel IRQSetIRQHandler; invocation_type label' = GenInvocationLabel IRQClearIRQHandler\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_irq_handler_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (case ui of IrqHandlerAckIntent \<Rightarrow> doE irq <- liftE $ assert_opt $ cdl_cap_irq cap;
returnOk $ AckIrq irq
odE \<sqinter> throw | IrqHandlerSetEndpointIntent \<Rightarrow> doE endpoint <- throw_on_none $ get_index excaps 0;
endpoint_cap <- returnOk $ fst endpoint;
endpoint_cap_ref <- returnOk $ snd endpoint;
irq <- liftE $ assert_opt $ cdl_cap_irq cap;
case endpoint_cap of cdl_cap.NotificationCap x xa xb \<Rightarrow> returnOk () | _ \<Rightarrow> throw;
returnOk $ SetIrqHandler irq endpoint_cap endpoint_cap_ref
odE \<sqinter> throw | IrqHandlerClearIntent \<Rightarrow> doE irq <- liftE $ assert_opt $ cdl_cap_irq cap;
returnOk $ ClearIrqHandler irq
odE \<sqinter> throw) (if gen_invocation_type label' = IRQAckIRQ then returnOk $ ACKIrq x' else if gen_invocation_type label' = IRQSetIRQHandler then if excaps' \<noteq> [] then let (cap, slot) = hd excaps' in if Structures_A.is_ntfn_cap cap \<and> AllowSend \<in> Structures_A.cap_rights cap then returnOk $ SetIRQHandler x' cap slot else throwError $ InvalidCapability 0 else throwError TruncatedMessage else if gen_invocation_type label' = IRQClearIRQHandler then returnOk $ ClearIRQHandler x' else throwError IllegalOperation)
 2. \<And>slot. \<lbrakk>Some (IrqHandlerIntent ui) = transform_intent (invocation_type label') args'; cap = transform_cap (IRQHandlerCap x'); excaps = transform_cap_list excaps'; invocation_type label' \<noteq> GenInvocationLabel IRQAckIRQ; invocation_type label' \<noteq> GenInvocationLabel IRQSetIRQHandler; invocation_type label' \<noteq> GenInvocationLabel IRQClearIRQHandler\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_irq_handler_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (case ui of IrqHandlerAckIntent \<Rightarrow> doE irq <- liftE $ assert_opt $ cdl_cap_irq cap;
returnOk $ AckIrq irq
odE \<sqinter> throw | IrqHandlerSetEndpointIntent \<Rightarrow> doE endpoint <- throw_on_none $ get_index excaps 0;
endpoint_cap <- returnOk $ fst endpoint;
endpoint_cap_ref <- returnOk $ snd endpoint;
irq <- liftE $ assert_opt $ cdl_cap_irq cap;
case endpoint_cap of cdl_cap.NotificationCap x xa xb \<Rightarrow> returnOk () | _ \<Rightarrow> throw;
returnOk $ SetIrqHandler irq endpoint_cap endpoint_cap_ref
odE \<sqinter> throw | IrqHandlerClearIntent \<Rightarrow> doE irq <- liftE $ assert_opt $ cdl_cap_irq cap;
returnOk $ ClearIrqHandler irq
odE \<sqinter> throw) (if gen_invocation_type label' = IRQAckIRQ then returnOk $ ACKIrq x' else if gen_invocation_type label' = IRQSetIRQHandler then if excaps' \<noteq> [] then let (cap, slot) = hd excaps' in if Structures_A.is_ntfn_cap cap \<and> AllowSend \<in> Structures_A.cap_rights cap then returnOk $ SetIRQHandler x' cap slot else throwError $ InvalidCapability 0 else throwError TruncatedMessage else if gen_invocation_type label' = IRQClearIRQHandler then returnOk $ ClearIRQHandler x' else throwError IllegalOperation) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ui = IrqHandlerClearIntent; cap = IrqHandlerCap x'; excaps = transform_cap_list excaps'; invocation_type label' = GenInvocationLabel IRQClearIRQHandler\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_irq_handler_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (returnOk (ClearIrqHandler x') \<sqinter> throw) (returnOk (ClearIRQHandler x'))
 2. \<And>slot. \<lbrakk>Some (IrqHandlerIntent ui) = transform_intent (invocation_type label') args'; cap = transform_cap (IRQHandlerCap x'); excaps = transform_cap_list excaps'; invocation_type label' \<noteq> GenInvocationLabel IRQAckIRQ; invocation_type label' \<noteq> GenInvocationLabel IRQSetIRQHandler; invocation_type label' \<noteq> GenInvocationLabel IRQClearIRQHandler\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_irq_handler_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (case ui of IrqHandlerAckIntent \<Rightarrow> doE irq <- liftE $ assert_opt $ cdl_cap_irq cap;
returnOk $ AckIrq irq
odE \<sqinter> throw | IrqHandlerSetEndpointIntent \<Rightarrow> doE endpoint <- throw_on_none $ get_index excaps 0;
endpoint_cap <- returnOk $ fst endpoint;
endpoint_cap_ref <- returnOk $ snd endpoint;
irq <- liftE $ assert_opt $ cdl_cap_irq cap;
case endpoint_cap of cdl_cap.NotificationCap x xa xb \<Rightarrow> returnOk () | _ \<Rightarrow> throw;
returnOk $ SetIrqHandler irq endpoint_cap endpoint_cap_ref
odE \<sqinter> throw | IrqHandlerClearIntent \<Rightarrow> doE irq <- liftE $ assert_opt $ cdl_cap_irq cap;
returnOk $ ClearIrqHandler irq
odE \<sqinter> throw) (if gen_invocation_type label' = IRQAckIRQ then returnOk $ ACKIrq x' else if gen_invocation_type label' = IRQSetIRQHandler then if excaps' \<noteq> [] then let (cap, slot) = hd excaps' in if Structures_A.is_ntfn_cap cap \<and> AllowSend \<in> Structures_A.cap_rights cap then returnOk $ SetIRQHandler x' cap slot else throwError $ InvalidCapability 0 else throwError TruncatedMessage else if gen_invocation_type label' = IRQClearIRQHandler then returnOk $ ClearIRQHandler x' else throwError IllegalOperation) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ui = IrqHandlerClearIntent; cap = IrqHandlerCap x'; excaps = transform_cap_list excaps'; invocation_type label' = GenInvocationLabel IRQClearIRQHandler\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_irq_handler_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (returnOk (ClearIrqHandler x')) (returnOk (ClearIRQHandler x'))
 2. \<And>slot. \<lbrakk>Some (IrqHandlerIntent ui) = transform_intent (invocation_type label') args'; cap = transform_cap (IRQHandlerCap x'); excaps = transform_cap_list excaps'; invocation_type label' \<noteq> GenInvocationLabel IRQAckIRQ; invocation_type label' \<noteq> GenInvocationLabel IRQSetIRQHandler; invocation_type label' \<noteq> GenInvocationLabel IRQClearIRQHandler\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_irq_handler_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (case ui of IrqHandlerAckIntent \<Rightarrow> doE irq <- liftE $ assert_opt $ cdl_cap_irq cap;
returnOk $ AckIrq irq
odE \<sqinter> throw | IrqHandlerSetEndpointIntent \<Rightarrow> doE endpoint <- throw_on_none $ get_index excaps 0;
endpoint_cap <- returnOk $ fst endpoint;
endpoint_cap_ref <- returnOk $ snd endpoint;
irq <- liftE $ assert_opt $ cdl_cap_irq cap;
case endpoint_cap of cdl_cap.NotificationCap x xa xb \<Rightarrow> returnOk () | _ \<Rightarrow> throw;
returnOk $ SetIrqHandler irq endpoint_cap endpoint_cap_ref
odE \<sqinter> throw | IrqHandlerClearIntent \<Rightarrow> doE irq <- liftE $ assert_opt $ cdl_cap_irq cap;
returnOk $ ClearIrqHandler irq
odE \<sqinter> throw) (if gen_invocation_type label' = IRQAckIRQ then returnOk $ ACKIrq x' else if gen_invocation_type label' = IRQSetIRQHandler then if excaps' \<noteq> [] then let (cap, slot) = hd excaps' in if Structures_A.is_ntfn_cap cap \<and> AllowSend \<in> Structures_A.cap_rights cap then returnOk $ SetIRQHandler x' cap slot else throwError $ InvalidCapability 0 else throwError TruncatedMessage else if gen_invocation_type label' = IRQClearIRQHandler then returnOk $ ClearIRQHandler x' else throwError IllegalOperation) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ui = IrqHandlerClearIntent; cap = IrqHandlerCap x'; excaps = transform_cap_list excaps'; invocation_type label' = GenInvocationLabel IRQClearIRQHandler\<rbrakk> \<Longrightarrow> cdl_irq_handler_invocation_relation (ClearIrqHandler x') (ClearIRQHandler x')
 2. \<And>slot. \<lbrakk>Some (IrqHandlerIntent ui) = transform_intent (invocation_type label') args'; cap = transform_cap (IRQHandlerCap x'); excaps = transform_cap_list excaps'; invocation_type label' \<noteq> GenInvocationLabel IRQAckIRQ; invocation_type label' \<noteq> GenInvocationLabel IRQSetIRQHandler; invocation_type label' \<noteq> GenInvocationLabel IRQClearIRQHandler\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_irq_handler_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (case ui of IrqHandlerAckIntent \<Rightarrow> doE irq <- liftE $ assert_opt $ cdl_cap_irq cap;
returnOk $ AckIrq irq
odE \<sqinter> throw | IrqHandlerSetEndpointIntent \<Rightarrow> doE endpoint <- throw_on_none $ get_index excaps 0;
endpoint_cap <- returnOk $ fst endpoint;
endpoint_cap_ref <- returnOk $ snd endpoint;
irq <- liftE $ assert_opt $ cdl_cap_irq cap;
case endpoint_cap of cdl_cap.NotificationCap x xa xb \<Rightarrow> returnOk () | _ \<Rightarrow> throw;
returnOk $ SetIrqHandler irq endpoint_cap endpoint_cap_ref
odE \<sqinter> throw | IrqHandlerClearIntent \<Rightarrow> doE irq <- liftE $ assert_opt $ cdl_cap_irq cap;
returnOk $ ClearIrqHandler irq
odE \<sqinter> throw) (if gen_invocation_type label' = IRQAckIRQ then returnOk $ ACKIrq x' else if gen_invocation_type label' = IRQSetIRQHandler then if excaps' \<noteq> [] then let (cap, slot) = hd excaps' in if Structures_A.is_ntfn_cap cap \<and> AllowSend \<in> Structures_A.cap_rights cap then returnOk $ SetIRQHandler x' cap slot else throwError $ InvalidCapability 0 else throwError TruncatedMessage else if gen_invocation_type label' = IRQClearIRQHandler then returnOk $ ClearIRQHandler x' else throwError IllegalOperation) proof (prove)
goal (1 subgoal):
 1. \<And>slot. \<lbrakk>Some (IrqHandlerIntent ui) = transform_intent (invocation_type label') args'; cap = transform_cap (IRQHandlerCap x'); excaps = transform_cap_list excaps'; invocation_type label' \<noteq> GenInvocationLabel IRQAckIRQ; invocation_type label' \<noteq> GenInvocationLabel IRQSetIRQHandler; invocation_type label' \<noteq> GenInvocationLabel IRQClearIRQHandler\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_irq_handler_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (case ui of IrqHandlerAckIntent \<Rightarrow> doE irq <- liftE $ assert_opt $ cdl_cap_irq cap;
returnOk $ AckIrq irq
odE \<sqinter> throw | IrqHandlerSetEndpointIntent \<Rightarrow> doE endpoint <- throw_on_none $ get_index excaps 0;
endpoint_cap <- returnOk $ fst endpoint;
endpoint_cap_ref <- returnOk $ snd endpoint;
irq <- liftE $ assert_opt $ cdl_cap_irq cap;
case endpoint_cap of cdl_cap.NotificationCap x xa xb \<Rightarrow> returnOk () | _ \<Rightarrow> throw;
returnOk $ SetIrqHandler irq endpoint_cap endpoint_cap_ref
odE \<sqinter> throw | IrqHandlerClearIntent \<Rightarrow> doE irq <- liftE $ assert_opt $ cdl_cap_irq cap;
returnOk $ ClearIrqHandler irq
odE \<sqinter> throw) (if gen_invocation_type label' = IRQAckIRQ then returnOk $ ACKIrq x' else if gen_invocation_type label' = IRQSetIRQHandler then if excaps' \<noteq> [] then let (cap, slot) = hd excaps' in if Structures_A.is_ntfn_cap cap \<and> AllowSend \<in> Structures_A.cap_rights cap then returnOk $ SetIRQHandler x' cap slot else throwError $ InvalidCapability 0 else throwError TruncatedMessage else if gen_invocation_type label' = IRQClearIRQHandler then returnOk $ ClearIRQHandler x' else throwError IllegalOperation) proof (prove)
goal:
No subgoals!