theory Syscall_DR

lemma decode_domain_corres:
  "\<lbrakk> Some (DomainIntent i) = transform_intent (invocation_type label') args';
     excaps = transform_cap_list excaps' \<rbrakk> \<Longrightarrow>
   dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). Invocations_A.invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) \<top> \<top>
     (Tcb_D.decode_domain_invocation excaps i)
     (Decode_A.decode_domain_invocation label' args' excaps')" apply (unfold Tcb_D.decode_domain_invocation_def Decode_A.decode_domain_invocation_def) apply (unfold transform_cap_list_def) apply (case_labels "invocation_type label'"; simp add: gen_invocation_type_eq) apply (clarsimp simp: transform_intent_def option_map_def
                                                            split: option.splits)+ defer apply (clarsimp simp: transform_intent_def option_map_def split: option.splits)+ apply (clarsimp simp: transform_intent_domain_def) apply (case_tac "args'") apply simp apply (clarsimp simp: bindE_def lift_def) apply (rule_tac Q'="\<lambda>rv s. case rv of Inr b \<Rightarrow> ucast a = b | _ \<Rightarrow> True" in corres_symb_exec_r) apply (case_tac "rv") apply (simp add: lift_def) apply (rule corres_alternate2, simp) apply (simp add: lift_def) apply (fold bindE_def) apply (rule dcorres_whenE_throwError_abstract') apply (rule corres_alternate2) apply simp apply (case_tac "fst (hd (excaps'))"; simp) apply ((rule corres_alternate2, simp)+)[6] apply (rule corres_alternate1) apply (clarsimp simp: returnOk_def cdl_invocation_relation_def translate_invocation_def split: list.splits) apply (simp add: fst_hd_map_eq) apply (rule corres_alternate2, simp)+ apply (rule validE_cases_valid) apply (wp whenE_inv| simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Some (DomainIntent i) = transform_intent (invocation_type label') args'; excaps = transform_cap_list excaps'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>_. True) (Tcb_D.decode_domain_invocation excaps i) (Decode_A.decode_domain_invocation label' args' excaps') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Some (DomainIntent i) = transform_intent (invocation_type label') args'; excaps = transform_cap_list excaps'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>_. True) (case i of DomainSetIntent d \<Rightarrow> returnOk (SetDomain (cap_object (fst (hd excaps))) d) \<sqinter> throw) (doE whenE (gen_invocation_type label' \<noteq> DomainSetSet) $ throwError IllegalOperation;
domain <- case args' of [] \<Rightarrow> throwError TruncatedMessage | x # xs \<Rightarrow> doE whenE (numDomains \<le> unat x) $ throwError $ InvalidArgument 0;
returnOk (UCAST(32 \<rightarrow> 8) x)
odE;
whenE (length excaps' = 0) $ throwError TruncatedMessage;
case fst (hd excaps') of ThreadCap ptr \<Rightarrow> returnOk $ (ptr, domain) | _ \<Rightarrow> throwError $ InvalidArgument 1
odE) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Some (DomainIntent i) = transform_intent (invocation_type label') args'; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>_. True) (case i of DomainSetIntent d \<Rightarrow> returnOk (SetDomain (cap_object (fst (hd excaps))) d) \<sqinter> throw) (doE whenE (gen_invocation_type label' \<noteq> DomainSetSet) $ throwError IllegalOperation;
domain <- case args' of [] \<Rightarrow> throwError TruncatedMessage | x # xs \<Rightarrow> doE whenE (numDomains \<le> unat x) $ throwError $ InvalidArgument 0;
returnOk (UCAST(32 \<rightarrow> 8) x)
odE;
whenE (length excaps' = 0) $ throwError TruncatedMessage;
case fst (hd excaps') of ThreadCap ptr \<Rightarrow> returnOk $ (ptr, domain) | _ \<Rightarrow> throwError $ InvalidArgument 1
odE) proof (prove)
goal (46 subgoals):
 1. \<And>x2. \<lbrakk>Some (DomainIntent i) = transform_intent (ArchInvocationLabel ARMPDClean_Data) args'; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; invocation_type label' = ArchInvocationLabel ARMPDClean_Data; x2 = ARMPDClean_Data\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>_. True) (case i of DomainSetIntent d \<Rightarrow> returnOk (SetDomain (cap_object (fst (hd excaps))) d) \<sqinter> throw) (doE y <- whenE (gen_invocation_type label' \<noteq> DomainSetSet) (throwError IllegalOperation);
domain <- case args' of [] \<Rightarrow> throwError TruncatedMessage | x # xs \<Rightarrow> doE whenE (numDomains \<le> unat x) $ throwError $ InvalidArgument 0;
returnOk (UCAST(32 \<rightarrow> 8) x)
odE;
y <- whenE (excaps' = []) (throwError TruncatedMessage);
case fst (hd excaps') of ThreadCap ptr \<Rightarrow> returnOk $ (ptr, domain) | _ \<Rightarrow> throwError $ InvalidArgument 1
odE)
 2. \<And>x1. \<lbrakk>Some (DomainIntent i) = transform_intent (GenInvocationLabel InvalidInvocation) args'; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; invocation_type label' = GenInvocationLabel InvalidInvocation; x1 = InvalidInvocation\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>_. True) (case i of DomainSetIntent d \<Rightarrow> returnOk (SetDomain (cap_object (fst (hd excaps))) d) \<sqinter> throw) (doE y <- whenE (gen_invocation_type label' \<noteq> DomainSetSet) (throwError IllegalOperation);
domain <- case args' of [] \<Rightarrow> throwError TruncatedMessage | x # xs \<Rightarrow> doE whenE (numDomains \<le> unat x) $ throwError $ InvalidArgument 0;
returnOk (UCAST(32 \<rightarrow> 8) x)
odE;
y <- whenE (excaps' = []) (throwError TruncatedMessage);
case fst (hd excaps') of ThreadCap ptr \<Rightarrow> returnOk $ (ptr, domain) | _ \<Rightarrow> throwError $ InvalidArgument 1
odE)
 3. \<And>x1. \<lbrakk>Some (DomainIntent i) = transform_intent (GenInvocationLabel UntypedRetype) args'; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; gen_invocation_type label' = UntypedRetype; x1 = UntypedRetype\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>_. True) (case i of DomainSetIntent d \<Rightarrow> returnOk (SetDomain (cap_object (fst (hd excaps))) d) \<sqinter> throw) (throwError IllegalOperation)
 4. \<And>x1. \<lbrakk>Some (DomainIntent i) = transform_intent (GenInvocationLabel TCBReadRegisters) args'; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; gen_invocation_type label' = TCBReadRegisters; x1 = TCBReadRegisters\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>_. True) (case i of DomainSetIntent d \<Rightarrow> returnOk (SetDomain (cap_object (fst (hd excaps))) d) \<sqinter> throw) (throwError IllegalOperation)
 5. \<And>x1. \<lbrakk>Some (DomainIntent i) = transform_intent (GenInvocationLabel TCBWriteRegisters) args'; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; gen_invocation_type label' = TCBWriteRegisters; x1 = TCBWriteRegisters\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>_. True) (case i of DomainSetIntent d \<Rightarrow> returnOk (SetDomain (cap_object (fst (hd excaps))) d) \<sqinter> throw) (throwError IllegalOperation)
 6. \<And>x1. \<lbrakk>Some (DomainIntent i) = transform_intent (GenInvocationLabel TCBCopyRegisters) args'; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; gen_invocation_type label' = TCBCopyRegisters; x1 = TCBCopyRegisters\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>_. True) (case i of DomainSetIntent d \<Rightarrow> returnOk (SetDomain (cap_object (fst (hd excaps))) d) \<sqinter> throw) (throwError IllegalOperation)
 7. \<And>x1. \<lbrakk>Some (DomainIntent i) = transform_intent (GenInvocationLabel TCBConfigure) args'; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; gen_invocation_type label' = TCBConfigure; x1 = TCBConfigure\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>_. True) (case i of DomainSetIntent d \<Rightarrow> returnOk (SetDomain (cap_object (fst (hd excaps))) d) \<sqinter> throw) (throwError IllegalOperation)
 8. \<And>x1. \<lbrakk>Some (DomainIntent i) = transform_intent (GenInvocationLabel TCBSetPriority) args'; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; gen_invocation_type label' = TCBSetPriority; x1 = TCBSetPriority\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>_. True) (case i of DomainSetIntent d \<Rightarrow> returnOk (SetDomain (cap_object (fst (hd excaps))) d) \<sqinter> throw) (throwError IllegalOperation)
 9. \<And>x1. \<lbrakk>Some (DomainIntent i) = transform_intent (GenInvocationLabel TCBSetMCPriority) args'; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; gen_invocation_type label' = TCBSetMCPriority; x1 = TCBSetMCPriority\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>_. True) (case i of DomainSetIntent d \<Rightarrow> returnOk (SetDomain (cap_object (fst (hd excaps))) d) \<sqinter> throw) (throwError IllegalOperation)
 10. \<And>x1. \<lbrakk>Some (DomainIntent i) = transform_intent (GenInvocationLabel TCBSetSchedParams) args'; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; gen_invocation_type label' = TCBSetSchedParams; x1 = TCBSetSchedParams\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>_. True) (case i of DomainSetIntent d \<Rightarrow> returnOk (SetDomain (cap_object (fst (hd excaps))) d) \<sqinter> throw) (throwError IllegalOperation)
A total of 46 subgoals... proof (prove)
goal (16 subgoals):
 1. \<lbrakk>gen_invocation_type label' = DomainSetSet; transform_intent_domain args' = Some i; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>_. True) (case i of DomainSetIntent d \<Rightarrow> returnOk (SetDomain (cap_object (fst (hd (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps')))) d) \<sqinter> throw) (doE domain <- case args' of [] \<Rightarrow> throwError TruncatedMessage | x # xs \<Rightarrow> doE whenE (numDomains \<le> unat x) $ throwError $ InvalidArgument 0;
returnOk (UCAST(32 \<rightarrow> 8) x)
odE;
y <- whenE (excaps' = []) (throwError TruncatedMessage);
case fst (hd excaps') of ThreadCap ptr \<Rightarrow> returnOk $ (ptr, domain) | _ \<Rightarrow> throwError $ InvalidArgument 1
odE)
 2. \<And>x2. \<lbrakk>Some (DomainIntent i) = transform_intent (ArchInvocationLabel ARMPDInvalidate_Data) args'; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; invocation_type label' = ArchInvocationLabel ARMPDInvalidate_Data; x2 = ARMPDInvalidate_Data\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>_. True) (case i of DomainSetIntent d \<Rightarrow> returnOk (SetDomain (cap_object (fst (hd excaps))) d) \<sqinter> throw) (doE y <- whenE (gen_invocation_type label' \<noteq> DomainSetSet) (throwError IllegalOperation);
domain <- case args' of [] \<Rightarrow> throwError TruncatedMessage | x # xs \<Rightarrow> doE whenE (numDomains \<le> unat x) $ throwError $ InvalidArgument 0;
returnOk (UCAST(32 \<rightarrow> 8) x)
odE;
y <- whenE (excaps' = []) (throwError TruncatedMessage);
case fst (hd excaps') of ThreadCap ptr \<Rightarrow> returnOk $ (ptr, domain) | _ \<Rightarrow> throwError $ InvalidArgument 1
odE)
 3. \<And>x2. \<lbrakk>Some (DomainIntent i) = transform_intent (ArchInvocationLabel ARMPDCleanInvalidate_Data) args'; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; invocation_type label' = ArchInvocationLabel ARMPDCleanInvalidate_Data; x2 = ARMPDCleanInvalidate_Data\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>_. True) (case i of DomainSetIntent d \<Rightarrow> returnOk (SetDomain (cap_object (fst (hd excaps))) d) \<sqinter> throw) (doE y <- whenE (gen_invocation_type label' \<noteq> DomainSetSet) (throwError IllegalOperation);
domain <- case args' of [] \<Rightarrow> throwError TruncatedMessage | x # xs \<Rightarrow> doE whenE (numDomains \<le> unat x) $ throwError $ InvalidArgument 0;
returnOk (UCAST(32 \<rightarrow> 8) x)
odE;
y <- whenE (excaps' = []) (throwError TruncatedMessage);
case fst (hd excaps') of ThreadCap ptr \<Rightarrow> returnOk $ (ptr, domain) | _ \<Rightarrow> throwError $ InvalidArgument 1
odE)
 4. \<And>x2. \<lbrakk>Some (DomainIntent i) = transform_intent (ArchInvocationLabel ARMPDUnify_Instruction) args'; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; invocation_type label' = ArchInvocationLabel ARMPDUnify_Instruction; x2 = ARMPDUnify_Instruction\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>_. True) (case i of DomainSetIntent d \<Rightarrow> returnOk (SetDomain (cap_object (fst (hd excaps))) d) \<sqinter> throw) (doE y <- whenE (gen_invocation_type label' \<noteq> DomainSetSet) (throwError IllegalOperation);
domain <- case args' of [] \<Rightarrow> throwError TruncatedMessage | x # xs \<Rightarrow> doE whenE (numDomains \<le> unat x) $ throwError $ InvalidArgument 0;
returnOk (UCAST(32 \<rightarrow> 8) x)
odE;
y <- whenE (excaps' = []) (throwError TruncatedMessage);
case fst (hd excaps') of ThreadCap ptr \<Rightarrow> returnOk $ (ptr, domain) | _ \<Rightarrow> throwError $ InvalidArgument 1
odE)
 5. \<And>x2. \<lbrakk>Some (DomainIntent i) = transform_intent (ArchInvocationLabel ARMPageTableMap) args'; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; invocation_type label' = ArchInvocationLabel ARMPageTableMap; x2 = ARMPageTableMap\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>_. True) (case i of DomainSetIntent d \<Rightarrow> returnOk (SetDomain (cap_object (fst (hd excaps))) d) \<sqinter> throw) (doE y <- whenE (gen_invocation_type label' \<noteq> DomainSetSet) (throwError IllegalOperation);
domain <- case args' of [] \<Rightarrow> throwError TruncatedMessage | x # xs \<Rightarrow> doE whenE (numDomains \<le> unat x) $ throwError $ InvalidArgument 0;
returnOk (UCAST(32 \<rightarrow> 8) x)
odE;
y <- whenE (excaps' = []) (throwError TruncatedMessage);
case fst (hd excaps') of ThreadCap ptr \<Rightarrow> returnOk $ (ptr, domain) | _ \<Rightarrow> throwError $ InvalidArgument 1
odE)
 6. \<And>x2. \<lbrakk>Some (DomainIntent i) = transform_intent (ArchInvocationLabel ARMPageTableUnmap) args'; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; invocation_type label' = ArchInvocationLabel ARMPageTableUnmap; x2 = ARMPageTableUnmap\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>_. True) (case i of DomainSetIntent d \<Rightarrow> returnOk (SetDomain (cap_object (fst (hd excaps))) d) \<sqinter> throw) (doE y <- whenE (gen_invocation_type label' \<noteq> DomainSetSet) (throwError IllegalOperation);
domain <- case args' of [] \<Rightarrow> throwError TruncatedMessage | x # xs \<Rightarrow> doE whenE (numDomains \<le> unat x) $ throwError $ InvalidArgument 0;
returnOk (UCAST(32 \<rightarrow> 8) x)
odE;
y <- whenE (excaps' = []) (throwError TruncatedMessage);
case fst (hd excaps') of ThreadCap ptr \<Rightarrow> returnOk $ (ptr, domain) | _ \<Rightarrow> throwError $ InvalidArgument 1
odE)
 7. \<And>x2. \<lbrakk>Some (DomainIntent i) = transform_intent (ArchInvocationLabel ARMPageMap) args'; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; invocation_type label' = ArchInvocationLabel ARMPageMap; x2 = ARMPageMap\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>_. True) (case i of DomainSetIntent d \<Rightarrow> returnOk (SetDomain (cap_object (fst (hd excaps))) d) \<sqinter> throw) (doE y <- whenE (gen_invocation_type label' \<noteq> DomainSetSet) (throwError IllegalOperation);
domain <- case args' of [] \<Rightarrow> throwError TruncatedMessage | x # xs \<Rightarrow> doE whenE (numDomains \<le> unat x) $ throwError $ InvalidArgument 0;
returnOk (UCAST(32 \<rightarrow> 8) x)
odE;
y <- whenE (excaps' = []) (throwError TruncatedMessage);
case fst (hd excaps') of ThreadCap ptr \<Rightarrow> returnOk $ (ptr, domain) | _ \<Rightarrow> throwError $ InvalidArgument 1
odE)
 8. \<And>x2. \<lbrakk>Some (DomainIntent i) = transform_intent (ArchInvocationLabel ARMPageUnmap) args'; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; invocation_type label' = ArchInvocationLabel ARMPageUnmap; x2 = ARMPageUnmap\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>_. True) (case i of DomainSetIntent d \<Rightarrow> returnOk (SetDomain (cap_object (fst (hd excaps))) d) \<sqinter> throw) (doE y <- whenE (gen_invocation_type label' \<noteq> DomainSetSet) (throwError IllegalOperation);
domain <- case args' of [] \<Rightarrow> throwError TruncatedMessage | x # xs \<Rightarrow> doE whenE (numDomains \<le> unat x) $ throwError $ InvalidArgument 0;
returnOk (UCAST(32 \<rightarrow> 8) x)
odE;
y <- whenE (excaps' = []) (throwError TruncatedMessage);
case fst (hd excaps') of ThreadCap ptr \<Rightarrow> returnOk $ (ptr, domain) | _ \<Rightarrow> throwError $ InvalidArgument 1
odE)
 9. \<And>x2. \<lbrakk>Some (DomainIntent i) = transform_intent (ArchInvocationLabel ARMPageClean_Data) args'; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; invocation_type label' = ArchInvocationLabel ARMPageClean_Data; x2 = ARMPageClean_Data\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>_. True) (case i of DomainSetIntent d \<Rightarrow> returnOk (SetDomain (cap_object (fst (hd excaps))) d) \<sqinter> throw) (doE y <- whenE (gen_invocation_type label' \<noteq> DomainSetSet) (throwError IllegalOperation);
domain <- case args' of [] \<Rightarrow> throwError TruncatedMessage | x # xs \<Rightarrow> doE whenE (numDomains \<le> unat x) $ throwError $ InvalidArgument 0;
returnOk (UCAST(32 \<rightarrow> 8) x)
odE;
y <- whenE (excaps' = []) (throwError TruncatedMessage);
case fst (hd excaps') of ThreadCap ptr \<Rightarrow> returnOk $ (ptr, domain) | _ \<Rightarrow> throwError $ InvalidArgument 1
odE)
 10. \<And>x2. \<lbrakk>Some (DomainIntent i) = transform_intent (ArchInvocationLabel ARMPageInvalidate_Data) args'; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; invocation_type label' = ArchInvocationLabel ARMPageInvalidate_Data; x2 = ARMPageInvalidate_Data\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>_. True) (case i of DomainSetIntent d \<Rightarrow> returnOk (SetDomain (cap_object (fst (hd excaps))) d) \<sqinter> throw) (doE y <- whenE (gen_invocation_type label' \<noteq> DomainSetSet) (throwError IllegalOperation);
domain <- case args' of [] \<Rightarrow> throwError TruncatedMessage | x # xs \<Rightarrow> doE whenE (numDomains \<le> unat x) $ throwError $ InvalidArgument 0;
returnOk (UCAST(32 \<rightarrow> 8) x)
odE;
y <- whenE (excaps' = []) (throwError TruncatedMessage);
case fst (hd excaps') of ThreadCap ptr \<Rightarrow> returnOk $ (ptr, domain) | _ \<Rightarrow> throwError $ InvalidArgument 1
odE)
A total of 16 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>x2. \<lbrakk>Some (DomainIntent i) = transform_intent (ArchInvocationLabel ARMPDInvalidate_Data) args'; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; invocation_type label' = ArchInvocationLabel ARMPDInvalidate_Data; x2 = ARMPDInvalidate_Data\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>_. True) (case i of DomainSetIntent d \<Rightarrow> returnOk (SetDomain (cap_object (fst (hd excaps))) d) \<sqinter> throw) (doE y <- whenE (gen_invocation_type label' \<noteq> DomainSetSet) (throwError IllegalOperation);
domain <- case args' of [] \<Rightarrow> throwError TruncatedMessage | x # xs \<Rightarrow> doE whenE (numDomains \<le> unat x) $ throwError $ InvalidArgument 0;
returnOk (UCAST(32 \<rightarrow> 8) x)
odE;
y <- whenE (excaps' = []) (throwError TruncatedMessage);
case fst (hd excaps') of ThreadCap ptr \<Rightarrow> returnOk $ (ptr, domain) | _ \<Rightarrow> throwError $ InvalidArgument 1
odE)
 2. \<And>x2. \<lbrakk>Some (DomainIntent i) = transform_intent (ArchInvocationLabel ARMPDCleanInvalidate_Data) args'; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; invocation_type label' = ArchInvocationLabel ARMPDCleanInvalidate_Data; x2 = ARMPDCleanInvalidate_Data\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>_. True) (case i of DomainSetIntent d \<Rightarrow> returnOk (SetDomain (cap_object (fst (hd excaps))) d) \<sqinter> throw) (doE y <- whenE (gen_invocation_type label' \<noteq> DomainSetSet) (throwError IllegalOperation);
domain <- case args' of [] \<Rightarrow> throwError TruncatedMessage | x # xs \<Rightarrow> doE whenE (numDomains \<le> unat x) $ throwError $ InvalidArgument 0;
returnOk (UCAST(32 \<rightarrow> 8) x)
odE;
y <- whenE (excaps' = []) (throwError TruncatedMessage);
case fst (hd excaps') of ThreadCap ptr \<Rightarrow> returnOk $ (ptr, domain) | _ \<Rightarrow> throwError $ InvalidArgument 1
odE)
 3. \<And>x2. \<lbrakk>Some (DomainIntent i) = transform_intent (ArchInvocationLabel ARMPDUnify_Instruction) args'; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; invocation_type label' = ArchInvocationLabel ARMPDUnify_Instruction; x2 = ARMPDUnify_Instruction\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>_. True) (case i of DomainSetIntent d \<Rightarrow> returnOk (SetDomain (cap_object (fst (hd excaps))) d) \<sqinter> throw) (doE y <- whenE (gen_invocation_type label' \<noteq> DomainSetSet) (throwError IllegalOperation);
domain <- case args' of [] \<Rightarrow> throwError TruncatedMessage | x # xs \<Rightarrow> doE whenE (numDomains \<le> unat x) $ throwError $ InvalidArgument 0;
returnOk (UCAST(32 \<rightarrow> 8) x)
odE;
y <- whenE (excaps' = []) (throwError TruncatedMessage);
case fst (hd excaps') of ThreadCap ptr \<Rightarrow> returnOk $ (ptr, domain) | _ \<Rightarrow> throwError $ InvalidArgument 1
odE)
 4. \<And>x2. \<lbrakk>Some (DomainIntent i) = transform_intent (ArchInvocationLabel ARMPageTableMap) args'; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; invocation_type label' = ArchInvocationLabel ARMPageTableMap; x2 = ARMPageTableMap\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>_. True) (case i of DomainSetIntent d \<Rightarrow> returnOk (SetDomain (cap_object (fst (hd excaps))) d) \<sqinter> throw) (doE y <- whenE (gen_invocation_type label' \<noteq> DomainSetSet) (throwError IllegalOperation);
domain <- case args' of [] \<Rightarrow> throwError TruncatedMessage | x # xs \<Rightarrow> doE whenE (numDomains \<le> unat x) $ throwError $ InvalidArgument 0;
returnOk (UCAST(32 \<rightarrow> 8) x)
odE;
y <- whenE (excaps' = []) (throwError TruncatedMessage);
case fst (hd excaps') of ThreadCap ptr \<Rightarrow> returnOk $ (ptr, domain) | _ \<Rightarrow> throwError $ InvalidArgument 1
odE)
 5. \<And>x2. \<lbrakk>Some (DomainIntent i) = transform_intent (ArchInvocationLabel ARMPageTableUnmap) args'; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; invocation_type label' = ArchInvocationLabel ARMPageTableUnmap; x2 = ARMPageTableUnmap\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>_. True) (case i of DomainSetIntent d \<Rightarrow> returnOk (SetDomain (cap_object (fst (hd excaps))) d) \<sqinter> throw) (doE y <- whenE (gen_invocation_type label' \<noteq> DomainSetSet) (throwError IllegalOperation);
domain <- case args' of [] \<Rightarrow> throwError TruncatedMessage | x # xs \<Rightarrow> doE whenE (numDomains \<le> unat x) $ throwError $ InvalidArgument 0;
returnOk (UCAST(32 \<rightarrow> 8) x)
odE;
y <- whenE (excaps' = []) (throwError TruncatedMessage);
case fst (hd excaps') of ThreadCap ptr \<Rightarrow> returnOk $ (ptr, domain) | _ \<Rightarrow> throwError $ InvalidArgument 1
odE)
 6. \<And>x2. \<lbrakk>Some (DomainIntent i) = transform_intent (ArchInvocationLabel ARMPageMap) args'; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; invocation_type label' = ArchInvocationLabel ARMPageMap; x2 = ARMPageMap\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>_. True) (case i of DomainSetIntent d \<Rightarrow> returnOk (SetDomain (cap_object (fst (hd excaps))) d) \<sqinter> throw) (doE y <- whenE (gen_invocation_type label' \<noteq> DomainSetSet) (throwError IllegalOperation);
domain <- case args' of [] \<Rightarrow> throwError TruncatedMessage | x # xs \<Rightarrow> doE whenE (numDomains \<le> unat x) $ throwError $ InvalidArgument 0;
returnOk (UCAST(32 \<rightarrow> 8) x)
odE;
y <- whenE (excaps' = []) (throwError TruncatedMessage);
case fst (hd excaps') of ThreadCap ptr \<Rightarrow> returnOk $ (ptr, domain) | _ \<Rightarrow> throwError $ InvalidArgument 1
odE)
 7. \<And>x2. \<lbrakk>Some (DomainIntent i) = transform_intent (ArchInvocationLabel ARMPageUnmap) args'; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; invocation_type label' = ArchInvocationLabel ARMPageUnmap; x2 = ARMPageUnmap\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>_. True) (case i of DomainSetIntent d \<Rightarrow> returnOk (SetDomain (cap_object (fst (hd excaps))) d) \<sqinter> throw) (doE y <- whenE (gen_invocation_type label' \<noteq> DomainSetSet) (throwError IllegalOperation);
domain <- case args' of [] \<Rightarrow> throwError TruncatedMessage | x # xs \<Rightarrow> doE whenE (numDomains \<le> unat x) $ throwError $ InvalidArgument 0;
returnOk (UCAST(32 \<rightarrow> 8) x)
odE;
y <- whenE (excaps' = []) (throwError TruncatedMessage);
case fst (hd excaps') of ThreadCap ptr \<Rightarrow> returnOk $ (ptr, domain) | _ \<Rightarrow> throwError $ InvalidArgument 1
odE)
 8. \<And>x2. \<lbrakk>Some (DomainIntent i) = transform_intent (ArchInvocationLabel ARMPageClean_Data) args'; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; invocation_type label' = ArchInvocationLabel ARMPageClean_Data; x2 = ARMPageClean_Data\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>_. True) (case i of DomainSetIntent d \<Rightarrow> returnOk (SetDomain (cap_object (fst (hd excaps))) d) \<sqinter> throw) (doE y <- whenE (gen_invocation_type label' \<noteq> DomainSetSet) (throwError IllegalOperation);
domain <- case args' of [] \<Rightarrow> throwError TruncatedMessage | x # xs \<Rightarrow> doE whenE (numDomains \<le> unat x) $ throwError $ InvalidArgument 0;
returnOk (UCAST(32 \<rightarrow> 8) x)
odE;
y <- whenE (excaps' = []) (throwError TruncatedMessage);
case fst (hd excaps') of ThreadCap ptr \<Rightarrow> returnOk $ (ptr, domain) | _ \<Rightarrow> throwError $ InvalidArgument 1
odE)
 9. \<And>x2. \<lbrakk>Some (DomainIntent i) = transform_intent (ArchInvocationLabel ARMPageInvalidate_Data) args'; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; invocation_type label' = ArchInvocationLabel ARMPageInvalidate_Data; x2 = ARMPageInvalidate_Data\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>_. True) (case i of DomainSetIntent d \<Rightarrow> returnOk (SetDomain (cap_object (fst (hd excaps))) d) \<sqinter> throw) (doE y <- whenE (gen_invocation_type label' \<noteq> DomainSetSet) (throwError IllegalOperation);
domain <- case args' of [] \<Rightarrow> throwError TruncatedMessage | x # xs \<Rightarrow> doE whenE (numDomains \<le> unat x) $ throwError $ InvalidArgument 0;
returnOk (UCAST(32 \<rightarrow> 8) x)
odE;
y <- whenE (excaps' = []) (throwError TruncatedMessage);
case fst (hd excaps') of ThreadCap ptr \<Rightarrow> returnOk $ (ptr, domain) | _ \<Rightarrow> throwError $ InvalidArgument 1
odE)
 10. \<And>x2. \<lbrakk>Some (DomainIntent i) = transform_intent (ArchInvocationLabel ARMPageCleanInvalidate_Data) args'; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; invocation_type label' = ArchInvocationLabel ARMPageCleanInvalidate_Data; x2 = ARMPageCleanInvalidate_Data\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>_. True) (case i of DomainSetIntent d \<Rightarrow> returnOk (SetDomain (cap_object (fst (hd excaps))) d) \<sqinter> throw) (doE y <- whenE (gen_invocation_type label' \<noteq> DomainSetSet) (throwError IllegalOperation);
domain <- case args' of [] \<Rightarrow> throwError TruncatedMessage | x # xs \<Rightarrow> doE whenE (numDomains \<le> unat x) $ throwError $ InvalidArgument 0;
returnOk (UCAST(32 \<rightarrow> 8) x)
odE;
y <- whenE (excaps' = []) (throwError TruncatedMessage);
case fst (hd excaps') of ThreadCap ptr \<Rightarrow> returnOk $ (ptr, domain) | _ \<Rightarrow> throwError $ InvalidArgument 1
odE)
A total of 16 subgoals... proof (prove)
goal (1 subgoal):
 1. \<lbrakk>gen_invocation_type label' = DomainSetSet; transform_intent_domain args' = Some i; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>_. True) (case i of DomainSetIntent d \<Rightarrow> returnOk (SetDomain (cap_object (fst (hd (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps')))) d) \<sqinter> throw) (doE domain <- case args' of [] \<Rightarrow> throwError TruncatedMessage | x # xs \<Rightarrow> doE whenE (numDomains \<le> unat x) $ throwError $ InvalidArgument 0;
returnOk (UCAST(32 \<rightarrow> 8) x)
odE;
y <- whenE (excaps' = []) (throwError TruncatedMessage);
case fst (hd excaps') of ThreadCap ptr \<Rightarrow> returnOk $ (ptr, domain) | _ \<Rightarrow> throwError $ InvalidArgument 1
odE) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>gen_invocation_type label' = DomainSetSet; (case args' of [] \<Rightarrow> Nothing | d # x \<Rightarrow> Some (DomainSetIntent (UCAST(32 \<rightarrow> 8) d))) = Some i; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>_. True) (case i of DomainSetIntent d \<Rightarrow> returnOk (SetDomain (cap_object (fst (hd (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps')))) d) \<sqinter> throw) (doE domain <- case args' of [] \<Rightarrow> throwError TruncatedMessage | x # xs \<Rightarrow> doE whenE (numDomains \<le> unat x) $ throwError $ InvalidArgument 0;
returnOk (UCAST(32 \<rightarrow> 8) x)
odE;
y <- whenE (excaps' = []) (throwError TruncatedMessage);
case fst (hd excaps') of ThreadCap ptr \<Rightarrow> returnOk $ (ptr, domain) | _ \<Rightarrow> throwError $ InvalidArgument 1
odE) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>gen_invocation_type label' = DomainSetSet; (case args' of [] \<Rightarrow> Nothing | d # x \<Rightarrow> Some (DomainSetIntent (UCAST(32 \<rightarrow> 8) d))) = Some i; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = []\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>_. True) (case i of DomainSetIntent d \<Rightarrow> returnOk (SetDomain (cap_object (fst (hd (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps')))) d) \<sqinter> throw) (doE domain <- case args' of [] \<Rightarrow> throwError TruncatedMessage | x # xs \<Rightarrow> doE whenE (numDomains \<le> unat x) $ throwError $ InvalidArgument 0;
returnOk (UCAST(32 \<rightarrow> 8) x)
odE;
y <- whenE (excaps' = []) (throwError TruncatedMessage);
case fst (hd excaps') of ThreadCap ptr \<Rightarrow> returnOk $ (ptr, domain) | _ \<Rightarrow> throwError $ InvalidArgument 1
odE)
 2. \<And>a list. \<lbrakk>gen_invocation_type label' = DomainSetSet; (case args' of [] \<Rightarrow> Nothing | d # x \<Rightarrow> Some (DomainSetIntent (UCAST(32 \<rightarrow> 8) d))) = Some i; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>_. True) (case i of DomainSetIntent d \<Rightarrow> returnOk (SetDomain (cap_object (fst (hd (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps')))) d) \<sqinter> throw) (doE domain <- case args' of [] \<Rightarrow> throwError TruncatedMessage | x # xs \<Rightarrow> doE whenE (numDomains \<le> unat x) $ throwError $ InvalidArgument 0;
returnOk (UCAST(32 \<rightarrow> 8) x)
odE;
y <- whenE (excaps' = []) (throwError TruncatedMessage);
case fst (hd excaps') of ThreadCap ptr \<Rightarrow> returnOk $ (ptr, domain) | _ \<Rightarrow> throwError $ InvalidArgument 1
odE) proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>gen_invocation_type label' = DomainSetSet; (case args' of [] \<Rightarrow> Nothing | d # x \<Rightarrow> Some (DomainSetIntent (UCAST(32 \<rightarrow> 8) d))) = Some i; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>_. True) (case i of DomainSetIntent d \<Rightarrow> returnOk (SetDomain (cap_object (fst (hd (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps')))) d) \<sqinter> throw) (doE domain <- case args' of [] \<Rightarrow> throwError TruncatedMessage | x # xs \<Rightarrow> doE whenE (numDomains \<le> unat x) $ throwError $ InvalidArgument 0;
returnOk (UCAST(32 \<rightarrow> 8) x)
odE;
y <- whenE (excaps' = []) (throwError TruncatedMessage);
case fst (hd excaps') of ThreadCap ptr \<Rightarrow> returnOk $ (ptr, domain) | _ \<Rightarrow> throwError $ InvalidArgument 1
odE) proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a)\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>_. True) (returnOk (SetDomain (cap_object (fst (hd (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps')))) (UCAST(32 \<rightarrow> 8) a)) \<sqinter> throw) (whenE (numDomains \<le> unat a) (throwError (InvalidArgument 0)) >>= lift (\<lambda>y. returnOk (UCAST(32 \<rightarrow> 8) a)) >>= lift (\<lambda>domain. whenE (excaps' = []) (throwError TruncatedMessage) >>= lift (\<lambda>y. case fst (hd excaps') of ThreadCap ptr \<Rightarrow> returnOk $ (ptr, domain) | _ \<Rightarrow> throwError $ InvalidArgument 1))) proof (prove)
goal (4 subgoals):
 1. \<And>a list rv. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a)\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>s. case rv of Inl aa \<Rightarrow> True | Inr b \<Rightarrow> UCAST(32 \<rightarrow> 8) a = b) (returnOk (SetDomain (cap_object (fst (hd (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps')))) (UCAST(32 \<rightarrow> 8) a)) \<sqinter> throw) (lift (\<lambda>domain. whenE (excaps' = []) (throwError TruncatedMessage) >>= lift (\<lambda>y. case fst (hd excaps') of ThreadCap ptr \<Rightarrow> returnOk $ (ptr, domain) | _ \<Rightarrow> throwError $ InvalidArgument 1)) rv)
 2. \<And>a list. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> whenE (numDomains \<le> unat a) (throwError (InvalidArgument 0)) >>= lift (\<lambda>y. returnOk (UCAST(32 \<rightarrow> 8) a)) \<lbrace>\<lambda>rv s. case rv of Inl aa \<Rightarrow> True | Inr b \<Rightarrow> UCAST(32 \<rightarrow> 8) a = b\<rbrace>
 3. \<And>a list s. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); True\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> whenE (numDomains \<le> unat a) (throwError (InvalidArgument 0)) >>= lift (\<lambda>y. returnOk (UCAST(32 \<rightarrow> 8) a)) \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>a list. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); False\<rbrakk> \<Longrightarrow> no_fail (\<lambda>_. True) (whenE (numDomains \<le> unat a) (throwError (InvalidArgument 0)) >>= lift (\<lambda>y. returnOk (UCAST(32 \<rightarrow> 8) a))) proof (prove)
goal (5 subgoals):
 1. \<And>a list rv aa. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); rv = Inl aa\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>s. case rv of Inl aa \<Rightarrow> True | Inr b \<Rightarrow> UCAST(32 \<rightarrow> 8) a = b) (returnOk (SetDomain (cap_object (fst (hd (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps')))) (UCAST(32 \<rightarrow> 8) a)) \<sqinter> throw) (lift (\<lambda>domain. whenE (excaps' = []) (throwError TruncatedMessage) >>= lift (\<lambda>y. case fst (hd excaps') of ThreadCap ptr \<Rightarrow> returnOk $ (ptr, domain) | _ \<Rightarrow> throwError $ InvalidArgument 1)) rv)
 2. \<And>a list rv b. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); rv = Inr b\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>s. case rv of Inl aa \<Rightarrow> True | Inr b \<Rightarrow> UCAST(32 \<rightarrow> 8) a = b) (returnOk (SetDomain (cap_object (fst (hd (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps')))) (UCAST(32 \<rightarrow> 8) a)) \<sqinter> throw) (lift (\<lambda>domain. whenE (excaps' = []) (throwError TruncatedMessage) >>= lift (\<lambda>y. case fst (hd excaps') of ThreadCap ptr \<Rightarrow> returnOk $ (ptr, domain) | _ \<Rightarrow> throwError $ InvalidArgument 1)) rv)
 3. \<And>a list. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> whenE (numDomains \<le> unat a) (throwError (InvalidArgument 0)) >>= lift (\<lambda>y. returnOk (UCAST(32 \<rightarrow> 8) a)) \<lbrace>\<lambda>rv s. case rv of Inl aa \<Rightarrow> True | Inr b \<Rightarrow> UCAST(32 \<rightarrow> 8) a = b\<rbrace>
 4. \<And>a list s. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); True\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> whenE (numDomains \<le> unat a) (throwError (InvalidArgument 0)) >>= lift (\<lambda>y. returnOk (UCAST(32 \<rightarrow> 8) a)) \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<And>a list. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); False\<rbrakk> \<Longrightarrow> no_fail (\<lambda>_. True) (whenE (numDomains \<le> unat a) (throwError (InvalidArgument 0)) >>= lift (\<lambda>y. returnOk (UCAST(32 \<rightarrow> 8) a))) proof (prove)
goal (5 subgoals):
 1. \<And>a list rv aa. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); rv = Inl aa\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>s. True) (returnOk (SetDomain (cap_object (fst (hd (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps')))) (UCAST(32 \<rightarrow> 8) a)) \<sqinter> throw) (throwError aa)
 2. \<And>a list rv b. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); rv = Inr b\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>s. case rv of Inl aa \<Rightarrow> True | Inr b \<Rightarrow> UCAST(32 \<rightarrow> 8) a = b) (returnOk (SetDomain (cap_object (fst (hd (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps')))) (UCAST(32 \<rightarrow> 8) a)) \<sqinter> throw) (lift (\<lambda>domain. whenE (excaps' = []) (throwError TruncatedMessage) >>= lift (\<lambda>y. case fst (hd excaps') of ThreadCap ptr \<Rightarrow> returnOk $ (ptr, domain) | _ \<Rightarrow> throwError $ InvalidArgument 1)) rv)
 3. \<And>a list. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> whenE (numDomains \<le> unat a) (throwError (InvalidArgument 0)) >>= lift (\<lambda>y. returnOk (UCAST(32 \<rightarrow> 8) a)) \<lbrace>\<lambda>rv s. case rv of Inl aa \<Rightarrow> True | Inr b \<Rightarrow> UCAST(32 \<rightarrow> 8) a = b\<rbrace>
 4. \<And>a list s. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); True\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> whenE (numDomains \<le> unat a) (throwError (InvalidArgument 0)) >>= lift (\<lambda>y. returnOk (UCAST(32 \<rightarrow> 8) a)) \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<And>a list. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); False\<rbrakk> \<Longrightarrow> no_fail (\<lambda>_. True) (whenE (numDomains \<le> unat a) (throwError (InvalidArgument 0)) >>= lift (\<lambda>y. returnOk (UCAST(32 \<rightarrow> 8) a))) proof (prove)
goal (4 subgoals):
 1. \<And>a list rv b. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); rv = Inr b\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>s. case rv of Inl aa \<Rightarrow> True | Inr b \<Rightarrow> UCAST(32 \<rightarrow> 8) a = b) (returnOk (SetDomain (cap_object (fst (hd (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps')))) (UCAST(32 \<rightarrow> 8) a)) \<sqinter> throw) (lift (\<lambda>domain. whenE (excaps' = []) (throwError TruncatedMessage) >>= lift (\<lambda>y. case fst (hd excaps') of ThreadCap ptr \<Rightarrow> returnOk $ (ptr, domain) | _ \<Rightarrow> throwError $ InvalidArgument 1)) rv)
 2. \<And>a list. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> whenE (numDomains \<le> unat a) (throwError (InvalidArgument 0)) >>= lift (\<lambda>y. returnOk (UCAST(32 \<rightarrow> 8) a)) \<lbrace>\<lambda>rv s. case rv of Inl aa \<Rightarrow> True | Inr b \<Rightarrow> UCAST(32 \<rightarrow> 8) a = b\<rbrace>
 3. \<And>a list s. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); True\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> whenE (numDomains \<le> unat a) (throwError (InvalidArgument 0)) >>= lift (\<lambda>y. returnOk (UCAST(32 \<rightarrow> 8) a)) \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>a list. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); False\<rbrakk> \<Longrightarrow> no_fail (\<lambda>_. True) (whenE (numDomains \<le> unat a) (throwError (InvalidArgument 0)) >>= lift (\<lambda>y. returnOk (UCAST(32 \<rightarrow> 8) a))) proof (prove)
goal (4 subgoals):
 1. \<And>a list rv b. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); rv = Inr b\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>s. UCAST(32 \<rightarrow> 8) a = b) (returnOk (SetDomain (cap_object (fst (hd (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps')))) (UCAST(32 \<rightarrow> 8) a)) \<sqinter> throw) (whenE (excaps' = []) (throwError TruncatedMessage) >>= lift (\<lambda>y. case fst (hd excaps') of ThreadCap ptr \<Rightarrow> returnOk $ (ptr, b) | _ \<Rightarrow> throwError $ InvalidArgument 1))
 2. \<And>a list. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> whenE (numDomains \<le> unat a) (throwError (InvalidArgument 0)) >>= lift (\<lambda>y. returnOk (UCAST(32 \<rightarrow> 8) a)) \<lbrace>\<lambda>rv s. case rv of Inl aa \<Rightarrow> True | Inr b \<Rightarrow> UCAST(32 \<rightarrow> 8) a = b\<rbrace>
 3. \<And>a list s. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); True\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> whenE (numDomains \<le> unat a) (throwError (InvalidArgument 0)) >>= lift (\<lambda>y. returnOk (UCAST(32 \<rightarrow> 8) a)) \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>a list. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); False\<rbrakk> \<Longrightarrow> no_fail (\<lambda>_. True) (whenE (numDomains \<le> unat a) (throwError (InvalidArgument 0)) >>= lift (\<lambda>y. returnOk (UCAST(32 \<rightarrow> 8) a))) proof (prove)
goal (4 subgoals):
 1. \<And>a list rv b. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); rv = Inr b\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>s. UCAST(32 \<rightarrow> 8) a = b) (returnOk (SetDomain (cap_object (fst (hd (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps')))) (UCAST(32 \<rightarrow> 8) a)) \<sqinter> throw) (doE y <- whenE (excaps' = []) (throwError TruncatedMessage);
case fst (hd excaps') of ThreadCap ptr \<Rightarrow> returnOk $ (ptr, b) | _ \<Rightarrow> throwError $ InvalidArgument 1
odE)
 2. \<And>a list. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> doE y <- whenE (numDomains \<le> unat a) (throwError (InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE \<lbrace>\<lambda>rv s. case rv of Inl aa \<Rightarrow> True | Inr b \<Rightarrow> UCAST(32 \<rightarrow> 8) a = b\<rbrace>
 3. \<And>a list s. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); True\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> doE y <- whenE (numDomains \<le> unat a) (throwError (InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>a list. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); False\<rbrakk> \<Longrightarrow> no_fail (\<lambda>_. True) (doE y <- whenE (numDomains \<le> unat a) (throwError (InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE) proof (prove)
goal (5 subgoals):
 1. \<And>a list rv b. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); rv = Inr b; excaps' = []\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>s. UCAST(32 \<rightarrow> 8) a = b) (returnOk (SetDomain (cap_object (fst (hd (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps')))) (UCAST(32 \<rightarrow> 8) a)) \<sqinter> throw) (throwError TruncatedMessage)
 2. \<And>a list rv b. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); rv = Inr b; excaps' \<noteq> []\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>s. UCAST(32 \<rightarrow> 8) a = b) (returnOk (SetDomain (cap_object (fst (hd (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps')))) (UCAST(32 \<rightarrow> 8) a)) \<sqinter> throw) (case fst (hd excaps') of ThreadCap ptr \<Rightarrow> returnOk $ (ptr, b) | _ \<Rightarrow> throwError $ InvalidArgument 1)
 3. \<And>a list. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> doE y <- whenE (numDomains \<le> unat a) (throwError (InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE \<lbrace>\<lambda>rv s. case rv of Inl aa \<Rightarrow> True | Inr b \<Rightarrow> UCAST(32 \<rightarrow> 8) a = b\<rbrace>
 4. \<And>a list s. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); True\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> doE y <- whenE (numDomains \<le> unat a) (throwError (InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<And>a list. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); False\<rbrakk> \<Longrightarrow> no_fail (\<lambda>_. True) (doE y <- whenE (numDomains \<le> unat a) (throwError (InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE) proof (prove)
goal (5 subgoals):
 1. \<And>a list rv b. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); rv = Inr b; excaps' = []\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>s. UCAST(32 \<rightarrow> 8) a = b) throw (throwError TruncatedMessage)
 2. \<And>a list rv b. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); rv = Inr b; excaps' \<noteq> []\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>s. UCAST(32 \<rightarrow> 8) a = b) (returnOk (SetDomain (cap_object (fst (hd (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps')))) (UCAST(32 \<rightarrow> 8) a)) \<sqinter> throw) (case fst (hd excaps') of ThreadCap ptr \<Rightarrow> returnOk $ (ptr, b) | _ \<Rightarrow> throwError $ InvalidArgument 1)
 3. \<And>a list. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> doE y <- whenE (numDomains \<le> unat a) (throwError (InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE \<lbrace>\<lambda>rv s. case rv of Inl aa \<Rightarrow> True | Inr b \<Rightarrow> UCAST(32 \<rightarrow> 8) a = b\<rbrace>
 4. \<And>a list s. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); True\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> doE y <- whenE (numDomains \<le> unat a) (throwError (InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<And>a list. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); False\<rbrakk> \<Longrightarrow> no_fail (\<lambda>_. True) (doE y <- whenE (numDomains \<le> unat a) (throwError (InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE) proof (prove)
goal (4 subgoals):
 1. \<And>a list rv b. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); rv = Inr b; excaps' \<noteq> []\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>s. UCAST(32 \<rightarrow> 8) a = b) (returnOk (SetDomain (cap_object (fst (hd (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps')))) (UCAST(32 \<rightarrow> 8) a)) \<sqinter> throw) (case fst (hd excaps') of ThreadCap ptr \<Rightarrow> returnOk $ (ptr, b) | _ \<Rightarrow> throwError $ InvalidArgument 1)
 2. \<And>a list. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> doE y <- whenE (numDomains \<le> unat a) (throwError (InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE \<lbrace>\<lambda>rv s. case rv of Inl aa \<Rightarrow> True | Inr b \<Rightarrow> UCAST(32 \<rightarrow> 8) a = b\<rbrace>
 3. \<And>a list s. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); True\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> doE y <- whenE (numDomains \<le> unat a) (throwError (InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>a list. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); False\<rbrakk> \<Longrightarrow> no_fail (\<lambda>_. True) (doE y <- whenE (numDomains \<le> unat a) (throwError (InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE) proof (prove)
goal (15 subgoals):
 1. \<And>a list rv b. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); rv = Inr b; excaps' \<noteq> []; fst (hd excaps') = cap.NullCap\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>s. UCAST(32 \<rightarrow> 8) a = b) (returnOk (SetDomain (cap_object (fst (hd (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps')))) (UCAST(32 \<rightarrow> 8) a)) \<sqinter> throw) (throwError (InvalidArgument (Suc 0)))
 2. \<And>a list rv b x21 x22 x23 x24. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); rv = Inr b; excaps' \<noteq> []; fst (hd excaps') = cap.UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>s. UCAST(32 \<rightarrow> 8) a = b) (returnOk (SetDomain (cap_object (fst (hd (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps')))) (UCAST(32 \<rightarrow> 8) a)) \<sqinter> throw) (throwError (InvalidArgument (Suc 0)))
 3. \<And>a list rv b x31 x32 x33. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); rv = Inr b; excaps' \<noteq> []; fst (hd excaps') = cap.EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>s. UCAST(32 \<rightarrow> 8) a = b) (returnOk (SetDomain (cap_object (fst (hd (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps')))) (UCAST(32 \<rightarrow> 8) a)) \<sqinter> throw) (throwError (InvalidArgument (Suc 0)))
 4. \<And>a list rv b x41 x42 x43. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); rv = Inr b; excaps' \<noteq> []; fst (hd excaps') = cap.NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>s. UCAST(32 \<rightarrow> 8) a = b) (returnOk (SetDomain (cap_object (fst (hd (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps')))) (UCAST(32 \<rightarrow> 8) a)) \<sqinter> throw) (throwError (InvalidArgument (Suc 0)))
 5. \<And>a list rv b x51 x52 x53. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); rv = Inr b; excaps' \<noteq> []; fst (hd excaps') = cap.ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>s. UCAST(32 \<rightarrow> 8) a = b) (returnOk (SetDomain (cap_object (fst (hd (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps')))) (UCAST(32 \<rightarrow> 8) a)) \<sqinter> throw) (throwError (InvalidArgument (Suc 0)))
 6. \<And>a list rv b x61 x62 x63. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); rv = Inr b; excaps' \<noteq> []; fst (hd excaps') = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>s. UCAST(32 \<rightarrow> 8) a = b) (returnOk (SetDomain (cap_object (fst (hd (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps')))) (UCAST(32 \<rightarrow> 8) a)) \<sqinter> throw) (throwError (InvalidArgument (Suc 0)))
 7. \<And>a list rv b x7. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); rv = Inr b; excaps' \<noteq> []; fst (hd excaps') = ThreadCap x7\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>s. UCAST(32 \<rightarrow> 8) a = b) (returnOk (SetDomain (cap_object (fst (hd (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps')))) (UCAST(32 \<rightarrow> 8) a)) \<sqinter> throw) (returnOk (x7, b))
 8. \<And>a list rv b. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); rv = Inr b; excaps' \<noteq> []; fst (hd excaps') = cap.DomainCap\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>s. UCAST(32 \<rightarrow> 8) a = b) (returnOk (SetDomain (cap_object (fst (hd (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps')))) (UCAST(32 \<rightarrow> 8) a)) \<sqinter> throw) (throwError (InvalidArgument (Suc 0)))
 9. \<And>a list rv b. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); rv = Inr b; excaps' \<noteq> []; fst (hd excaps') = IRQControlCap\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>s. UCAST(32 \<rightarrow> 8) a = b) (returnOk (SetDomain (cap_object (fst (hd (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps')))) (UCAST(32 \<rightarrow> 8) a)) \<sqinter> throw) (throwError (InvalidArgument (Suc 0)))
 10. \<And>a list rv b x10. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); rv = Inr b; excaps' \<noteq> []; fst (hd excaps') = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>s. UCAST(32 \<rightarrow> 8) a = b) (returnOk (SetDomain (cap_object (fst (hd (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps')))) (UCAST(32 \<rightarrow> 8) a)) \<sqinter> throw) (throwError (InvalidArgument (Suc 0)))
A total of 15 subgoals... proof (prove)
goal (9 subgoals):
 1. \<And>a list rv b x7. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); rv = Inr b; excaps' \<noteq> []; fst (hd excaps') = ThreadCap x7\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>s. UCAST(32 \<rightarrow> 8) a = b) (returnOk (SetDomain (cap_object (fst (hd (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps')))) (UCAST(32 \<rightarrow> 8) a)) \<sqinter> throw) (returnOk (x7, b))
 2. \<And>a list rv b. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); rv = Inr b; excaps' \<noteq> []; fst (hd excaps') = cap.DomainCap\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>s. UCAST(32 \<rightarrow> 8) a = b) (returnOk (SetDomain (cap_object (fst (hd (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps')))) (UCAST(32 \<rightarrow> 8) a)) \<sqinter> throw) (throwError (InvalidArgument (Suc 0)))
 3. \<And>a list rv b. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); rv = Inr b; excaps' \<noteq> []; fst (hd excaps') = IRQControlCap\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>s. UCAST(32 \<rightarrow> 8) a = b) (returnOk (SetDomain (cap_object (fst (hd (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps')))) (UCAST(32 \<rightarrow> 8) a)) \<sqinter> throw) (throwError (InvalidArgument (Suc 0)))
 4. \<And>a list rv b x10. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); rv = Inr b; excaps' \<noteq> []; fst (hd excaps') = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>s. UCAST(32 \<rightarrow> 8) a = b) (returnOk (SetDomain (cap_object (fst (hd (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps')))) (UCAST(32 \<rightarrow> 8) a)) \<sqinter> throw) (throwError (InvalidArgument (Suc 0)))
 5. \<And>a list rv b x111 x112 x113. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); rv = Inr b; excaps' \<noteq> []; fst (hd excaps') = Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>s. UCAST(32 \<rightarrow> 8) a = b) (returnOk (SetDomain (cap_object (fst (hd (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps')))) (UCAST(32 \<rightarrow> 8) a)) \<sqinter> throw) (throwError (InvalidArgument (Suc 0)))
 6. \<And>a list rv b x12. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); rv = Inr b; excaps' \<noteq> []; fst (hd excaps') = ArchObjectCap x12\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>s. UCAST(32 \<rightarrow> 8) a = b) (returnOk (SetDomain (cap_object (fst (hd (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps')))) (UCAST(32 \<rightarrow> 8) a)) \<sqinter> throw) (throwError (InvalidArgument (Suc 0)))
 7. \<And>a list. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> doE y <- whenE (numDomains \<le> unat a) (throwError (InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE \<lbrace>\<lambda>rv s. case rv of Inl aa \<Rightarrow> True | Inr b \<Rightarrow> UCAST(32 \<rightarrow> 8) a = b\<rbrace>
 8. \<And>a list s. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); True\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> doE y <- whenE (numDomains \<le> unat a) (throwError (InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE \<lbrace>\<lambda>r. (=) s\<rbrace>
 9. \<And>a list. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); False\<rbrakk> \<Longrightarrow> no_fail (\<lambda>_. True) (doE y <- whenE (numDomains \<le> unat a) (throwError (InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE) proof (prove)
goal (9 subgoals):
 1. \<And>a list rv b x7. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); rv = Inr b; excaps' \<noteq> []; fst (hd excaps') = ThreadCap x7\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>s. UCAST(32 \<rightarrow> 8) a = b) (returnOk (SetDomain (cap_object (fst (hd (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps')))) (UCAST(32 \<rightarrow> 8) a))) (returnOk (x7, b))
 2. \<And>a list rv b. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); rv = Inr b; excaps' \<noteq> []; fst (hd excaps') = cap.DomainCap\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>s. UCAST(32 \<rightarrow> 8) a = b) (returnOk (SetDomain (cap_object (fst (hd (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps')))) (UCAST(32 \<rightarrow> 8) a)) \<sqinter> throw) (throwError (InvalidArgument (Suc 0)))
 3. \<And>a list rv b. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); rv = Inr b; excaps' \<noteq> []; fst (hd excaps') = IRQControlCap\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>s. UCAST(32 \<rightarrow> 8) a = b) (returnOk (SetDomain (cap_object (fst (hd (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps')))) (UCAST(32 \<rightarrow> 8) a)) \<sqinter> throw) (throwError (InvalidArgument (Suc 0)))
 4. \<And>a list rv b x10. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); rv = Inr b; excaps' \<noteq> []; fst (hd excaps') = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>s. UCAST(32 \<rightarrow> 8) a = b) (returnOk (SetDomain (cap_object (fst (hd (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps')))) (UCAST(32 \<rightarrow> 8) a)) \<sqinter> throw) (throwError (InvalidArgument (Suc 0)))
 5. \<And>a list rv b x111 x112 x113. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); rv = Inr b; excaps' \<noteq> []; fst (hd excaps') = Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>s. UCAST(32 \<rightarrow> 8) a = b) (returnOk (SetDomain (cap_object (fst (hd (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps')))) (UCAST(32 \<rightarrow> 8) a)) \<sqinter> throw) (throwError (InvalidArgument (Suc 0)))
 6. \<And>a list rv b x12. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); rv = Inr b; excaps' \<noteq> []; fst (hd excaps') = ArchObjectCap x12\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>s. UCAST(32 \<rightarrow> 8) a = b) (returnOk (SetDomain (cap_object (fst (hd (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps')))) (UCAST(32 \<rightarrow> 8) a)) \<sqinter> throw) (throwError (InvalidArgument (Suc 0)))
 7. \<And>a list. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> doE y <- whenE (numDomains \<le> unat a) (throwError (InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE \<lbrace>\<lambda>rv s. case rv of Inl aa \<Rightarrow> True | Inr b \<Rightarrow> UCAST(32 \<rightarrow> 8) a = b\<rbrace>
 8. \<And>a list s. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); True\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> doE y <- whenE (numDomains \<le> unat a) (throwError (InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE \<lbrace>\<lambda>r. (=) s\<rbrace>
 9. \<And>a list. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); False\<rbrakk> \<Longrightarrow> no_fail (\<lambda>_. True) (doE y <- whenE (numDomains \<le> unat a) (throwError (InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE) proof (prove)
goal (9 subgoals):
 1. \<And>a list x7. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); excaps' \<noteq> []; fst (hd excaps') = ThreadCap x7\<rbrakk> \<Longrightarrow> cap_object (fst (hd (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'))) = x7
 2. \<And>a list rv b. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); rv = Inr b; excaps' \<noteq> []; fst (hd excaps') = cap.DomainCap\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>s. UCAST(32 \<rightarrow> 8) a = b) (returnOk (SetDomain (cap_object (fst (hd (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps')))) (UCAST(32 \<rightarrow> 8) a)) \<sqinter> throw) (throwError (InvalidArgument (Suc 0)))
 3. \<And>a list rv b. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); rv = Inr b; excaps' \<noteq> []; fst (hd excaps') = IRQControlCap\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>s. UCAST(32 \<rightarrow> 8) a = b) (returnOk (SetDomain (cap_object (fst (hd (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps')))) (UCAST(32 \<rightarrow> 8) a)) \<sqinter> throw) (throwError (InvalidArgument (Suc 0)))
 4. \<And>a list rv b x10. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); rv = Inr b; excaps' \<noteq> []; fst (hd excaps') = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>s. UCAST(32 \<rightarrow> 8) a = b) (returnOk (SetDomain (cap_object (fst (hd (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps')))) (UCAST(32 \<rightarrow> 8) a)) \<sqinter> throw) (throwError (InvalidArgument (Suc 0)))
 5. \<And>a list rv b x111 x112 x113. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); rv = Inr b; excaps' \<noteq> []; fst (hd excaps') = Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>s. UCAST(32 \<rightarrow> 8) a = b) (returnOk (SetDomain (cap_object (fst (hd (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps')))) (UCAST(32 \<rightarrow> 8) a)) \<sqinter> throw) (throwError (InvalidArgument (Suc 0)))
 6. \<And>a list rv b x12. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); rv = Inr b; excaps' \<noteq> []; fst (hd excaps') = ArchObjectCap x12\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>s. UCAST(32 \<rightarrow> 8) a = b) (returnOk (SetDomain (cap_object (fst (hd (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps')))) (UCAST(32 \<rightarrow> 8) a)) \<sqinter> throw) (throwError (InvalidArgument (Suc 0)))
 7. \<And>a list. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> doE y <- whenE (numDomains \<le> unat a) (throwError (InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE \<lbrace>\<lambda>rv s. case rv of Inl aa \<Rightarrow> True | Inr b \<Rightarrow> UCAST(32 \<rightarrow> 8) a = b\<rbrace>
 8. \<And>a list s. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); True\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> doE y <- whenE (numDomains \<le> unat a) (throwError (InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE \<lbrace>\<lambda>r. (=) s\<rbrace>
 9. \<And>a list. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); False\<rbrakk> \<Longrightarrow> no_fail (\<lambda>_. True) (doE y <- whenE (numDomains \<le> unat a) (throwError (InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE) proof (prove)
goal (8 subgoals):
 1. \<And>a list rv b. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); rv = Inr b; excaps' \<noteq> []; fst (hd excaps') = cap.DomainCap\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>s. UCAST(32 \<rightarrow> 8) a = b) (returnOk (SetDomain (cap_object (fst (hd (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps')))) (UCAST(32 \<rightarrow> 8) a)) \<sqinter> throw) (throwError (InvalidArgument (Suc 0)))
 2. \<And>a list rv b. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); rv = Inr b; excaps' \<noteq> []; fst (hd excaps') = IRQControlCap\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>s. UCAST(32 \<rightarrow> 8) a = b) (returnOk (SetDomain (cap_object (fst (hd (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps')))) (UCAST(32 \<rightarrow> 8) a)) \<sqinter> throw) (throwError (InvalidArgument (Suc 0)))
 3. \<And>a list rv b x10. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); rv = Inr b; excaps' \<noteq> []; fst (hd excaps') = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>s. UCAST(32 \<rightarrow> 8) a = b) (returnOk (SetDomain (cap_object (fst (hd (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps')))) (UCAST(32 \<rightarrow> 8) a)) \<sqinter> throw) (throwError (InvalidArgument (Suc 0)))
 4. \<And>a list rv b x111 x112 x113. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); rv = Inr b; excaps' \<noteq> []; fst (hd excaps') = Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>s. UCAST(32 \<rightarrow> 8) a = b) (returnOk (SetDomain (cap_object (fst (hd (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps')))) (UCAST(32 \<rightarrow> 8) a)) \<sqinter> throw) (throwError (InvalidArgument (Suc 0)))
 5. \<And>a list rv b x12. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); rv = Inr b; excaps' \<noteq> []; fst (hd excaps') = ArchObjectCap x12\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>s. UCAST(32 \<rightarrow> 8) a = b) (returnOk (SetDomain (cap_object (fst (hd (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps')))) (UCAST(32 \<rightarrow> 8) a)) \<sqinter> throw) (throwError (InvalidArgument (Suc 0)))
 6. \<And>a list. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> doE y <- whenE (numDomains \<le> unat a) (throwError (InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE \<lbrace>\<lambda>rv s. case rv of Inl aa \<Rightarrow> True | Inr b \<Rightarrow> UCAST(32 \<rightarrow> 8) a = b\<rbrace>
 7. \<And>a list s. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); True\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> doE y <- whenE (numDomains \<le> unat a) (throwError (InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE \<lbrace>\<lambda>r. (=) s\<rbrace>
 8. \<And>a list. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); False\<rbrakk> \<Longrightarrow> no_fail (\<lambda>_. True) (doE y <- whenE (numDomains \<le> unat a) (throwError (InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE) proof (prove)
goal (3 subgoals):
 1. \<And>a list. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> doE y <- whenE (numDomains \<le> unat a) (throwError (InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE \<lbrace>\<lambda>rv s. case rv of Inl aa \<Rightarrow> True | Inr b \<Rightarrow> UCAST(32 \<rightarrow> 8) a = b\<rbrace>
 2. \<And>a list s. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); True\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> doE y <- whenE (numDomains \<le> unat a) (throwError (InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>a list. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); False\<rbrakk> \<Longrightarrow> no_fail (\<lambda>_. True) (doE y <- whenE (numDomains \<le> unat a) (throwError (InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE) proof (prove)
goal (3 subgoals):
 1. \<And>a list. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> doE y <- whenE (numDomains \<le> unat a) (throwError (InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE \<lbrace>\<lambda>rv s. case Inr rv of Inl aa \<Rightarrow> True | Inr b \<Rightarrow> UCAST(32 \<rightarrow> 8) a = b\<rbrace>, \<lbrace>\<lambda>rv s. case Inl rv of Inl aa \<Rightarrow> True | Inr b \<Rightarrow> UCAST(32 \<rightarrow> 8) a = b\<rbrace>
 2. \<And>a list s. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); True\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> doE y <- whenE (numDomains \<le> unat a) (throwError (InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>a list. \<lbrakk>gen_invocation_type label' = DomainSetSet; excaps = map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) excaps'; args' = a # list; i = DomainSetIntent (UCAST(32 \<rightarrow> 8) a); False\<rbrakk> \<Longrightarrow> no_fail (\<lambda>_. True) (doE y <- whenE (numDomains \<le> unat a) (throwError (InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE) proof (prove)
goal:
No subgoals!