<p>The interactions between the different contracts are simpler and stateless. In a stateful model like Ethereum's, you can have contract <code>a</code> call contract <code>b</code> and contract <code>b</code> call contract <code>c</code>, and then contract <code>c</code> can call back contract <code>b</code> while, at the same time, <code>b</code> is still waiting for contract <code>c</code> to answer. And during the calls, the state of each of the contracts may change.</p>
<p>So reasoning about this kind of interactions is more complicated than reasoning about pure predicates (functions that return a boolean value, like validators) that only depend on the contents of the transaction that is being validated. In other words, the computation that the different validators require does not produce side-effects that affect each other</p>

CC BY-SA 4.0
2022-02-18T20:40:54.257Z
Ah! That's seems like the core insight I was missing, that validators in eUTxO are pure predicates without side effects. As a follow up, can/do smart contracts in the eUTxO model "call out" to other smart contracts? I have a strong feeling that they can't but I'm still not confident in my understanding of the technology.
Paymahn Moghadasian
CC BY-SA 4.0
2022-02-18T21:29:57.640Z
Another follow up question, you say `The interactions between the different contracts are simpler and stateless` - I thought the datum is used to track state. From the paper: `and a datum δ, where δ contains arbitrary contract-specific
data` and `datum δmsc stores the machine state`. Do you mind clarifying?
Paymahn Moghadasian
CC BY-SA 4.0
2022-02-18T20:36:19.190Z
2022-02-18T20:36:19.190Z
Palas
<blockquote>
<p>As a follow up, can/do smart contracts in the eUTxO model &quot;call out&quot;
to other smart contracts?</p>
</blockquote>
<p>A smart contract (plutus script) can only be triggered by a transaction from a wallet.</p>
<blockquote>
<p>Another follow up question, you say The interactions between the different &gt; contracts are simpler and stateless</p>
</blockquote>
<p>A Plutus script can see the whole transaction (all inputs of txn, all outputs, redeemer and datum). Arbitrary data (state) can be stored within the datum. But the context is restricted and so the only way the script can persist state or pass data (state) to another script is via a EUTxO which has a datum.</p>

CC BY-SA 4.0
2022-02-18T22:17:00.593Z
2022-02-18T22:17:00.593Z
cyberruss
<p>I've heard that the eUTxO model is more amenable to static and formal analysis than the account model. If true, why is that?</p>
<p>I understand that the account model makes formal and static analysis difficult because of the nature of global state. For example, if smart contract <code>a</code> interacts with smart contracts <code>b</code> and <code>c</code>, a formal analysis of smart contract <code>a</code> requires formal analysis of contracts <code>b</code> and <code>c</code> (and all of their dependencies). Is that correct?</p>
<p>If the above is correct, don't similar ideas apply to the eUTxO model?</p>
<p>How exactly does the local nature of UTxOs make this model more amenable (if at all) to static and formal analysis?</p>

<eutxo><formal-verification>
Why is the eUTxO model more amenable to static and formal analysis?
# Why is the eUTxO model more amenable to static and formal analysis?

(Asked by: username_0 on 2022-02-18)

I've heard that the eUTxO model is more amenable to static and formal analysis than the account model. If true, why is that?

I understand that the account model makes formal and static analysis difficult because of the nature of global state. For example, if smart contract `a` interacts with smart contracts `b` and `c`, a formal analysis of smart contract `a` requires formal analysis of contracts `b` and `c` (and all of their dependencies). Is that correct?

If the above is correct, don't similar ideas apply to the eUTxO model?

How exactly does the local nature of UTxOs make this model more amenable (if at all) to static and formal analysis?

**Tags:** eutxo, formal-verification

---

## 2 answers

### Answer by username_1 on 2022-02-18. Score: 2 | Accepted answer

The interactions between the different contracts are simpler and stateless. In a stateful model like Ethereum's, you can have contract `a` call contract `b` and contract `b` call contract `c`, and then contract `c` can call back contract `b` while, at the same time, `b` is still waiting for contract `c` to answer. And during the calls, the state of each of the contracts may change.

So reasoning about this kind of interactions is more complicated than reasoning about pure predicates (functions that return a boolean value, like validators) that only depend on the contents of the transaction that is being validated. In other words, the computation that the different validators require does not produce side-effects that affect each other

> **Comments:**
> **username_0**: Ah! That's seems like the core insight I was missing, that validators in eUTxO are pure predicates without side effects. As a follow up, can/do smart contracts in the eUTxO model "call out" to other smart contracts? I have a strong feeling that they can't but I'm still not confident in my understanding of the technology.  
> **username_0**: Another follow up question, you say `The interactions between the different contracts are simpler and stateless` - I thought the datum is used to track state. From the paper: `and a datum δ, where δ contains arbitrary contract-specific data` and `datum δmsc stores the machine state`. Do you mind clarifying?  

---

### Answer by username_2 on 2022-02-18. Score: 1

> As a follow up, can/do smart contracts in the eUTxO model "call out"
> to other smart contracts?

A smart contract (plutus script) can only be triggered by a transaction from a wallet.

> Another follow up question, you say The interactions between the different > contracts are simpler and stateless

A Plutus script can see the whole transaction (all inputs of txn, all outputs, redeemer and datum). Arbitrary data (state) can be stored within the datum. But the context is restricted and so the only way the script can persist state or pass data (state) to another script is via a EUTxO which has a datum.


---

