Staged Multi-step UTXO Workflows via Recursive Invariants
Open Access
- 1 October 2026
- journal article
- Published by Association for Computing Machinery (ACM) in Proceedings of the ACM on Programming Languages
- Vol. 10 (OOPSLA2) , 1192-1216
Abstract
Stateless UTXO-style execution validates transactions using local and referenced data, enabling parallel validation and predictable serialized-size/weight accounting. However, multi-step workflows must thread state across outputs, and a prepared next-step transaction may become stale when another valid spend confirms first. Explicit state threading therefore shifts consistency maintenance, off-chain tracking, and transaction rebuilding onto the protocol boundary, potentially increasing coordination cost and latency. Recursive invariants (RIs), our proposed transaction-level logic and toolchain, address this gap by expressing workflow rules as transaction-level predicates over a transaction's inputs and indexed successor positions referenced by the RI. Modeled this way, an accepted transaction that realizes such a successor position re-checks the predecessor's RI one step later, carrying the workflow rule forward without introducing application-level shared mutable state or executable logic attached to outputs. Accordingly, multi-step protocol rules preserve validation-time locality and admit explicit cost accounting, while cross-transaction guarantees arise from repeated one-step checking. Not all successor clauses are checkable when the current transaction is validated, so our small statically typed domain-specific language (DSL) uses three-valued semantics over true, false, unknown to defer future-dependent obligations until they become checkable. Co-designed with this DSL, our framework formalizes UTXO validation and ledger extension, identifies the validation-time-evaluable one-step fragment, and proves the deduction system sound with respect to the three-valued semantics. Here, we also give validation and ledger-extension algorithms corresponding to the formal model. On the systems side, we implement a prototype RI interpreter and benchmarking toolchain for the six reported workloads. With six practice-motivated case studies, the reported benchmark traces exhibit approximately linear cumulative validation-cost proxy growth, while illustrating staged workflow constraints without committing each step to a preconstructed successor transaction.Keywords
All Related Versions
Funding Information
- Collaborative Research Fund, Research Grants Council of Hong Kong (C5097-25G)
- General Research Fund, Research Grants Council of Hong Kong (14210825)
- National Natural Science Foundation of China (62572294)
This publication has 7 references indexed in Scilit:
- Scalable UTXO smart contracts via fine-grained distributed stateFuture Generation Computer Systems, 2025
- Properties of UTxO Ledgers and Programs Implemented on ThemElectronic Proceedings in Theoretical Computer Science, 2025
- Issue InformationClinical Pharmacology in Drug Development, 2023
- Computationally sound Bitcoin tokens2021
- Safer smart contract programming with ScillaProceedings of the ACM on Programming Languages, 2019
- BitML2018
- Counter machines and counter languagesTheory of Computing Systems, 1968