Prototyping generic Bitcoin Smart contract

While ago, I’ve been building F# library for the Bitcoin Lightning Network (LN), DotNetLightning.
After (barely) finishing my first iteration, I’ve noticed that there is a more matured library called rust-lightning for doing the same for the rustlang, and I’ve switched my efforts to its .NET binding with C#
After working for both F# and C# for a decent amount of time, I noticed that it both has goodies and baddies for different domains.
One particular domain I think that F# is a clear winner is for prototyping a new idea.

So today, I will sketch out my recent idea about Bitcoin and how I use F# to organize my thoughts in my head.

But before that, I have to describe the overview about bitcoin smart contract and my thoughts about it.

What is a Smart contract?

1. Smart contract as a scripting language

The word “Smart contract” is mostly used to refer to a byte code which is executed on the blockchain as a part of the consensus mechanism, and sometimes including a programming environment to write that byte code.
One example of this is Solidity on Ethereum which compiles to the EVM byte code.

The bitcoin has a similar construction (bitcoin script) which is intentionally made less descriptive than the EVM byte code. and there is a proposal for a high level language which compiles down to the actual bitcoin script, namely Miniscript and its predecessor ivy-bitcoin BitML

However, at the same time at least in the Bitcoin community there is a consensus that writing a secure byte code is just a very little part of building the secure multi-party protocol.

2. Smart contract as a multi-party procedure

Recently, the trend is to bring the statefulness to outside of the blockchain, and use the blockchain as a “dumb” settlement layer. Which makes sense in terms of privacy and scalability.

In other words, the "smartness" of the contract is not in the blockchain but in the procedure among related party.

To note a few keywords for such trend, there is a Scriptless Scripts, Lightning Network (LN) , Discreet Log Contract DLC, etc.

All these contracts are defined as a set of procedure among multi-party (in most case, two-party)
For example something like

Alice and Bob shares specific transaction and some of those signatures
Both Verify signature and the shape of the transaction, if it is Ok Alice broadcast transaction XXX
If Bob sees the transaction on the blockchain before timeout, he sends an Adapter Signature with the same key with XXX and Alice verifies it and… otherwise ...

Such a way of defining the contract is secure and fine. But can we achieve more generality somehow? If we could make some kind of universal language to describe the “shape” of the contract, it would be a good mental model for protocol developers to build/communicate new Smart contracts.

3. Smart contract as a Transaction graph

At the same time, there is an old proposal by Jeremy Rubin called TXGL , which defines not only the script for the contract but also the shape of whole transactions which could be involved in the contract. This is great as a mental model for the developers, but in reality it is not enough. Because, some transactions are related with each other outside of the shape (e.g. by Adaptor Signature) and those relations will affect how we communicate with each other in course of the contract.

Objective

So, my hypothetical objective is

Could we make a declarative Universal language (or DSL) to describe the “shape” of the contract? and
Could we automatically compile that into an actual procedure describing what each party should do while executing the contract?

This is a very bold claim to make. And it might be impossible or overkill. But I have to try to make a PoC to see if it is really so.

The idea is affected by a proposal named Improv, which achieves something similar with the Miniscript but for a payment on the Lightning Network.
It is supposed to look similar to the Miniscript but compiles down to a multi-party-procedure instead of the byte code.

So, let’s first survey existing proposed contracts, and try to abstract properties of those.

Note for readers those familiar to the bitcoin protocol: I assume we are able to use Taproot and PTLC

types of on-chain contracts

It seems that most, if not every, on-chain contract has roughly three phases

Setup: exchange transaction graph and some of its signatures, adaptor signatures
Start: broadcast the root ancestor of those transactions (often called funding tx)
Act: react to events which happen on the blockchain or through communication with another party.

My purpose here is to define the language to describe 1 and 2, and deterministically generate 3 from it.
So, hopefully I can describe a contract with a set of transaction graphs. and the relation of the transactions in each graph.

With that in mind, let’s make a graphical model for Atomic swap with an adaptor signature. I won’t go into the details about the protocol.. The model will be something like

Similarly, the model for SAS: Succinct Atomic Swap will be

Modeling with FSharp

Then let’s model these relations using F# type. We are going to use NBitcoin to represent Bitcoin specific classes, and my own DotNetLightning off-chain specific types.

Let’s say we call each node in the above graph TxEntry,

open NBitcoin;
open DotNetLightning;

/// The object for describing the “Lock condition” of the on-chain payment.
/// It is not ready since the Miniscript is still in a research phase.
type Miniscript = NotYetReady
  with
  static member Parse(str: string): Miniscript =
    failwith “TODO”

type OnChainLock = Miniscript * Money

type EntryRelation =
  | AtomicallySetup
  | AtomicallyExecuted

type EntryId = int

// each node in the graph.
type TxEntry = {
  Id: EntryId
  Prev: TxEntry option
  Lock: OnChainLock
  Next: EntryId seq option
  RelatedEntry: (EntryId * EntryRelation) seq
}

type Entry = OnChain of TxEntry

The Contract is a set of graph of the TxEntry, so let’s define it as

type TxTree = TxEntry seq
type Contract = TxTree list

types of off-chain contracts

Bitcoin has two ways of payments, one is on-chain payment which must be recorded on the blockchain, and another is off-chain payment which is accomplished by the Lightning Network.

The mechanism of off-chain payment is quite different from those of on-chain, but some operations are analogous. (e.g. “we must commit to payment atomically to prevent option problem” or “Iff one payment is executed, another payment must be able to execute”).

So we can use a similar terminology to describe the contract.
See below table for how the “relation” of each entry is achieved in both on-chain and off-chain.

So for example, Submarine swap in the graphical representation could be.

Modeling in FSharp

So next let’s include the concept of an “off-chain” entry into the above code. It will be like

open NBitcoin;
open DotNetLightning;


/// The object for describing the “Lock condition” of the on-chain payment.
/// It is not ready since the Miniscript is still in a research phase.
type Miniscript = NotYetReady
  with
  static member Parse(str: string): Miniscript =
    failwith “TODO”

/// Same for off-chain Lock condition. Which also is not ready yet.
type Improv = NotYetReady

type OnChainLock = Miniscript * Money
type OffChainLock = Improv * Money

type EntryRelation =
  | AtomicallySetup
  | AtomicallyExecuted

type EntryId = int

// each node in the graph.
type TxEntry = {
  Id: EntryId
  Prev: TxEntry option
  Lock: OnChainLock
  Next: EntryId seq option
  RelatedEntry: (EntryId * EntryRelation) seq
}
type L2PaymentEntry = {
  Id: EntryId
  Lock: OffChainLock
  RelatedEntry: (EntryId * EntryRelation) seq 
}

type Entry =
  | OnChain of TxEntry
  | OffChain of L2PaymentEntry

We also update Contract type to include both on-chain and off-chain concept

type TxTree = TxEntry seq
type PaymentTree = L2PaymentEntry seq
type Contract = TxTree list * PaymentTree list

Finally, let’s define an actual Contract object for Submarine Swap.

let submarine_swap (alice_key: Key) (bob_key: Key) (amount_to_bob: Money) (amount_to_alice: LNMoney): Contract =
    let funding_tx_entry = {
        Id = 0
        Prev = None
        Lock =  Miniscript.Parse($“or(and( pkh({alice_key}), pkh({bob_key}) ), and(after(144), pkh(alice_key)))”), amount_to_bob
        Next = [1] |> Seq.ofList |> Some
        RelatedEntry = [(2, AtomicallySetup)]
    }
    let swap_tx_entry = {
        Id = 1
        Prev = Some funding_tx_entry
        Lock = (Miniscript.Parse($"pkh({bob_key})"), amount_to_bob)
        Next = None
        RelatedEntry = [(2, AtomicallyExecuted);]
    }

    let off_chain_payment_entry =
        let lock_condition = bob_key.PubKey
        {
            Id = 2
            Lock = lock_condition, amount_to_alice
            RelatedEntry = [(1, AtomicallyExecuted)]
        }
    [ (seq { funding_tx_entry; swap_tx_entry }) ], [ seq { off_chain_payment_entry } ]

Conclusion

This is a very rough sketch of my recent thoughts, and it is still in an early phase.

The next step will be to define the function to compile the Contract object to an actual state machine to handle the procedure of an interaction with the another party (and the blockchain), that is, function with the type

type ContractToProcedure = Contract -> Async<unit>

That is the most difficult part, and I will probably change the definition of the Contract on the way.

What I want to point out here is that in the research phase like this, it is important for me to define an algebraic data type in a succinct way so that I can alter the definition while I go back and forward with an implementation.

In other words, F# is very nice tool for Exploratory programming