I am trying to understand the EVM in the context of a classic Turing Machine. I have read through the yellow paper and taken what I can from the internet, but I still feel like I could use some help pinning my question down.
In the paper, they call the EVM "quasi-Turing complete", and I understand this to mean that it is Turing complete as long as there is gas to run a smart contract. The reasoning behind this is to protect against spamming the network. However, it seems to me that this also has implications in the halting problem. It is not that we can detect infinite loops, but we can terminate possible infinite loops if code is running longer than expected. Is that accurate?
Now, I see where the gas requirement of code execution is a parameter in the exception handling state. The first one in fact.
Z(σ, µ, I) ≡ µ_g < C(σ, µ, I) ∨ ...
What I would like to do is boil this down to a formal 7-tuple Turing Machine.
My intuition is to say that the transition function contains a jump to the reject state if an exception state is detected. So the transition function is something like: δ : Q × Γ = Q × Γ × {L, R, Reject}?
I could be way off base here. I guess where I am having trouble is that the gas requirement of running code in the EVM is handled in Exception Halting and not in the Transition Function. I can't find where the yellow paper unifies state transitions and exception states, other than they say:
"It is assumed that any transactions executed first pass the initial tests of intrinsic validity"
which I assume they mean they run the exception handling before the state transition.
Is there an accurate way to define the EVM in terms of a Turing Machine? Are there any TM's or automatas that accurately represent a limited number of state transitions like the EVM? Is it accurate to say that the EVM is decidable considering it will halt eventually on all inputs? Any thoughts or comments on my ramblings here would be very appreciated!
