Properties of UTxO Ledgers and Programs Implemented on Them

TL;DR

This paper formalizes trace-based analysis of UTxO cryptocurrency ledgers and smart contracts using topology, graph, and category theory, providing a rigorous framework for understanding ledger behaviors and safety properties.

Contribution

It introduces a novel formal framework for analyzing UTxO ledger traces and smart contracts using advanced mathematical tools like topology and category theory.

Findings

Formalization of valid UTxO traces as graph paths

Proofs of safety properties of UTxO ledger traces

Characterization of smart contract programs as non-expanding maps

Abstract

Trace-based properties are the gold standard for program behaviour analysis. One of the domains of application of this type of analysis is cryptocurrency ledgers, both for the purpose of analyzing the behaviour of the ledger itself, and any user-defined programs called by it, known as smart contracts. The (extended) UTxO ledger model is a kind of ledger model where all smart contract code is stateless, and additional work must be done to model stateful programs. We formalize the application of trace-based analysis to UTxO ledgers and contracts, expressing it in the languages of topology, as well as graph and category theory. To describe valid traces of UTxO ledger executions, and their relation to the behaviour of stateful programs implemented on the ledger, we define a category of simple graphs, infinite paths in which form an ultra-metric space. Maps in this category are arbitrary partial sieve-define homomorphisms of simple graphs. Programs implemented on the ledger correspond to non-expanding maps out of the graph of valid UTxO execution traces. We reason about safety properties in this framework, and prove properties of valid UTxO ledger traces.