Staged Multi-step UTXO Workflows via Recursive Invariants
Paper proposes recursive invariants, a transaction-level logic and typed DSL, to enforce multi-step UTXO workflow rules without shared mutable state.
The paper introduces Recursive Invariants (RIs), transaction-level predicates over inputs and indexed successor positions that carry multi-step workflow rules forward via repeated one-step checking. A statically typed DSL with three-valued semantics (true/false/unknown) defers future-dependent obligations until they become checkable at validation time. The authors formalize UTXO validation and ledger extension, prove the deduction system sound, and implement a prototype interpreter benchmarked on six workloads and six practice-motivated case studies showing roughly linear cumulative validation-cost growth.
- Recursive Invariants express multi-step UTXO workflow rules as transaction-level predicates
- Three-valued DSL semantics defers future-dependent obligations until checkable
- Deduction system proven sound for validation and ledger extension
- Prototype toolchain benchmarked on six workloads and case studies
Full article235 words · extracted from arxiv.org · click to collapse
Stateless UTXO-style execution validates transactions using local and referenced data, enabling parallel validation and predictable serialized-size/weight accounting. Multi-step workflows thread state across outputs, and a prepared next-step transaction may become stale if another valid spend confirms first. Explicit state threading therefore shifts consistency maintenance, off-chain tracking, and transaction rebuilding to the protocol boundary, 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. An accepted transaction realizing such a successor position re-checks the predecessor's RI one step later, carrying the workflow rule forward without shared mutable application state or executable output logic. Thus, 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 at validation time, so our small statically typed domain-specific language (DSL) uses three-valued semantics (true, false, unknown) to defer future-dependent obligations until 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 w.r.t. the three-valued semantics. We give validation and ledger-extension algorithms for this model. We implement a prototype RI interpreter and benchmarking toolchain for six workloads. Six practice-motivated case studies exhibit roughly linear cumulative validation-cost proxy growth and illustrate staged workflow constraints without preconstructing each successor.
Text extracted automatically; images, tables and formatting may be missing. Original: https://arxiv.org/abs/2609.26305