theory Tcb_R

lemma decodeCopyReg_wf:
  "\<lbrace>invs' and tcb_at' t and ex_nonz_cap_to' t
       and (\<lambda>s. \<forall>x \<in> set extras. s \<turnstile>' x
                \<and> (\<forall>y \<in> zobj_refs' x. ex_nonz_cap_to' y s))\<rbrace>
     decodeCopyRegisters args (ThreadCap t) extras
   \<lbrace>tcb_inv_wf'\<rbrace>,-" apply (simp add: decodeCopyRegisters_def whenE_def decodeTransfer_def
             cong: list.case_cong capability.case_cong bool.case_cong
               split del: if_split) apply (rule hoare_pre) apply (wp | wpc)+ apply (clarsimp simp: null_def neq_Nil_conv
                        valid_cap'_def[where c="ThreadCap t" for t]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and tcb_at' t and ex_nonz_cap_to' t and (\<lambda>s. \<forall>x\<in>set extras. valid_cap' x s \<and> (\<forall>y\<in>zobj_refs' x. ex_nonz_cap_to' y s))\<rbrace> decodeCopyRegisters args (capability.ThreadCap t) 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 (\<lambda>s. \<forall>x\<in>set extras. valid_cap' x s \<and> (\<forall>y\<in>zobj_refs' x. ex_nonz_cap_to' y s))\<rbrace> case args of [] \<Rightarrow> throwError Fault_H.syscall_error.TruncatedMessage | flags # x \<Rightarrow> doE y <- if null extras then throwError Fault_H.syscall_error.TruncatedMessage else returnOk ();
srcTCB <- case hd extras of capability.ThreadCap x1 \<Rightarrow> returnOk x1 | _ \<Rightarrow> throwError (Fault_H.syscall_error.InvalidCapability (Suc 0));
returnOk (tcbinvocation.CopyRegisters t srcTCB (flags !! 0) (flags !! Suc 0) (flags !! 2) (flags !! 3) copy_register_sets.ARMNoExtraRegisters)
odE \<lbrace>tcb_inv_wf'\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'94\<rbrace> case args of [] \<Rightarrow> throwError Fault_H.syscall_error.TruncatedMessage | flags # x \<Rightarrow> doE y <- if null extras then throwError Fault_H.syscall_error.TruncatedMessage else returnOk ();
srcTCB <- case hd extras of capability.ThreadCap x1 \<Rightarrow> returnOk x1 | _ \<Rightarrow> throwError (Fault_H.syscall_error.InvalidCapability (Suc 0));
returnOk (tcbinvocation.CopyRegisters t srcTCB (flags !! 0) (flags !! Suc 0) (flags !! 2) (flags !! 3) copy_register_sets.ARMNoExtraRegisters)
odE \<lbrace>tcb_inv_wf'\<rbrace>, -
 2. \<And>s. (invs' and tcb_at' t and ex_nonz_cap_to' t and (\<lambda>s. \<forall>x\<in>set extras. valid_cap' x s \<and> (\<forall>y\<in>zobj_refs' x. ex_nonz_cap_to' y s))) s \<Longrightarrow> ?P'94 s proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs' and tcb_at' t and ex_nonz_cap_to' t and (\<lambda>s. \<forall>x\<in>set extras. valid_cap' x s \<and> (\<forall>y\<in>zobj_refs' x. ex_nonz_cap_to' y s))) s \<Longrightarrow> (args = [] \<longrightarrow> True) \<and> (\<forall>x xa. args = x # xa \<longrightarrow> True \<and> True \<and> (null extras \<longrightarrow> True) \<and> (\<not> null extras \<longrightarrow> (\<forall>xa. hd extras = capability.ThreadCap xa \<longrightarrow> tcb_inv_wf' (tcbinvocation.CopyRegisters t xa (x !! 0) (x !! Suc 0) (x !! 2) (x !! 3) copy_register_sets.ARMNoExtraRegisters) s) \<and> (hd extras = capability.NullCap \<longrightarrow> True) \<and> (\<forall>x xa xb xc. hd extras = capability.NotificationCap x xa xb xc \<longrightarrow> True) \<and> (\<forall>x. hd extras = capability.IRQHandlerCap x \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe. hd extras = capability.EndpointCap x xa xb xc xd xe \<longrightarrow> True) \<and> (hd extras = capability.DomainCap \<longrightarrow> True) \<and> (\<forall>x xa xb. hd extras = capability.Zombie x xa xb \<longrightarrow> True) \<and> (\<forall>x. hd extras = capability.ArchObjectCap x \<longrightarrow> True) \<and> (\<forall>x xa xb. hd extras = capability.ReplyCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb xc. hd extras = capability.UntypedCap x xa xb xc \<longrightarrow> True) \<and> (\<forall>x xa xb xc. hd extras = capability.CNodeCap x xa xb xc \<longrightarrow> True) \<and> (hd extras = capability.IRQControlCap \<longrightarrow> True))) proof (prove)
goal:
No subgoals!