theory Tcb_R

lemma inv_tcb_IRQInactive:
  "\<lbrace>valid_irq_states'\<rbrace> invokeTCB tcb_inv
  -, \<lbrace>\<lambda>rv s. intStateIRQTable (ksInterruptState s) rv \<noteq> irqstate.IRQInactive\<rbrace>" including no_pre apply (simp add: invokeTCB_def) apply (rule hoare_pre) apply (wpc |
          wp withoutPreemption_R cteDelete_IRQInactive checkCap_inv
             hoare_vcg_const_imp_lift_R cteDelete_irq_states'
             hoare_vcg_const_imp_lift |
          simp add: split_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_states'\<rbrace> invokeTCB tcb_inv -, \<lbrace>\<lambda>rv s. intStateIRQTable (ksInterruptState s) rv \<noteq> irqstate.IRQInactive\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_states'\<rbrace> invokeTCB tcb_inv -, \<lbrace>\<lambda>rv s. intStateIRQTable (ksInterruptState s) rv \<noteq> irqstate.IRQInactive\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_states'\<rbrace> case tcb_inv 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;
performTransfer arch self dest;
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;
performTransfer arch src self;
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;
performTransfer transferArch src dest;
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 s. intStateIRQTable (ksInterruptState s) rv \<noteq> irqstate.IRQInactive\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> case tcb_inv 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;
performTransfer arch self dest;
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;
performTransfer arch src self;
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;
performTransfer transferArch src dest;
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 s. intStateIRQTable (ksInterruptState s) rv \<noteq> irqstate.IRQInactive\<rbrace>
 2. \<And>s. valid_irq_states' s \<Longrightarrow> ?P' s proof (prove)
goal:
No subgoals!