theory Tcb_R

lemma decodeSetSpace_tc_slot[wp]:
  "\<lbrace>\<lambda>s. P slot\<rbrace> decodeSetSpace args cap slot extras \<lbrace>\<lambda>rv s. P (tcThreadCapSlot rv)\<rbrace>,-" apply (simp add: decodeSetSpace_def split_def unlessE_def
                   getThreadVSpaceRoot getThreadCSpaceRoot
             cong: list.case_cong) apply (rule hoare_pre) apply (wp hoare_drop_imps | wpcw | simp only: tcbinvocation.sel)+ apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P slot\<rbrace> decodeSetSpace args cap slot extras \<lbrace>\<lambda>rv s. P (tcThreadCapSlot rv)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P slot\<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. P (tcThreadCapSlot 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. P (tcThreadCapSlot rv)\<rbrace>, -
 2. \<And>s. P slot \<Longrightarrow> ?P'23 s proof (prove)
goal (1 subgoal):
 1. \<And>s. P slot \<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!