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})$： 必須評估為 True。它檢查：
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 Symposium on Security and Privacy 社群對以太坊智能合約所做的工作。
- 第二層協議簡化： 重新設計像閃電網路或側鏈（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.