Is there a version of MIP=NEXP with relatively efficient provers? (My question is not a duplicate of this question.)

Fix a good coding of non-deterministic random-access machines.

For non-negative integers $m$ that code such a machine, let

$\operatorname{states}(m)$ denote the number of internal states in the coded machine.

("hc" stands for "hard-coded".)

Choose some polynomial function $hcpoly$, and let $L$ be the language

$\{\langle m\hspace{.02 in},\hspace{-0.025 in}t,\hspace{-0.02 in}s\hspace{-0.02 in}\rangle \;\; : \;\; m$ codes such a machine and $\:t\leq 2^{hcpoly(\operatorname{states}(m))}\:$ and

there is a sequence of non-deterministic choices which will make that machine

accept the empty string in at most $t$ time without using more than $s$ space$\}\;$.


  Is there a MIP protocol for $L\hspace{.02 in}$ in which the provers use not
  
  much more than $t$ time and/or not much more than $s$ space?


That could just mean $\:poly(\hspace{.02 in}\operatorname{length}(\langle m\hspace{.02 in},\hspace{-0.025 in}t,\hspace{-0.02 in}s\hspace{-0.02 in}\rangle))\:$ time and space, although

ideally it would be $\:poly(\operatorname{states}(m))\hspace{-0.03 in}\cdot \hspace{-0.03 in}t\:$ time and $\:poly(\operatorname{states}(m))\hspace{-0.03 in}+\hspace{-0.03 in}s\:$ space.
Yes. ​ ​ ​ This paper constructs "a one-round succinct MIP of knowledge, where each prover runs in time $t\cdot \operatorname{polylog}(t)$ and space $s\cdot \operatorname{polylog}(t)$ and the verifier runs in time" ​ $\operatorname{length}(m) \cdot \operatorname{polylog}(t)$ .