一句话:提出递归不变式与三值 DSL,在 UTXO 上实现分阶段多步工作流并证明验证可靠。
无状态 UTXO 支持并行验证与可预测计量,但多步工作流需跨输出传递状态,预构造的下一步交易可能因先被花费而失效,增加链下跟踪与重建成本。论文提出递归不变式(RI):把工作流规则写成交易级谓词,引用输入及带索引的后继位置;当后继位置被实现时,下一步重查前驱 RI,无需应用层共享可变状态即可跨交易传递规则。其静态类型 DSL 用真/假/未知三值语义延迟不可检查义务;框架形式化 UTXO 验证与账本扩展,刻画可求值的一步片段并证明演绎系统相对三值语义可靠。原型与六个案例显示累积验证成本代理近似线性增长。
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.
@article{paperbot12094,
title = {Staged Multi-step UTXO Workflows via Recursive Invariants},
author = {Shuyang Tang and Sherman S. M. Chow and Hongfei Fu and Zihan Guo and Guoqiang Li},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {OOPSLA2},
year = {2026},
doi = {10.1145/3839489}
}