2026-07-24T05:16:00Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:19875 2024-05-21T15:18:57Z ddc:004 open_access

Structured Contracts in the EUTxO Ledger Model Vinogradova, Polina Melkonian, Orestis Wadler, Philip Chakravarty, Manuel Krijnen, Jacco Jones, Michael Peyton Chapman, James Ferariu, Tudor blockchain ledger smart contract formal verification specification transition systems Agda UTxO EUTxO small-step semantics Blockchain ledgers based on the extended UTxO model support fully expressive smart contracts to specify permissions for performing certain actions, such as spending transaction outputs or minting assets. There have been some attempts to standardize the implementation of stateful programs using this infrastructure, with varying degrees of success. To remedy this, we introduce the framework of structured contracts to formalize what it means for a stateful program to be correctly implemented on the ledger. Using small-step semantics, our approach relates low-level ledger transitions to high-level transitions of the smart contract being specified, thus allowing users to prove that their abstract specification is adequately realized on the blockchain. We argue that the framework is versatile enough to cover a range of examples, in particular proving the equivalence of multiple concrete implementations of the same abstract specification. Building upon prior meta-theoretical results, our results have been mechanized in the Agda proof assistant, paving the way to rigorous verification of smart contracts. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Polina Vinogradova and Orestis Melkonian and Philip Wadler and Manuel Chakravarty and Jacco Krijnen and Michael Peyton Jones and James Chapman and Tudor Ferariu 2024 Is Part Of OASIcs, Volume 118, 5th International Workshop on Formal Methods for Blockchains (FMBC 2024) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/OASIcs.FMBC.2024.10 urn:nbn:de:0030-drops-198757 https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2024.10 eng https://creativecommons.org/licenses/by/4.0/legalcode