Native Custom Tokens in the Extended UTXO Model

User-defined tokens-both fungible ERC-20 and non-fungible ERC-721 tokens-are central to the majority of contracts deployed on Ethereum. User-defined tokens are non-native on Ethereum; i.e., they are not directly supported by the ledger, but require custom code. This makes them unnecessarily inefficient, expensive, and complex. The Extended UTXO Model (EUTXO) [5] has been introduced as a generalisation of Bitcoin-style UTXO ledgers, allowing support of more expressive smart contracts, approaching the functionality available to contracts on Ethereum. Specifically, a bisimulation argument established a formal relationship between the EUTXO ledger and a general form of state machines. Nevertheless, transaction outputs in the EUTXO model lock integral quantities of a single native cryptocurrency only, just like Bitcoin. In this paper, we study a generalisation of the EUTXO ledger model with native user-defined tokens. Following the approach proposed in a companion paper [4] for the simpler case of plain Bitcoin-style UTXO ledgers, we generalise transaction outputs to lock not merely coins of a single cryptocurrency, but entire token bundles, including custom tokens whose forging is controlled by forging policy scripts. We show that this leads to a rich ledger model that supports a broad range of interesting use cases. Our main technical contribution is a formalisation of the multi-asset EUTXO ledger in Agda, which we use to establish that the ledger with custom tokens is strictly more expressive than the original EUTXO ledger. In particular, we state and prove a transfer result for inductive and temporal properties from state machines to the multi-asset EUTXO ledger, which was out of scope for the single-currency EUTXO ledger. In practical terms, the resulting system is the basis for the smart contract system of the Cardano blockchain.