通过递归不变量的分阶段多步UTXO工作流
Staged Multi-step UTXO Workflows via Recursive Invariants
浏览论文内容
中文总结 AI 辅助
本文提出递归不变量（RIs）及配套DSL，通过交易级谓词和三值语义实现UTXO多步工作流的分阶段验证，降低协调成本，并证明系统可靠性及线性成本增长。
中文摘要 AI 辅助
无状态UTXO风格的执行使用本地和引用数据验证交易，实现并行验证和可预测的序列化大小/权重核算。多步工作流通过输出传递状态，如果另一个有效花费先确认，准备好的下一步交易可能会变得过时。因此，显式状态传递将一致性维护、链下跟踪和交易重建转移到协议边界，增加了协调成本和延迟。递归不变量（RIs），我们提出的交易级逻辑和工具链，通过将工作流规则表示为交易级谓词，作用于交易的输入和由RI引用的索引后继位置，来解决这一差距。接受实现此类后继位置的交易会在一步后重新检查前驱的RI，将工作流规则向前推进，而无需共享的可变应用状态或可执行输出逻辑。因此，多步协议规则保留了验证时的局部性并允许显式成本核算，而跨交易保证源于重复的一步检查。并非所有后继子句在验证时都可检查，因此我们的小型静态类型领域特定语言（DSL）使用三值语义（真、假、未知）将依赖未来的义务推迟到可检查时。与这种DSL协同设计，我们的框架形式化了UTXO验证和账本扩展，识别出验证时可评估的一步片段，并证明了演绎系统相对于三值语义的可靠性。我们为此模型给出了验证和账本扩展算法。我们实现了原型RI解释器和针对六个工作负载的基准测试工具链。六个实践驱动的案例研究展示了近似线性的累积验证成本代理增长，并说明了无需预构建每个后继的分阶段工作流约束。
英文摘要
Stateless UTXO-style execution validates transactions from local and referenced data, supporting parallel validation and predictable serialized-size/weight accounting, but multi-step workflows must explicitly thread state through outputs. However, a prepared next-step transaction may become stale when another valid spend confirms first, shifting consistency maintenance, off-chain tracking, and transaction rebuilding to the protocol boundary and potentially increasing coordination cost and latency. Explicitly addressing this gap, recursive invariants (RIs) provide a transaction-level logic and toolchain in which workflow rules are predicates over a transaction's inputs and indexed successor positions referenced by the RI. Realizing such a successor causes the accepted transaction to re-check its predecessor's RI one step later, carrying the workflow rule forward without application-level shared mutable state or executable logic attached to outputs; repeated one-step checks thereby preserve validation-time locality and make validation work explicitly accountable. Many successor clauses are not decidable when the current transaction is validated, so our small statically typed DSL uses Kleene-style three-valued semantics over true, false, and unknown to defer future-dependent obligations until they become checkable. Alongside the DSL, we formalize UTXO validation and ledger extension in our model, identify the validation-time-evaluable one-step fragment, prove the deduction system sound for the three-valued semantics, and give corresponding transaction-validation and ledger-extension algorithms. Notably, a prototype RI interpreter and benchmarking toolchain evaluate six practice-motivated workflows; the reported traces show approximately linear cumulative validation-cost proxy growth while illustrating staged constraints without committing each step to a preconstructed successor transaction.
发表机构
- Shanghai Jiao Tong University（上海交通大学）
- The Chinese University of Hong Kong（香港中文大学）
- Shanghai University of Finance and Economics（上海财经大学）
- Sun Yat-sen University（中山大学）
机构由 AI 辅助整理，请以论文原文为准。
