theory Tcb_R

lemma decodeSetSpace_inv[wp]:
  "\<lbrace>P\<rbrace> decodeSetSpace args cap slot extras \<lbrace>\<lambda>rv. P\<rbrace>" apply (simp       add: decodeSetSpace_def Let_def split_def
                         unlessE_def getThreadVSpaceRoot getThreadCSpaceRoot
              split del: if_split cong: if_cong list.case_cong) apply (rule hoare_pre) apply (wp hoare_drop_imps
            | simp add: o_def split_def split del: if_split
            | wpcw)+ done

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