BitML in a nutshell¶
BitML contracts allow two or more participants to exchange their bitcoins according to complex pre-agreed rules. Below we illustrate the primitives of BitML through a series of simple examples (see [CCS18] for a reference to BitML syntax and semantics).
The first step in designing a BitML contract is to declare the involved participants.
For instance, we can declare three participants
"C" as follows:
(participant "A" "029c5f6f5ef0095f547799cb7861488b9f4282140d59a6289fbc90c70209c1cced") (participant "B" "0316589526daa876ef27937e48176da08fc95eaef7315fa20a07114d5fb8866553") (participant "C" "03c7e157beee3815300c678840988713c9928d986b26fe0dc2533f304c19268a2f") (debug-mode)
Each participant is associated to a public key: for instance,
has the public key
(debug-mode) is needed to generate auxiliary keys
which are used by the BitML compiler,
instead of declaring them as you are supposed to when executing a contract in
a real life scenario.
"A" simply wants to donate 1 BTC to
To this purpose,
"A" must first declare that she owns
a transaction output with 1 BTC.
We can define this transaction output as follows:
(define (txA) "tx:02000000000102f28b8ec15a48abd9cda80d1c770ff9770dc0c549ddb1b8013b9e50a8799614aa000000001716001412a88716720982b693ab2bd2a2fcd4d98bdd2485feffffff08d59c3aeafd6003e6e099adde64f17d6ec7950619c22b50466281afa782e9d4000000001716001433845a8590dbf145b52bdd777103d1ddfdaa9cedfeffffff022fac1f000000000017a914e9f772646a0b6174c936806dab1b882e750ac04a8740420f00000000001976a914ded135b86a7ff97aece531c8b97dc8a3cb3ddc7488ac02473044022060135384eafe9a8021e8b8c46da20e7cd5713d581c3f79b1da3d2f7860a1bfed02206ca1ac1616d7ab778bcbb235b4b24286c2181ec171b8cadeaa9ee5f4f78fd330012102d5f8f263a81427330e7f26ba5832a2cd01e960bf145be2101bc0b6bb0fde8c2d0247304402200e02da2228774b47ff03a5a7c1bf1d070d0cec6cd9a08d6862e1855ba33dfb9f0220011511f10aaefbf402b2944b6a877c1ff9890a7fc3e266bbb74318b4540c555d012103ef2a573fbd46356dcbdbedcecc9aa25dcb500512e2be394297475ed157a9cfc6bdb51600@1")
In the definition above,
are the bytes of the serialized transaction, and the trailing
"@1" is the index of the output.
The contract advertised by
"A" is the following:
(contract (pre (deposit "A" 1 (ref (txA)))) (withdraw "B"))
The contract precondition
(pre (deposit "A" 1 (ref (txA))))
agrees to transfer the 1 BTC referenced by the transaction output
under the control of the contract.
The actual contract is
this just transfers the funds deposited into the contract to
In the previous contract, the initial deposit has been provided by a transaction output;
more in general, a contract can gather money from more than one transaction.
For instance, assume that another participant
"C" wants to contribute 1 BTC to the donation.
The contract precondition is modified as follows:
(contract (pre (deposit "A" 1 (ref (txA))) (deposit "C" 1 "tx:020000000193c18c921ed3947b862c746ddfe8a8b7459da00825822e09b95c61aaedc71dbf00000000e347304402204b77785e510ab83746732ce435e28a0e46d415ed0ebb8de407c45c66824530bf02202fdf08cd26b5ce376bcb215fe974dddc413be3b74b87e8beae27b1d812c3869d01473044022071b0ced4dd60799531eefe4e61892602637897a18f69f4e5cec22247c59b6c770220768ecc22e772477c8bbd762366d121b0b3d48a3b91334e1a369bbd848373fde3014c516b6b006c766c766b7c6b52210339bd7fade9167e09681d68c5fc80b72166fe55bbb84211fd12bde1d57247fbe121034a7192e922118173906555a39f28fa1e0b65657fc7f403094da4f85701a5f80952aeffffffff01a0bb0d00000000001976a914ce07ee1448bbb80b38ae0c03b6cdeff40ff326ba88ac00000000@0")) (withdraw "B"))
Assume now that
"A" wants to donate 1 BTC to
but only after a certain time
For instance, the 1 BTC could be a birthday present to be withdrawn
only after the birthday date; or the amount of a rent to the landlord,
to be paid only after the 1st of the month.
We represent the time
t as a block height.
For instance, we set
t to 500000
(note that the block at this height was actually mined on
To craft this contract we use the primitive
after height contract,
which locks the
the block at the given
height is appended to the blockchain.
We also reuse the transaction output
txA from the previous example:
(define (t) 500000) (contract (pre (deposit "A" 1 (ref (txA)))) (after (ref (t)) (withdraw "B")))
This contract ensures that only after
the block at height
t has been appended to the blockchain,
"B" will be able to redeem 1 BTC from the contract,
by performing the action
The following contract allows
"A" to recover her deposit if
"B" has not withdrawn within a given deadline
(define (t) 500000) (define (t1) 510000) (contract (pre (deposit "A" 1 (ref (txA)))) (choice (after (ref (t)) (withdraw "B")) (after (ref (t1)) (withdraw "A"))))
The contract allows two (mutually exclusive) behaviours:
"B" can withdraw 1 BTC.
Before the deadline
t no one can withdraw;
t (but before
"B" can withdraw,
while after the
t1 both withdraw actions are enabled,
so the first one who performs their withdraw will get the money.
In all the previous examples, the deposit within the contract is transferred to
a single participant. More in general, deposits can be split in many parts, to
be transferred to different participants. For instance, assume that
"A" wants her
1 BTC deposit to be transferred in equal parts to
"B1" and to
We can model this behaviour as follows:
(define (Pay-split) (split (0.5 -> (withdraw "B1")) (0.5 -> (withdraw "B2"))))
The split construct splits the contract in two or more parallel subcontracts, each with its own balance. Of course, the choice of their balances must be less than or equal to the deposit of the whole contract.
We can use split together with the other primitives presented so far to
craft more complex contracts. For instance, assume that
"A" wants pay 0.9 BTC to
"B", routing the payment through an intermediary
"I" who can choose whether to
authorize it (in this case retaining a 0.1 BTC fee), or not. Since
"A" does not trust
she wants to use a contract to guarantee that: (i) if
"I" authorizes the payment
then 0.9 BTC are transferred to
"B"; (ii) otherwise,
"A" does not lose money.
We can model this behaviour as follows:
(contract (pre (deposit "A" 1 (ref (txA)))) (choice (auth "I" (split (0.1 -> (withdraw "I")) (0.9 -> (withdraw "B")))) (after (ref (d)) (withdraw "A"))))
The first branch can only be taken if
"I" authorizes the payment: in this case,
"I" gets his fee, and
"B" gets his payment. Instead, if
"I" denies his authorization, then
"A" can redeem her deposit after block height
So far, we have seen participants using persistent deposits, that are assimilated by the contract upon stipulation. Besides these, participants can also use volatile deposits, which are not assimilated upon stipulation. For instance:
(pre (deposit "A" 1 (ref (txA1))) (vol-deposit "A" x 1 (ref (txA2))))
"A" the possibility of contributing 1 BTC during the contract execution.
"A" can choose instead to spend her volatile deposit outside the contract.
x is a handle to the volatile deposit, which can be used as follows:
(define (Pay?) (put (x) (withdraw "B")))
x is not paid upfront, there is no guarantee that
x will be
available when the contract demands it, as
"A" can spend it for other purposes.
Volatile deposits can be exploited within more complex contracts, to handle
situations where a participant wants to add some funds to the contract. For
instance, assume a scenario where
"A2" want to give
"B" 2 BTC as a present,
paying 1 BTC each. However,
"A2" is not sure a priori she will be able to pay, because
she may need her 1 BTC for more urgent purposes: in this case,
"A1" is willing to
pay an extra bitcoin. We can model this scenario as follows:
"A1" puts 2 BTC as a
persistent deposit, while
"A2" makes available a volatile deposit
x of 1 BTC:
(contract (pre (deposit "A1" 2 (ref (txA1))) (vol-deposit "A2" x 1 (ref (txA2)))) (choice (put (x) (split (2 -> (withdraw "B")) (1 -> (withdraw "A1")))) (after 700000 (withdraw "B"))))
In the first branch,
"A2" puts 1 BTC in the contract, and the balance is split
"B" (who takes 2 BTC, as expected), and
(who takes her extra deposit back).
The second branch is enabled after
d, and it deals with the case where
"A2" has not put her deposit by such deadline. In this case,
"B" can redeem 2 BTC,
"A2" loses the extra deposit. Note that, in both cases,
"B" will receive 2 BTC.
A useful feature of Bitcoin smart contracts is the possibility for a participant to choose a secret, and unblock some action only when the secret is revealed. Further, different actions can be enabled according to the length of the secret. Secrets must be declared in the contract precondition, as follows:
(pre (secret "A" a "f9292914bfd27c426a23465fc122322abbdb63b7")
"A" is the participant who owns the secret,
a is its name,
"f9292914bfd27c426a23465fc122322abbdb63b7" is its
We never denote the value of the secret
itself. A basic contract which exploits this feature is the following:
(define (PaySecret) (revealif (a) (pred (> a 1)) (withdraw "A")))
This contract asks
"A" to commit to a secret of length greater than one,
as stated in the predicate
(pred (> a 1)).
a, it allows
"A" to redeem 1 BTC upon revealing the secret. Until then, the deposit is frozen.
To reveal a secret without imposing a predicate use
(reveal (a) (withdraw "A"))
Note that we never refer to the value itself of the secret, rather we use its length. After compiling to Bitcoin, the actual length of the secret will be increased by η, where η is a security parameter, large enough to avoid brute-force preimage attack.