theory Orphanage

lemma settlsbase_no_orphans:
  "\<lbrace> \<lambda>s. no_orphans s \<and> invs' s \<rbrace>
     invokeTCB (tcbinvocation.SetTLSBase src dest)
   \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>" unfolding invokeTCB_def performTransfer_def apply simp apply (wp hoare_vcg_if_lift hoare_weak_lift_imp) apply (wpsimp wp: hoare_vcg_imp_lift' mapM_x_wp' asUser_no_orphans)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> invs' s\<rbrace> invokeTCB (tcbinvocation.SetTLSBase src dest) \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> invs' s\<rbrace> case tcbinvocation.SetTLSBase src dest 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 $ postModifyRegisters self dest;
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 $ postModifyRegisters thread dest;
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\<rbrace> liftE (do y <- asUser src (setRegister TCB_H.tlsBaseRegister dest);
cur <- getCurThread;
y <- when (src = cur) rescheduleRequired;
return []
od) \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> asUser src (setRegister TCB_H.tlsBaseRegister dest) \<lbrace>\<lambda>y s. (if src = ksCurThread s then \<lambda>s. no_orphans s \<and> valid_queues' s else no_orphans) s\<rbrace>
 2. \<And>s. no_orphans s \<and> invs' s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!