theory Tcb_R

lemma decodeSetSpace_is_tc[wp]:
  "\<lbrace>\<top>\<rbrace> decodeSetSpace args cap slot extras \<lbrace>\<lambda>rv s. isThreadControl rv\<rbrace>,-" apply (simp       add: decodeSetSpace_def Let_def split_def
                         unlessE_def getThreadVSpaceRoot getThreadCSpaceRoot
              split del: if_split cong: list.case_cong) apply (rule hoare_pre) apply (wp hoare_drop_imps
           | simp only: isThreadControl_def tcbinvocation.simps
           | wpcw)+ apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> decodeSetSpace args cap slot extras \<lbrace>\<lambda>rv s. isThreadControl rv\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> case args 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 extras 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 (slotCapLongRunningDelete (capTCBPtr cap)));
canChangeVRoot <- liftE (liftM Not (slotCapLongRunningDelete (capTCBPtr cap + 2 ^ cteSizeBits)));
y <- if canChangeCRoot \<and> canChangeVRoot then returnOk () else 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 <- case cRootCap' of capability.CNodeCap x xa xb xc \<Rightarrow> returnOk (cRootCap', snd cRootArg) | _ \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation;
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) slot (Some faultEP) None None (Some cRoot) (Some vRoot) None)
odE \<lbrace>\<lambda>rv s. isThreadControl rv\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'23\<rbrace> case args 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 extras 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 (slotCapLongRunningDelete (capTCBPtr cap)));
canChangeVRoot <- liftE (liftM Not (slotCapLongRunningDelete (capTCBPtr cap + 2 ^ cteSizeBits)));
y <- if canChangeCRoot \<and> canChangeVRoot then returnOk () else 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 <- case cRootCap' of capability.CNodeCap x xa xb xc \<Rightarrow> returnOk (cRootCap', snd cRootArg) | _ \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation;
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) slot (Some faultEP) None None (Some cRoot) (Some vRoot) None)
odE \<lbrace>\<lambda>rv s. isThreadControl rv\<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> True \<and> True))))) proof (prove)
goal:
No subgoals!