theory Tcb_R

lemma decodeSetSpaceSome[wp]:
  "\<lbrace>\<top>\<rbrace> decodeSetSpace xs cap y zs
   \<lbrace>\<lambda>rv s. tcNewCRoot rv \<noteq> None\<rbrace>,-" apply (simp add: decodeSetSpace_def split_def cap_CNode_case_throw
             cong: list.case_cong if_cong del: not_None_eq) apply (rule hoare_pre) apply (wp hoare_drop_imps | wpcw
             | simp only: tcbinvocation.sel option.simps)+ apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> decodeSetSpace xs cap y zs \<lbrace>\<lambda>rv s. tcNewCRoot rv \<noteq> None\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> case xs of [] \<Rightarrow> throwError Fault_H.syscall_error.TruncatedMessage | [faultEP] \<Rightarrow> throwError Fault_H.syscall_error.TruncatedMessage | [faultEP, cRootData] \<Rightarrow> throwError Fault_H.syscall_error.TruncatedMessage | faultEP # cRootData # vRootData # x \<Rightarrow> case zs of [] \<Rightarrow> throwError Fault_H.syscall_error.TruncatedMessage | [cRootArg] \<Rightarrow> throwError Fault_H.syscall_error.TruncatedMessage | cRootArg # vRootArg # xa \<Rightarrow> doE canChangeCRoot <- liftE (liftM Not (getThreadCSpaceRoot (capTCBPtr cap) >>= slotCapLongRunningDelete));
canChangeVRoot <- liftE (liftM Not (getThreadVSpaceRoot (capTCBPtr cap) >>= slotCapLongRunningDelete));
ya <- unlessE (canChangeCRoot \<and> canChangeVRoot) (throwError Fault_H.syscall_error.IllegalOperation);
cRootCap' <- global.deriveCap (snd cRootArg) (if cRootData = 0 then fst cRootArg else global.updateCapData False cRootData (fst cRootArg));
cRoot <- doE y <- unlessE (isCNodeCap cRootCap') (throwError Fault_H.syscall_error.IllegalOperation);
returnOk (cRootCap', snd cRootArg)
odE;
vRootCap' <- global.deriveCap (snd vRootArg) (if vRootData = 0 then fst vRootArg else global.updateCapData False vRootData (fst vRootArg));
vRoot <- if isValidVTableRoot vRootCap' then returnOk (vRootCap', snd vRootArg) else throwError Fault_H.syscall_error.IllegalOperation;
returnOk (tcbinvocation.ThreadControl (capTCBPtr cap) y (Some faultEP) None None (Some cRoot) (Some vRoot) None)
odE \<lbrace>\<lambda>rv s. tcNewCRoot rv \<noteq> None\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'23\<rbrace> case xs of [] \<Rightarrow> throwError Fault_H.syscall_error.TruncatedMessage | [faultEP] \<Rightarrow> throwError Fault_H.syscall_error.TruncatedMessage | [faultEP, cRootData] \<Rightarrow> throwError Fault_H.syscall_error.TruncatedMessage | faultEP # cRootData # vRootData # x \<Rightarrow> case zs of [] \<Rightarrow> throwError Fault_H.syscall_error.TruncatedMessage | [cRootArg] \<Rightarrow> throwError Fault_H.syscall_error.TruncatedMessage | cRootArg # vRootArg # xa \<Rightarrow> doE canChangeCRoot <- liftE (liftM Not (getThreadCSpaceRoot (capTCBPtr cap) >>= slotCapLongRunningDelete));
canChangeVRoot <- liftE (liftM Not (getThreadVSpaceRoot (capTCBPtr cap) >>= slotCapLongRunningDelete));
ya <- unlessE (canChangeCRoot \<and> canChangeVRoot) (throwError Fault_H.syscall_error.IllegalOperation);
cRootCap' <- global.deriveCap (snd cRootArg) (if cRootData = 0 then fst cRootArg else global.updateCapData False cRootData (fst cRootArg));
cRoot <- doE y <- unlessE (isCNodeCap cRootCap') (throwError Fault_H.syscall_error.IllegalOperation);
returnOk (cRootCap', snd cRootArg)
odE;
vRootCap' <- global.deriveCap (snd vRootArg) (if vRootData = 0 then fst vRootArg else global.updateCapData False vRootData (fst vRootArg));
vRoot <- if isValidVTableRoot vRootCap' then returnOk (vRootCap', snd vRootArg) else throwError Fault_H.syscall_error.IllegalOperation;
returnOk (tcbinvocation.ThreadControl (capTCBPtr cap) y (Some faultEP) None None (Some cRoot) (Some vRoot) None)
odE \<lbrace>\<lambda>rv s. tcNewCRoot rv \<noteq> None\<rbrace>, -
 2. \<And>s. True \<Longrightarrow> ?P'23 s proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> True \<and> (\<forall>x xa. True \<and> (\<forall>x xa. True \<and> (\<forall>x xa. True \<and> (\<forall>x xa. True \<and> (\<forall>x xa. True \<and> True \<and> True \<and> True \<and> True \<and> True \<and> True \<and> \<not> False \<and> True))))) proof (prove)
goal:
No subgoals!