theory Tcb_R

lemma decodeSetSchedParams_corres:
  "\<lbrakk> cap_relation cap cap'; is_thread_cap cap;
     list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) extras extras' \<rbrakk> \<Longrightarrow>
   corres (ser \<oplus> tcbinv_relation)
       (cur_tcb and valid_etcbs and (\<lambda>s. \<forall>x \<in> set extras. s \<turnstile> (fst x)))
       (invs' and (\<lambda>s. \<forall>x \<in> set extras'. s \<turnstile>' (fst x)))
       (decode_set_sched_params args cap slot extras)
       (decodeSetSchedParams args cap' extras')" apply (simp add: decode_set_sched_params_def decodeSetSchedParams_def) apply (cases "length args < 2") apply (clarsimp split: list.split) apply (cases "length extras < 1") apply (clarsimp split: list.split simp: list_all2_Cons2) apply (clarsimp simp: list_all2_Cons1 neq_Nil_conv val_le_length_Cons linorder_not_less) apply (rule corres_split_eqrE) apply corresKsimp apply (rule corres_split_norE[OF checkPrio_corres]) apply (rule corres_splitEE[OF checkPrio_corres]) apply (rule corres_returnOkTT) apply (clarsimp simp: newroot_rel_def elim!: is_thread_cap.elims(2)) apply (wpsimp wp: check_prio_inv checkPrio_inv
                   simp: valid_cap_def valid_cap'_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) extras extras'\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (cur_tcb and valid_etcbs and (\<lambda>s. \<forall>x\<in>set extras. s \<turnstile> fst x)) (invs' and (\<lambda>s. \<forall>x\<in>set extras'. valid_cap' (fst x) s)) (decode_set_sched_params args cap slot extras) (decodeSetSchedParams args cap' extras') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) extras extras'\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (cur_tcb and valid_etcbs and (\<lambda>s. \<forall>x\<in>set extras. s \<turnstile> fst x)) (invs' and (\<lambda>s. \<forall>x\<in>set extras'. valid_cap' (fst x) s)) (doE y <- whenE (length args < 2) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage);
y <- whenE (extras = []) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage);
auth_tcb <- case fst (extras ! 0) of cap.ThreadCap x \<Rightarrow> returnOk x | _ \<Rightarrow> throwError (ExceptionTypes_A.syscall_error.InvalidCapability 1);
y <- check_prio (args ! 0) auth_tcb;
y <- check_prio (args ! Suc 0) auth_tcb;
returnOk (tcb_invocation.ThreadControl (obj_ref_of cap) slot None (Some (UCAST(32 \<rightarrow> 8) (args ! 0), auth_tcb)) (Some (UCAST(32 \<rightarrow> 8) (args ! Suc 0), auth_tcb)) None None None)
odE) (case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [newMCP] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | newMCP # newPrio # xa \<Rightarrow> case extras' of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (authCap, xa) # xb \<Rightarrow> doE authTCB <- case authCap of capability.ThreadCap x \<Rightarrow> returnOk x | _ \<Rightarrow> throw $ Fault_H.syscall_error.InvalidCapability 1;
checkPrio newMCP authTCB;
checkPrio newPrio authTCB;
returnOk $ tcbinvocation.ThreadControl (capTCBPtr cap') 0 Nothing (Just $ (fromIntegral newMCP, authTCB)) (Just $ (fromIntegral newPrio, authTCB)) Nothing Nothing Nothing
odE) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) extras extras'; length args < 2\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (cur_tcb and valid_etcbs and (\<lambda>s. \<forall>x\<in>set extras. s \<turnstile> fst x)) (invs' and (\<lambda>s. \<forall>x\<in>set extras'. valid_cap' (fst x) s)) (doE y <- whenE (length args < 2) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage);
y <- whenE (extras = []) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage);
auth_tcb <- case fst (extras ! 0) of cap.ThreadCap x \<Rightarrow> returnOk x | _ \<Rightarrow> throwError (ExceptionTypes_A.syscall_error.InvalidCapability 1);
y <- check_prio (args ! 0) auth_tcb;
y <- check_prio (args ! Suc 0) auth_tcb;
returnOk (tcb_invocation.ThreadControl (obj_ref_of cap) slot None (Some (UCAST(32 \<rightarrow> 8) (args ! 0), auth_tcb)) (Some (UCAST(32 \<rightarrow> 8) (args ! Suc 0), auth_tcb)) None None None)
odE) (case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [newMCP] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | newMCP # newPrio # xa \<Rightarrow> case extras' of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (authCap, xa) # xb \<Rightarrow> doE authTCB <- case authCap of capability.ThreadCap x \<Rightarrow> returnOk x | _ \<Rightarrow> throw $ Fault_H.syscall_error.InvalidCapability 1;
checkPrio newMCP authTCB;
checkPrio newPrio authTCB;
returnOk $ tcbinvocation.ThreadControl (capTCBPtr cap') 0 Nothing (Just $ (fromIntegral newMCP, authTCB)) (Just $ (fromIntegral newPrio, authTCB)) Nothing Nothing Nothing
odE)
 2. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) extras extras'; \<not> length args < 2\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (cur_tcb and valid_etcbs and (\<lambda>s. \<forall>x\<in>set extras. s \<turnstile> fst x)) (invs' and (\<lambda>s. \<forall>x\<in>set extras'. valid_cap' (fst x) s)) (doE y <- whenE (length args < 2) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage);
y <- whenE (extras = []) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage);
auth_tcb <- case fst (extras ! 0) of cap.ThreadCap x \<Rightarrow> returnOk x | _ \<Rightarrow> throwError (ExceptionTypes_A.syscall_error.InvalidCapability 1);
y <- check_prio (args ! 0) auth_tcb;
y <- check_prio (args ! Suc 0) auth_tcb;
returnOk (tcb_invocation.ThreadControl (obj_ref_of cap) slot None (Some (UCAST(32 \<rightarrow> 8) (args ! 0), auth_tcb)) (Some (UCAST(32 \<rightarrow> 8) (args ! Suc 0), auth_tcb)) None None None)
odE) (case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [newMCP] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | newMCP # newPrio # xa \<Rightarrow> case extras' of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (authCap, xa) # xb \<Rightarrow> doE authTCB <- case authCap of capability.ThreadCap x \<Rightarrow> returnOk x | _ \<Rightarrow> throw $ Fault_H.syscall_error.InvalidCapability 1;
checkPrio newMCP authTCB;
checkPrio newPrio authTCB;
returnOk $ tcbinvocation.ThreadControl (capTCBPtr cap') 0 Nothing (Just $ (fromIntegral newMCP, authTCB)) (Just $ (fromIntegral newPrio, authTCB)) Nothing Nothing Nothing
odE) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) extras extras'; \<not> length args < 2\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (cur_tcb and valid_etcbs and (\<lambda>s. \<forall>x\<in>set extras. s \<turnstile> fst x)) (invs' and (\<lambda>s. \<forall>x\<in>set extras'. valid_cap' (fst x) s)) (doE y <- whenE (length args < 2) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage);
y <- whenE (extras = []) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage);
auth_tcb <- case fst (extras ! 0) of cap.ThreadCap x \<Rightarrow> returnOk x | _ \<Rightarrow> throwError (ExceptionTypes_A.syscall_error.InvalidCapability 1);
y <- check_prio (args ! 0) auth_tcb;
y <- check_prio (args ! Suc 0) auth_tcb;
returnOk (tcb_invocation.ThreadControl (obj_ref_of cap) slot None (Some (UCAST(32 \<rightarrow> 8) (args ! 0), auth_tcb)) (Some (UCAST(32 \<rightarrow> 8) (args ! Suc 0), auth_tcb)) None None None)
odE) (case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [newMCP] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | newMCP # newPrio # xa \<Rightarrow> case extras' of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (authCap, xa) # xb \<Rightarrow> doE authTCB <- case authCap of capability.ThreadCap x \<Rightarrow> returnOk x | _ \<Rightarrow> throw $ Fault_H.syscall_error.InvalidCapability 1;
checkPrio newMCP authTCB;
checkPrio newPrio authTCB;
returnOk $ tcbinvocation.ThreadControl (capTCBPtr cap') 0 Nothing (Just $ (fromIntegral newMCP, authTCB)) (Just $ (fromIntegral newPrio, authTCB)) Nothing Nothing Nothing
odE) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) extras extras'; \<not> length args < 2; length extras < 1\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (cur_tcb and valid_etcbs and (\<lambda>s. \<forall>x\<in>set extras. s \<turnstile> fst x)) (invs' and (\<lambda>s. \<forall>x\<in>set extras'. valid_cap' (fst x) s)) (doE y <- whenE (length args < 2) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage);
y <- whenE (extras = []) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage);
auth_tcb <- case fst (extras ! 0) of cap.ThreadCap x \<Rightarrow> returnOk x | _ \<Rightarrow> throwError (ExceptionTypes_A.syscall_error.InvalidCapability 1);
y <- check_prio (args ! 0) auth_tcb;
y <- check_prio (args ! Suc 0) auth_tcb;
returnOk (tcb_invocation.ThreadControl (obj_ref_of cap) slot None (Some (UCAST(32 \<rightarrow> 8) (args ! 0), auth_tcb)) (Some (UCAST(32 \<rightarrow> 8) (args ! Suc 0), auth_tcb)) None None None)
odE) (case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [newMCP] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | newMCP # newPrio # xa \<Rightarrow> case extras' of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (authCap, xa) # xb \<Rightarrow> doE authTCB <- case authCap of capability.ThreadCap x \<Rightarrow> returnOk x | _ \<Rightarrow> throw $ Fault_H.syscall_error.InvalidCapability 1;
checkPrio newMCP authTCB;
checkPrio newPrio authTCB;
returnOk $ tcbinvocation.ThreadControl (capTCBPtr cap') 0 Nothing (Just $ (fromIntegral newMCP, authTCB)) (Just $ (fromIntegral newPrio, authTCB)) Nothing Nothing Nothing
odE)
 2. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) extras extras'; \<not> length args < 2; \<not> length extras < 1\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (cur_tcb and valid_etcbs and (\<lambda>s. \<forall>x\<in>set extras. s \<turnstile> fst x)) (invs' and (\<lambda>s. \<forall>x\<in>set extras'. valid_cap' (fst x) s)) (doE y <- whenE (length args < 2) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage);
y <- whenE (extras = []) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage);
auth_tcb <- case fst (extras ! 0) of cap.ThreadCap x \<Rightarrow> returnOk x | _ \<Rightarrow> throwError (ExceptionTypes_A.syscall_error.InvalidCapability 1);
y <- check_prio (args ! 0) auth_tcb;
y <- check_prio (args ! Suc 0) auth_tcb;
returnOk (tcb_invocation.ThreadControl (obj_ref_of cap) slot None (Some (UCAST(32 \<rightarrow> 8) (args ! 0), auth_tcb)) (Some (UCAST(32 \<rightarrow> 8) (args ! Suc 0), auth_tcb)) None None None)
odE) (case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [newMCP] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | newMCP # newPrio # xa \<Rightarrow> case extras' of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (authCap, xa) # xb \<Rightarrow> doE authTCB <- case authCap of capability.ThreadCap x \<Rightarrow> returnOk x | _ \<Rightarrow> throw $ Fault_H.syscall_error.InvalidCapability 1;
checkPrio newMCP authTCB;
checkPrio newPrio authTCB;
returnOk $ tcbinvocation.ThreadControl (capTCBPtr cap') 0 Nothing (Just $ (fromIntegral newMCP, authTCB)) (Just $ (fromIntegral newPrio, authTCB)) Nothing Nothing Nothing
odE) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) extras extras'; \<not> length args < 2; \<not> length extras < 1\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (cur_tcb and valid_etcbs and (\<lambda>s. \<forall>x\<in>set extras. s \<turnstile> fst x)) (invs' and (\<lambda>s. \<forall>x\<in>set extras'. valid_cap' (fst x) s)) (doE y <- whenE (length args < 2) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage);
y <- whenE (extras = []) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage);
auth_tcb <- case fst (extras ! 0) of cap.ThreadCap x \<Rightarrow> returnOk x | _ \<Rightarrow> throwError (ExceptionTypes_A.syscall_error.InvalidCapability 1);
y <- check_prio (args ! 0) auth_tcb;
y <- check_prio (args ! Suc 0) auth_tcb;
returnOk (tcb_invocation.ThreadControl (obj_ref_of cap) slot None (Some (UCAST(32 \<rightarrow> 8) (args ! 0), auth_tcb)) (Some (UCAST(32 \<rightarrow> 8) (args ! Suc 0), auth_tcb)) None None None)
odE) (case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [newMCP] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | newMCP # newPrio # xa \<Rightarrow> case extras' of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (authCap, xa) # xb \<Rightarrow> doE authTCB <- case authCap of capability.ThreadCap x \<Rightarrow> returnOk x | _ \<Rightarrow> throw $ Fault_H.syscall_error.InvalidCapability 1;
checkPrio newMCP authTCB;
checkPrio newPrio authTCB;
returnOk $ tcbinvocation.ThreadControl (capTCBPtr cap') 0 Nothing (Just $ (fromIntegral newMCP, authTCB)) (Just $ (fromIntegral newPrio, authTCB)) Nothing Nothing Nothing
odE) proof (prove)
goal (1 subgoal):
 1. \<And>y a aa b ysa ya ysb ab zs. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; extras = (a, aa, b) # ysa; args = y # ya # ysb; extras' = (ab, cte_map (aa, b)) # zs; cap_relation a ab; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) ysa zs\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (cur_tcb and valid_etcbs and (\<lambda>s. s \<turnstile> a \<and> (\<forall>x\<in>set ysa. s \<turnstile> fst x))) (invs' and (\<lambda>s. valid_cap' ab s \<and> (\<forall>x\<in>set zs. valid_cap' (fst x) s))) (doE auth_tcb <- case a of cap.ThreadCap x \<Rightarrow> returnOk x | _ \<Rightarrow> throwError (ExceptionTypes_A.syscall_error.InvalidCapability 1);
yb <- check_prio y auth_tcb;
yb <- check_prio ya auth_tcb;
returnOk (tcb_invocation.ThreadControl (obj_ref_of cap) slot None (Some (UCAST(32 \<rightarrow> 8) y, auth_tcb)) (Some (UCAST(32 \<rightarrow> 8) ya, auth_tcb)) None None None)
odE) (doE authTCB <- case ab of capability.ThreadCap x \<Rightarrow> returnOk x | _ \<Rightarrow> throw $ Fault_H.syscall_error.InvalidCapability 1;
yb <- checkPrio y authTCB;
yb <- checkPrio ya authTCB;
returnOk (tcbinvocation.ThreadControl (capTCBPtr cap') 0 None (Some (UCAST(32 \<rightarrow> 8) y, authTCB)) (Some (UCAST(32 \<rightarrow> 8) ya, authTCB)) None None None)
odE) proof (prove)
goal (4 subgoals):
 1. \<And>y a aa b ysa ya ysb ab zs. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; extras = (a, aa, b) # ysa; args = y # ya # ysb; extras' = (ab, cte_map (aa, b)) # zs; cap_relation a ab; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) ysa zs\<rbrakk> \<Longrightarrow> corres (ser \<oplus> (=)) (cur_tcb and valid_etcbs) invs' (case a of cap.ThreadCap x \<Rightarrow> returnOk x | _ \<Rightarrow> throwError (ExceptionTypes_A.syscall_error.InvalidCapability 1)) (case ab of capability.ThreadCap x \<Rightarrow> returnOk x | _ \<Rightarrow> throw $ Fault_H.syscall_error.InvalidCapability 1)
 2. \<And>y a aa b ysa ya ysb ab zs auth_tcb. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; extras = (a, aa, b) # ysa; args = y # ya # ysb; extras' = (ab, cte_map (aa, b)) # zs; cap_relation a ab; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) ysa zs\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (?R75 y a aa b ysa ya ysb ab zs auth_tcb) (?R'75 y a aa b ysa ya ysb ab zs auth_tcb) (doE yb <- check_prio y auth_tcb;
yb <- check_prio ya auth_tcb;
returnOk (tcb_invocation.ThreadControl (obj_ref_of cap) slot None (Some (UCAST(32 \<rightarrow> 8) y, auth_tcb)) (Some (UCAST(32 \<rightarrow> 8) ya, auth_tcb)) None None None)
odE) (doE yb <- checkPrio y auth_tcb;
yb <- checkPrio ya auth_tcb;
returnOk (tcbinvocation.ThreadControl (capTCBPtr cap') 0 None (Some (UCAST(32 \<rightarrow> 8) y, auth_tcb)) (Some (UCAST(32 \<rightarrow> 8) ya, auth_tcb)) None None None)
odE)
 3. \<And>y a aa b ysa ya ysb ab zs. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; extras = (a, aa, b) # ysa; args = y # ya # ysb; extras' = (ab, cte_map (aa, b)) # zs; cap_relation a ab; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) ysa zs\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. s \<turnstile> a \<and> (\<forall>x\<in>set ysa. s \<turnstile> fst x)\<rbrace> case a of cap.ThreadCap x \<Rightarrow> returnOk x | _ \<Rightarrow> throwError (ExceptionTypes_A.syscall_error.InvalidCapability 1) \<lbrace>?R75 y a aa b ysa ya ysb ab zs\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>y a aa b ysa ya ysb ab zs. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; extras = (a, aa, b) # ysa; args = y # ya # ysb; extras' = (ab, cte_map (aa, b)) # zs; cap_relation a ab; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) ysa zs\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. valid_cap' ab s \<and> (\<forall>x\<in>set zs. valid_cap' (fst x) s)\<rbrace> case ab of capability.ThreadCap x \<Rightarrow> returnOk x | _ \<Rightarrow> throw $ Fault_H.syscall_error.InvalidCapability 1 \<lbrace>?R'75 y a aa b ysa ya ysb ab zs\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>y a aa b ysa ya ysb ab zs auth_tcb. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; extras = (a, aa, b) # ysa; args = y # ya # ysb; extras' = (ab, cte_map (aa, b)) # zs; cap_relation a ab; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) ysa zs\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (?R75 y a aa b ysa ya ysb ab zs auth_tcb) (?R'75 y a aa b ysa ya ysb ab zs auth_tcb) (doE yb <- check_prio y auth_tcb;
yb <- check_prio ya auth_tcb;
returnOk (tcb_invocation.ThreadControl (obj_ref_of cap) slot None (Some (UCAST(32 \<rightarrow> 8) y, auth_tcb)) (Some (UCAST(32 \<rightarrow> 8) ya, auth_tcb)) None None None)
odE) (doE yb <- checkPrio y auth_tcb;
yb <- checkPrio ya auth_tcb;
returnOk (tcbinvocation.ThreadControl (capTCBPtr cap') 0 None (Some (UCAST(32 \<rightarrow> 8) y, auth_tcb)) (Some (UCAST(32 \<rightarrow> 8) ya, auth_tcb)) None None None)
odE)
 2. \<And>y a aa b ysa ya ysb ab zs. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; extras = (a, aa, b) # ysa; args = y # ya # ysb; extras' = (ab, cte_map (aa, b)) # zs; cap_relation a ab; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) ysa zs\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. s \<turnstile> a \<and> (\<forall>x\<in>set ysa. s \<turnstile> fst x)\<rbrace> case a of cap.ThreadCap x \<Rightarrow> returnOk x | _ \<Rightarrow> throwError (ExceptionTypes_A.syscall_error.InvalidCapability 1) \<lbrace>?R75 y a aa b ysa ya ysb ab zs\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>y a aa b ysa ya ysb ab zs. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; extras = (a, aa, b) # ysa; args = y # ya # ysb; extras' = (ab, cte_map (aa, b)) # zs; cap_relation a ab; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) ysa zs\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. valid_cap' ab s \<and> (\<forall>x\<in>set zs. valid_cap' (fst x) s)\<rbrace> case ab of capability.ThreadCap x \<Rightarrow> returnOk x | _ \<Rightarrow> throw $ Fault_H.syscall_error.InvalidCapability 1 \<lbrace>?R'75 y a aa b ysa ya ysb ab zs\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>y a aa b ysa ya ysb ab zs auth_tcb. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; extras = (a, aa, b) # ysa; args = y # ya # ysb; extras' = (ab, cte_map (aa, b)) # zs; cap_relation a ab; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) ysa zs\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (?R7955 y a aa b ysa ya ysb ab zs auth_tcb) (?R'7955 y a aa b ysa ya ysb ab zs auth_tcb) (doE yb <- check_prio ya auth_tcb;
returnOk (tcb_invocation.ThreadControl (obj_ref_of cap) slot None (Some (UCAST(32 \<rightarrow> 8) y, auth_tcb)) (Some (UCAST(32 \<rightarrow> 8) ya, auth_tcb)) None None None)
odE) (doE yb <- checkPrio ya auth_tcb;
returnOk (tcbinvocation.ThreadControl (capTCBPtr cap') 0 None (Some (UCAST(32 \<rightarrow> 8) y, auth_tcb)) (Some (UCAST(32 \<rightarrow> 8) ya, auth_tcb)) None None None)
odE)
 2. \<And>y a aa b ysa ya ysb ab zs auth_tcb. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; extras = (a, aa, b) # ysa; args = y # ya # ysb; extras' = (ab, cte_map (aa, b)) # zs; cap_relation a ab; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) ysa zs\<rbrakk> \<Longrightarrow> \<lbrace>?Q7955 y a aa b ysa ya ysb ab zs auth_tcb\<rbrace> check_prio y auth_tcb \<lbrace>\<lambda>x. ?R7955 y a aa b ysa ya ysb ab zs auth_tcb\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>y a aa b ysa ya ysb ab zs auth_tcb. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; extras = (a, aa, b) # ysa; args = y # ya # ysb; extras' = (ab, cte_map (aa, b)) # zs; cap_relation a ab; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) ysa zs\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7955 y a aa b ysa ya ysb ab zs auth_tcb\<rbrace> checkPrio y auth_tcb \<lbrace>\<lambda>x. ?R'7955 y a aa b ysa ya ysb ab zs auth_tcb\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>y a aa b ysa ya ysb ab zs. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; extras = (a, aa, b) # ysa; args = y # ya # ysb; extras' = (ab, cte_map (aa, b)) # zs; cap_relation a ab; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) ysa zs\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. s \<turnstile> a \<and> (\<forall>x\<in>set ysa. s \<turnstile> fst x)\<rbrace> case a of cap.ThreadCap x \<Rightarrow> returnOk x | _ \<Rightarrow> throwError (ExceptionTypes_A.syscall_error.InvalidCapability 1) \<lbrace>\<lambda>auth_tcb. tcb_at auth_tcb and ?Q7955 y a aa b ysa ya ysb ab zs auth_tcb\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>y a aa b ysa ya ysb ab zs. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; extras = (a, aa, b) # ysa; args = y # ya # ysb; extras' = (ab, cte_map (aa, b)) # zs; cap_relation a ab; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) ysa zs\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. valid_cap' ab s \<and> (\<forall>x\<in>set zs. valid_cap' (fst x) s)\<rbrace> case ab of capability.ThreadCap x \<Rightarrow> returnOk x | _ \<Rightarrow> throw $ Fault_H.syscall_error.InvalidCapability 1 \<lbrace>\<lambda>auth_tcb. tcb_at' auth_tcb and ?Q'7955 y a aa b ysa ya ysb ab zs auth_tcb\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>y a aa b ysa ya ysb ab zs auth_tcb yb yc. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; extras = (a, aa, b) # ysa; args = y # ya # ysb; extras' = (ab, cte_map (aa, b)) # zs; cap_relation a ab; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) ysa zs; dc yb yc\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (?R7960 y a aa b ysa ya ysb ab zs auth_tcb yb) (?R'7960 y a aa b ysa ya ysb ab zs auth_tcb yc) (returnOk (tcb_invocation.ThreadControl (obj_ref_of cap) slot None (Some (UCAST(32 \<rightarrow> 8) y, auth_tcb)) (Some (UCAST(32 \<rightarrow> 8) ya, auth_tcb)) None None None)) (returnOk (tcbinvocation.ThreadControl (capTCBPtr cap') 0 None (Some (UCAST(32 \<rightarrow> 8) y, auth_tcb)) (Some (UCAST(32 \<rightarrow> 8) ya, auth_tcb)) None None None))
 2. \<And>y a aa b ysa ya ysb ab zs auth_tcb. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; extras = (a, aa, b) # ysa; args = y # ya # ysb; extras' = (ab, cte_map (aa, b)) # zs; cap_relation a ab; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) ysa zs\<rbrakk> \<Longrightarrow> \<lbrace>?Q7960 y a aa b ysa ya ysb ab zs auth_tcb\<rbrace> check_prio ya auth_tcb \<lbrace>?R7960 y a aa b ysa ya ysb ab zs auth_tcb\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>y a aa b ysa ya ysb ab zs auth_tcb. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; extras = (a, aa, b) # ysa; args = y # ya # ysb; extras' = (ab, cte_map (aa, b)) # zs; cap_relation a ab; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) ysa zs\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7960 y a aa b ysa ya ysb ab zs auth_tcb\<rbrace> checkPrio ya auth_tcb \<lbrace>?R'7960 y a aa b ysa ya ysb ab zs auth_tcb\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>y a aa b ysa ya ysb ab zs auth_tcb. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; extras = (a, aa, b) # ysa; args = y # ya # ysb; extras' = (ab, cte_map (aa, b)) # zs; cap_relation a ab; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) ysa zs\<rbrakk> \<Longrightarrow> \<lbrace>?Q7955 y a aa b ysa ya ysb ab zs auth_tcb\<rbrace> check_prio y auth_tcb \<lbrace>\<lambda>x. tcb_at auth_tcb and ?Q7960 y a aa b ysa ya ysb ab zs auth_tcb\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>y a aa b ysa ya ysb ab zs auth_tcb. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; extras = (a, aa, b) # ysa; args = y # ya # ysb; extras' = (ab, cte_map (aa, b)) # zs; cap_relation a ab; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) ysa zs\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7955 y a aa b ysa ya ysb ab zs auth_tcb\<rbrace> checkPrio y auth_tcb \<lbrace>\<lambda>x. tcb_at' auth_tcb and ?Q'7960 y a aa b ysa ya ysb ab zs auth_tcb\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>y a aa b ysa ya ysb ab zs. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; extras = (a, aa, b) # ysa; args = y # ya # ysb; extras' = (ab, cte_map (aa, b)) # zs; cap_relation a ab; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) ysa zs\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. s \<turnstile> a \<and> (\<forall>x\<in>set ysa. s \<turnstile> fst x)\<rbrace> case a of cap.ThreadCap x \<Rightarrow> returnOk x | _ \<Rightarrow> throwError (ExceptionTypes_A.syscall_error.InvalidCapability 1) \<lbrace>\<lambda>auth_tcb. tcb_at auth_tcb and ?Q7955 y a aa b ysa ya ysb ab zs auth_tcb\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>y a aa b ysa ya ysb ab zs. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; extras = (a, aa, b) # ysa; args = y # ya # ysb; extras' = (ab, cte_map (aa, b)) # zs; cap_relation a ab; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) ysa zs\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. valid_cap' ab s \<and> (\<forall>x\<in>set zs. valid_cap' (fst x) s)\<rbrace> case ab of capability.ThreadCap x \<Rightarrow> returnOk x | _ \<Rightarrow> throw $ Fault_H.syscall_error.InvalidCapability 1 \<lbrace>\<lambda>auth_tcb. tcb_at' auth_tcb and ?Q'7955 y a aa b ysa ya ysb ab zs auth_tcb\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>y a aa b ysa ya ysb ab zs auth_tcb yb yc. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; extras = (a, aa, b) # ysa; args = y # ya # ysb; extras' = (ab, cte_map (aa, b)) # zs; cap_relation a ab; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) ysa zs; dc yb yc\<rbrakk> \<Longrightarrow> tcbinv_relation (tcb_invocation.ThreadControl (obj_ref_of cap) slot None (Some (UCAST(32 \<rightarrow> 8) y, auth_tcb)) (Some (UCAST(32 \<rightarrow> 8) ya, auth_tcb)) None None None) (tcbinvocation.ThreadControl (capTCBPtr cap') 0 None (Some (UCAST(32 \<rightarrow> 8) y, auth_tcb)) (Some (UCAST(32 \<rightarrow> 8) ya, auth_tcb)) None None None)
 2. \<And>y a aa b ysa ya ysb ab zs auth_tcb. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; extras = (a, aa, b) # ysa; args = y # ya # ysb; extras' = (ab, cte_map (aa, b)) # zs; cap_relation a ab; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) ysa zs\<rbrakk> \<Longrightarrow> \<lbrace>?Q7960 y a aa b ysa ya ysb ab zs auth_tcb\<rbrace> check_prio ya auth_tcb \<lbrace>\<lambda>yb _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>y a aa b ysa ya ysb ab zs auth_tcb. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; extras = (a, aa, b) # ysa; args = y # ya # ysb; extras' = (ab, cte_map (aa, b)) # zs; cap_relation a ab; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) ysa zs\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7960 y a aa b ysa ya ysb ab zs auth_tcb\<rbrace> checkPrio ya auth_tcb \<lbrace>\<lambda>yc _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>y a aa b ysa ya ysb ab zs auth_tcb. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; extras = (a, aa, b) # ysa; args = y # ya # ysb; extras' = (ab, cte_map (aa, b)) # zs; cap_relation a ab; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) ysa zs\<rbrakk> \<Longrightarrow> \<lbrace>?Q7955 y a aa b ysa ya ysb ab zs auth_tcb\<rbrace> check_prio y auth_tcb \<lbrace>\<lambda>x. tcb_at auth_tcb and ?Q7960 y a aa b ysa ya ysb ab zs auth_tcb\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>y a aa b ysa ya ysb ab zs auth_tcb. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; extras = (a, aa, b) # ysa; args = y # ya # ysb; extras' = (ab, cte_map (aa, b)) # zs; cap_relation a ab; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) ysa zs\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7955 y a aa b ysa ya ysb ab zs auth_tcb\<rbrace> checkPrio y auth_tcb \<lbrace>\<lambda>x. tcb_at' auth_tcb and ?Q'7960 y a aa b ysa ya ysb ab zs auth_tcb\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>y a aa b ysa ya ysb ab zs. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; extras = (a, aa, b) # ysa; args = y # ya # ysb; extras' = (ab, cte_map (aa, b)) # zs; cap_relation a ab; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) ysa zs\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. s \<turnstile> a \<and> (\<forall>x\<in>set ysa. s \<turnstile> fst x)\<rbrace> case a of cap.ThreadCap x \<Rightarrow> returnOk x | _ \<Rightarrow> throwError (ExceptionTypes_A.syscall_error.InvalidCapability 1) \<lbrace>\<lambda>auth_tcb. tcb_at auth_tcb and ?Q7955 y a aa b ysa ya ysb ab zs auth_tcb\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>y a aa b ysa ya ysb ab zs. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; extras = (a, aa, b) # ysa; args = y # ya # ysb; extras' = (ab, cte_map (aa, b)) # zs; cap_relation a ab; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) ysa zs\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. valid_cap' ab s \<and> (\<forall>x\<in>set zs. valid_cap' (fst x) s)\<rbrace> case ab of capability.ThreadCap x \<Rightarrow> returnOk x | _ \<Rightarrow> throw $ Fault_H.syscall_error.InvalidCapability 1 \<lbrace>\<lambda>auth_tcb. tcb_at' auth_tcb and ?Q'7955 y a aa b ysa ya ysb ab zs auth_tcb\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>y a aa b ysa ya ysb ab zs auth_tcb. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; extras = (a, aa, b) # ysa; args = y # ya # ysb; extras' = (ab, cte_map (aa, b)) # zs; cap_relation a ab; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) ysa zs\<rbrakk> \<Longrightarrow> \<lbrace>?Q7960 y a aa b ysa ya ysb ab zs auth_tcb\<rbrace> check_prio ya auth_tcb \<lbrace>\<lambda>yb _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>y a aa b ysa ya ysb ab zs auth_tcb. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; extras = (a, aa, b) # ysa; args = y # ya # ysb; extras' = (ab, cte_map (aa, b)) # zs; cap_relation a ab; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) ysa zs\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7960 y a aa b ysa ya ysb ab zs auth_tcb\<rbrace> checkPrio ya auth_tcb \<lbrace>\<lambda>yc _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>y a aa b ysa ya ysb ab zs auth_tcb. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; extras = (a, aa, b) # ysa; args = y # ya # ysb; extras' = (ab, cte_map (aa, b)) # zs; cap_relation a ab; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) ysa zs\<rbrakk> \<Longrightarrow> \<lbrace>?Q7955 y a aa b ysa ya ysb ab zs auth_tcb\<rbrace> check_prio y auth_tcb \<lbrace>\<lambda>x. tcb_at auth_tcb and ?Q7960 y a aa b ysa ya ysb ab zs auth_tcb\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>y a aa b ysa ya ysb ab zs auth_tcb. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; extras = (a, aa, b) # ysa; args = y # ya # ysb; extras' = (ab, cte_map (aa, b)) # zs; cap_relation a ab; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) ysa zs\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7955 y a aa b ysa ya ysb ab zs auth_tcb\<rbrace> checkPrio y auth_tcb \<lbrace>\<lambda>x. tcb_at' auth_tcb and ?Q'7960 y a aa b ysa ya ysb ab zs auth_tcb\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>y a aa b ysa ya ysb ab zs. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; extras = (a, aa, b) # ysa; args = y # ya # ysb; extras' = (ab, cte_map (aa, b)) # zs; cap_relation a ab; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) ysa zs\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. s \<turnstile> a \<and> (\<forall>x\<in>set ysa. s \<turnstile> fst x)\<rbrace> case a of cap.ThreadCap x \<Rightarrow> returnOk x | _ \<Rightarrow> throwError (ExceptionTypes_A.syscall_error.InvalidCapability 1) \<lbrace>\<lambda>auth_tcb. tcb_at auth_tcb and ?Q7955 y a aa b ysa ya ysb ab zs auth_tcb\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>y a aa b ysa ya ysb ab zs. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; extras = (a, aa, b) # ysa; args = y # ya # ysb; extras' = (ab, cte_map (aa, b)) # zs; cap_relation a ab; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) ysa zs\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. valid_cap' ab s \<and> (\<forall>x\<in>set zs. valid_cap' (fst x) s)\<rbrace> case ab of capability.ThreadCap x \<Rightarrow> returnOk x | _ \<Rightarrow> throw $ Fault_H.syscall_error.InvalidCapability 1 \<lbrace>\<lambda>auth_tcb. tcb_at' auth_tcb and ?Q'7955 y a aa b ysa ya ysb ab zs auth_tcb\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal:
No subgoals!