A Conversation with the Creators of BitML

Tooling and Languages
,
1

A Conversation with the Creators of BitML

Background on BitML

Bitcoin smart contracts have historically been intentionally restricted to a small set of use cases, as its community prioritizes security and efficiency over expressiveness and feature completeness. BitML is a novel, domain-specific language for writing smart contracts which could bring greater flexibility to Bitcoin smart contracts. Its design is intended to enable the implementation of Turing-complete programs atop Bitcoin, with minimal changes to its core protocol.

A contract written in BitML is compiled to a set of standard Bitcoin transactions and executed on the blockchain. The power of BitML is that it guarantees a faithful execution of the high-level contract. Nothing is lost in translation. As a result, a developer using BitML can reason about the correctness of the BitML contract instead of having to analyze the resulting Bitcoin protocol. This means Bitcoin smart contracts can remain secure (and in alignment with the community’s security ethos) while having much broader applicability.

For more on BitML, be sure to check out SCRF’s Summaries on BitML: A Calculus for Bitcoin Smart Contracts, and Bitcoin Covenants Unchained.

Background on the Interviewees

  • Massimo Bartoletti is an Associate Professor at the Department of Mathematics and Computer Science of the University of Cagliari and has a Ph.D. in Computer Science at the University of Pisa.
  • Roberto Zunino is an Adjunct Professor at the University of Trento where he focuses on formal techniques for cryptographic protocol analysis and with an emphasis on blockchain systems.
  • The following authors have also contributed to the body of research that supports BitML: Stefano Lande, Nicola Atzei, Nobuko Yoshida, and Maurizio Murgia.

Interview

Q1: Are you aware of groups/companies using BitML to design real-world Bitcoin smart contracts nowadays? If not, what are the main obstacles that you currently see hindering deployment?

A: Although we are not aware of any attempt to use BitML in the wild, we are in touch with blockchain companies which are developing new UTXO-based smart contract languages inspired by the BitML design. In our view, the main obstacle that hinders the adoption of BitML is its limited expressiveness, which is a direct consequence of using Bitcoin as a compilation target. Indeed, our primary goal when designing BitML was executing BitML contracts in Bitcoin as-is, without using non-standard transactions or relying on sidechains, like RSK or Elements. The good news is that the expressiveness of BitML can be significantly increased with minimal extensions of the compilation target: for instance, adding covenants to Bitcoin would make it possible to have a (nearly) Turing-complete language. We discuss this point more in detail below.

Q2: In a follow-up work, you created a toolchain; what is the amount of knowledge/expertise expected from protocol designers to use this toolchain?

A: BitML is easy to learn: it only has a handful of constructs, each one having an intuitive semantics. Even if it is different from everyday programming languages, developers should be able to understand how to use it in a few hours.

On the other hand, designing a smart contract for a complex task can be challenging, whether one is using BitML or not. This is because one needs to ensure that the contract behaves correctly not only when run by honest participants, but also in the presence of adversaries. Fair gambling games, for instance, are notoriously hard to design. The verifier included in the tool chain helps designers verify complex contracts. For instance, it is possible to ensure that in no case the currency can get “frozen” inside the contract, or that honest players eventually get their collateral back.

Q3: How easy is it to specify meaningful correctness and security properties for Bitcoin smart contracts?

A: Currently, BitML supports the verification of two kinds of properties: liquidity, and linear temporal logic (LTL) properties. Specifying liquidity is straightforward, since the query language features a dedicated construct for this property. Specifying LTL properties instead requires a basic understanding of LTL, which perhaps is not among the skills of average developers.

Q4: The current soundness result for BitML covers trace properties. Do you think that there is the possibility to extend this result to broader property classes (like hyperproperties)?

A: We believe that it is possible to extend our results to cover branching-time properties, such as those expressible in CTL, or even in the probabilistic logic PCTL. We are working in this direction right now.

Extending our results to hyperproperties could be possible, but at this moment it seems difficult to do without neglecting the probabilistic aspects of the BitML transition system.

Q5: Do you consider it a possibility to add support for quantitative or probabilistic reasoning to BitML (e.g., to reason about the winning chances/expected outcomes of parties in a contract)?

A: Some forms of quantitative reasoning are already available. For instance, in BitML we can verify that a participant can eventually redeem at least a certain amount of currency from the contract. Further, in some cases it is possible to automate the verification of fairness: we did this, for instance, for a lottery contract. In the general case, though, it seems hard to verify that a game contract is fair, or that the expected payoffs of the participants are the intended ones.

We are currently working on supporting more probabilistic reasoning in BitML, using the PCTL logic to express some probabilistic properties of interest.

Q6: BitML currently is, as you describe, not “Bitcoin-complete”. Are there concrete plans to extend BitML to a “Bitcoin-complete” language?

A: BitML is not Bitcoin-complete, in the sense that there exist contracts which are executable in Bitcoin but are not expressible in BitML. The main sources of incompleteness are two:

  1. off-chain interactions are limited to stipulation, revealing secrets and providing authorizations. In particular, stipulation requires that all the transactions obtained by the BitML compiler must be signed by all the participants before the contract starts.
  2. partial signatures (like those obtained through SIGHASH_ANYONECANPAY and SIGHASH_SINGLE) are not used.

As a consequence of the design choices above, contracts with a dynamically-defined set of players, or an unbounded number of iterations, are not expressible in BitML.

Recently, we have proposed an extension of BitML ([2011.14165] Verifying liquidity of recursive Bitcoin contracts) which partially overcomes the first limitation. More precisely, the extended BitML allows participants to “renegotiate” a contract at run-time. Besides allowing participants to provide new deposits and to commit to new secrets at run-time, renegotiation also allows for “consensual” recursion, still admitting compilation to standard Bitcoin transactions, and a sound analysis for contract liquidity.

Relaxing also the other constraint would allow to further extend the expressiveness of BitML. For instance, recursion and partial signatures enable crowdfunding contracts, and more complex off-chain protocols enable micro-payment channels. Notably, these extensions could be implemented without modifying Bitcoin.

Q7: Do you see applications for Bitcoin competing with Ethereum as a smart contract platform (with the introduction of covenants)?

A: It is difficult to predict which platform will win this competition, since this depends on many factors besides the effectiveness of the smart contracts machinery (not mentioning the impact on the competition of emerging blockchain platforms like Cardano and Algorand, to cite a few).

However, abstracting from the actual blockchain platform, we envision a competition between stateless and stateful smart contracts. Both types of design have pros and cons. On the one hand, programming contracts in a stateful model (like in Ethereum) is perhaps more natural for most developers, whereas encoding state in a stateless model (like we do in BitML) requires a different way of thinking. On the other hand, the stateless UTXO model (like Bitcoin’s) simplifies the blockchain design, as the global state of the blockchain is just the set of unspent transaction outputs. This has a direct consequence on scalability and throughput, since more transactions can be executed concurrently. Another advantage of the stateless approach is that it seems more amenable to verification. For instance, BitML features a sound and complete verification technique for contract liquidity.

Q8: How do you see the future of extensions of the Bitcoin scripting language for more efficient Bitcoin smart contracts? Which would be the specific additions to the language that you would promote?

A: In general, we believe that adding covenants would be crucial to enable a large class of Bitcoin smart contracts. Covenants may come in many flavors, and the recent BIP119 proposes one of them. We also proposed our own flavor of covenants in https://arxiv.org/abs/2006.03918. Our covenants allow Bitcoin scripts to inspect the transactions in their neighborhood, i.e. those which are close in the transaction graph. For instance, we have shown that our covenants would allow Bitcoin to support fungible tokens efficiently.

Further, it would be nice to have “user data” fields in transactions, where one can store the current state of the contract, and ensure state invariants using covenants. These stateful contracts could require large scripts, exceeding the current 520 bytes limit. The adoption of Taproot would mitigate this issue, by allowing transactions to witness only the part of the contract to be executed.

Crucially, these extensions would keep the feature that scripts are run in constant time, so avoiding to resort to a “gas” mechanism as in Ethereum.

Key Takeaways & Follow-Ups

  • We’d like to thank the authors of BitML for their work on this topic over the years and for taking the time to write such thoughtful answers.
  • SCRF is also thankful to @clara.schneidewind for contributing to the questions posed to the authors and for writing an excellent summary on BitML.
  • As covered in the interview, BitML can be instrumental in increasing the usage of smart contracts on Bitcoin through a set of trade-offs that are compatible with the ethos of its community.
  • Taproot has been mostly overlooked because, as a foundational technology, it is difficult for the average user to envision some of the use-cases it enables.
  • However, as discussed here and in our previous summaries, Taproot may serve as a building block for the adoption of languages such as BitML, which can push Bitcoin’s functionality closer to Turing-completeness.
7 Likes
2

A particularly interesting point that I found raised here is the distinction between stateful and stateless computation (mentioned in question 7). I have been wondering to which extent this distinction can be potentially hidden from the contract developers in the end? E.g., by the development of suitable stateful high-level languages that are compiled to Bitcoin smart contracts?
In particular, given that an extension (such as the proposed covenants) that would make Bitcoin Turing complete would be implemented, one should be able to compile classical stateful programming languages into Bitcoin protocols?

6 Likes
3

First of all, thanks to both you and @cipherix for putting this together. And obviously a really big thank you to the authors for their great work and for answering these questions with some depth!

I was also interested in that stateful/stateless answer. From my reading, it looked like the pro of the stateless was verification and scalability. Can that pro be maintained if stateful computation is introduced through an extension?

I also thought it was interesting that the completion between these two seems to be framed as a competition between convention and utility. It seems here that the primary pro for the stateful approach is that it’s familiar and comfortable to use for developers. I have to imagine there are other advantages, but it if really is mostly convention, should we then be concerned with maintaining or hiding stateful approaches for contract developers?

5 Likes
4

Stateless contracts provide some very interesting benefits, especially when it comes to privacy and scalability.

With BitML and technologies like Merkelized Abstract Syntax Trees (MAST), you can have a single commit on-chain representing full-fledged applications, whereby only the stakeholders within that application share the application’s state.

Beyond privacy, this approach also reduces the amount of data that is ultimately stored on-chain since everything except the contract’s commits, accompanying proofs and execution outcomes can be pruned. As the authors point out, this promotes better scalability for base layers.

I echo the author’s point that there are many factors beyond the effectiveness of the smart contracts machinery that will determine whether a stateful or stateless approach is appropriate. It should be interesting to discuss how these approaches will evolve with the advent of zk-rollups, which seem to live at the intersection of stateful and stateless.

5 Likes
5

Thank you both for joining us. This was a wonderful conversation to read. A quick question: How might something like BitML work in conjunction with an L2 like Lightning Network?

2 Likes
6

It wouldn’t be very relevant for Lightning, but it could potentially simplify the creation of new types of payment channels as well as channel factories. It’s a very new paradigm so it’s hard to tell what people will use it for.

2 Likes
7

I really enjoyed reading about the potential uses of a BitML-enhanced Bitcoin. This is more of a question for the community than for our guests specifically: How do you all envision Bitcoin’s status changing once features like the ones promised by BitML that become available? If it’s too slow and restricted to compete directly with Ethereum-based projects, what will its use case be? What would a Bitcoin DAO look like? And what might it do?

3 Likes
8

Here are some non-technical questions. I was wondering how the learning curve of BitML compares with languages like Solidity or Vyper? Does its syntax bear resemblance with these or other languages?

2 Likes
9

Great question! I have not attempted to build an application using BitML, but I would imagine that as the language evolves, there would be compilers that convert code from high-level programming languages down to BitML.

Given how novel the area of stateless contracts is, the learning curve is potentially steeper as there isn’t the same level of tooling and educational resources available relative to Solidity or Vyper.

There are, however, very interesting properties that make BitML easier to use relative to other languages when it comes to developing safe applications. For example, one can guarantee that a BitML smart contract will not freeze funds whereas achieving the same level of guarantee with Solidity could be much more resource intensive.

4 Likes
10

Is it fair to say that BitML uses a model similar to functional programming (pure functions and data immutability) and comparing solidity to BitML would be akin to comparing a language that embraces the imperative style such as Java with something like OCaml?

This has me wondering if some of the guarantees offered by BitML are also available in smart contract languages made in the spirit of existing functional languages such as Michelson (OCaml) and Plutus (Haskell)?

3 Likes
11

BitML has no first-order functions, so it would be inappropriate to classify it as a functional language. The closest programming paradigm is that of process calculi, whose early exponents are Milner’s CCS and pi-calculus, and Hoare’s CSP. Compared to these calculi, BitML is somehow simpler, since parallel processes (contracts) proceed independently, being unable to synchronize or communicate with each other. Further, recursion is only possible if all participants consent to that after stipulation.

Regarding the learning curve, we think that the main issue here is not the idiosyncrasies of the language, but the “defensive” style of programming which is inherent to smart contracts development (whatever language is used).

Indeed, the basic version of BitML features only a few language primitives, whose choice derives from the fact that we want to compile BitML contracts to (sets of) standard Bitcoin transactions, whose redeem logic is subject to the limitations of Bitcoin script. More precisely, BitML contracts are guarded choices between subcontracts, where subcontracts may have one of the following forms:

withdraw A — transfers all the funds to A
split v1 -> C1 | … | vn -> Cn — split balance between subcontracts C1,...,Cn
reveal a if p. C — if a secret has been revealed, proceeds as C
after t:D — after time t, proceed as D
A:D — if user A authorizes the move, proceed as D

Despite their minimality, the combination of these primitives gives rise to a wide variety of smart contracts, proving the security of which could be surprisingly complex. Just to give the idea, gambling games (like lotteries, poker, etc.) require the developer to devise economic mechanisms to disincentivize players from behaving dishonestly (where dishonest behaviour also includes stopping interacting).

In our experience, the main difficulty in developing contracts is to anticipate all the possible forms of misbehaviour, and to devise suitable countermeasures in the form of economic incentives / disincentives.

6 Likes
12

We implemented stateful contracts on Bitcoin SV, which uses the original opcodes from Bitcoin launched in 2009. It is based on covenants, which we also implemented without new opcodes. Our high-level programming language sCrypt is an embedded DSL in TypeScript. In addition, we have implemented Schnorr Signatures, Taproot and zero-knowledge proof, among other things. Surprisingly, all of these can be done without introducing new opcodes.

image
image2704Ă—774 145 KB

1 Like