It would also be interesting to investigate which of those protocols are guaranteed to eventually halt on all inputs.
I can see that in last protocol (relativized for RE) a malicious prover can prevent verifier from ever terminating, if the verifier is required to accept all valid move sequences / pointers / … however long they might be. (That is a mathematical theorem and not fixed by choosing a clever encoding for numbers of arbitrary length.)
I think both protocols mentioned (MIP* = RE and the pointers one) already do what you want here. In the background the provers have to do unbounded work to prepare for the stuff they show the verifier, but the verifier’s work is limited to a fixed polynomial in the input size.
And more strongly: in the pointer version where we have two competing provers, a malicious prover can’t force an honest prover to do significantly more work than would be required in an honest case.
It would also be interesting to investigate which of those protocols are guaranteed to eventually halt on all inputs.
I can see that in last protocol (relativized for RE) a malicious prover can prevent verifier from ever terminating, if the verifier is required to accept all valid move sequences / pointers / … however long they might be. (That is a mathematical theorem and not fixed by choosing a clever encoding for numbers of arbitrary length.)
I think both protocols mentioned (MIP* = RE and the pointers one) already do what you want here. In the background the provers have to do unbounded work to prepare for the stuff they show the verifier, but the verifier’s work is limited to a fixed polynomial in the input size.
And more strongly: in the pointer version where we have two competing provers, a malicious prover can’t force an honest prover to do significantly more work than would be required in an honest case.