theory Orphanage

lemma copyreg_no_orphans:
  "\<lbrace> \<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' src s
         \<and> tcb_at' dest s \<and> ex_nonz_cap_to' src s \<and> ex_nonz_cap_to' dest s \<rbrace>
     invokeTCB (tcbinvocation.CopyRegisters dest src susp resume frames ints arch)
   \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>" unfolding invokeTCB_def performTransfer_def postModifyRegisters_def supply if_weak_cong[cong] apply simp apply (wp hoare_vcg_if_lift hoare_weak_lift_imp) apply (wp hoare_vcg_imp_lift' mapM_x_wp' asUser_no_orphans
             | wpc | clarsimp split del: if_splits)+ apply (wp hoare_weak_lift_imp hoare_vcg_conj_lift hoare_drop_imp mapM_x_wp' restart_invs'
              restart_no_orphans asUser_no_orphans suspend_nonz_cap_to_tcb
              | strengthen invs_valid_queues' | wpc | simp add: if_apply_def2)+ apply (fastforce simp: invs'_def valid_state'_def dest!: global'_no_ex_cap) done

(* 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' src s \<and> tcb_at' dest s \<and> ex_nonz_cap_to' src s \<and> ex_nonz_cap_to' dest s\<rbrace> invokeTCB (tcbinvocation.CopyRegisters dest src susp resume frames ints 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' src s \<and> tcb_at' dest s \<and> ex_nonz_cap_to' src s \<and> ex_nonz_cap_to' dest s\<rbrace> case tcbinvocation.CopyRegisters dest src susp resume frames ints 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' src s \<and> tcb_at' dest s \<and> ex_nonz_cap_to' src s \<and> ex_nonz_cap_to' dest s\<rbrace> case tcbinvocation.CopyRegisters dest src susp resume frames ints 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' src s \<and> tcb_at' dest s \<and> ex_nonz_cap_to' src s \<and> ex_nonz_cap_to' dest s\<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 (return ());
y <- when (dest = thread) rescheduleRequired;
return []
od) \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>y ya yb. ints \<Longrightarrow> \<lbrace>?Q21 y ya yb\<rbrace> mapM_x (\<lambda>r. do v <- asUser src (getRegister r);
asUser dest (setRegister r v)
od) TCB_H.gpRegisters \<lbrace>\<lambda>yc s. (dest = ksCurThread s \<longrightarrow> no_orphans s \<and> valid_queues' s) \<and> (dest \<noteq> ksCurThread s \<longrightarrow> no_orphans s)\<rbrace>
 2. \<And>y ya. \<lbrace>?B4 y ya\<rbrace> 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) \<lbrace>\<lambda>yb. if ints then ?Q21 y ya yb else (\<lambda>s. (dest = ksCurThread s \<longrightarrow> no_orphans s \<and> valid_queues' s) \<and> (dest \<noteq> ksCurThread s \<longrightarrow> no_orphans s))\<rbrace>
 3. \<And>y. \<lbrace>?B3 y\<rbrace> when resume (ThreadDecls_H.restart dest) \<lbrace>?B4 y\<rbrace>
 4. \<lbrace>?Q\<rbrace> when susp (ThreadDecls_H.suspend src) \<lbrace>?B3\<rbrace>
 5. \<And>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' src s \<and> tcb_at' dest s \<and> ex_nonz_cap_to' src s \<and> ex_nonz_cap_to' dest s \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>pc. frames \<Longrightarrow> \<lbrace>?B54 () () () pc\<rbrace> asUser dest (setNextPC pc) \<lbrace>\<lambda>yb. if ints then \<lambda>s. (\<not> dest \<noteq> ksCurThread s \<longrightarrow> no_orphans s \<and> valid_queues' s) \<and> (\<not> \<not> dest \<noteq> ksCurThread s \<longrightarrow> no_orphans s) else (\<lambda>s. (dest = ksCurThread s \<longrightarrow> no_orphans s \<and> valid_queues' s) \<and> (dest \<noteq> ksCurThread s \<longrightarrow> no_orphans s))\<rbrace>
 2. \<And>y ya yb. frames \<Longrightarrow> \<lbrace>?B53 y ya yb\<rbrace> asUser dest getRestartPC \<lbrace>?B54 y ya yb\<rbrace>
 3. \<And>y ya. frames \<Longrightarrow> \<lbrace>?Q52 y ya\<rbrace> mapM_x (\<lambda>r. do v <- asUser src (getRegister r);
asUser dest (setRegister r v)
od) TCB_H.frameRegisters \<lbrace>?B53 y ya\<rbrace>
 4. \<And>y. \<lbrace>?B3 y\<rbrace> when resume (ThreadDecls_H.restart dest) \<lbrace>\<lambda>ya. if frames then ?Q52 y ya else if ints then \<lambda>s. (\<not> dest \<noteq> ksCurThread s \<longrightarrow> no_orphans s \<and> valid_queues' s) \<and> (\<not> \<not> dest \<noteq> ksCurThread s \<longrightarrow> no_orphans s) else (\<lambda>s. (dest = ksCurThread s \<longrightarrow> no_orphans s \<and> valid_queues' s) \<and> (dest \<noteq> ksCurThread s \<longrightarrow> no_orphans s))\<rbrace>
 5. \<lbrace>?Q\<rbrace> when susp (ThreadDecls_H.suspend src) \<lbrace>?B3\<rbrace>
 6. \<And>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' src s \<and> tcb_at' dest s \<and> ex_nonz_cap_to' src s \<and> ex_nonz_cap_to' dest s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' src s \<and> tcb_at' dest s \<and> ex_nonz_cap_to' src s \<and> ex_nonz_cap_to' dest s \<Longrightarrow> (susp \<longrightarrow> (resume \<longrightarrow> src \<noteq> ksIdleThread s \<and> dest \<noteq> ksIdleThread s \<and> src \<noteq> ksIdleThread s) \<and> (\<not> resume \<longrightarrow> src \<noteq> ksIdleThread s)) \<and> (\<not> susp \<longrightarrow> resume \<longrightarrow> dest \<noteq> ksIdleThread s) proof (prove)
goal:
No subgoals!