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) 呢種形式化然後自然咁促成高階語言設計。呢個係一個經典嘅「理論促成實踐」流程，執行得非常精確。
優點與缺陷： 主要優點係彌合咗密碼學/編程語言理論同比特幣工程之間嘅差距——呢個差距導致咗以太坊基於賬戶嘅模型中出現咗代價高昂嘅錯誤。形式化語義允許進行屬性驗證，係一個巨大嘅優勢。隱含承認嘅缺陷係比特幣嘅政治經濟學。正如本文指出，比特幣嘅「極度謹慎嘅方法」使得部署新操作碼（如盟約）成為一項艱巨嘅任務，無論佢哋嘅形式化優雅程度如何。閃電網絡等無需原生盟約嘅第2層協議嘅成功，亦引發咗關於必要性與便利性嘅問題。此外，模型嘅安全性基於一個假設，即受約束嘅字段（如腳本哈希）係足夠嘅；與其他操作碼嘅未預見交互效應可能仍然存在。
可行見解： 對於研究人員，呢篇論文係一個藍圖：使用形式化方法來降低風險並澄清區塊鏈升級。對於開發者，立即開始設計假設盟約將會存在嘅合約框架（正如喺 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天以區塊計） AND $\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 社區對以太坊智能合約所做嘅工作。
- 第2層協議簡化： 重新設計如閃電網絡或側鏈（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.