theory Orphanage

lemma writereg_no_orphans:
  "\<lbrace> \<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s
       \<and> tcb_at' dest s \<and> ex_nonz_cap_to' dest s\<rbrace>
     invokeTCB (tcbinvocation.WriteRegisters dest resume values arch)
   \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>" unfolding invokeTCB_def performTransfer_def postModifyRegisters_def apply simp apply (rule hoare_pre) by (wp hoare_vcg_if_lift hoare_vcg_conj_lift restart_invs' hoare_weak_lift_imp
       | strengthen invs_valid_queues'  | clarsimp  simp: invs'_def valid_state'_def dest!: global'_no_ex_cap )+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' dest s \<and> ex_nonz_cap_to' dest s\<rbrace> invokeTCB (tcbinvocation.WriteRegisters dest resume values arch) \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' dest s \<and> ex_nonz_cap_to' dest s\<rbrace> case tcbinvocation.WriteRegisters dest resume values arch of tcbinvocation.Suspend thread \<Rightarrow> withoutPreemption $ do ThreadDecls_H.suspend thread;
return []
od | tcbinvocation.Resume thread \<Rightarrow> withoutPreemption $ do ThreadDecls_H.restart thread;
return []
od | tcbinvocation.ThreadControl target slot faultep mcp priority cRoot vRoot buffer \<Rightarrow> doE tCap <- returnOk (capability.ThreadCap target);
withoutPreemption $ maybe (return ()) (\<lambda>ep. threadSet (tcbFaultHandler_update (\<lambda>_. ep)) target) faultep;
withoutPreemption $ maybe (return ()) (setMCPriority target) (map_option fst mcp);
maybe (returnOk ()) (\<lambda>(newCap, srcSlot). doE rootSlot <- withoutPreemption $ getThreadCSpaceRoot target;
cteDelete rootSlot True;
withoutPreemption $ checkCapAt newCap srcSlot $ checkCapAt tCap slot $ assertDerived srcSlot newCap $ cteInsert newCap srcSlot rootSlot
odE) cRoot;
maybe (returnOk ()) (\<lambda>(newCap, srcSlot). doE rootSlot <- withoutPreemption $ getThreadVSpaceRoot target;
cteDelete rootSlot True;
withoutPreemption $ checkCapAt newCap srcSlot $ checkCapAt tCap slot $ assertDerived srcSlot newCap $ cteInsert newCap srcSlot rootSlot
odE) vRoot;
maybe (returnOk ()) (\<lambda>(ptr, frame). doE bufferSlot <- withoutPreemption $ getThreadBufferSlot target;
cteDelete bufferSlot True;
withoutPreemption $ threadSet (tcbIPCBuffer_update (\<lambda>_. ptr)) target;
withoutPreemption $ case frame of None \<Rightarrow> return () | Some (newCap, srcSlot) \<Rightarrow> checkCapAt newCap srcSlot $ checkCapAt tCap slot $ assertDerived srcSlot newCap $ cteInsert newCap srcSlot bufferSlot;
thread <- withoutPreemption $ getCurThread;
withoutPreemption $ when (target = thread) $ rescheduleRequired
odE) buffer;
withoutPreemption $ maybe (return ()) (setPriority target) (map_option fst priority);
returnOk []
odE | tcbinvocation.NotificationControl tcb None \<Rightarrow> withoutPreemption $ do unbindNotification tcb;
return []
od | tcbinvocation.NotificationControl tcb (Some ntfnPtr) \<Rightarrow> withoutPreemption $ do bindNotification tcb ntfnPtr;
return []
od | tcbinvocation.WriteRegisters dest resumeTarget values arch \<Rightarrow> withoutPreemption $ do self <- getCurThread;
return ();
t <- local.getSanitiseRegisterInfo dest;
asUser dest $ do zipWithM (\<lambda>r v. setRegister r (local.sanitiseRegister t r v)) (TCB_H.frameRegisters @ TCB_H.gpRegisters) values;
getRestartPC >>= setNextPC
od;
asUser dest $ return ();
when resumeTarget $ ThreadDecls_H.restart dest;
when (dest = self) $ rescheduleRequired;
return []
od | tcbinvocation.ReadRegisters src suspendSource n arch \<Rightarrow> withoutPreemption $ do when suspendSource $ ThreadDecls_H.suspend src;
self <- getCurThread;
return ();
regs <- return (genericTake n $ TCB_H.frameRegisters @ TCB_H.gpRegisters);
asUser src $ mapM getRegister regs
od | tcbinvocation.CopyRegisters dest src suspendSource resumeTarget transferFrame transferInteger transferArch \<Rightarrow> withoutPreemption $ do when suspendSource $ ThreadDecls_H.suspend src;
when resumeTarget $ ThreadDecls_H.restart dest;
when transferFrame $ do 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;
when transferInteger $ mapM_x (\<lambda>r. do v <- asUser src $ getRegister r;
asUser dest $ setRegister r v
od) TCB_H.gpRegisters;
thread <- getCurThread;
asUser dest $ return ();
when (dest = thread) $ rescheduleRequired;
return ();
return []
od | tcbinvocation.SetTLSBase tcb tls_base \<Rightarrow> withoutPreemption $ do asUser tcb $ setRegister TCB_H.tlsBaseRegister tls_base;
cur <- getCurThread;
when (tcb = cur) rescheduleRequired;
return []
od \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' dest s \<and> ex_nonz_cap_to' dest s\<rbrace> liftE (do self <- getCurThread;
t <- local.getSanitiseRegisterInfo dest;
y <- asUser dest (do y <- zipWithM (\<lambda>r v. setRegister r (local.sanitiseRegister t r v)) (TCB_H.frameRegisters @ TCB_H.gpRegisters) values;
getRestartPC >>= setNextPC
od);
y <- asUser dest (return ());
y <- when resume (ThreadDecls_H.restart dest);
y <- when (dest = self) rescheduleRequired;
return []
od) \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> liftE (do self <- getCurThread;
t <- local.getSanitiseRegisterInfo dest;
y <- asUser dest (do y <- zipWithM (\<lambda>r v. setRegister r (local.sanitiseRegister t r v)) (TCB_H.frameRegisters @ TCB_H.gpRegisters) values;
getRestartPC >>= setNextPC
od);
y <- asUser dest (return ());
y <- when resume (ThreadDecls_H.restart dest);
y <- when (dest = self) rescheduleRequired;
return []
od) \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 2. \<And>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' dest s \<and> ex_nonz_cap_to' dest s \<Longrightarrow> ?Q s