# Can PDA model Turing Complete objects if the objects' state are finite?

I am currently reading the extended Version of the Paper Online Detection of Effectively Callback Free Objects with Applications of Smart Contract.

I am trying to understand the proofs of Chapter 6. In particular, I cannot understand the premise of proofs 6.2. Indeed, the authors use a variant of SMAC, an Object-oriented and Turing Complete (SMAC) and they claim that (I underlined the suspicious claim with bold)

Thus, we focus on verifying $$sECF$$, namely, statically verifying whether all executions of an object are $$dECF_{FS}$$ or $$ECF_{C}$$, where the domains of the object variables are restricted to finite sets. Hence, such objects can be modeled with a pushdown-automaton (PDA). Such a PDA for an object o is able to simulate any modular well-formed execution $$\kappa \in \pi$$ where the active object of all states in $$\pi$$ is o.

In my understanding, this premise should be wrong, because although the state of this SMAC program is final, it is not computable by Push-Down-Automata (which compute total functions).

Foo:
int x = 0 // field of the object
enter // enter the single method of the object/contract
while true do
x = 1
return


## This question had a bounty worth +100 reputation from Briomkez that ended 3 hours ago. Grace period ends in 20 hours

This question has not received enough attention.

Such a PDA for an object o is able to simulate any modular well-formed execution $$\kappa \in \pi$$ where the active object of all states in $$\pi$$ is o