theory Tcb_R

lemma copyreg_invs'':
  "\<lbrace>invs' and sch_act_simple and tcb_at' src and tcb_at' dest and ex_nonz_cap_to' src and ex_nonz_cap_to' dest\<rbrace>
     invokeTCB (tcbinvocation.CopyRegisters dest src susp resume frames ints arch)
   \<lbrace>\<lambda>rv. invs' and tcb_at' dest\<rbrace>" supply if_weak_cong[cong] apply (simp add: invokeTCB_def performTransfer_def if_apply_def2) apply (wp mapM_x_wp' restart_invs' | simp)+ apply (rule conjI) apply (wp | clarsimp)+ by (fastforce simp: invs'_def valid_state'_def dest!: global'_no_ex_cap)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and sch_act_simple and tcb_at' src and tcb_at' dest and ex_nonz_cap_to' src and ex_nonz_cap_to' dest\<rbrace> invokeTCB (tcbinvocation.CopyRegisters dest src susp resume frames ints arch) \<lbrace>\<lambda>rv. invs' and tcb_at' dest\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and sch_act_simple and tcb_at' src and tcb_at' dest and ex_nonz_cap_to' src and ex_nonz_cap_to' dest\<rbrace> invokeTCB (tcbinvocation.CopyRegisters dest src susp resume frames ints arch) \<lbrace>\<lambda>rv. invs' and tcb_at' dest\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and sch_act_simple and tcb_at' src and tcb_at' dest and ex_nonz_cap_to' src and ex_nonz_cap_to' dest\<rbrace> liftE (do y <- when susp (ThreadDecls_H.suspend src);
y <- when resume (ThreadDecls_H.restart dest);
y <- when frames (do y <- mapM_x (\<lambda>r. do v <- asUser src (getRegister r);
asUser dest (setRegister r v)
od) TCB_H.frameRegisters;
pc <- asUser dest getRestartPC;
asUser dest (setNextPC pc)
od);
y <- when ints (mapM_x (\<lambda>r. do v <- asUser src (getRegister r);
asUser dest (setRegister r v)
od) TCB_H.gpRegisters);
thread <- getCurThread;
y <- asUser dest (postModifyRegisters thread dest);
y <- when (dest = thread) rescheduleRequired;
return []
od) \<lbrace>\<lambda>rv. invs' and tcb_at' dest\<rbrace> proof (prove)
goal (2 subgoals):
 1. susp \<Longrightarrow> (resume \<longrightarrow> \<lbrace>?Q98\<rbrace> ThreadDecls_H.suspend src \<lbrace>\<lambda>y a. invs' a \<and> ex_nonz_cap_to' dest a \<and> dest \<noteq> ksIdleThread a \<and> tcb_at' dest a\<rbrace>) \<and> (\<not> resume \<longrightarrow> \<lbrace>?Q98\<rbrace> ThreadDecls_H.suspend src \<lbrace>\<lambda>y s. invs' s \<and> tcb_at' dest s\<rbrace>)
 2. \<And>s. (invs' and sch_act_simple and tcb_at' src and tcb_at' dest and ex_nonz_cap_to' src and ex_nonz_cap_to' dest) s \<Longrightarrow> (if susp then ?Q98 else if resume then \<lambda>a. (invs' and ex_nonz_cap_to' dest and (\<lambda>s. dest \<noteq> ksIdleThread s)) a \<and> tcb_at' dest a else if frames then \<lambda>s. (invs' and tcb_at' dest) s \<and> tcb_at' dest s \<and> tcb_at' dest s else if ints then \<lambda>s. invs' s \<and> tcb_at' dest s \<and> tcb_at' dest s else (\<lambda>s. invs' s \<and> tcb_at' dest s \<and> tcb_at' dest s)) s proof (prove)
goal (3 subgoals):
 1. susp \<Longrightarrow> resume \<longrightarrow> \<lbrace>?Q98\<rbrace> ThreadDecls_H.suspend src \<lbrace>\<lambda>y a. invs' a \<and> ex_nonz_cap_to' dest a \<and> dest \<noteq> ksIdleThread a \<and> tcb_at' dest a\<rbrace>
 2. susp \<Longrightarrow> \<not> resume \<longrightarrow> \<lbrace>?Q98\<rbrace> ThreadDecls_H.suspend src \<lbrace>\<lambda>y s. invs' s \<and> tcb_at' dest s\<rbrace>
 3. \<And>s. (invs' and sch_act_simple and tcb_at' src and tcb_at' dest and ex_nonz_cap_to' src and ex_nonz_cap_to' dest) s \<Longrightarrow> (if susp then ?Q98 else if resume then \<lambda>a. (invs' and ex_nonz_cap_to' dest and (\<lambda>s. dest \<noteq> ksIdleThread s)) a \<and> tcb_at' dest a else if frames then \<lambda>s. (invs' and tcb_at' dest) s \<and> tcb_at' dest s \<and> tcb_at' dest s else if ints then \<lambda>s. invs' s \<and> tcb_at' dest s \<and> tcb_at' dest s else (\<lambda>s. invs' s \<and> tcb_at' dest s \<and> tcb_at' dest s)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>invs' s; sch_act_simple s; tcb_at' src s; tcb_at' dest s; ex_nonz_cap_to' src s; ex_nonz_cap_to' dest s\<rbrakk> \<Longrightarrow> (resume \<longrightarrow> (susp \<longrightarrow> src \<noteq> ksIdleThread s \<and> dest \<noteq> ksIdleThread s) \<and> (\<not> susp \<longrightarrow> dest \<noteq> ksIdleThread s)) \<and> (\<not> resume \<longrightarrow> susp \<longrightarrow> src \<noteq> ksIdleThread s \<and> dest \<noteq> ksIdleThread s)