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
where the domains of the object variables are restricted to finite sets. Hence, such objects can be modeled with a pushdown-automaton (PDA).


You are correct that if you understand it as using a pushdown-automaton to model the full behavior of the object, since as you indicated, you can put a Turing complete Turing machine inside any object.

However, I would believe that the authors intend to use a pushdown-automaton to mode an object in the domain with its possible states as defined by the values of its fields and its execution stack, since the whole paper is focusing on the ECF(Effectively Callback Free) property for objects. The actual moments when the object is still in the middle of changing from one state to another state are ignored/irrelevant/transparent/skipped. More specifically, the following shows the purpose of the object.


  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