theory Syscall_R

lemma invokeTCB_typ_at'[wp]:
  "\<lbrace>\<lambda>s. P (typ_at' T p s)\<rbrace>
     invokeTCB tinv
   \<lbrace>\<lambda>rv s. P (typ_at' T p s)\<rbrace>" apply (cases tinv,
         simp_all add: invokeTCB_def
                       getThreadBufferSlot_def locateSlot_conv
            split del: if_split) apply (simp only: cases_simp if_cancel simp_thms conj_comms pred_conj_def
                     Let_def split_def getThreadVSpaceRoot
          | (simp split del: if_split cong: if_cong)
          | (wp mapM_x_wp[where S=UNIV, simplified]
                checkCap_inv_typ_at'
                case_options_weak_wp)[1]
          | wpcw)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (typ_at' T p s)\<rbrace> invokeTCB tinv \<lbrace>\<lambda>rv s. P (typ_at' T p s)\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>x1. tinv = tcbinvocation.Suspend x1 \<Longrightarrow> \<lbrace>\<lambda>s. P (typ_at' T p s)\<rbrace> liftE (do y <- ThreadDecls_H.suspend x1;
return []
od) \<lbrace>\<lambda>rv s. P (typ_at' T p s)\<rbrace>
 2. \<And>x2. tinv = tcbinvocation.Resume x2 \<Longrightarrow> \<lbrace>\<lambda>s. P (typ_at' T p s)\<rbrace> liftE (do y <- ThreadDecls_H.restart x2;
return []
od) \<lbrace>\<lambda>rv s. P (typ_at' T p s)\<rbrace>
 3. \<And>x31 x32 x33 x34 x35 x36 x37 x38. tinv = tcbinvocation.ThreadControl x31 x32 x33 x34 x35 x36 x37 x38 \<Longrightarrow> \<lbrace>\<lambda>s. P (typ_at' T p s)\<rbrace> doE y <- liftE (case x33 of None \<Rightarrow> return () | Some ep \<Rightarrow> threadSet (tcbFaultHandler_update (\<lambda>_. ep)) x31);
y <- liftE (case x34 of None \<Rightarrow> return () | Some x2 \<Rightarrow> setMCPriority x31 (fst x2));
y <- case x36 of None \<Rightarrow> returnOk () | Some (newCap, srcSlot) \<Rightarrow> doE rootSlot <- liftE (getThreadCSpaceRoot x31);
y <- cteDelete rootSlot True;
liftE (checkCapAt newCap srcSlot (checkCapAt (capability.ThreadCap x31) x32 (assertDerived srcSlot newCap (cteInsert newCap srcSlot rootSlot))))
odE;
y <- case x37 of None \<Rightarrow> returnOk () | Some (newCap, srcSlot) \<Rightarrow> doE rootSlot <- liftE (getThreadVSpaceRoot x31);
y <- cteDelete rootSlot True;
liftE (checkCapAt newCap srcSlot (checkCapAt (capability.ThreadCap x31) x32 (assertDerived srcSlot newCap (cteInsert newCap srcSlot rootSlot))))
odE;
y <- case x38 of None \<Rightarrow> returnOk () | Some (ptr, frame) \<Rightarrow> doE bufferSlot <- liftE (return (x31 + 2 ^ cte_level_bits * tcbIPCBufferSlot));
y <- cteDelete bufferSlot True;
y <- liftE (threadSet (tcbIPCBuffer_update (\<lambda>_. ptr)) x31);
y <- liftE (case frame of None \<Rightarrow> return () | Some (newCap, srcSlot) \<Rightarrow> checkCapAt newCap srcSlot (checkCapAt (capability.ThreadCap x31) x32 (assertDerived srcSlot newCap (cteInsert newCap srcSlot bufferSlot))));
thread <- liftE getCurThread;
liftE (when (x31 = thread) rescheduleRequired)
odE;
y <- liftE (case x35 of None \<Rightarrow> return () | Some x2 \<Rightarrow> setPriority x31 (fst x2));
returnOk []
odE \<lbrace>\<lambda>rv s. P (typ_at' T p s)\<rbrace>
 4. \<And>x41 x42. tinv = tcbinvocation.NotificationControl x41 x42 \<Longrightarrow> \<lbrace>\<lambda>s. P (typ_at' T p s)\<rbrace> case x42 of None \<Rightarrow> liftE (do y <- unbindNotification x41;
return []
od) | Some ntfnPtr \<Rightarrow> liftE (do y <- bindNotification x41 ntfnPtr;
return []
od) \<lbrace>\<lambda>rv s. P (typ_at' T p s)\<rbrace>
 5. \<And>x51 x52 x53 x54. tinv = tcbinvocation.WriteRegisters x51 x52 x53 x54 \<Longrightarrow> \<lbrace>\<lambda>s. P (typ_at' T p s)\<rbrace> liftE (do self <- getCurThread;
y <- performTransfer x54 self x51;
t <- local.getSanitiseRegisterInfo x51;
y <- asUser x51 (do y <- zipWithM (\<lambda>r v. setRegister r (local.sanitiseRegister t r v)) (TCB_H.frameRegisters @ TCB_H.gpRegisters) x53;
getRestartPC >>= setNextPC
od);
y <- asUser x51 (postModifyRegisters self x51);
y <- when x52 (ThreadDecls_H.restart x51);
y <- when (x51 = self) rescheduleRequired;
return []
od) \<lbrace>\<lambda>rv s. P (typ_at' T p s)\<rbrace>
 6. \<And>x61 x62 x63 x64. tinv = tcbinvocation.ReadRegisters x61 x62 x63 x64 \<Longrightarrow> \<lbrace>\<lambda>s. P (typ_at' T p s)\<rbrace> liftE (do y <- when x62 (ThreadDecls_H.suspend x61);
self <- getCurThread;
y <- performTransfer x64 x61 self;
asUser x61 (mapM getRegister (genericTake x63 (TCB_H.frameRegisters @ TCB_H.gpRegisters)))
od) \<lbrace>\<lambda>rv s. P (typ_at' T p s)\<rbrace>
 7. \<And>x71 x72 x73 x74 x75 x76 x77. tinv = tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77 \<Longrightarrow> \<lbrace>\<lambda>s. P (typ_at' T p s)\<rbrace> liftE (do y <- when x73 (ThreadDecls_H.suspend x72);
y <- when x74 (ThreadDecls_H.restart x71);
y <- when x75 (do y <- mapM_x (\<lambda>r. do v <- asUser x72 (getRegister r);
asUser x71 (setRegister r v)
od) TCB_H.frameRegisters;
pc <- asUser x71 getRestartPC;
asUser x71 (setNextPC pc)
od);
y <- when x76 (mapM_x (\<lambda>r. do v <- asUser x72 (getRegister r);
asUser x71 (setRegister r v)
od) TCB_H.gpRegisters);
thread <- getCurThread;
y <- asUser x71 (postModifyRegisters thread x71);
y <- when (x71 = thread) rescheduleRequired;
y <- performTransfer x77 x72 x71;
return []
od) \<lbrace>\<lambda>rv s. P (typ_at' T p s)\<rbrace>
 8. \<And>x81 x82. tinv = tcbinvocation.SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>\<lambda>s. P (typ_at' T p s)\<rbrace> liftE (do y <- asUser x81 (setRegister TCB_H.tlsBaseRegister x82);
cur <- getCurThread;
y <- when (x81 = cur) rescheduleRequired;
return []
od) \<lbrace>\<lambda>rv s. P (typ_at' T p s)\<rbrace> proof (prove)
goal:
No subgoals!