Formalizing Extended UTxO and BitML Calculus in Agda

Abstract

Smart contracts – programs that run on a blockchain – allow for sophisticated transactional schemes, but their concurrent execution makes it difficult to reason about their behaviour and bugs in smart contracts have lead to significant monetary losses (e.g. DAO attack). For that reason, increasingly more attention is given to formal methods, that guarantee that such fatal scenarios are not possible. We attempt to advance the state-of-the-art for a language-oriented, type-driven account of smart contracts by formalizing two well-established models in Agda and mechanizing the corresponding meta-theory. The first concerns an abstract model for UTxO-based ledgers, such as Bitcoin, which we further extend to cover features of the Cardano blockchain, namely more expressive scripts and built-in support for user-issued cryptocurrencies. The second object of study is BitML, a process calculus specifically targeting Bitcoin smart con- tracts. We present a mechanized semantics of BitML contracts and its small-step semantics, as well as a mechanized account of BitML’s symbolic model over participant strategies. Finally, we sketch the way towards a certified compiler from BitML contracts to UTxO transac- tions, where all behaviours manifesting on BitML’s symbolic model can safely be transported to the UTxO level.