theory Syscall_R

lemma decodeDomainInvocation_corres:
  shows "\<lbrakk> list_all2 cap_relation (map fst cs) (map fst cs');
           list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs' \<rbrakk> \<Longrightarrow>
        corres (ser \<oplus> ((\<lambda>x. inv_relation x \<circ> uncurry Invocations_H.invocation.InvokeDomain) \<circ> (\<lambda>(x,y). Invocations_A.invocation.InvokeDomain x y))) \<top> \<top>
          (decode_domain_invocation label args cs)
          (decodeDomainInvocation label args cs')" apply (simp add: decode_domain_invocation_def decodeDomainInvocation_def) apply (rule whenE_throwError_corres_initial) apply (simp+)[2] apply (case_tac "args", simp_all) apply (rule corres_guard_imp) apply (rule_tac r'="\<lambda>domain domain'. domain = domain'" and R="\<lambda>_. \<top>" and R'="\<lambda>_. \<top>"
            in corres_splitEE) apply (rule whenE_throwError_corres) apply (simp+)[2] apply (rule corres_returnOkTT) apply simp apply (rule whenE_throwError_corres_initial) apply simp apply (case_tac "cs") apply ((case_tac "cs'", ((simp add: null_def)+)[2])+)[2] apply (subgoal_tac "cap_relation (fst (hd cs)) (fst (hd cs'))") apply (case_tac "fst (hd cs)") apply (case_tac "fst (hd cs')", simp+, rule corres_returnOkTT) apply (simp add: inv_relation_def o_def uncurry_def) apply (case_tac "fst (hd cs')", fastforce+) apply (case_tac "cs") apply (case_tac "cs'", ((simp add: list_all2_map2 list_all2_map1)+)[2]) apply (case_tac "cs'", ((simp add: list_all2_map2 list_all2_map1)+)[2]) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'\<rbrakk> \<Longrightarrow> corres (ser \<oplus> ((\<lambda>x. inv_relation x \<circ> uncurry Invocations_H.invocation.InvokeDomain) \<circ> (\<lambda>(x, y). Invocations_A.invocation.InvokeDomain x y))) (\<lambda>_. True) (\<lambda>_. True) (decode_domain_invocation label args cs) (decodeDomainInvocation label args cs') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'\<rbrakk> \<Longrightarrow> corres (ser \<oplus> ((\<lambda>x. inv_relation x \<circ> uncurry Invocations_H.invocation.InvokeDomain) \<circ> (\<lambda>(x, y). Invocations_A.invocation.InvokeDomain x y))) (\<lambda>_. True) (\<lambda>_. True) (doE y <- whenE (gen_invocation_type label \<noteq> DomainSetSet) (throwError ExceptionTypes_A.syscall_error.IllegalOperation);
domain <- case args of [] \<Rightarrow> throwError ExceptionTypes_A.syscall_error.TruncatedMessage | x # xs \<Rightarrow> doE whenE (numDomains \<le> unat x) $ throwError $ ExceptionTypes_A.syscall_error.InvalidArgument 0;
returnOk (UCAST(32 \<rightarrow> 8) x)
odE;
y <- whenE (cs = []) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage);
case fst (hd cs) of cap.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, domain) | _ \<Rightarrow> throwError $ ExceptionTypes_A.syscall_error.InvalidArgument 1
odE) (doE y <- whenE (gen_invocation_type label \<noteq> DomainSetSet) (throwError Fault_H.syscall_error.IllegalOperation);
domain <- case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | x # xa \<Rightarrow> doE whenE (numDomains \<le> fromIntegral x) $ throw (Fault_H.syscall_error.InvalidArgument 0);
returnOk $ fromIntegral x
odE;
y <- whenE (null cs') (throwError Fault_H.syscall_error.TruncatedMessage);
case fst (hd cs') of capability.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, domain) | _ \<Rightarrow> throw (Fault_H.syscall_error.InvalidArgument 1)
odE) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'\<rbrakk> \<Longrightarrow> ser ExceptionTypes_A.syscall_error.IllegalOperation Fault_H.syscall_error.IllegalOperation
 2. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'\<rbrakk> \<Longrightarrow> (gen_invocation_type label \<noteq> DomainSetSet) = (gen_invocation_type label \<noteq> DomainSetSet)
 3. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; \<not> gen_invocation_type label \<noteq> DomainSetSet\<rbrakk> \<Longrightarrow> corres (ser \<oplus> ((\<lambda>x. inv_relation x \<circ> uncurry Invocations_H.invocation.InvokeDomain) \<circ> (\<lambda>(x, y). Invocations_A.invocation.InvokeDomain x y))) (\<lambda>_. True) (\<lambda>_. True) (doE domain <- case args of [] \<Rightarrow> throwError ExceptionTypes_A.syscall_error.TruncatedMessage | x # xs \<Rightarrow> doE whenE (numDomains \<le> unat x) $ throwError $ ExceptionTypes_A.syscall_error.InvalidArgument 0;
returnOk (UCAST(32 \<rightarrow> 8) x)
odE;
y <- whenE (cs = []) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage);
case fst (hd cs) of cap.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, domain) | _ \<Rightarrow> throwError $ ExceptionTypes_A.syscall_error.InvalidArgument 1
odE) (doE domain <- case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | x # xa \<Rightarrow> doE whenE (numDomains \<le> fromIntegral x) $ throw (Fault_H.syscall_error.InvalidArgument 0);
returnOk $ fromIntegral x
odE;
y <- whenE (null cs') (throwError Fault_H.syscall_error.TruncatedMessage);
case fst (hd cs') of capability.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, domain) | _ \<Rightarrow> throw (Fault_H.syscall_error.InvalidArgument 1)
odE) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; \<not> gen_invocation_type label \<noteq> DomainSetSet\<rbrakk> \<Longrightarrow> corres (ser \<oplus> ((\<lambda>x. inv_relation x \<circ> uncurry Invocations_H.invocation.InvokeDomain) \<circ> (\<lambda>(x, y). Invocations_A.invocation.InvokeDomain x y))) (\<lambda>_. True) (\<lambda>_. True) (doE domain <- case args of [] \<Rightarrow> throwError ExceptionTypes_A.syscall_error.TruncatedMessage | x # xs \<Rightarrow> doE whenE (numDomains \<le> unat x) $ throwError $ ExceptionTypes_A.syscall_error.InvalidArgument 0;
returnOk (UCAST(32 \<rightarrow> 8) x)
odE;
y <- whenE (cs = []) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage);
case fst (hd cs) of cap.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, domain) | _ \<Rightarrow> throwError $ ExceptionTypes_A.syscall_error.InvalidArgument 1
odE) (doE domain <- case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | x # xa \<Rightarrow> doE whenE (numDomains \<le> fromIntegral x) $ throw (Fault_H.syscall_error.InvalidArgument 0);
returnOk $ fromIntegral x
odE;
y <- whenE (null cs') (throwError Fault_H.syscall_error.TruncatedMessage);
case fst (hd cs') of capability.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, domain) | _ \<Rightarrow> throw (Fault_H.syscall_error.InvalidArgument 1)
odE) proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list\<rbrakk> \<Longrightarrow> corres (ser \<oplus> ((\<lambda>x. inv_relation x \<circ> uncurry Invocations_H.invocation.InvokeDomain) \<circ> (\<lambda>(x, y). Invocations_A.invocation.InvokeDomain x y))) (\<lambda>_. True) (\<lambda>_. True) (doE domain <- doE y <- whenE (numDomains \<le> unat a) (throwError (ExceptionTypes_A.syscall_error.InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE;
y <- whenE (cs = []) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage);
case fst (hd cs) of cap.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, domain) | _ \<Rightarrow> throwError $ ExceptionTypes_A.syscall_error.InvalidArgument 1
odE) (doE domain <- doE y <- whenE (numDomains \<le> unat a) (throwError (Fault_H.syscall_error.InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE;
y <- whenE (null cs') (throwError Fault_H.syscall_error.TruncatedMessage);
case fst (hd cs') of capability.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, domain) | _ \<Rightarrow> throw (Fault_H.syscall_error.InvalidArgument 1)
odE) proof (prove)
goal (3 subgoals):
 1. \<And>a list. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list\<rbrakk> \<Longrightarrow> corres (ser \<oplus> ((\<lambda>x. inv_relation x \<circ> uncurry Invocations_H.invocation.InvokeDomain) \<circ> (\<lambda>(x, y). Invocations_A.invocation.InvokeDomain x y))) (?Q9 a list) (?Q'9 a list) (doE domain <- doE y <- whenE (numDomains \<le> unat a) (throwError (ExceptionTypes_A.syscall_error.InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE;
y <- whenE (cs = []) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage);
case fst (hd cs) of cap.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, domain) | _ \<Rightarrow> throwError $ ExceptionTypes_A.syscall_error.InvalidArgument 1
odE) (doE domain <- doE y <- whenE (numDomains \<le> unat a) (throwError (Fault_H.syscall_error.InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE;
y <- whenE (null cs') (throwError Fault_H.syscall_error.TruncatedMessage);
case fst (hd cs') of capability.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, domain) | _ \<Rightarrow> throw (Fault_H.syscall_error.InvalidArgument 1)
odE)
 2. \<And>a list s. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; True\<rbrakk> \<Longrightarrow> ?Q9 a list s
 3. \<And>a list s. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; True\<rbrakk> \<Longrightarrow> ?Q'9 a list s proof (prove)
goal (6 subgoals):
 1. \<And>a list. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list\<rbrakk> \<Longrightarrow> corres (ser \<oplus> (=)) (?P13 a list) (?P'13 a list) (doE y <- whenE (numDomains \<le> unat a) (throwError (ExceptionTypes_A.syscall_error.InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE) (doE y <- whenE (numDomains \<le> unat a) (throwError (Fault_H.syscall_error.InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE)
 2. \<And>a list rv rv'. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; rv = rv'\<rbrakk> \<Longrightarrow> corres (ser \<oplus> ((\<lambda>x. inv_relation x \<circ> uncurry Invocations_H.invocation.InvokeDomain) \<circ> (\<lambda>(x, y). Invocations_A.invocation.InvokeDomain x y))) (\<lambda>_. True) (\<lambda>_. True) (doE y <- whenE (cs = []) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage);
case fst (hd cs) of cap.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, rv) | _ \<Rightarrow> throwError $ ExceptionTypes_A.syscall_error.InvalidArgument 1
odE) (doE y <- whenE (null cs') (throwError Fault_H.syscall_error.TruncatedMessage);
case fst (hd cs') of capability.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, rv') | _ \<Rightarrow> throw (Fault_H.syscall_error.InvalidArgument 1)
odE)
 3. \<And>a list. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list\<rbrakk> \<Longrightarrow> \<lbrace>?Q13 a list\<rbrace> doE y <- whenE (numDomains \<le> unat a) (throwError (ExceptionTypes_A.syscall_error.InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>a list. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list\<rbrakk> \<Longrightarrow> \<lbrace>?Q'13 a list\<rbrace> doE y <- whenE (numDomains \<le> unat a) (throwError (Fault_H.syscall_error.InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>a list s. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; True\<rbrakk> \<Longrightarrow> (?P13 a list and ?Q13 a list) s
 6. \<And>a list s. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; True\<rbrakk> \<Longrightarrow> (?P'13 a list and ?Q'13 a list) s proof (prove)
goal (8 subgoals):
 1. \<And>a list. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list\<rbrakk> \<Longrightarrow> ser (ExceptionTypes_A.syscall_error.InvalidArgument 0) (Fault_H.syscall_error.InvalidArgument 0)
 2. \<And>a list. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list\<rbrakk> \<Longrightarrow> (numDomains \<le> unat a) = (numDomains \<le> unat a)
 3. \<And>a list. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; \<not> numDomains \<le> unat a\<rbrakk> \<Longrightarrow> corres (ser \<oplus> (=)) (?Q15 a list) (?Q'15 a list) (returnOk (UCAST(32 \<rightarrow> 8) a)) (returnOk (UCAST(32 \<rightarrow> 8) a))
 4. \<And>a list rv rv'. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; rv = rv'\<rbrakk> \<Longrightarrow> corres (ser \<oplus> ((\<lambda>x. inv_relation x \<circ> uncurry Invocations_H.invocation.InvokeDomain) \<circ> (\<lambda>(x, y). Invocations_A.invocation.InvokeDomain x y))) (\<lambda>_. True) (\<lambda>_. True) (doE y <- whenE (cs = []) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage);
case fst (hd cs) of cap.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, rv) | _ \<Rightarrow> throwError $ ExceptionTypes_A.syscall_error.InvalidArgument 1
odE) (doE y <- whenE (null cs') (throwError Fault_H.syscall_error.TruncatedMessage);
case fst (hd cs') of capability.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, rv') | _ \<Rightarrow> throw (Fault_H.syscall_error.InvalidArgument 1)
odE)
 5. \<And>a list. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list\<rbrakk> \<Longrightarrow> \<lbrace>?Q13 a list\<rbrace> doE y <- whenE (numDomains \<le> unat a) (throwError (ExceptionTypes_A.syscall_error.InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>a list. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list\<rbrakk> \<Longrightarrow> \<lbrace>?Q'13 a list\<rbrace> doE y <- whenE (numDomains \<le> unat a) (throwError (Fault_H.syscall_error.InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>a list s. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; True\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<not> numDomains \<le> unat a \<longrightarrow> ?Q15 a list s) and ?Q13 a list) s
 8. \<And>a list s. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; True\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<not> numDomains \<le> unat a \<longrightarrow> ?Q'15 a list s) and ?Q'13 a list) s proof (prove)
goal (6 subgoals):
 1. \<And>a list. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; \<not> numDomains \<le> unat a\<rbrakk> \<Longrightarrow> corres (ser \<oplus> (=)) (?Q15 a list) (?Q'15 a list) (returnOk (UCAST(32 \<rightarrow> 8) a)) (returnOk (UCAST(32 \<rightarrow> 8) a))
 2. \<And>a list rv rv'. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; rv = rv'\<rbrakk> \<Longrightarrow> corres (ser \<oplus> ((\<lambda>x. inv_relation x \<circ> uncurry Invocations_H.invocation.InvokeDomain) \<circ> (\<lambda>(x, y). Invocations_A.invocation.InvokeDomain x y))) (\<lambda>_. True) (\<lambda>_. True) (doE y <- whenE (cs = []) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage);
case fst (hd cs) of cap.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, rv) | _ \<Rightarrow> throwError $ ExceptionTypes_A.syscall_error.InvalidArgument 1
odE) (doE y <- whenE (null cs') (throwError Fault_H.syscall_error.TruncatedMessage);
case fst (hd cs') of capability.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, rv') | _ \<Rightarrow> throw (Fault_H.syscall_error.InvalidArgument 1)
odE)
 3. \<And>a list. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list\<rbrakk> \<Longrightarrow> \<lbrace>?Q13 a list\<rbrace> doE y <- whenE (numDomains \<le> unat a) (throwError (ExceptionTypes_A.syscall_error.InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>a list. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list\<rbrakk> \<Longrightarrow> \<lbrace>?Q'13 a list\<rbrace> doE y <- whenE (numDomains \<le> unat a) (throwError (Fault_H.syscall_error.InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>a list s. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; True\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<not> numDomains \<le> unat a \<longrightarrow> ?Q15 a list s) and ?Q13 a list) s
 6. \<And>a list s. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; True\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<not> numDomains \<le> unat a \<longrightarrow> ?Q'15 a list s) and ?Q'13 a list) s proof (prove)
goal (6 subgoals):
 1. \<And>a list. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; \<not> numDomains \<le> unat a\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 8) a = UCAST(32 \<rightarrow> 8) a
 2. \<And>a list rv rv'. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; rv = rv'\<rbrakk> \<Longrightarrow> corres (ser \<oplus> ((\<lambda>x. inv_relation x \<circ> uncurry Invocations_H.invocation.InvokeDomain) \<circ> (\<lambda>(x, y). Invocations_A.invocation.InvokeDomain x y))) (\<lambda>_. True) (\<lambda>_. True) (doE y <- whenE (cs = []) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage);
case fst (hd cs) of cap.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, rv) | _ \<Rightarrow> throwError $ ExceptionTypes_A.syscall_error.InvalidArgument 1
odE) (doE y <- whenE (null cs') (throwError Fault_H.syscall_error.TruncatedMessage);
case fst (hd cs') of capability.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, rv') | _ \<Rightarrow> throw (Fault_H.syscall_error.InvalidArgument 1)
odE)
 3. \<And>a list. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list\<rbrakk> \<Longrightarrow> \<lbrace>?Q13 a list\<rbrace> doE y <- whenE (numDomains \<le> unat a) (throwError (ExceptionTypes_A.syscall_error.InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>a list. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list\<rbrakk> \<Longrightarrow> \<lbrace>?Q'13 a list\<rbrace> doE y <- whenE (numDomains \<le> unat a) (throwError (Fault_H.syscall_error.InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>a list s. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; True\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<not> numDomains \<le> unat a \<longrightarrow> True) and ?Q13 a list) s
 6. \<And>a list s. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; True\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<not> numDomains \<le> unat a \<longrightarrow> True) and ?Q'13 a list) s proof (prove)
goal (5 subgoals):
 1. \<And>a list rv rv'. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; rv = rv'\<rbrakk> \<Longrightarrow> corres (ser \<oplus> ((\<lambda>x. inv_relation x \<circ> uncurry Invocations_H.invocation.InvokeDomain) \<circ> (\<lambda>(x, y). Invocations_A.invocation.InvokeDomain x y))) (\<lambda>_. True) (\<lambda>_. True) (doE y <- whenE (cs = []) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage);
case fst (hd cs) of cap.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, rv) | _ \<Rightarrow> throwError $ ExceptionTypes_A.syscall_error.InvalidArgument 1
odE) (doE y <- whenE (null cs') (throwError Fault_H.syscall_error.TruncatedMessage);
case fst (hd cs') of capability.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, rv') | _ \<Rightarrow> throw (Fault_H.syscall_error.InvalidArgument 1)
odE)
 2. \<And>a list. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list\<rbrakk> \<Longrightarrow> \<lbrace>?Q13 a list\<rbrace> doE y <- whenE (numDomains \<le> unat a) (throwError (ExceptionTypes_A.syscall_error.InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>a list. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list\<rbrakk> \<Longrightarrow> \<lbrace>?Q'13 a list\<rbrace> doE y <- whenE (numDomains \<le> unat a) (throwError (Fault_H.syscall_error.InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>a list s. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; True\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<not> numDomains \<le> unat a \<longrightarrow> True) and ?Q13 a list) s
 5. \<And>a list s. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; True\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<not> numDomains \<le> unat a \<longrightarrow> True) and ?Q'13 a list) s proof (prove)
goal (7 subgoals):
 1. \<And>a list rv rv'. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; rv = rv'\<rbrakk> \<Longrightarrow> ser ExceptionTypes_A.syscall_error.TruncatedMessage Fault_H.syscall_error.TruncatedMessage
 2. \<And>a list rv rv'. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; rv = rv'\<rbrakk> \<Longrightarrow> (cs = []) = null cs'
 3. \<And>a list rv rv'. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; rv = rv'; cs \<noteq> []\<rbrakk> \<Longrightarrow> corres (ser \<oplus> ((\<lambda>x. inv_relation x \<circ> uncurry Invocations_H.invocation.InvokeDomain) \<circ> (\<lambda>(x, y). Invocations_A.invocation.InvokeDomain x y))) (\<lambda>_. True) (\<lambda>_. True) (case fst (hd cs) of cap.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, rv) | _ \<Rightarrow> throwError $ ExceptionTypes_A.syscall_error.InvalidArgument 1) (case fst (hd cs') of capability.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, rv') | _ \<Rightarrow> throw (Fault_H.syscall_error.InvalidArgument 1))
 4. \<And>a list. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list\<rbrakk> \<Longrightarrow> \<lbrace>?Q13 a list\<rbrace> doE y <- whenE (numDomains \<le> unat a) (throwError (ExceptionTypes_A.syscall_error.InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>a list. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list\<rbrakk> \<Longrightarrow> \<lbrace>?Q'13 a list\<rbrace> doE y <- whenE (numDomains \<le> unat a) (throwError (Fault_H.syscall_error.InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>a list s. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; True\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<not> numDomains \<le> unat a \<longrightarrow> True) and ?Q13 a list) s
 7. \<And>a list s. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; True\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<not> numDomains \<le> unat a \<longrightarrow> True) and ?Q'13 a list) s proof (prove)
goal (6 subgoals):
 1. \<And>a list rv rv'. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; rv = rv'\<rbrakk> \<Longrightarrow> (cs = []) = null cs'
 2. \<And>a list rv rv'. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; rv = rv'; cs \<noteq> []\<rbrakk> \<Longrightarrow> corres (ser \<oplus> ((\<lambda>x. inv_relation x \<circ> uncurry Invocations_H.invocation.InvokeDomain) \<circ> (\<lambda>(x, y). Invocations_A.invocation.InvokeDomain x y))) (\<lambda>_. True) (\<lambda>_. True) (case fst (hd cs) of cap.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, rv) | _ \<Rightarrow> throwError $ ExceptionTypes_A.syscall_error.InvalidArgument 1) (case fst (hd cs') of capability.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, rv') | _ \<Rightarrow> throw (Fault_H.syscall_error.InvalidArgument 1))
 3. \<And>a list. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list\<rbrakk> \<Longrightarrow> \<lbrace>?Q13 a list\<rbrace> doE y <- whenE (numDomains \<le> unat a) (throwError (ExceptionTypes_A.syscall_error.InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>a list. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list\<rbrakk> \<Longrightarrow> \<lbrace>?Q'13 a list\<rbrace> doE y <- whenE (numDomains \<le> unat a) (throwError (Fault_H.syscall_error.InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>a list s. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; True\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<not> numDomains \<le> unat a \<longrightarrow> True) and ?Q13 a list) s
 6. \<And>a list s. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; True\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<not> numDomains \<le> unat a \<longrightarrow> True) and ?Q'13 a list) s proof (prove)
goal (7 subgoals):
 1. \<And>a list rv rv'. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; rv = rv'; cs = []\<rbrakk> \<Longrightarrow> (cs = []) = null cs'
 2. \<And>a list rv rv' aa lista. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; rv = rv'; cs = aa # lista\<rbrakk> \<Longrightarrow> (cs = []) = null cs'
 3. \<And>a list rv rv'. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; rv = rv'; cs \<noteq> []\<rbrakk> \<Longrightarrow> corres (ser \<oplus> ((\<lambda>x. inv_relation x \<circ> uncurry Invocations_H.invocation.InvokeDomain) \<circ> (\<lambda>(x, y). Invocations_A.invocation.InvokeDomain x y))) (\<lambda>_. True) (\<lambda>_. True) (case fst (hd cs) of cap.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, rv) | _ \<Rightarrow> throwError $ ExceptionTypes_A.syscall_error.InvalidArgument 1) (case fst (hd cs') of capability.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, rv') | _ \<Rightarrow> throw (Fault_H.syscall_error.InvalidArgument 1))
 4. \<And>a list. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list\<rbrakk> \<Longrightarrow> \<lbrace>?Q13 a list\<rbrace> doE y <- whenE (numDomains \<le> unat a) (throwError (ExceptionTypes_A.syscall_error.InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>a list. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list\<rbrakk> \<Longrightarrow> \<lbrace>?Q'13 a list\<rbrace> doE y <- whenE (numDomains \<le> unat a) (throwError (Fault_H.syscall_error.InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>a list s. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; True\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<not> numDomains \<le> unat a \<longrightarrow> True) and ?Q13 a list) s
 7. \<And>a list s. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; True\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<not> numDomains \<le> unat a \<longrightarrow> True) and ?Q'13 a list) s proof (prove)
goal (5 subgoals):
 1. \<And>a list rv rv'. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; rv = rv'; cs \<noteq> []\<rbrakk> \<Longrightarrow> corres (ser \<oplus> ((\<lambda>x. inv_relation x \<circ> uncurry Invocations_H.invocation.InvokeDomain) \<circ> (\<lambda>(x, y). Invocations_A.invocation.InvokeDomain x y))) (\<lambda>_. True) (\<lambda>_. True) (case fst (hd cs) of cap.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, rv) | _ \<Rightarrow> throwError $ ExceptionTypes_A.syscall_error.InvalidArgument 1) (case fst (hd cs') of capability.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, rv') | _ \<Rightarrow> throw (Fault_H.syscall_error.InvalidArgument 1))
 2. \<And>a list. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list\<rbrakk> \<Longrightarrow> \<lbrace>?Q13 a list\<rbrace> doE y <- whenE (numDomains \<le> unat a) (throwError (ExceptionTypes_A.syscall_error.InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>a list. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list\<rbrakk> \<Longrightarrow> \<lbrace>?Q'13 a list\<rbrace> doE y <- whenE (numDomains \<le> unat a) (throwError (Fault_H.syscall_error.InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>a list s. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; True\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<not> numDomains \<le> unat a \<longrightarrow> True) and ?Q13 a list) s
 5. \<And>a list s. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; True\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<not> numDomains \<le> unat a \<longrightarrow> True) and ?Q'13 a list) s proof (prove)
goal (6 subgoals):
 1. \<And>a list rv rv'. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; rv = rv'; cs \<noteq> []; cap_relation (fst (hd cs)) (fst (hd cs'))\<rbrakk> \<Longrightarrow> corres (ser \<oplus> ((\<lambda>x. inv_relation x \<circ> uncurry Invocations_H.invocation.InvokeDomain) \<circ> (\<lambda>(x, y). Invocations_A.invocation.InvokeDomain x y))) (\<lambda>_. True) (\<lambda>_. True) (case fst (hd cs) of cap.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, rv) | _ \<Rightarrow> throwError $ ExceptionTypes_A.syscall_error.InvalidArgument 1) (case fst (hd cs') of capability.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, rv') | _ \<Rightarrow> throw (Fault_H.syscall_error.InvalidArgument 1))
 2. \<And>a list rv rv'. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; rv = rv'; cs \<noteq> []\<rbrakk> \<Longrightarrow> cap_relation (fst (hd cs)) (fst (hd cs'))
 3. \<And>a list. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list\<rbrakk> \<Longrightarrow> \<lbrace>?Q13 a list\<rbrace> doE y <- whenE (numDomains \<le> unat a) (throwError (ExceptionTypes_A.syscall_error.InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>a list. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list\<rbrakk> \<Longrightarrow> \<lbrace>?Q'13 a list\<rbrace> doE y <- whenE (numDomains \<le> unat a) (throwError (Fault_H.syscall_error.InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>a list s. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; True\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<not> numDomains \<le> unat a \<longrightarrow> True) and ?Q13 a list) s
 6. \<And>a list s. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; True\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<not> numDomains \<le> unat a \<longrightarrow> True) and ?Q'13 a list) s proof (prove)
goal (17 subgoals):
 1. \<And>a list rv rv'. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; rv = rv'; cs \<noteq> []; cap_relation (fst (hd cs)) (fst (hd cs')); fst (hd cs) = cap.NullCap\<rbrakk> \<Longrightarrow> corres (ser \<oplus> ((\<lambda>x. inv_relation x \<circ> uncurry Invocations_H.invocation.InvokeDomain) \<circ> (\<lambda>(x, y). Invocations_A.invocation.InvokeDomain x y))) (\<lambda>_. True) (\<lambda>_. True) (case fst (hd cs) of cap.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, rv) | _ \<Rightarrow> throwError $ ExceptionTypes_A.syscall_error.InvalidArgument 1) (case fst (hd cs') of capability.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, rv') | _ \<Rightarrow> throw (Fault_H.syscall_error.InvalidArgument 1))
 2. \<And>a list rv rv' x21 x22 x23 x24. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; rv = rv'; cs \<noteq> []; cap_relation (fst (hd cs)) (fst (hd cs')); fst (hd cs) = cap.UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> corres (ser \<oplus> ((\<lambda>x. inv_relation x \<circ> uncurry Invocations_H.invocation.InvokeDomain) \<circ> (\<lambda>(x, y). Invocations_A.invocation.InvokeDomain x y))) (\<lambda>_. True) (\<lambda>_. True) (case fst (hd cs) of cap.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, rv) | _ \<Rightarrow> throwError $ ExceptionTypes_A.syscall_error.InvalidArgument 1) (case fst (hd cs') of capability.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, rv') | _ \<Rightarrow> throw (Fault_H.syscall_error.InvalidArgument 1))
 3. \<And>a list rv rv' x31 x32 x33. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; rv = rv'; cs \<noteq> []; cap_relation (fst (hd cs)) (fst (hd cs')); fst (hd cs) = cap.EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> corres (ser \<oplus> ((\<lambda>x. inv_relation x \<circ> uncurry Invocations_H.invocation.InvokeDomain) \<circ> (\<lambda>(x, y). Invocations_A.invocation.InvokeDomain x y))) (\<lambda>_. True) (\<lambda>_. True) (case fst (hd cs) of cap.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, rv) | _ \<Rightarrow> throwError $ ExceptionTypes_A.syscall_error.InvalidArgument 1) (case fst (hd cs') of capability.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, rv') | _ \<Rightarrow> throw (Fault_H.syscall_error.InvalidArgument 1))
 4. \<And>a list rv rv' x41 x42 x43. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; rv = rv'; cs \<noteq> []; cap_relation (fst (hd cs)) (fst (hd cs')); fst (hd cs) = cap.NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> corres (ser \<oplus> ((\<lambda>x. inv_relation x \<circ> uncurry Invocations_H.invocation.InvokeDomain) \<circ> (\<lambda>(x, y). Invocations_A.invocation.InvokeDomain x y))) (\<lambda>_. True) (\<lambda>_. True) (case fst (hd cs) of cap.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, rv) | _ \<Rightarrow> throwError $ ExceptionTypes_A.syscall_error.InvalidArgument 1) (case fst (hd cs') of capability.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, rv') | _ \<Rightarrow> throw (Fault_H.syscall_error.InvalidArgument 1))
 5. \<And>a list rv rv' x51 x52 x53. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; rv = rv'; cs \<noteq> []; cap_relation (fst (hd cs)) (fst (hd cs')); fst (hd cs) = cap.ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> corres (ser \<oplus> ((\<lambda>x. inv_relation x \<circ> uncurry Invocations_H.invocation.InvokeDomain) \<circ> (\<lambda>(x, y). Invocations_A.invocation.InvokeDomain x y))) (\<lambda>_. True) (\<lambda>_. True) (case fst (hd cs) of cap.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, rv) | _ \<Rightarrow> throwError $ ExceptionTypes_A.syscall_error.InvalidArgument 1) (case fst (hd cs') of capability.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, rv') | _ \<Rightarrow> throw (Fault_H.syscall_error.InvalidArgument 1))
 6. \<And>a list rv rv' x61 x62 x63. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; rv = rv'; cs \<noteq> []; cap_relation (fst (hd cs)) (fst (hd cs')); fst (hd cs) = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> corres (ser \<oplus> ((\<lambda>x. inv_relation x \<circ> uncurry Invocations_H.invocation.InvokeDomain) \<circ> (\<lambda>(x, y). Invocations_A.invocation.InvokeDomain x y))) (\<lambda>_. True) (\<lambda>_. True) (case fst (hd cs) of cap.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, rv) | _ \<Rightarrow> throwError $ ExceptionTypes_A.syscall_error.InvalidArgument 1) (case fst (hd cs') of capability.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, rv') | _ \<Rightarrow> throw (Fault_H.syscall_error.InvalidArgument 1))
 7. \<And>a list rv rv' x7. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; rv = rv'; cs \<noteq> []; cap_relation (fst (hd cs)) (fst (hd cs')); fst (hd cs) = cap.ThreadCap x7\<rbrakk> \<Longrightarrow> corres (ser \<oplus> ((\<lambda>x. inv_relation x \<circ> uncurry Invocations_H.invocation.InvokeDomain) \<circ> (\<lambda>(x, y). Invocations_A.invocation.InvokeDomain x y))) (\<lambda>_. True) (\<lambda>_. True) (case fst (hd cs) of cap.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, rv) | _ \<Rightarrow> throwError $ ExceptionTypes_A.syscall_error.InvalidArgument 1) (case fst (hd cs') of capability.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, rv') | _ \<Rightarrow> throw (Fault_H.syscall_error.InvalidArgument 1))
 8. \<And>a list rv rv'. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; rv = rv'; cs \<noteq> []; cap_relation (fst (hd cs)) (fst (hd cs')); fst (hd cs) = cap.DomainCap\<rbrakk> \<Longrightarrow> corres (ser \<oplus> ((\<lambda>x. inv_relation x \<circ> uncurry Invocations_H.invocation.InvokeDomain) \<circ> (\<lambda>(x, y). Invocations_A.invocation.InvokeDomain x y))) (\<lambda>_. True) (\<lambda>_. True) (case fst (hd cs) of cap.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, rv) | _ \<Rightarrow> throwError $ ExceptionTypes_A.syscall_error.InvalidArgument 1) (case fst (hd cs') of capability.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, rv') | _ \<Rightarrow> throw (Fault_H.syscall_error.InvalidArgument 1))
 9. \<And>a list rv rv'. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; rv = rv'; cs \<noteq> []; cap_relation (fst (hd cs)) (fst (hd cs')); fst (hd cs) = cap.IRQControlCap\<rbrakk> \<Longrightarrow> corres (ser \<oplus> ((\<lambda>x. inv_relation x \<circ> uncurry Invocations_H.invocation.InvokeDomain) \<circ> (\<lambda>(x, y). Invocations_A.invocation.InvokeDomain x y))) (\<lambda>_. True) (\<lambda>_. True) (case fst (hd cs) of cap.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, rv) | _ \<Rightarrow> throwError $ ExceptionTypes_A.syscall_error.InvalidArgument 1) (case fst (hd cs') of capability.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, rv') | _ \<Rightarrow> throw (Fault_H.syscall_error.InvalidArgument 1))
 10. \<And>a list rv rv' x10. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; rv = rv'; cs \<noteq> []; cap_relation (fst (hd cs)) (fst (hd cs')); fst (hd cs) = cap.IRQHandlerCap x10\<rbrakk> \<Longrightarrow> corres (ser \<oplus> ((\<lambda>x. inv_relation x \<circ> uncurry Invocations_H.invocation.InvokeDomain) \<circ> (\<lambda>(x, y). Invocations_A.invocation.InvokeDomain x y))) (\<lambda>_. True) (\<lambda>_. True) (case fst (hd cs) of cap.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, rv) | _ \<Rightarrow> throwError $ ExceptionTypes_A.syscall_error.InvalidArgument 1) (case fst (hd cs') of capability.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, rv') | _ \<Rightarrow> throw (Fault_H.syscall_error.InvalidArgument 1))
A total of 17 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>a list rv rv' x7. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; rv = rv'; cs \<noteq> []; fst (hd cs') = capability.ThreadCap x7; fst (hd cs) = cap.ThreadCap x7\<rbrakk> \<Longrightarrow> ((\<lambda>x. inv_relation x \<circ> uncurry Invocations_H.invocation.InvokeDomain) \<circ> (\<lambda>(x, y). Invocations_A.invocation.InvokeDomain x y)) (x7, rv') (x7, rv')
 2. \<And>a list rv rv'. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; rv = rv'; cs \<noteq> []; cap_relation (fst (hd cs)) (fst (hd cs')); fst (hd cs) = cap.DomainCap\<rbrakk> \<Longrightarrow> corres (ser \<oplus> ((\<lambda>x. inv_relation x \<circ> uncurry Invocations_H.invocation.InvokeDomain) \<circ> (\<lambda>(x, y). Invocations_A.invocation.InvokeDomain x y))) (\<lambda>_. True) (\<lambda>_. True) (case fst (hd cs) of cap.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, rv) | _ \<Rightarrow> throwError $ ExceptionTypes_A.syscall_error.InvalidArgument 1) (case fst (hd cs') of capability.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, rv') | _ \<Rightarrow> throw (Fault_H.syscall_error.InvalidArgument 1))
 3. \<And>a list rv rv'. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; rv = rv'; cs \<noteq> []; cap_relation (fst (hd cs)) (fst (hd cs')); fst (hd cs) = cap.IRQControlCap\<rbrakk> \<Longrightarrow> corres (ser \<oplus> ((\<lambda>x. inv_relation x \<circ> uncurry Invocations_H.invocation.InvokeDomain) \<circ> (\<lambda>(x, y). Invocations_A.invocation.InvokeDomain x y))) (\<lambda>_. True) (\<lambda>_. True) (case fst (hd cs) of cap.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, rv) | _ \<Rightarrow> throwError $ ExceptionTypes_A.syscall_error.InvalidArgument 1) (case fst (hd cs') of capability.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, rv') | _ \<Rightarrow> throw (Fault_H.syscall_error.InvalidArgument 1))
 4. \<And>a list rv rv' x10. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; rv = rv'; cs \<noteq> []; cap_relation (fst (hd cs)) (fst (hd cs')); fst (hd cs) = cap.IRQHandlerCap x10\<rbrakk> \<Longrightarrow> corres (ser \<oplus> ((\<lambda>x. inv_relation x \<circ> uncurry Invocations_H.invocation.InvokeDomain) \<circ> (\<lambda>(x, y). Invocations_A.invocation.InvokeDomain x y))) (\<lambda>_. True) (\<lambda>_. True) (case fst (hd cs) of cap.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, rv) | _ \<Rightarrow> throwError $ ExceptionTypes_A.syscall_error.InvalidArgument 1) (case fst (hd cs') of capability.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, rv') | _ \<Rightarrow> throw (Fault_H.syscall_error.InvalidArgument 1))
 5. \<And>a list rv rv' x111 x112 x113. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; rv = rv'; cs \<noteq> []; cap_relation (fst (hd cs)) (fst (hd cs')); fst (hd cs) = cap.Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> corres (ser \<oplus> ((\<lambda>x. inv_relation x \<circ> uncurry Invocations_H.invocation.InvokeDomain) \<circ> (\<lambda>(x, y). Invocations_A.invocation.InvokeDomain x y))) (\<lambda>_. True) (\<lambda>_. True) (case fst (hd cs) of cap.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, rv) | _ \<Rightarrow> throwError $ ExceptionTypes_A.syscall_error.InvalidArgument 1) (case fst (hd cs') of capability.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, rv') | _ \<Rightarrow> throw (Fault_H.syscall_error.InvalidArgument 1))
 6. \<And>a list rv rv' x12. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; rv = rv'; cs \<noteq> []; cap_relation (fst (hd cs)) (fst (hd cs')); fst (hd cs) = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> corres (ser \<oplus> ((\<lambda>x. inv_relation x \<circ> uncurry Invocations_H.invocation.InvokeDomain) \<circ> (\<lambda>(x, y). Invocations_A.invocation.InvokeDomain x y))) (\<lambda>_. True) (\<lambda>_. True) (case fst (hd cs) of cap.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, rv) | _ \<Rightarrow> throwError $ ExceptionTypes_A.syscall_error.InvalidArgument 1) (case fst (hd cs') of capability.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, rv') | _ \<Rightarrow> throw (Fault_H.syscall_error.InvalidArgument 1))
 7. \<And>a list rv rv'. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; rv = rv'; cs \<noteq> []\<rbrakk> \<Longrightarrow> cap_relation (fst (hd cs)) (fst (hd cs'))
 8. \<And>a list. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list\<rbrakk> \<Longrightarrow> \<lbrace>?Q13 a list\<rbrace> doE y <- whenE (numDomains \<le> unat a) (throwError (ExceptionTypes_A.syscall_error.InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 9. \<And>a list. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list\<rbrakk> \<Longrightarrow> \<lbrace>?Q'13 a list\<rbrace> doE y <- whenE (numDomains \<le> unat a) (throwError (Fault_H.syscall_error.InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 10. \<And>a list s. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; True\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<not> numDomains \<le> unat a \<longrightarrow> True) and ?Q13 a list) s
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>a list rv rv'. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; rv = rv'; cs \<noteq> []; cap_relation (fst (hd cs)) (fst (hd cs')); fst (hd cs) = cap.DomainCap\<rbrakk> \<Longrightarrow> corres (ser \<oplus> ((\<lambda>x. inv_relation x \<circ> uncurry Invocations_H.invocation.InvokeDomain) \<circ> (\<lambda>(x, y). Invocations_A.invocation.InvokeDomain x y))) (\<lambda>_. True) (\<lambda>_. True) (case fst (hd cs) of cap.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, rv) | _ \<Rightarrow> throwError $ ExceptionTypes_A.syscall_error.InvalidArgument 1) (case fst (hd cs') of capability.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, rv') | _ \<Rightarrow> throw (Fault_H.syscall_error.InvalidArgument 1))
 2. \<And>a list rv rv'. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; rv = rv'; cs \<noteq> []; cap_relation (fst (hd cs)) (fst (hd cs')); fst (hd cs) = cap.IRQControlCap\<rbrakk> \<Longrightarrow> corres (ser \<oplus> ((\<lambda>x. inv_relation x \<circ> uncurry Invocations_H.invocation.InvokeDomain) \<circ> (\<lambda>(x, y). Invocations_A.invocation.InvokeDomain x y))) (\<lambda>_. True) (\<lambda>_. True) (case fst (hd cs) of cap.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, rv) | _ \<Rightarrow> throwError $ ExceptionTypes_A.syscall_error.InvalidArgument 1) (case fst (hd cs') of capability.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, rv') | _ \<Rightarrow> throw (Fault_H.syscall_error.InvalidArgument 1))
 3. \<And>a list rv rv' x10. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; rv = rv'; cs \<noteq> []; cap_relation (fst (hd cs)) (fst (hd cs')); fst (hd cs) = cap.IRQHandlerCap x10\<rbrakk> \<Longrightarrow> corres (ser \<oplus> ((\<lambda>x. inv_relation x \<circ> uncurry Invocations_H.invocation.InvokeDomain) \<circ> (\<lambda>(x, y). Invocations_A.invocation.InvokeDomain x y))) (\<lambda>_. True) (\<lambda>_. True) (case fst (hd cs) of cap.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, rv) | _ \<Rightarrow> throwError $ ExceptionTypes_A.syscall_error.InvalidArgument 1) (case fst (hd cs') of capability.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, rv') | _ \<Rightarrow> throw (Fault_H.syscall_error.InvalidArgument 1))
 4. \<And>a list rv rv' x111 x112 x113. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; rv = rv'; cs \<noteq> []; cap_relation (fst (hd cs)) (fst (hd cs')); fst (hd cs) = cap.Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> corres (ser \<oplus> ((\<lambda>x. inv_relation x \<circ> uncurry Invocations_H.invocation.InvokeDomain) \<circ> (\<lambda>(x, y). Invocations_A.invocation.InvokeDomain x y))) (\<lambda>_. True) (\<lambda>_. True) (case fst (hd cs) of cap.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, rv) | _ \<Rightarrow> throwError $ ExceptionTypes_A.syscall_error.InvalidArgument 1) (case fst (hd cs') of capability.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, rv') | _ \<Rightarrow> throw (Fault_H.syscall_error.InvalidArgument 1))
 5. \<And>a list rv rv' x12. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; rv = rv'; cs \<noteq> []; cap_relation (fst (hd cs)) (fst (hd cs')); fst (hd cs) = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> corres (ser \<oplus> ((\<lambda>x. inv_relation x \<circ> uncurry Invocations_H.invocation.InvokeDomain) \<circ> (\<lambda>(x, y). Invocations_A.invocation.InvokeDomain x y))) (\<lambda>_. True) (\<lambda>_. True) (case fst (hd cs) of cap.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, rv) | _ \<Rightarrow> throwError $ ExceptionTypes_A.syscall_error.InvalidArgument 1) (case fst (hd cs') of capability.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, rv') | _ \<Rightarrow> throw (Fault_H.syscall_error.InvalidArgument 1))
 6. \<And>a list rv rv'. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; rv = rv'; cs \<noteq> []\<rbrakk> \<Longrightarrow> cap_relation (fst (hd cs)) (fst (hd cs'))
 7. \<And>a list. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list\<rbrakk> \<Longrightarrow> \<lbrace>?Q13 a list\<rbrace> doE y <- whenE (numDomains \<le> unat a) (throwError (ExceptionTypes_A.syscall_error.InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 8. \<And>a list. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list\<rbrakk> \<Longrightarrow> \<lbrace>?Q'13 a list\<rbrace> doE y <- whenE (numDomains \<le> unat a) (throwError (Fault_H.syscall_error.InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 9. \<And>a list s. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; True\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<not> numDomains \<le> unat a \<longrightarrow> True) and ?Q13 a list) s
 10. \<And>a list s. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; True\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<not> numDomains \<le> unat a \<longrightarrow> True) and ?Q'13 a list) s proof (prove)
goal (5 subgoals):
 1. \<And>a list rv rv'. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; rv = rv'; cs \<noteq> []\<rbrakk> \<Longrightarrow> cap_relation (fst (hd cs)) (fst (hd cs'))
 2. \<And>a list. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list\<rbrakk> \<Longrightarrow> \<lbrace>?Q13 a list\<rbrace> doE y <- whenE (numDomains \<le> unat a) (throwError (ExceptionTypes_A.syscall_error.InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>a list. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list\<rbrakk> \<Longrightarrow> \<lbrace>?Q'13 a list\<rbrace> doE y <- whenE (numDomains \<le> unat a) (throwError (Fault_H.syscall_error.InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>a list s. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; True\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<not> numDomains \<le> unat a \<longrightarrow> True) and ?Q13 a list) s
 5. \<And>a list s. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; True\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<not> numDomains \<le> unat a \<longrightarrow> True) and ?Q'13 a list) s proof (prove)
goal (6 subgoals):
 1. \<And>a list rv rv'. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; rv = rv'; cs \<noteq> []; cs = []\<rbrakk> \<Longrightarrow> cap_relation (fst (hd cs)) (fst (hd cs'))
 2. \<And>a list rv rv' aa lista. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; rv = rv'; cs \<noteq> []; cs = aa # lista\<rbrakk> \<Longrightarrow> cap_relation (fst (hd cs)) (fst (hd cs'))
 3. \<And>a list. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list\<rbrakk> \<Longrightarrow> \<lbrace>?Q13 a list\<rbrace> doE y <- whenE (numDomains \<le> unat a) (throwError (ExceptionTypes_A.syscall_error.InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>a list. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list\<rbrakk> \<Longrightarrow> \<lbrace>?Q'13 a list\<rbrace> doE y <- whenE (numDomains \<le> unat a) (throwError (Fault_H.syscall_error.InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>a list s. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; True\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<not> numDomains \<le> unat a \<longrightarrow> True) and ?Q13 a list) s
 6. \<And>a list s. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; True\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<not> numDomains \<le> unat a \<longrightarrow> True) and ?Q'13 a list) s proof (prove)
goal (5 subgoals):
 1. \<And>a list rv rv' aa lista. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; rv = rv'; cs \<noteq> []; cs = aa # lista\<rbrakk> \<Longrightarrow> cap_relation (fst (hd cs)) (fst (hd cs'))
 2. \<And>a list. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list\<rbrakk> \<Longrightarrow> \<lbrace>?Q13 a list\<rbrace> doE y <- whenE (numDomains \<le> unat a) (throwError (ExceptionTypes_A.syscall_error.InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>a list. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list\<rbrakk> \<Longrightarrow> \<lbrace>?Q'13 a list\<rbrace> doE y <- whenE (numDomains \<le> unat a) (throwError (Fault_H.syscall_error.InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>a list s. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; True\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<not> numDomains \<le> unat a \<longrightarrow> True) and ?Q13 a list) s
 5. \<And>a list s. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; True\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<not> numDomains \<le> unat a \<longrightarrow> True) and ?Q'13 a list) s proof (prove)
goal (4 subgoals):
 1. \<And>a list. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list\<rbrakk> \<Longrightarrow> \<lbrace>?Q13 a list\<rbrace> doE y <- whenE (numDomains \<le> unat a) (throwError (ExceptionTypes_A.syscall_error.InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>a list. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list\<rbrakk> \<Longrightarrow> \<lbrace>?Q'13 a list\<rbrace> doE y <- whenE (numDomains \<le> unat a) (throwError (Fault_H.syscall_error.InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>a list s. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; True\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<not> numDomains \<le> unat a \<longrightarrow> True) and ?Q13 a list) s
 4. \<And>a list s. \<lbrakk>list_all2 cap_relation (map fst cs) (map fst cs'); list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs'; gen_invocation_type label = DomainSetSet; args = a # list; True\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<not> numDomains \<le> unat a \<longrightarrow> True) and ?Q'13 a list) s proof (prove)
goal:
No subgoals!