Research Summary: Bitcoin Covenants Unchained

TLDR:

  • Covenants are linguistic primitives that extend the Bitcoin script language, allowing transactions to constrain scripts (smart contracts) that considerably expand the functionality of Bitcoin.
  • This paper provides the first formal model of covenants, which can be implemented with minor modifications to Bitcoin.
  • The advent of Taproot makes the framework described in this paper substantially more interesting because it enables vast functionality to be validated via a single hash function.

Core Research Question

How can protocols that implement covenants circumvent the limitations of Bitcoin’s native scripting language?

Citation

Bartoletti, M., Lande, S., Zunino, R. (2020). Bitcoin covenants unchained. https://arxiv.org/pdf/2006.03918.pdf

Background

  • Bitcoin has implemented a model of computation called Unspent Transaction Output (UTXO) where each transaction holds an amount of currency and specifies conditions under which this amount can be redeemed by a subsequent transaction, which spends the old one.
  • Compared to the Account-based model, implemented e.g. by Ethereum, the UTXO model does not require a shared mutable state: the current state is given just by the set of unspent transaction outputs on the blockchain.
  • While, on the one hand, the UTXO design choice fits well with the inherent concurrency of transactions, on the other hand, the lack of a shared mutable state substantially complicates leveraging Bitcoin to implement contracts, i.e. protocols which transfer cryptocurrency according to programmable rules.
  • Bitcoin scripts are small programs written in a non-Turing equivalent language represented by machine operation codes (opcodes). Whoever provides a witness that makes the script evaluate to “true” can redeem the bitcoins retained in the associated (unspent) output.
  • As previously explored here, the Bitcoin script language is intentionally restricted to a small set of opcodes, prioritizing security and efficiency over expressiveness and feature-completeness.
  • Historically, this has protected Bitcoin programs from catastrophic bugs that stemmed from excessive functionality at the protocol layer.
  • Bitcoin covenants are a promising solution as they carry a milder set of trade-offs relative to an expansion of the opcodes supported.

Summary

  • The authors begin the paper by laying a foundation for the semantic properties of Bitcoin covenants, as well a historical background of their implementation.
  • Then, the authors introduce a formal model of Bitcoin covenants, inspired by an informal, low-level presentation from previous works.
  • They use a formal model to specify complex Bitcoin contracts, which largely extend the set of use cases expressible in Bitcoin.
  • The use of covenants in the design of high-level language primitives for Bitcoin contracts is then discussed, and a big portion of the paper comprises examples of applications built using this technology. These examples are direct representations of the exploratory method employed by the authors to depict covenant scripts. As such, they are showcased in the Results section of this summary.
  • Finally, a practical implementation strategy for Bitcoin covenants is discussed. The authors note that previous approaches to covenants entailed operators to generate valid unlocking scripts and therefore to be able to spend funds encumbered by a set of covenants. They used the current implementation to propose a new operator, CheckSigFromStack, which checks a signature against data that is built by implicitly accessing the redeeming transaction.
  • While more specific implementation details were left out of the paper, the authors do suggest the use of Pay-to-Script-Hash (P2SH) transactions where covenants could represent a multi-signature transaction.

Method

  • In order to semantically represent Bitcoin covenants, the authors formally define Bitcoin’s script using a framework first described here

  • To contextualize this method of semantic representation, they apply a framework to the simplest form of a Bitcoin transaction, a coinbase transaction:

    image

  • Since coinbase transactions issue monetary units that did not exist previously, both the input (in) and signature/witness (wit) fields are formally modeled as undefined.

  • The out field contains a pair, whose first element is a script, and the second one is the number of bitcoins that will be redeemed by a subsequent transaction which points to T0 and satisfies its script.

  • In particular, the script versig(pkA,rtx.wit) verifies the signature (versig) in the wit field of the redeeming transaction (rtx) against a miner’s (A) public key pkA.

  • The miner (A) of T0 then decides to spend the recently mined bitcoins by sending them to user (B).

    image

  • The in field points to the transaction T0, and the wit field contains A’s signature on T1 (but for the wit field itself). This witness makes the script within T0.out evaluate to true, hence the redemption succeeds, and T0 is spent.

  • Once the semantic method is represented in two simple transactions, the authors then define two additional fields to better reason about covenants, absolute lock (absLock) and relative lock (relLock).

  • absLock is a value, indicating the first moment in time when the transaction can be added to the blockchain.

  • relLock is a list of values, of the same length as the list of inputs. Intuitively, if the value at index i is n, the transaction can be appended to the blockchain only if at least n time units have passed since the input transaction at index i has been appended.

Results

  • Through the use of the aforementioned semantic primitives, the authors provide practical use cases for Bitcoin covenants.
  • Out of all covenant scripts showcased in the paper, three examples stand out: an on-chain crowdfunding, the creation of Non-Fungible Tokens (NFTs), and the creation of Bitcoin vaults.
  • To contextualize the crowdfunding (CF) example, the authors hypothesize the following scenario: a start-up (Z) wants to raise funds through a crowdfunding campaign. The target of the campaign is to gather more than a specific amount of bitcoins (vB) by an amount of time (t), which is semantically represented below:
    image
  • The script above provides strong guarantees of two desirable conditions in this hypothetical crowdfunding example: the first guarantee is that Z can redeem the bitcoins deposited in this output, provided that the output at index 1 of the redeeming transaction pays at least the predetermined amount vB. The second condition allows an investor (Ai) to get back her contribution after the expiration date t.
  • Next, the authors depict the implementation of a Non-Fungible Token, which is defined as a token that represents the ownership of a physical or logical asset, which can be transferred between users.
  • Unlike fungible tokens (e.g., ERC-20 tokens in Ethereum), where each token unit is interchangeable with every other unit, non-fungible ones have unique identities.
  • Under the proposed architecture, a covenant-powered NFT could be represented using the following script:
    image
  • To claim ownership of the NFT above, a hypothetical user A mints the NFT by depositing 1 bitcoin to out(1).arg that is tied to her public key.
  • To transfer this NFT to user B, user A appends the transaction that minted the token, thereby changing its out(1).arg to B’s public key.
  • Lastly, the authors showcase how covenants can be used to create Bitcoin vaults (V), and unlock vaulted funds (S):
    image
  • Vaults are special bitcoin transactions that implement clawback mechanisms that enable users to retrieve funds once they have already been broadcast.
  • This is done through the use of timelocks in the unlocking script where, for a period of time, only the user who broadcast a transaction can redeem it.

Discussion and Key Takeaways

  • Previous approaches to highly functional Bitcoin smart contracts required the introduction of new sets of opcodes to support additional functionality at the stack level.
  • Such approaches were ultimately unsuccessful because of the Bitcoin’s community focus on security, and the unwillingness to change core consensus rules through hard forks.
  • Bitcoin’s script language is restricted to a set of essential opcodes that minimize the attack surface and prioritize computational efficiency at the expense of highly expressive functionality.
  • The focus of this paper is to introduce a formal method to implement Bitcoin covenants with minimal changes to Bitcoin’s stack machine operations.
  • To do that, this approach to covenants consists of a smart contract development framework (a protocol) that sits atop Bitcoin’s signature verification system.
  • Under this framework, smart contract execution outcomes are represented as keys, whereby the successful computation of a script produces a valid signature that “unlocks” funds, thereby enabling them to be transferred from user A to user B.

Implications and Follow-ups

  • This approach to smart contract execution can circumvent the current opcode limitations that exist in Bitcoin and the creation of highly expressive, potentially Turing-complete smart contracts.
  • As mentioned previously, in order to produce standard transactions from non-standard scripts, the authors propose the use of P2SH, which is widely used to develop simple smart contracts, such as multisig.
  • For context, in P2SH a transaction’s output is committed to the hash of the script, while the actual script is revealed in the witness of the redeeming transaction.
  • Since, to check its hash, the script needs to be pushed to the stack, the maximum size of a stack element is 520 bytes. This severely limits the extent of functionality that could currently be implemented using a covenant framework.
  • As noted by the authors, the introduction of Taproot would mitigate this limit. Taproot uses Merkle Trees to preserve the consistency of bitcoin smart contracts, and only a Merkle root would be captured on-chain. This would circumvent the 520-byte limitation and considerably increase the functionality of covenants.
  • An interesting development since the introduction of this paper is the release of BitML, which further formalizes the creation of bitcoin covenants through a compiler.
  • In conjunction with Taproot, BitML could provide a practical mechanism to develop highly expressive bitcoin smart contracts at some point in the future.

Applicability

  • Given the wide scope of applications and use cases for smart contracts, the advent of a safe, practical approach to Bitcoin smart contracts could give birth to a host of new applications built atop the Bitcoin blockchain.
  • There are, however, some computational limitations to the expressiveness of some hypothetical smart contracts. The absence of a full-fledged virtual machine with globally shared state does not make bitcoin covenants directly competitive to smart contract platforms.
  • It is likely that this technology will be applied predominantly to bitcoin custody products at first, given the significance of Bitcoin vaults, as described in the Results section of this summary.
  • The advent of advanced tooling for the creation of Bitcoin covenants, such as BitML, could also make possible the creation of bitcoin-denominated derivatives with functionality such as clawbacks clauses, dynamic terms, and liens.
6 Likes

This is a terrific summary, thank you for posting it. You mention that there’s a connection to BitML, which you describe as advanced tooling for the creation of Bitcoin covenants. Could you please elaborate on the connection to BitML? Aside from derivatives and the examples mentioned in the text (the vaults, the NFT, and the crowd funding campaign) what might some other potential uses be?

2 Likes

BitML is the evolution of the work presented here. It’s essentially a compiler that can be used to create practical programs that make use of this technology.

In terms of use-cases, there are several that come to mind. One could create financial derivatives with complex clauses, or multi-layered spending policies to add additional security layers to their custody scheme, or even clawback techniques that can “recover” funds in the event of a hack.

It used to be that these programs had to be limited to 520-bytes with P2SH, but the advent of Taproot really makes these use cases feasible. Due to how Tapscript contracts are structured, any arbitrarily complex contract can be represented as a hash digest weighing only 256 bits.

3 Likes

Thank you a lot for that nice summary!
Since you were mentioning in the Implications and Follow-ups section that the approach can enable the creation of “highly expressive, potentially Turing-complete smart contracts”, I have been wondering whether the authors comment in more detail on what the modelled covenants can express and what they cannot express?
I recently came across this paper by the same authors where they actually show that when extending Bitcoin’s scripting language with support for neighbourhood covenants this would make Bitcoin Turing-complete.
So, I have been wondering whether the summarised paper also includes some theoretical considerations concerning the expressiveness or whether it gives some concrete examples of functionalities that cannot be expressed?

4 Likes

That is a fascinating paper, thank you for linking!

The advent of Neighborhood Covenants seems to address a lot of the limitations disclosed in the original work, such as the notion that covenants are limited to the scripts of their redeeming transactions. While that was sufficient to implement an NFT in the original paper, the authors did note that fungible tokens would require more powerful mechanisms.

Correct me if I’m wrong, but Neighborhood Covenants circumvent this limitation by linking the scripts of a UTXO to that of its parents and grandparents. In turn, this substantially increases the expressiveness and applicability of this technology, and makes Bitcoin Turing-complete. :exploding_head:

Although the authors apply this to a hypothetical implementation of fungible tokens, I wonder if there would be broader applicability for covenants if there existed a high-level programming language that developers could make use of? Are you familiar with any attempts at creating one, or is it too early for something like this?

2 Likes

When I understand it correctly, then yes, neighborhoud covenants should make Bitcoin Turing-complete!
Actually, I also read a bit more deeply into the paper, and there it is said that
“Our neighbourhood covenants make Bitcoin Turing-complete. Indeed, this is also true without exploiting the stxo() and ptxo() operators, i.e. by only using covenants between the current and the redeeming transaction.”

When I get this sentence right, then the authors even say that also “normal covenants” (as formalized by them, only restricting the redeeming transaction and not the sibling or parent transaction) would already make Bitcoin Turing-complete.

So, technically, even the example of the Token implementation provided by them should be implementable without accessing the parent and the sibling transaction, but this would result in a rather inefficient implementation. When commenting on the proof for the Turing-completeness the authors say: “To improve the efficiency of tokens, instead of limiting to covenants on the redeeming transaction, as in the simulation above, we could also use covenants on the parent and sibling transactions”.

But, as you pointed out, this should really mean that smart contracts written in a high-level language should be compilable to Bitcoin protocols (in the worst case by using the brute-force approach described in the proof of the paper, so by expressing the contract as a register machine). I guess that the challenge, in the end, will really be to design a language that allows for an efficient compilation. Unfortunately, I am not aware of any work on that, but that would be a fascinating research direction! What do you think?

5 Likes

Thank you for the clarification w.r.t to the inefficient implementation approach still being Turing-complete, it makes sense!

Better high-level compilers would indeed be an incredibly interesting research area. Even if it takes time to create more efficient compilation techniques, it is still quite impressive what can be achieved with BitML alone. The lack of efficiency may be an acceptable trade-off in light of the existing guarantees (liveness, correctness, security) of these smart contracts.

If it is discovered that increased efficiency is hard to attain (or, alternatively, that it carries non-trivial trade-offs), what ways do you think the brute-force approach would hinder the usability of this technology?

3 Likes

I guess that the main problem with the encoding used for the proof is that the inefficiency would show up in terms of many steps in the contract execution. And every execution step would correspond to a Bitcoin transaction that needs to be included in the blockchain. So that may get really expensive in terms of fees and also may take a lot of time till the execution of a contract is completed (and during the whole execution, the money would be “locked” in the contract).

So that may not be feasible in practice. Maybe an interesting direction to investigate would be whether such executions (once enforceable on the blockchain) can be transferred to an off-chain setting so that the bad running times + costs would at least only constitute a worst-case scenario?
Another question, which came to my mind, was what, once such Turing-complete smart contracts have been made realizable (e.g., due to the introduction of taproot), are the “philosophical” arguments against adding more language primitives for making smart contract programming more practical?
So, e.g., add support for neighborhood covenants (in addition to “normal” covenants)?
There have been quite some arguments made for staying in a restricted computational setting. But once Turing-completeness is achieved anyway, optimizing the language for efficiency could be less controversial? (Being a theoretician speaking here, I would be very interested in your opinion on that! :slight_smile: )

4 Likes

I think it depends on the complexity of the addition. Schnorr+Tapscript+Taproot have been in the works for nearly 4 years, and are only now being deployed due to the focus on security and soft-fork minimization.

I’m cautiously optimistic about OP_CHECKTEMPLATEVERIFY, though. Even though it may not be expressive enough to support the implementation of things like fungible tokens, it could be an interesting starting point. If it is proven successful, there might be more openness to optimizing these constructs in layer 1.

When it comes to neighborhood covenants, do the authors get into which hypothetical functionality and/or opcodes would have to exist to make their implementation more practical?

4 Likes

Sorry for the late reply!

In the paper, the authors do not go so much into the technical details of the opcodes that would be needed but describe the required functionality/opcodes on a formal level.
They propose quite some extensions to the scripting language that are summarized by the following figures:

image

Unfortunately, the formatting makes one a bit hard to read, but I think that the main additions that are required would be the following:

  • An additional output field arg that can be used to encode state information
  • The ability to access different outputs (and their fields) related to the output/transaction that contains the script
    • rtxo(n): n-th output of the redeeming transaction (this is needed to implement “normal” covenants)
    • stxo(n): output redeemed by the n-th input of the redeeming transaction (this is needed to implement neighbourhood covenants)
    • ptxo(n): output redeemed by the n-th input of the current transaction
    • (One should note that it is, in particular, possible to access the arg fields of these outputs)
  • Some opcodes that can operate on outputs (access information about them and their fields) and in particular:
    • A verrec(o) functionality/opcode that takes as input an (accessible) output o and requires that this output has the same script as the current output (whose script contains verrec). This implements a recursive covenant
    • A verscr(scr, o): functionality/opcode that checks that the script of output o is syntactically equal to scrabble. This implements a “standard” covenants (without recursion)

The authors also make some points concerning the practicability of the proposed extension is that the covenant-checking itself should be rather cheap (computations/memory-wise) for the clients:

  • It would be required that Light nodes (only) must store parent transactions in addition to UTXOs
  • The implementation of covenants (so the verrec and verscr) can be done very efficiently since they only require comparing scripts for their syntactic identity (which can be simply done by comparing their hashes). This would be an advantage compared to other proposed opcodes, as CheckOutputVerify, which would also enable covenants.
4 Likes

Thank you for this excellent breakdown. This system indeed carries more optimal trade-offs when compared with CheckOutputVerify and it should be interesting to see where this is going.

2 Likes

@cipherix
I applaud your work; it is fascinating to read again. I won’t just read about this fascinating subject without contributing.

The scripting language used by Bitcoin has a number of significant drawbacks, though: Lack of Turing-completeness, which means that while a sizable portion of computing is supported by the Bitcoin scripting language, it is not nearly all supported. Loops are the main category that is absent.

I find this topic worthy, Old but Gold

We have implemented covenants without new opcodes on Bitcoin SV. Schnorr Signatures, Taproot and zero-knowledge proof can also be implemented with the original opcodes from Bitcoin launched in 2009.

1 Like