1. 引言
比特币的未花费交易输出（UTXO）模型虽然在并发货币转移方面很优雅，但由于缺乏共享可变状态，在实现复杂的、有状态的智能合约方面存在显著限制。契约作为一种关键的语言原语被提出，旨在扩展比特币脚本，允许一笔交易对未来赎回交易的脚本施加约束。本文旨在填补契约形式化抽象模型的空白，自2013年左右提出以来，契约主要从底层、实现导向的视角进行描述。通过提供一个形式化基础，本工作旨在简化对合约属性的推理，使得能够规范超出比特币当前能力的高级用例，并促进更高级别编程抽象的设计。
2. 纯比特币模型
本文采用了核心比特币交易模型的形式化表述。在UTXO模型中，区块链状态由一组未花费交易输出定义。每个输出包含一个值（比特币数量）和一个scriptPubKey（锁定脚本），该脚本指定了花费它所需的条件。一笔花费交易提供一个scriptSig（解锁脚本）并引用它希望消费的UTXO。验证涉及执行拼接后的脚本。关键的是，标准比特币脚本是受限的：除了签名验证和基本算术/逻辑外，它无法内省或约束花费交易的结构，这阻碍了强制执行多步骤协议的合约的创建。
3. 契约的形式化模型
核心贡献是一个形式化模型，它抽象了提议的契约操作码（如OP_CHECKTEMPLATEVERIFY）。
3.1. 契约原语与语法
该模型将契约谓词作为比特币脚本的扩展引入。契约本质上是一个评估为真或假的约束 $C(T_x, T_{next})$，其中 $T_x$ 是正在被花费的当前交易，$T_{next}$ 是提议的花费交易。该谓词可以检查 $T_{next}$ 的字段，例如其输出脚本、金额或锁定时间。
3.2. 操作语义
验证规则被扩展：对于一个带有契约的UTXO，花费交易 $T_{next}$ 的验证不仅要求其scriptSig满足原始的scriptPubKey，还要求契约谓词 $C$ 对交易对 $(T_x, T_{next})$ 成立。这通过操作语义规则进行了形式化定义，该规则将契约检查集成到现有的比特币验证逻辑中。
3.3. 递归契约与状态机
一个强大的变体是递归契约，其中 $C$ 可以强制要求 $T_{next}$ 的输出本身包含相同（或相关）的契约 $C'$。这使得在比特币上实现状态机成为可能：每笔交易代表一次状态转换，契约确保状态机规则在一系列交易中得到遵守。本文将其形式化为一个交易序列 $T_1, T_2, ..., T_n$，其中对于每个 $i$，$C(T_i, T_{i+1})$ 成立。
4. 复杂比特币合约的规范
该形式化模型被应用于规范目前在纯比特币中无法表达或表达繁琐的合约。
4.1. 保险库与时间锁定提款
契约可以创建“保险库”，被盗资金可以从中恢复。一笔交易可以要求任何大额提款必须首先进入一个时间锁定的输出，允许所有者在未经授权的情况下取消它。这是通过一个检查 $T_{next}$ 的 nLockTime 字段和输出结构的契约来规范的。
4.2. 支付通道与闪电网络
虽然闪电网络已经存在，但契约可以简化并加固其底层构造。它们可以通过约束花费交易以匹配预先签名的更新，来强制要求通道的关闭交易必须是最新状态，从而防止旧状态广播。
4.3. 去中心化金融（DeFi）原语
简单的DeFi结构，如抵押债务或非托管交换，成为可能。契约可以将资金锁定在一笔交易中，该资金只能由一笔提供了来自交易对手的有效加密支付证明或清算证明的交易花费。
5. 高级语言原语
本文讨论了契约如何作为高级合约语言的编译目标。诸如“在时间T后提款”、“仅在交易对手签名时花费”或“从状态A转换到状态B”等原语可以直接映射到特定的契约约束，从而为比特币合约开发者提高了抽象级别。
6. 核心洞见与分析视角
核心洞见： Bartoletti等人不仅仅是提出另一个契约操作码；他们正在提供缺失的形式化理论，将一个聪明的技巧转变为比特币合法、可分析的编程范式。这是解锁在UTXO区块链上系统化工程复杂、安全合约的关键，超越了临时性的脚本编写。
逻辑脉络： 论证过程极具说服力且简洁：1）比特币的UTXO模型缺乏状态，限制了合约。2）作为解决方案提出的契约在形式化上理解不足。3）因此，我们构建一个形式化模型。4）使用这个模型，我们证明它可以表达有价值的、复杂的用例（保险库、通道、DeFi）。5）这种形式化自然使得更高级别的语言设计成为可能。这是一个经典的“理论指导实践”流程的精准执行。
优势与不足： 主要优势在于弥合了密码学/编程语言理论与比特币工程之间的鸿沟——这个鸿沟曾导致以太坊基于账户的模型中出现了代价高昂的错误。形式化语义允许进行属性验证，这是一个巨大的优势。隐含承认的不足在于比特币的政治经济学。正如本文所指出的，比特币“极其谨慎的做法”使得部署像契约这样的新操作码成为一项艰巨的任务，无论其形式化多么优雅。像闪电网络这样的第二层解决方案在没有原生契约的情况下取得成功，也引发了关于必要性与锦上添花的疑问。此外，模型的安全性依赖于一个假设，即受约束的字段（如脚本哈希）是充分的；与其他操作码之间不可预见的交互效应可能仍然存在。
可操作的见解： 对于研究人员，本文是一个蓝图：使用形式化方法来降低风险并澄清区块链升级。对于开发者，现在就开始设计假设契约存在的合约框架（如在Liquid或Stacks上所见）。对于比特币协议开发者，本文提供了论证BIP 119（OP_CTV）或类似提案所需的严格基础——它将一个功能请求转变为一个工程规范。最重要的启示是：比特币智能合约的未来不在于模仿以太坊，而在于利用独特的UTXO+契约范式，创建一类新的、可能更安全、更具可扩展性的去中心化应用。
7. 技术细节与形式化
形式化模型在上下文中定义了交易、脚本和验证。一个关键的技术细节是契约约束的表示。令 $ exttt{tx}$ 表示一笔交易。契约可以看作一个函数：
$\text{Covenant}_{\text{cond}} : \texttt{tx}_{\text{current}} \times \texttt{tx}_{\text{next}} \times \sigma \rightarrow \{\text{True}, \text{False}\}$
其中 $\sigma$ 代表验证上下文（区块高度等）。谓词 $\text{cond}$ 可以是 $\texttt{tx}_{\text{next}}$ 字段检查的合取：
$\text{cond} \equiv (\texttt{hashOutputs}(\texttt{tx}_{\text{next}}) = H) \land (\texttt{nLockTime}(\texttt{tx}_{\text{next}}) > T) \land ...$
这与像OP_CHECKTEMPLATEVERIFY这样的提案一致，该操作码将花费交易指定部分的哈希推入栈中进行比较。递归属性通过确保 $\texttt{tx}_{\text{next}}$ 的一个输出包含一个脚本 $S'$ 来形式化，该脚本本身强制执行一个契约 $\text{Covenant}_{\text{cond}'}$。
8. 分析框架与示例案例
示例：一个简单的保险库合约
目标： 创建一个UTXO，可以通过两种方式花费：1）即时，但只能到一个特定的“冷存储”地址。2）到任何地址，但只能在30天延迟后（允许取消盗窃）。
使用形式化模型的应用框架：
1. 初始锁定脚本（scriptPubKey）： 包含一个契约条件 $C_1$。
2. 契约 $C_1(T_{vault}, T_{spend})$： 必须评估为真。它检查：
a) 路径A（即时）： $\texttt{hashOutputs}(T_{spend}) = H_{cold}$ // 输出必须哈希到预先承诺的冷存储地址。
b) 路径B（延迟）： $\texttt{nLockTime}(T_{spend}) \geq \text{currentBlock} + 4320$（30天对应的区块数）且 $\texttt{hashOutputs}(T_{spend})$ 可以是任意值。
3. 验证： 当使用 $T_{spend}$ 花费保险库UTXO时，比特币节点执行脚本。它需要保险库所有者的签名并且验证 $C_1$ 对该交易对成立。
此示例展示了形式化模型的谓词 $C(T_x, T_{next})$ 如何通过对下一笔交易字段的具体检查来实例化，从而实现在基础比特币中不可能的安全属性（盗窃恢复）。
9. 未来应用与方向
形式化开辟了几个未来方向：
- 经过验证的编译器： 构建从高级语言（如Simplicity或Miniscript扩展）到嵌入契约的比特币脚本的编译器，并附带正确性的形式化证明。
- 跨链契约： 探索那些以其他区块链或预言机的事件为条件的花费契约，使用像SPV这样的加密证明，正如早期关于“桥”的研究和最近关于Rollup的研究所暗示的那样。
- 隐私保护契约： 将契约检查与零知识证明（例如，使用Taproot/Schnorr签名）相结合，以隐藏合约逻辑同时仍强制执行它，这是在Ark等项目正在探索的方向。
- 形式化安全分析： 使用该模型系统地分析提议的契约构造针对经济和密码攻击的安全性，类似于IEEE安全与隐私研讨会社区对以太坊智能合约所做的工作。
- 第二层协议简化： 通过利用原生契约，重新设计像闪电网络或侧链（Liquid）这样的协议，使其更高效、信任最小化，减少对复杂瞭望塔或联盟的需求。
10. 参考文献
- M. Bartoletti, S. Lande, R. Zunino. Bitcoin covenants unchained. arXiv:2006.03918v2 [cs.PL]. 2020.
- S. Nakamoto. Bitcoin: A Peer-to-Peer Electronic Cash System. 2008.
- J. Poon, T. Dryja. The Bitcoin Lightning Network: Scalable Off-Chain Instant Payments. 2016.
- M. Moser, I. Eyal, E. G. Sirer. Bitcoin Covenants. Financial Cryptography 2016 Workshops.
- Bitcoin Improvement Proposal 119 (BIP 119). OP_CHECKTEMPLATEVERIFY.
- G. Wood. Ethereum: A Secure Decentralised Generalised Transaction Ledger. Ethereum Yellow Paper. 2014.
- A. Miller, et al. Hashed Timelock Contracts (HTLCs). 2017.
- R. O'Connor. Simplicity: A New Language for Blockchains. Proceedings of the 2017 Workshop on Programming Languages and Analysis for Security.
- Blockstream. Liquid Network. https://blockstream.com/liquid/
- IEEE Symposium on Security and Privacy. Multiple papers on smart contract security analysis. Various years.