theory Tcb_R

lemma decodeSetMCPriority_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_mcpriority args cap slot extras)
       (decodeSetMCPriority args cap' extras')" apply (cases args; cases extras; cases extras';
         clarsimp simp: decode_set_mcpriority_def decodeSetMCPriority_def) apply (rename_tac auth_cap auth_slot auth_path rest auth_cap' rest') apply (rule corres_split_eqrE) apply corresKsimp 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 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_mcpriority args cap slot extras) (decodeSetMCPriority args cap' extras') proof (prove)
goal (1 subgoal):
 1. \<And>a list aa ab b lista ac listb. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = a # list; extras = (aa, ab, b) # lista; extras' = (ac, cte_map (ab, b)) # listb; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) lista listb; cap_relation aa ac\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (cur_tcb and valid_etcbs and (\<lambda>s. s \<turnstile> aa \<and> (\<forall>x\<in>set lista. s \<turnstile> fst x))) (invs' and (\<lambda>s. valid_cap' ac s \<and> (\<forall>x\<in>set listb. valid_cap' (fst x) s))) (doE auth_tcb <- case aa of cap.ThreadCap x \<Rightarrow> returnOk x | _ \<Rightarrow> throwError (ExceptionTypes_A.syscall_error.InvalidCapability 1);
y <- check_prio a auth_tcb;
returnOk (tcb_invocation.ThreadControl (obj_ref_of cap) slot None (Some (UCAST(32 \<rightarrow> 8) a, auth_tcb)) None None None None)
odE) (doE authTCB <- case ac of capability.ThreadCap x \<Rightarrow> returnOk x | _ \<Rightarrow> throw $ Fault_H.syscall_error.InvalidCapability 1;
y <- checkPrio a authTCB;
returnOk (tcbinvocation.ThreadControl (capTCBPtr cap') 0 None (Some (UCAST(32 \<rightarrow> 8) a, authTCB)) None None None None)
odE) proof (prove)
goal (1 subgoal):
 1. \<And>a list auth_cap auth_slot auth_path rest auth_cap' rest'. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = a # list; extras = (auth_cap, auth_slot, auth_path) # rest; extras' = (auth_cap', cte_map (auth_slot, auth_path)) # rest'; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) rest rest'; cap_relation auth_cap auth_cap'\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (cur_tcb and valid_etcbs and (\<lambda>s. s \<turnstile> auth_cap \<and> (\<forall>x\<in>set rest. s \<turnstile> fst x))) (invs' and (\<lambda>s. valid_cap' auth_cap' s \<and> (\<forall>x\<in>set rest'. valid_cap' (fst x) s))) (doE auth_tcb <- case auth_cap of cap.ThreadCap x \<Rightarrow> returnOk x | _ \<Rightarrow> throwError (ExceptionTypes_A.syscall_error.InvalidCapability 1);
y <- check_prio a auth_tcb;
returnOk (tcb_invocation.ThreadControl (obj_ref_of cap) slot None (Some (UCAST(32 \<rightarrow> 8) a, auth_tcb)) None None None None)
odE) (doE authTCB <- case auth_cap' of capability.ThreadCap x \<Rightarrow> returnOk x | _ \<Rightarrow> throw $ Fault_H.syscall_error.InvalidCapability 1;
y <- checkPrio a authTCB;
returnOk (tcbinvocation.ThreadControl (capTCBPtr cap') 0 None (Some (UCAST(32 \<rightarrow> 8) a, authTCB)) None None None None)
odE) proof (prove)
goal (4 subgoals):
 1. \<And>a list auth_cap auth_slot auth_path rest auth_cap' rest'. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = a # list; extras = (auth_cap, auth_slot, auth_path) # rest; extras' = (auth_cap', cte_map (auth_slot, auth_path)) # rest'; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) rest rest'; cap_relation auth_cap auth_cap'\<rbrakk> \<Longrightarrow> corres (ser \<oplus> (=)) (cur_tcb and valid_etcbs) invs' (case auth_cap of cap.ThreadCap x \<Rightarrow> returnOk x | _ \<Rightarrow> throwError (ExceptionTypes_A.syscall_error.InvalidCapability 1)) (case auth_cap' of capability.ThreadCap x \<Rightarrow> returnOk x | _ \<Rightarrow> throw $ Fault_H.syscall_error.InvalidCapability 1)
 2. \<And>a list auth_cap auth_slot auth_path rest auth_cap' rest' auth_tcb. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = a # list; extras = (auth_cap, auth_slot, auth_path) # rest; extras' = (auth_cap', cte_map (auth_slot, auth_path)) # rest'; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) rest rest'; cap_relation auth_cap auth_cap'\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (?R40 a list auth_cap auth_slot auth_path rest auth_cap' rest' auth_tcb) (?R'40 a list auth_cap auth_slot auth_path rest auth_cap' rest' auth_tcb) (doE y <- check_prio a auth_tcb;
returnOk (tcb_invocation.ThreadControl (obj_ref_of cap) slot None (Some (UCAST(32 \<rightarrow> 8) a, auth_tcb)) None None None None)
odE) (doE y <- checkPrio a auth_tcb;
returnOk (tcbinvocation.ThreadControl (capTCBPtr cap') 0 None (Some (UCAST(32 \<rightarrow> 8) a, auth_tcb)) None None None None)
odE)
 3. \<And>a list auth_cap auth_slot auth_path rest auth_cap' rest'. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = a # list; extras = (auth_cap, auth_slot, auth_path) # rest; extras' = (auth_cap', cte_map (auth_slot, auth_path)) # rest'; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) rest rest'; cap_relation auth_cap auth_cap'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. s \<turnstile> auth_cap \<and> (\<forall>x\<in>set rest. s \<turnstile> fst x)\<rbrace> case auth_cap of cap.ThreadCap x \<Rightarrow> returnOk x | _ \<Rightarrow> throwError (ExceptionTypes_A.syscall_error.InvalidCapability 1) \<lbrace>?R40 a list auth_cap auth_slot auth_path rest auth_cap' rest'\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>a list auth_cap auth_slot auth_path rest auth_cap' rest'. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = a # list; extras = (auth_cap, auth_slot, auth_path) # rest; extras' = (auth_cap', cte_map (auth_slot, auth_path)) # rest'; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) rest rest'; cap_relation auth_cap auth_cap'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. valid_cap' auth_cap' s \<and> (\<forall>x\<in>set rest'. valid_cap' (fst x) s)\<rbrace> case auth_cap' of capability.ThreadCap x \<Rightarrow> returnOk x | _ \<Rightarrow> throw $ Fault_H.syscall_error.InvalidCapability 1 \<lbrace>?R'40 a list auth_cap auth_slot auth_path rest auth_cap' rest'\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>a list auth_cap auth_slot auth_path rest auth_cap' rest' auth_tcb. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = a # list; extras = (auth_cap, auth_slot, auth_path) # rest; extras' = (auth_cap', cte_map (auth_slot, auth_path)) # rest'; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) rest rest'; cap_relation auth_cap auth_cap'\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (?R40 a list auth_cap auth_slot auth_path rest auth_cap' rest' auth_tcb) (?R'40 a list auth_cap auth_slot auth_path rest auth_cap' rest' auth_tcb) (doE y <- check_prio a auth_tcb;
returnOk (tcb_invocation.ThreadControl (obj_ref_of cap) slot None (Some (UCAST(32 \<rightarrow> 8) a, auth_tcb)) None None None None)
odE) (doE y <- checkPrio a auth_tcb;
returnOk (tcbinvocation.ThreadControl (capTCBPtr cap') 0 None (Some (UCAST(32 \<rightarrow> 8) a, auth_tcb)) None None None None)
odE)
 2. \<And>a list auth_cap auth_slot auth_path rest auth_cap' rest'. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = a # list; extras = (auth_cap, auth_slot, auth_path) # rest; extras' = (auth_cap', cte_map (auth_slot, auth_path)) # rest'; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) rest rest'; cap_relation auth_cap auth_cap'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. s \<turnstile> auth_cap \<and> (\<forall>x\<in>set rest. s \<turnstile> fst x)\<rbrace> case auth_cap of cap.ThreadCap x \<Rightarrow> returnOk x | _ \<Rightarrow> throwError (ExceptionTypes_A.syscall_error.InvalidCapability 1) \<lbrace>?R40 a list auth_cap auth_slot auth_path rest auth_cap' rest'\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>a list auth_cap auth_slot auth_path rest auth_cap' rest'. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = a # list; extras = (auth_cap, auth_slot, auth_path) # rest; extras' = (auth_cap', cte_map (auth_slot, auth_path)) # rest'; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) rest rest'; cap_relation auth_cap auth_cap'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. valid_cap' auth_cap' s \<and> (\<forall>x\<in>set rest'. valid_cap' (fst x) s)\<rbrace> case auth_cap' of capability.ThreadCap x \<Rightarrow> returnOk x | _ \<Rightarrow> throw $ Fault_H.syscall_error.InvalidCapability 1 \<lbrace>?R'40 a list auth_cap auth_slot auth_path rest auth_cap' rest'\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>a list auth_cap auth_slot auth_path rest auth_cap' rest' auth_tcb y ya. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = a # list; extras = (auth_cap, auth_slot, auth_path) # rest; extras' = (auth_cap', cte_map (auth_slot, auth_path)) # rest'; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) rest rest'; cap_relation auth_cap auth_cap'; dc y ya\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (?R7920 a list auth_cap auth_slot auth_path rest auth_cap' rest' auth_tcb y) (?R'7920 a list auth_cap auth_slot auth_path rest auth_cap' rest' auth_tcb ya) (returnOk (tcb_invocation.ThreadControl (obj_ref_of cap) slot None (Some (UCAST(32 \<rightarrow> 8) a, auth_tcb)) None None None None)) (returnOk (tcbinvocation.ThreadControl (capTCBPtr cap') 0 None (Some (UCAST(32 \<rightarrow> 8) a, auth_tcb)) None None None None))
 2. \<And>a list auth_cap auth_slot auth_path rest auth_cap' rest' auth_tcb. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = a # list; extras = (auth_cap, auth_slot, auth_path) # rest; extras' = (auth_cap', cte_map (auth_slot, auth_path)) # rest'; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) rest rest'; cap_relation auth_cap auth_cap'\<rbrakk> \<Longrightarrow> \<lbrace>?Q7920 a list auth_cap auth_slot auth_path rest auth_cap' rest' auth_tcb\<rbrace> check_prio a auth_tcb \<lbrace>?R7920 a list auth_cap auth_slot auth_path rest auth_cap' rest' auth_tcb\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>a list auth_cap auth_slot auth_path rest auth_cap' rest' auth_tcb. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = a # list; extras = (auth_cap, auth_slot, auth_path) # rest; extras' = (auth_cap', cte_map (auth_slot, auth_path)) # rest'; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) rest rest'; cap_relation auth_cap auth_cap'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7920 a list auth_cap auth_slot auth_path rest auth_cap' rest' auth_tcb\<rbrace> checkPrio a auth_tcb \<lbrace>?R'7920 a list auth_cap auth_slot auth_path rest auth_cap' rest' auth_tcb\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>a list auth_cap auth_slot auth_path rest auth_cap' rest'. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = a # list; extras = (auth_cap, auth_slot, auth_path) # rest; extras' = (auth_cap', cte_map (auth_slot, auth_path)) # rest'; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) rest rest'; cap_relation auth_cap auth_cap'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. s \<turnstile> auth_cap \<and> (\<forall>x\<in>set rest. s \<turnstile> fst x)\<rbrace> case auth_cap of cap.ThreadCap x \<Rightarrow> returnOk x | _ \<Rightarrow> throwError (ExceptionTypes_A.syscall_error.InvalidCapability 1) \<lbrace>\<lambda>auth_tcb. tcb_at auth_tcb and ?Q7920 a list auth_cap auth_slot auth_path rest auth_cap' rest' auth_tcb\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>a list auth_cap auth_slot auth_path rest auth_cap' rest'. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = a # list; extras = (auth_cap, auth_slot, auth_path) # rest; extras' = (auth_cap', cte_map (auth_slot, auth_path)) # rest'; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) rest rest'; cap_relation auth_cap auth_cap'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. valid_cap' auth_cap' s \<and> (\<forall>x\<in>set rest'. valid_cap' (fst x) s)\<rbrace> case auth_cap' 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'7920 a list auth_cap auth_slot auth_path rest auth_cap' rest' auth_tcb\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>a list auth_cap auth_slot auth_path rest auth_cap' rest' auth_tcb y ya. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = a # list; extras = (auth_cap, auth_slot, auth_path) # rest; extras' = (auth_cap', cte_map (auth_slot, auth_path)) # rest'; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) rest rest'; cap_relation auth_cap auth_cap'; dc y ya\<rbrakk> \<Longrightarrow> tcbinv_relation (tcb_invocation.ThreadControl (obj_ref_of cap) slot None (Some (UCAST(32 \<rightarrow> 8) a, auth_tcb)) None None None None) (tcbinvocation.ThreadControl (capTCBPtr cap') 0 None (Some (UCAST(32 \<rightarrow> 8) a, auth_tcb)) None None None None)
 2. \<And>a list auth_cap auth_slot auth_path rest auth_cap' rest' auth_tcb. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = a # list; extras = (auth_cap, auth_slot, auth_path) # rest; extras' = (auth_cap', cte_map (auth_slot, auth_path)) # rest'; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) rest rest'; cap_relation auth_cap auth_cap'\<rbrakk> \<Longrightarrow> \<lbrace>?Q7920 a list auth_cap auth_slot auth_path rest auth_cap' rest' auth_tcb\<rbrace> check_prio a auth_tcb \<lbrace>\<lambda>y _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>a list auth_cap auth_slot auth_path rest auth_cap' rest' auth_tcb. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = a # list; extras = (auth_cap, auth_slot, auth_path) # rest; extras' = (auth_cap', cte_map (auth_slot, auth_path)) # rest'; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) rest rest'; cap_relation auth_cap auth_cap'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7920 a list auth_cap auth_slot auth_path rest auth_cap' rest' auth_tcb\<rbrace> checkPrio a auth_tcb \<lbrace>\<lambda>ya _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>a list auth_cap auth_slot auth_path rest auth_cap' rest'. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = a # list; extras = (auth_cap, auth_slot, auth_path) # rest; extras' = (auth_cap', cte_map (auth_slot, auth_path)) # rest'; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) rest rest'; cap_relation auth_cap auth_cap'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. s \<turnstile> auth_cap \<and> (\<forall>x\<in>set rest. s \<turnstile> fst x)\<rbrace> case auth_cap of cap.ThreadCap x \<Rightarrow> returnOk x | _ \<Rightarrow> throwError (ExceptionTypes_A.syscall_error.InvalidCapability 1) \<lbrace>\<lambda>auth_tcb. tcb_at auth_tcb and ?Q7920 a list auth_cap auth_slot auth_path rest auth_cap' rest' auth_tcb\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>a list auth_cap auth_slot auth_path rest auth_cap' rest'. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = a # list; extras = (auth_cap, auth_slot, auth_path) # rest; extras' = (auth_cap', cte_map (auth_slot, auth_path)) # rest'; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) rest rest'; cap_relation auth_cap auth_cap'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. valid_cap' auth_cap' s \<and> (\<forall>x\<in>set rest'. valid_cap' (fst x) s)\<rbrace> case auth_cap' 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'7920 a list auth_cap auth_slot auth_path rest auth_cap' rest' auth_tcb\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>a list auth_cap auth_slot auth_path rest auth_cap' rest' auth_tcb. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = a # list; extras = (auth_cap, auth_slot, auth_path) # rest; extras' = (auth_cap', cte_map (auth_slot, auth_path)) # rest'; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) rest rest'; cap_relation auth_cap auth_cap'\<rbrakk> \<Longrightarrow> \<lbrace>?Q7920 a list auth_cap auth_slot auth_path rest auth_cap' rest' auth_tcb\<rbrace> check_prio a auth_tcb \<lbrace>\<lambda>y _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>a list auth_cap auth_slot auth_path rest auth_cap' rest' auth_tcb. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = a # list; extras = (auth_cap, auth_slot, auth_path) # rest; extras' = (auth_cap', cte_map (auth_slot, auth_path)) # rest'; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) rest rest'; cap_relation auth_cap auth_cap'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7920 a list auth_cap auth_slot auth_path rest auth_cap' rest' auth_tcb\<rbrace> checkPrio a auth_tcb \<lbrace>\<lambda>ya _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>a list auth_cap auth_slot auth_path rest auth_cap' rest'. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = a # list; extras = (auth_cap, auth_slot, auth_path) # rest; extras' = (auth_cap', cte_map (auth_slot, auth_path)) # rest'; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) rest rest'; cap_relation auth_cap auth_cap'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. s \<turnstile> auth_cap \<and> (\<forall>x\<in>set rest. s \<turnstile> fst x)\<rbrace> case auth_cap of cap.ThreadCap x \<Rightarrow> returnOk x | _ \<Rightarrow> throwError (ExceptionTypes_A.syscall_error.InvalidCapability 1) \<lbrace>\<lambda>auth_tcb. tcb_at auth_tcb and ?Q7920 a list auth_cap auth_slot auth_path rest auth_cap' rest' auth_tcb\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>a list auth_cap auth_slot auth_path rest auth_cap' rest'. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = a # list; extras = (auth_cap, auth_slot, auth_path) # rest; extras' = (auth_cap', cte_map (auth_slot, auth_path)) # rest'; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) rest rest'; cap_relation auth_cap auth_cap'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. valid_cap' auth_cap' s \<and> (\<forall>x\<in>set rest'. valid_cap' (fst x) s)\<rbrace> case auth_cap' 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'7920 a list auth_cap auth_slot auth_path rest auth_cap' rest' auth_tcb\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal:
No subgoals!