theory Tcb_R

lemma decodeSetSpace_wf[wp]:
  "\<lbrace>invs' and tcb_at' t and ex_nonz_cap_to' t and cte_at' slot
      and (\<lambda>s. \<forall>x \<in> set extras. s \<turnstile>' fst x \<and> cte_at' (snd x) s \<and> t \<noteq> snd x \<and> t + 16 \<noteq> snd x)\<rbrace>
     decodeSetSpace args (ThreadCap t) slot extras
   \<lbrace>tcb_inv_wf'\<rbrace>,-" apply (simp       add: decodeSetSpace_def Let_def split_def
                         unlessE_def getThreadVSpaceRoot getThreadCSpaceRoot
                         cap_CNode_case_throw
              split del: if_split cong: if_cong list.case_cong) apply (rule hoare_pre) apply (wp
             | simp    add: o_def split_def
                 split del: if_split
             | wpc
             | rule hoare_drop_imps)+ apply (clarsimp simp del: length_greater_0_conv
                 split del: if_split) apply (simp del: length_greater_0_conv add: valid_updateCapDataI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and tcb_at' t and ex_nonz_cap_to' t and cte_wp_at' (\<lambda>_. True) slot and (\<lambda>s. \<forall>x\<in>set extras. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s \<and> t \<noteq> snd x \<and> t + 0x10 \<noteq> snd x)\<rbrace> decodeSetSpace args (capability.ThreadCap t) slot extras \<lbrace>tcb_inv_wf'\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and tcb_at' t and ex_nonz_cap_to' t and cte_wp_at' (\<lambda>_. True) slot and (\<lambda>s. \<forall>x\<in>set extras. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s \<and> t \<noteq> snd x \<and> t + 0x10 \<noteq> snd x)\<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 t));
canChangeVRoot <- liftE (liftM Not (slotCapLongRunningDelete (t + 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 <- doE y <- if isCNodeCap cRootCap' then returnOk () else 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 t slot (Some faultEP) None None (Some cRoot) (Some vRoot) None)
odE \<lbrace>tcb_inv_wf'\<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 t));
canChangeVRoot <- liftE (liftM Not (slotCapLongRunningDelete (t + 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 <- doE y <- if isCNodeCap cRootCap' then returnOk () else 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 t slot (Some faultEP) None None (Some cRoot) (Some vRoot) None)
odE \<lbrace>tcb_inv_wf'\<rbrace>, -
 2. \<And>s. (invs' and tcb_at' t and ex_nonz_cap_to' t and cte_wp_at' (\<lambda>_. True) slot and (\<lambda>s. \<forall>x\<in>set extras. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s \<and> t \<noteq> snd x \<and> t + 0x10 \<noteq> snd x)) s \<Longrightarrow> ?P'23 s proof (prove)
goal (1 subgoal):
 1. \<And>s. invs' s \<and> tcb_at' t s \<and> ex_nonz_cap_to' t s \<and> cte_wp_at' (\<lambda>_. True) slot s \<and> (\<forall>x\<in>set extras. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s \<and> t \<noteq> snd x \<and> t + 0x10 \<noteq> snd x) \<Longrightarrow> \<forall>x xa. args = x # xa \<longrightarrow> (\<forall>x xb. xa = x # xb \<longrightarrow> (\<forall>xa. (\<exists>x. xb = xa # x) \<longrightarrow> (\<forall>a b xb. extras = (a, b) # xb \<longrightarrow> (\<forall>aa. (\<exists>b x. xb = (aa, b) # x) \<longrightarrow> valid_cap' (if x = 0 then a else global.updateCapData False x a) s \<and> valid_cap' (if xa = 0 then aa else global.updateCapData False xa aa) s)))) proof (prove)
goal (1 subgoal):
 1. \<And>s x xb xd xe a b aa ba xg. \<lbrakk>invs' s; tcb_at' t s; ex_nonz_cap_to' t s; cte_wp_at' (\<lambda>_. True) slot s; args = x # xb # xd # xe; extras = (a, b) # (aa, ba) # xg; valid_cap' a s; cte_wp_at' (\<lambda>_. True) b s; t \<noteq> b; t + 0x10 \<noteq> b; valid_cap' aa s; cte_wp_at' (\<lambda>_. True) ba s; t \<noteq> ba; t + 0x10 \<noteq> ba; \<forall>x\<in>set xg. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s \<and> t \<noteq> snd x \<and> t + 0x10 \<noteq> snd x\<rbrakk> \<Longrightarrow> valid_cap' (if xb = 0 then a else global.updateCapData False xb a) s \<and> valid_cap' (if xd = 0 then aa else global.updateCapData False xd aa) s proof (prove)
goal:
No subgoals!