# Formal definition of the EVM as a Turing Machine

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!

I can confirm the following:

they run the exception handling before the state transition.

If exception handling is triggered, the ongoing transaction is being reverted, so the state remains the same.

But I don't see any possibility for this:

Is it accurate to say that the EVM is decidable considering it will halt eventually on all inputs?

There should be no way to halt the EVM (from within the EVM). Stack depth limit and gas prices enforce every transaction to either finish successfully or abort.

• Thanks for the response! I was looking into this a while back and did come up with more of a refined explanation for what was going on (at least in my head). Your response regarding successful or aborted txs is closer to what I meant to say. Every transaction will either finish or abort. From this concept you can build a decider to show that the language is decidable. I don't think I ever able to concisely articulate the EVM as decidable through the transition functions and validity check that I was hoping for, but I do think you can show the EVM as being decidable without too much trouble. – le_sanglier Mar 9 '18 at 18:27