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
Top comments (0)