2

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?

Improve this question

2 Answers 2

Reset to default
2

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

Improve this answer
2
  • 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
    Feb 18, 2022 at 20:40
  • 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
    Feb 18, 2022 at 21:29
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.

Improve this answer

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.