paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Staged Multi-step UTXO Workflows via Recursive Invariants

基于递归不变式的分阶段多步 UTXO 工作流
OOPSLA 10(OOPSLA2)2026匹配度 2/10 · 该论文属于形式语义、领域特定语言与验证工具链方向,虽涉及三值语义和可靠性证明,但与用户核心关注的静态分析×ML/Agent、浮点程序分析、贝叶斯程序分析均无直接关联,应用场景为 UTXO/区块链工作流。引用 0 inbox
Shuyang Tang, Sherman S. M. Chow, Hongfei Fu, Zihan Guo, Guoqiang Li
crossref: 2026-10-02

AI 速览

一句话:提出递归不变式与三值 DSL,在 UTXO 上实现分阶段多步工作流并证明验证可靠。

无状态 UTXO 支持并行验证与可预测计量,但多步工作流需跨输出传递状态,预构造的下一步交易可能因先被花费而失效,增加链下跟踪与重建成本。论文提出递归不变式(RI):把工作流规则写成交易级谓词,引用输入及带索引的后继位置;当后继位置被实现时,下一步重查前驱 RI,无需应用层共享可变状态即可跨交易传递规则。其静态类型 DSL 用真/假/未知三值语义延迟不可检查义务;框架形式化 UTXO 验证与账本扩展,刻画可求值的一步片段并证明演绎系统相对三值语义可靠。原型与六个案例显示累积验证成本代理近似线性增长。

问题
无状态 UTXO 多步工作流需要跨交易传递状态;若预先构造下一步交易,可能因其他有效花费先确认而失效,导致链下跟踪、协调与重建成本高。
方法
提出递归不变式(RI)及静态类型 DSL,将工作流规则写成交易级谓词并引用后继位置,以三值语义延迟未来依赖义务;形式化 UTXO 验证和账本扩展并证明演绎系统可靠。
评估
实现 RI 解释器与基准工具链,在六个实践驱动的案例中展示分阶段工作流约束,并报告累积验证成本代理近似线性增长。
原文摘要(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.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@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}
}