Message-Passing in the Extended UTxO Ledger

A notable problem faced by developers of smart contracts running on an extended UTxO (EUTxO) ledger is double satisfaction: interacting contracts that make payouts may validate with insufficient payments made to some recipients. In this work, we formalize the notion of a stateful contract constraint being vulnerable to double satisfaction. Next, we formalize interaction among scripts and stateful contracts via message-passing, consisting of a specification and an implementation of a stateful distributed message-passing contract, together with a proof of the integrity of its implementation. Messages specify sender and receiver outputs, as well as the data and assets being communicated, which are recorded on the ledger in the form of special NFT tokens distributed across UTxO entries that also contain the sent assets. We give two applications of our design by considering a message: (1) as a record of a successful script computation, akin to memoization, and (2) as a mechanism for asynchronous structured contracts communication that enables a principled separation of contract communication from its computation. Building on this application of message-passing, we present a result stating that making payouts from stateful contracts using message-passing is not vulnerable to double satisfaction.