theory Syscall_C

lemma handleInvocation_def2:
  "handleInvocation isCall isBlocking =
   do thread \<leftarrow> getCurThread;
      info \<leftarrow> getMessageInfo thread;
      ptr \<leftarrow> asUser thread (getRegister ARM_H.capRegister);
      v \<leftarrow> (doE (cap, slot) \<leftarrow> capFaultOnFailure ptr False (lookupCapAndSlot thread ptr);
          buffer \<leftarrow> withoutFailure (VSpace_H.lookupIPCBuffer False thread);
          extracaps \<leftarrow> lookupExtraCaps thread buffer info;
          returnOk (slot, cap, extracaps, buffer)
      odE);
      case v of Inl f \<Rightarrow> liftE (when isBlocking (handleFault thread f))
        | Inr (slot, cap, extracaps, buffer) \<Rightarrow>
               do args \<leftarrow> getMRs thread buffer info;
                  v' \<leftarrow> do v \<leftarrow> RetypeDecls_H.decodeInvocation (msgLabel info) args ptr slot cap extracaps;
                               invocationCatch thread isBlocking isCall id v od;
                  case v' of Inr _ \<Rightarrow> liftE (replyOnRestart thread [] isCall)
                           | Inl (Inl syserr) \<Rightarrow> liftE (when isCall (replyFromKernel thread
                                                                   (msgFromSyscallError syserr)))
                           | Inl (Inr preempt) \<Rightarrow> throwError preempt
               od
   od" apply (simp add: handleInvocation_def Syscall_H.syscall_def runExceptT_def
                   liftE_bindE cong: sum.case_cong) apply (rule ext, (rule bind_apply_cong [OF refl])+) apply (clarsimp simp: bind_assoc split: sum.split) apply (rule bind_apply_cong [OF refl])+ apply (clarsimp simp: invocationCatch_def throwError_bind
                        liftE_bindE bind_assoc
                 split: sum.split) apply (rule bind_apply_cong [OF refl])+ apply (simp add: bindE_def bind_assoc) apply (rule bind_apply_cong [OF refl])+ apply (clarsimp simp: lift_def throwError_bind returnOk_bind split: sum.split) apply (simp cong: bind_cong add: ts_Restart_case_helper') apply (simp add: when_def[symmetric] replyOnRestart_def[symmetric]) apply (simp add: liftE_def replyOnRestart_twice alternative_bind
                   alternative_refl split: if_split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. handleInvocation isCall isBlocking = do thread <- getCurThread;
info <- getMessageInfo thread;
ptr <- asUser thread (getRegister Thread_H.capRegister);
v <- doE (cap, slot) <- capFaultOnFailure ptr False (lookupCapAndSlot thread ptr);
buffer <- withoutFailure (lookupIPCBuffer False thread);
extracaps <- lookupExtraCaps thread buffer info;
returnOk (slot, cap, extracaps, buffer)
odE;
case v of Inl f \<Rightarrow> liftE (when isBlocking (handleFault thread f)) | Inr (slot, cap, extracaps, buffer) \<Rightarrow> do args <- getMRs thread buffer info;
v' <- global.decodeInvocation (msgLabel info) args ptr slot cap extracaps >>= invocationCatch thread isBlocking isCall id;
case v' of Inl (Inl syserr) \<Rightarrow> liftE (when isCall (replyFromKernel thread (msgFromSyscallError syserr))) | Inl (Inr preempt) \<Rightarrow> throwError preempt | Inr x \<Rightarrow> liftE (replyOnRestart thread [] isCall)
od
od proof (prove)
goal (1 subgoal):
 1. do thread <- getCurThread;
info <- getMessageInfo thread;
ptr <- asUser thread (getRegister Thread_H.capRegister);
doE (cap, slot) <- capFaultOnFailure ptr False (lookupCapAndSlot thread ptr);
do buffer <- lookupIPCBuffer False thread;
doE extracaps <- lookupExtraCaps thread buffer info;
returnOk (slot, cap, extracaps, buffer)
odE
od
odE >>= case_sum (\<lambda>f. liftE (when isBlocking (handleFault thread f))) (\<lambda>a. (case a of (slot, cap, extracaps, buffer) \<Rightarrow> do args <- getMRs thread buffer info;
global.decodeInvocation (msgLabel info) args ptr slot cap extracaps
od) >>= case_sum (\<lambda>e. liftE (when isCall (replyFromKernel thread (msgFromSyscallError e)))) (\<lambda>b. do y <- setThreadState Structures_H.thread_state.Restart thread;
doE reply <- global.performInvocation isBlocking isCall b;
liftE (getThreadState thread >>= Structures_H.thread_state.case_thread_state (\<lambda>word bool. return ()) (return ()) (\<lambda>word. return ()) (return ()) (return ()) (return ()) (\<lambda>word1 word2 bool1 bool2 bool3. return ()) (do y <- when isCall (replyFromKernel thread (0, reply));
setThreadState Structures_H.thread_state.Running thread
od))
odE
od))
od = do thread <- getCurThread;
info <- getMessageInfo thread;
ptr <- asUser thread (getRegister Thread_H.capRegister);
v <- doE (cap, slot) <- capFaultOnFailure ptr False (lookupCapAndSlot thread ptr);
do buffer <- lookupIPCBuffer False thread;
doE extracaps <- lookupExtraCaps thread buffer info;
returnOk (slot, cap, extracaps, buffer)
odE
od
odE;
case v of Inl f \<Rightarrow> liftE (when isBlocking (handleFault thread f)) | Inr (slot, cap, extracaps, buffer) \<Rightarrow> do args <- getMRs thread buffer info;
v' <- global.decodeInvocation (msgLabel info) args ptr slot cap extracaps >>= invocationCatch thread isBlocking isCall id;
case v' of Inl (Inl syserr) \<Rightarrow> liftE (when isCall (replyFromKernel thread (msgFromSyscallError syserr))) | Inl (Inr preempt) \<Rightarrow> throwError preempt | Inr x \<Rightarrow> liftE (replyOnRestart thread [] isCall)
od
od proof (prove)
goal (1 subgoal):
 1. \<And>x rv st rva sta rvb stb rvc stc. \<lbrakk>(rv, st) \<in> fst (getCurThread x); (rva, sta) \<in> fst (getMessageInfo rv st); (rvb, stb) \<in> fst (asUser rv (getRegister Thread_H.capRegister) sta); (rvc, stc) \<in> fst ((doE (cap, slot) <- capFaultOnFailure rvb False (lookupCapAndSlot rv rvb);
do buffer <- lookupIPCBuffer False rv;
doE extracaps <- lookupExtraCaps rv buffer rva;
returnOk (slot, cap, extracaps, buffer)
odE
od
odE) stb)\<rbrakk> \<Longrightarrow> (case rvc of Inl f \<Rightarrow> liftE (when isBlocking (handleFault rv f)) | Inr a \<Rightarrow> (case a of (slot, cap, extracaps, buffer) \<Rightarrow> do args <- getMRs rv buffer rva;
global.decodeInvocation (msgLabel rva) args rvb slot cap extracaps
od) >>= case_sum (\<lambda>e. liftE (when isCall (replyFromKernel rv (msgFromSyscallError e)))) (\<lambda>b. do y <- setThreadState Structures_H.thread_state.Restart rv;
doE reply <- global.performInvocation isBlocking isCall b;
liftE (getThreadState rv >>= Structures_H.thread_state.case_thread_state (\<lambda>word bool. return ()) (return ()) (\<lambda>word. return ()) (return ()) (return ()) (return ()) (\<lambda>word1 word2 bool1 bool2 bool3. return ()) (do y <- when isCall (replyFromKernel rv (0, reply));
setThreadState Structures_H.thread_state.Running rv
od))
odE
od)) stc = (case rvc of Inl f \<Rightarrow> liftE (when isBlocking (handleFault rv f)) | Inr (slot, cap, extracaps, buffer) \<Rightarrow> do args <- getMRs rv buffer rva;
v' <- global.decodeInvocation (msgLabel rva) args rvb slot cap extracaps >>= invocationCatch rv isBlocking isCall id;
case v' of Inl (Inl syserr) \<Rightarrow> liftE (when isCall (replyFromKernel rv (msgFromSyscallError syserr))) | Inl (Inr preempt) \<Rightarrow> throwError preempt | Inr x \<Rightarrow> liftE (replyOnRestart rv [] isCall)
od) stc proof (prove)
goal (1 subgoal):
 1. \<And>x rv st rva sta rvb stb stc a aa ab b. \<lbrakk>(rv, st) \<in> fst (getCurThread x); (rva, sta) \<in> fst (getMessageInfo rv st); (rvb, stb) \<in> fst (asUser rv (getRegister Thread_H.capRegister) sta); (Inr (a, aa, ab, b), stc) \<in> fst ((doE (cap, slot) <- capFaultOnFailure rvb False (lookupCapAndSlot rv rvb);
do buffer <- lookupIPCBuffer False rv;
doE extracaps <- lookupExtraCaps rv buffer rva;
returnOk (slot, cap, extracaps, buffer)
odE
od
odE) stb)\<rbrakk> \<Longrightarrow> (do args <- getMRs rv b rva;
global.decodeInvocation (msgLabel rva) args rvb a aa ab >>= case_sum (\<lambda>e. liftE (when isCall (replyFromKernel rv (msgFromSyscallError e)))) (\<lambda>b. do y <- setThreadState Structures_H.thread_state.Restart rv;
doE reply <- global.performInvocation isBlocking isCall b;
liftE (getThreadState rv >>= Structures_H.thread_state.case_thread_state (\<lambda>word bool. return ()) (return ()) (\<lambda>word. return ()) (return ()) (return ()) (return ()) (\<lambda>word1 word2 bool1 bool2 bool3. return ()) (do y <- when isCall (replyFromKernel rv (0, reply));
setThreadState Structures_H.thread_state.Running rv
od))
odE
od)
od) stc = (do args <- getMRs rv b rva;
x <- global.decodeInvocation (msgLabel rva) args rvb a aa ab;
invocationCatch rv isBlocking isCall id x >>= case_sum (case_sum (\<lambda>syserr. liftE (when isCall (replyFromKernel rv (msgFromSyscallError syserr)))) throwError) (\<lambda>x. liftE (replyOnRestart rv [] isCall))
od) stc proof (prove)
goal (1 subgoal):
 1. \<And>x rv st rva sta rvb stb stc a aa ab b rvc std rvd ste. \<lbrakk>(rv, st) \<in> fst (getCurThread x); (rva, sta) \<in> fst (getMessageInfo rv st); (rvb, stb) \<in> fst (asUser rv (getRegister Thread_H.capRegister) sta); (Inr (a, aa, ab, b), stc) \<in> fst ((doE (cap, slot) <- capFaultOnFailure rvb False (lookupCapAndSlot rv rvb);
do buffer <- lookupIPCBuffer False rv;
doE extracaps <- lookupExtraCaps rv buffer rva;
returnOk (slot, cap, extracaps, buffer)
odE
od
odE) stb); (rvc, std) \<in> fst (getMRs rv b rva stc); (rvd, ste) \<in> fst (global.decodeInvocation (msgLabel rva) rvc rvb a aa ab std)\<rbrakk> \<Longrightarrow> (case rvd of Inl e \<Rightarrow> liftE (when isCall (replyFromKernel rv (msgFromSyscallError e))) | Inr b \<Rightarrow> do y <- setThreadState Structures_H.thread_state.Restart rv;
doE reply <- global.performInvocation isBlocking isCall b;
liftE (getThreadState rv >>= Structures_H.thread_state.case_thread_state (\<lambda>word bool. return ()) (return ()) (\<lambda>word. return ()) (return ()) (return ()) (return ()) (\<lambda>word1 word2 bool1 bool2 bool3. return ()) (do y <- when isCall (replyFromKernel rv (0, reply));
setThreadState Structures_H.thread_state.Running rv
od))
odE
od) ste = (invocationCatch rv isBlocking isCall id rvd >>= case_sum (case_sum (\<lambda>syserr. liftE (when isCall (replyFromKernel rv (msgFromSyscallError syserr)))) throwError) (\<lambda>x. liftE (replyOnRestart rv [] isCall))) ste proof (prove)
goal (1 subgoal):
 1. \<And>x rv st rva sta rvb stb stc a aa ab b rvc std ste x2. \<lbrakk>(rv, st) \<in> fst (getCurThread x); (rva, sta) \<in> fst (getMessageInfo rv st); (rvb, stb) \<in> fst (asUser rv (getRegister Thread_H.capRegister) sta); (Inr (a, aa, ab, b), stc) \<in> fst ((doE (cap, slot) <- capFaultOnFailure rvb False (lookupCapAndSlot rv rvb);
do buffer <- lookupIPCBuffer False rv;
doE extracaps <- lookupExtraCaps rv buffer rva;
returnOk (slot, cap, extracaps, buffer)
odE
od
odE) stb); (rvc, std) \<in> fst (getMRs rv b rva stc); (Inr x2, ste) \<in> fst (global.decodeInvocation (msgLabel rva) rvc rvb a aa ab std)\<rbrakk> \<Longrightarrow> (do y <- setThreadState Structures_H.thread_state.Restart rv;
doE reply <- global.performInvocation isBlocking isCall x2;
liftE (getThreadState rv >>= Structures_H.thread_state.case_thread_state (\<lambda>word bool. return ()) (return ()) (\<lambda>word. return ()) (return ()) (return ()) (return ()) (\<lambda>word1 word2 bool1 bool2 bool3. return ()) (do y <- when isCall (replyFromKernel rv (0, reply));
setThreadState Structures_H.thread_state.Running rv
od))
odE
od) ste = (do y <- setThreadState Structures_H.thread_state.Restart rv;
doE reply <- global.performInvocation isBlocking isCall x2 >>= case_sum (throwError \<circ> Inr) returnOk;
liftE (if reply = [] then replyOnRestart rv [] isCall \<sqinter> return () else replyOnRestart rv reply isCall)
odE >>= case_sum (case_sum (\<lambda>syserr. liftE (when isCall (replyFromKernel rv (msgFromSyscallError syserr)))) throwError) (\<lambda>x. liftE (replyOnRestart rv [] isCall))
od) ste proof (prove)
goal (1 subgoal):
 1. \<And>x rv st rva sta rvb stb stc a aa ab b rvc std ste x2 rvd stf. \<lbrakk>(rv, st) \<in> fst (getCurThread x); (rva, sta) \<in> fst (getMessageInfo rv st); (rvb, stb) \<in> fst (asUser rv (getRegister Thread_H.capRegister) sta); (Inr (a, aa, ab, b), stc) \<in> fst ((doE (cap, slot) <- capFaultOnFailure rvb False (lookupCapAndSlot rv rvb);
do buffer <- lookupIPCBuffer False rv;
doE extracaps <- lookupExtraCaps rv buffer rva;
returnOk (slot, cap, extracaps, buffer)
odE
od
odE) stb); (rvc, std) \<in> fst (getMRs rv b rva stc); (Inr x2, ste) \<in> fst (global.decodeInvocation (msgLabel rva) rvc rvb a aa ab std); (rvd, stf) \<in> fst (setThreadState Structures_H.thread_state.Restart rv ste)\<rbrakk> \<Longrightarrow> (doE reply <- global.performInvocation isBlocking isCall x2;
liftE (getThreadState rv >>= Structures_H.thread_state.case_thread_state (\<lambda>word bool. return ()) (return ()) (\<lambda>word. return ()) (return ()) (return ()) (return ()) (\<lambda>word1 word2 bool1 bool2 bool3. return ()) (do y <- when isCall (replyFromKernel rv (0, reply));
setThreadState Structures_H.thread_state.Running rv
od))
odE) stf = (doE reply <- global.performInvocation isBlocking isCall x2 >>= case_sum (throwError \<circ> Inr) returnOk;
liftE (if reply = [] then replyOnRestart rv [] isCall \<sqinter> return () else replyOnRestart rv reply isCall)
odE >>= case_sum (case_sum (\<lambda>syserr. liftE (when isCall (replyFromKernel rv (msgFromSyscallError syserr)))) throwError) (\<lambda>x. liftE (replyOnRestart rv [] isCall))) stf proof (prove)
goal (1 subgoal):
 1. \<And>x rv st rva sta rvb stb stc a aa ab b rvc std ste x2 stf. \<lbrakk>(rv, st) \<in> fst (getCurThread x); (rva, sta) \<in> fst (getMessageInfo rv st); (rvb, stb) \<in> fst (asUser rv (getRegister Thread_H.capRegister) sta); (Inr (a, aa, ab, b), stc) \<in> fst ((capFaultOnFailure rvb False (lookupCapAndSlot rv rvb) >>= Nondet_Monad.lift (\<lambda>(cap, slot). do buffer <- lookupIPCBuffer False rv;
lookupExtraCaps rv buffer rva >>= Nondet_Monad.lift (\<lambda>extracaps. returnOk (slot, cap, extracaps, buffer))
od)) stb); (rvc, std) \<in> fst (getMRs rv b rva stc); (Inr x2, ste) \<in> fst (global.decodeInvocation (msgLabel rva) rvc rvb a aa ab std); ((), stf) \<in> fst (setThreadState Structures_H.thread_state.Restart rv ste)\<rbrakk> \<Longrightarrow> (global.performInvocation isBlocking isCall x2 >>= Nondet_Monad.lift (\<lambda>reply. liftE (getThreadState rv >>= Structures_H.thread_state.case_thread_state (\<lambda>word bool. return ()) (return ()) (\<lambda>word. return ()) (return ()) (return ()) (return ()) (\<lambda>word1 word2 bool1 bool2 bool3. return ()) (do y <- when isCall (replyFromKernel rv (0, reply));
setThreadState Structures_H.thread_state.Running rv
od)))) stf = (do x <- global.performInvocation isBlocking isCall x2;
x <- case x of Inl x \<Rightarrow> (throwError \<circ> Inr) x | Inr x \<Rightarrow> returnOk x;
Nondet_Monad.lift (\<lambda>reply. liftE (if reply = [] then replyOnRestart rv [] isCall \<sqinter> return () else replyOnRestart rv reply isCall)) x >>= case_sum (case_sum (\<lambda>syserr. liftE (when isCall (replyFromKernel rv (msgFromSyscallError syserr)))) throwError) (\<lambda>x. liftE (replyOnRestart rv [] isCall))
od) stf proof (prove)
goal (1 subgoal):
 1. \<And>x rv st rva sta rvb stb stc a aa ab b rvc std ste x2 stf rvd stg. \<lbrakk>(rv, st) \<in> fst (getCurThread x); (rva, sta) \<in> fst (getMessageInfo rv st); (rvb, stb) \<in> fst (asUser rv (getRegister Thread_H.capRegister) sta); (Inr (a, aa, ab, b), stc) \<in> fst ((capFaultOnFailure rvb False (lookupCapAndSlot rv rvb) >>= Nondet_Monad.lift (\<lambda>(cap, slot). do buffer <- lookupIPCBuffer False rv;
lookupExtraCaps rv buffer rva >>= Nondet_Monad.lift (\<lambda>extracaps. returnOk (slot, cap, extracaps, buffer))
od)) stb); (rvc, std) \<in> fst (getMRs rv b rva stc); (Inr x2, ste) \<in> fst (global.decodeInvocation (msgLabel rva) rvc rvb a aa ab std); ((), stf) \<in> fst (setThreadState Structures_H.thread_state.Restart rv ste); (rvd, stg) \<in> fst (global.performInvocation isBlocking isCall x2 stf)\<rbrakk> \<Longrightarrow> Nondet_Monad.lift (\<lambda>reply. liftE (getThreadState rv >>= Structures_H.thread_state.case_thread_state (\<lambda>word bool. return ()) (return ()) (\<lambda>word. return ()) (return ()) (return ()) (return ()) (\<lambda>word1 word2 bool1 bool2 bool3. return ()) (do y <- when isCall (replyFromKernel rv (0, reply));
setThreadState Structures_H.thread_state.Running rv
od))) rvd stg = (do x <- case rvd of Inl x \<Rightarrow> (throwError \<circ> Inr) x | Inr x \<Rightarrow> returnOk x;
Nondet_Monad.lift (\<lambda>reply. liftE (if reply = [] then replyOnRestart rv [] isCall \<sqinter> return () else replyOnRestart rv reply isCall)) x >>= case_sum (case_sum (\<lambda>syserr. liftE (when isCall (replyFromKernel rv (msgFromSyscallError syserr)))) throwError) (\<lambda>x. liftE (replyOnRestart rv [] isCall))
od) stg proof (prove)
goal (1 subgoal):
 1. \<And>x rv st rva sta rvb stb stc a aa ab b rvc std ste x2 stf stg x2a. \<lbrakk>(rv, st) \<in> fst (getCurThread x); (rva, sta) \<in> fst (getMessageInfo rv st); (rvb, stb) \<in> fst (asUser rv (getRegister Thread_H.capRegister) sta); (Inr (a, aa, ab, b), stc) \<in> fst ((capFaultOnFailure rvb False (lookupCapAndSlot rv rvb) >>= Nondet_Monad.lift (\<lambda>(cap, slot). do buffer <- lookupIPCBuffer False rv;
lookupExtraCaps rv buffer rva >>= Nondet_Monad.lift (\<lambda>extracaps. returnOk (slot, cap, extracaps, buffer))
od)) stb); (rvc, std) \<in> fst (getMRs rv b rva stc); (Inr x2, ste) \<in> fst (global.decodeInvocation (msgLabel rva) rvc rvb a aa ab std); ((), stf) \<in> fst (setThreadState Structures_H.thread_state.Restart rv ste); (Inr x2a, stg) \<in> fst (global.performInvocation isBlocking isCall x2 stf)\<rbrakk> \<Longrightarrow> liftE (getThreadState rv >>= Structures_H.thread_state.case_thread_state (\<lambda>word bool. return ()) (return ()) (\<lambda>word. return ()) (return ()) (return ()) (return ()) (\<lambda>word1 word2 bool1 bool2 bool3. return ()) (do y <- when isCall (replyFromKernel rv (0, x2a));
setThreadState Structures_H.thread_state.Running rv
od)) stg = (liftE (if x2a = [] then replyOnRestart rv [] isCall \<sqinter> return () else replyOnRestart rv x2a isCall) >>= case_sum (case_sum (\<lambda>syserr. liftE (when isCall (replyFromKernel rv (msgFromSyscallError syserr)))) throwError) (\<lambda>x. liftE (replyOnRestart rv [] isCall))) stg proof (prove)
goal (1 subgoal):
 1. \<And>x rv st rva sta rvb stb stc a aa ab b rvc std ste x2 stf stg x2a. \<lbrakk>(rv, st) \<in> fst (getCurThread x); (rva, sta) \<in> fst (getMessageInfo rv st); (rvb, stb) \<in> fst (asUser rv (getRegister Thread_H.capRegister) sta); (Inr (a, aa, ab, b), stc) \<in> fst ((capFaultOnFailure rvb False (lookupCapAndSlot rv rvb) >>= Nondet_Monad.lift (\<lambda>(cap, slot). do v <- lookupIPCBuffer False rv;
lookupExtraCaps rv v rva >>= Nondet_Monad.lift (\<lambda>extracaps. returnOk (slot, cap, extracaps, v))
od)) stb); (rvc, std) \<in> fst (getMRs rv b rva stc); (Inr x2, ste) \<in> fst (global.decodeInvocation (msgLabel rva) rvc rvb a aa ab std); ((), stf) \<in> fst (setThreadState Structures_H.thread_state.Restart rv ste); (Inr x2a, stg) \<in> fst (global.performInvocation isBlocking isCall x2 stf)\<rbrakk> \<Longrightarrow> liftE (do v <- getThreadState rv;
if v = Structures_H.thread_state.Restart then do y <- when isCall (replyFromKernel rv (0, x2a));
setThreadState Structures_H.thread_state.Running rv
od else return ()
od) stg = (do v <- liftE (if x2a = [] then replyOnRestart rv [] isCall \<sqinter> return () else replyOnRestart rv x2a isCall);
case v of Inl (Inl syserr) \<Rightarrow> liftE (when isCall (replyFromKernel rv (msgFromSyscallError syserr))) | Inl (Inr xa) \<Rightarrow> throwError xa | Inr x \<Rightarrow> liftE (replyOnRestart rv [] isCall)
od) stg proof (prove)
goal (1 subgoal):
 1. \<And>x rv st rva sta rvb stb stc a aa ab b rvc std ste x2 stf stg x2a. \<lbrakk>(rv, st) \<in> fst (getCurThread x); (rva, sta) \<in> fst (getMessageInfo rv st); (rvb, stb) \<in> fst (asUser rv (getRegister Thread_H.capRegister) sta); (Inr (a, aa, ab, b), stc) \<in> fst ((capFaultOnFailure rvb False (lookupCapAndSlot rv rvb) >>= Nondet_Monad.lift (\<lambda>(cap, slot). do v <- lookupIPCBuffer False rv;
lookupExtraCaps rv v rva >>= Nondet_Monad.lift (\<lambda>extracaps. returnOk (slot, cap, extracaps, v))
od)) stb); (rvc, std) \<in> fst (getMRs rv b rva stc); (Inr x2, ste) \<in> fst (global.decodeInvocation (msgLabel rva) rvc rvb a aa ab std); ((), stf) \<in> fst (setThreadState Structures_H.thread_state.Restart rv ste); (Inr x2a, stg) \<in> fst (global.performInvocation isBlocking isCall x2 stf)\<rbrakk> \<Longrightarrow> liftE (replyOnRestart rv x2a isCall) stg = (do v <- liftE (if x2a = [] then replyOnRestart rv [] isCall \<sqinter> return () else replyOnRestart rv x2a isCall);
case v of Inl (Inl syserr) \<Rightarrow> liftE (when isCall (replyFromKernel rv (msgFromSyscallError syserr))) | Inl (Inr xa) \<Rightarrow> throwError xa | Inr x \<Rightarrow> liftE (replyOnRestart rv [] isCall)
od) stg proof (prove)
goal:
No subgoals!