theory Tcb_AI

lemma (in Tcb_AI) decode_copyreg_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>
     decode_copy_registers args (cap.ThreadCap t) extras
   \<lbrace>tcb_inv_wf\<rbrace>,-" apply (simp add: decode_copy_registers_def whenE_def
             cong: list.case_cong split del: if_split) apply (rule hoare_pre) apply (wp | wpc)+ apply (clarsimp simp: valid_cap_def[where c="cap.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. s \<turnstile> x \<and> (\<forall>y\<in>zobj_refs x. ex_nonz_cap_to y s))\<rbrace> decode_copy_registers args (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. s \<turnstile> x \<and> (\<forall>y\<in>zobj_refs x. ex_nonz_cap_to y s))\<rbrace> case args of [] \<Rightarrow> throwError TruncatedMessage | flags # x \<Rightarrow> doE y <- if extras = [] then throwError TruncatedMessage else returnOk ();
src_tcb <- case extras of [] \<Rightarrow> throwError (InvalidCapability (Suc 0)) | ThreadCap xa # x \<Rightarrow> returnOk xa | _ # x \<Rightarrow> throwError $ InvalidCapability 1;
returnOk (CopyRegisters t src_tcb (flags !! 0) (flags !! Suc 0) (flags !! 2) (flags !! 3) ArchDefaultExtraRegisters)
odE \<lbrace>tcb_inv_wf\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'6\<rbrace> case args of [] \<Rightarrow> throwError TruncatedMessage | flags # x \<Rightarrow> doE y <- if extras = [] then throwError TruncatedMessage else returnOk ();
src_tcb <- case extras of [] \<Rightarrow> throwError (InvalidCapability (Suc 0)) | ThreadCap xa # x \<Rightarrow> returnOk xa | _ # x \<Rightarrow> throwError $ InvalidCapability 1;
returnOk (CopyRegisters t src_tcb (flags !! 0) (flags !! Suc 0) (flags !! 2) (flags !! 3) ArchDefaultExtraRegisters)
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. s \<turnstile> x \<and> (\<forall>y\<in>zobj_refs x. ex_nonz_cap_to y s))) s \<Longrightarrow> ?P'6 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. s \<turnstile> x \<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> (extras = [] \<longrightarrow> True) \<and> (extras = [] \<longrightarrow> True) \<and> (extras \<noteq> [] \<longrightarrow> (\<forall>xa xb. extras = xa # xb \<longrightarrow> (xa = NullCap \<longrightarrow> True) \<and> (\<forall>x xb xc xd. xa = UntypedCap x xb xc xd \<longrightarrow> True) \<and> (\<forall>x xb xc. xa = EndpointCap x xb xc \<longrightarrow> True) \<and> (\<forall>x xb xc. xa = NotificationCap x xb xc \<longrightarrow> True) \<and> (\<forall>x xb xc. xa = ReplyCap x xb xc \<longrightarrow> True) \<and> (\<forall>x xb xc. xa = CNodeCap x xb xc \<longrightarrow> True) \<and> (\<forall>xb. xa = ThreadCap xb \<longrightarrow> tcb_inv_wf (CopyRegisters t xb (x !! 0) (x !! Suc 0) (x !! 2) (x !! 3) ArchDefaultExtraRegisters) s) \<and> (xa = DomainCap \<longrightarrow> True) \<and> (xa = IRQControlCap \<longrightarrow> True) \<and> (\<forall>x. xa = IRQHandlerCap x \<longrightarrow> True) \<and> (\<forall>x xb xc. xa = Zombie x xb xc \<longrightarrow> True) \<and> (\<forall>x. xa = ArchObjectCap x \<longrightarrow> True)))) proof (prove)
goal:
No subgoals!