Staged Multi-step UTXO Workflows via Recursive Invariants

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.