<p>In short, yes (kinda).</p>

<p>More in detail, Balzac can perform the operations required for HTLC transactions. The following transaction is redeemable by Alice providing the premimage of <em>h</em>, or by Bob after the timelock block 1550000 expires.</p>

<pre><code>transaction T_BtoA {
    input = B_funds: sig(kA)
    output = 1 BTC:
        fun(x,s:string) . sha256(s) == h &amp;&amp; versig(kApub;x)
            || checkBlock 1550000 : versig(kBpub;x)
}
</code></pre>

<p>So, Balzac can be used to express the transactions of an HTLC, or any payment channel.</p>

<p>BitML is designed to express contracts, and compiles to a set of Balzac transactions.
Thereby, it cannot be used to express arbitrary transactions.
Nonetheless, we can express a similar logic in BitML with the following contract (<a href="https://gist.github.com/stefanolande/e703afbd6e14befb6346e523a7f62065" rel="nofollow noreferrer">full code</a>):</p>

<pre><code>(choice 
  (reveal (h) (withdraw "Alice"))
  (after 1550000 (withdraw "Bob")))
</code></pre>

<p>This contract compiles to three transactions, one similar to <em>T_BtoA</em> above, and other two to move the bitcoin from the first transaction to either Alice or Bob.
Note that all transactions need to be signed by both participants when stipulating the contract, so they cannot be changed unilaterally.</p>

<p>While BitML can be used to express such transactions, at the moment it cannot express payment channels. With BitML you cannot design contract where the values of transactions are not known at compile time, or that require an unbound number of iterations. However, there is ongoing research to extend BitML with these features.</p>

CC BY-SA 4.0
2019-11-07T22:09:22.310Z
2019-11-07T22:09:22.310Z
Stefano Lande
<p>I have been reading the <a href="https://arxiv.org/pdf/1905.07639.pdf" rel="nofollow noreferrer">BitML</a> paper.  The language compiles to another language (Balzac [which in turn compiles to Bitcoin Script]), which can do <a href="https://github.com/balzac-lang/balzac/tree/master/xyz.balzaclang.balzac.examples/src/main/java/timelock" rel="nofollow noreferrer">relative and absolute timelocks</a>. Balzac can also do <a href="https://github.com/balzac-lang/balzac/blob/master/xyz.balzaclang.balzac.examples/src/main/java/time-commitment.balzac" rel="nofollow noreferrer">something that looks like an HTLC</a>. So it looks like Balzac could encode Lightning. Can BitML also do this?</p>

<lightning-network>
Can BitML encode Lightning?
Janus Troelsen
# Can BitML encode Lightning?

(Asked by: username_0 on 2019-10-12)

I have been reading the [BitML](https://arxiv.org/pdf/1905.07639.pdf) paper. The language compiles to another language (Balzac [which in turn compiles to Bitcoin Script]), which can do [relative and absolute timelocks](https://github.com/balzac-lang/balzac/tree/master/xyz.balzaclang.balzac.examples/src/main/java/timelock). Balzac can also do [something that looks like an HTLC](https://github.com/balzac-lang/balzac/blob/master/xyz.balzaclang.balzac.examples/src/main/java/time-commitment.balzac). So it looks like Balzac could encode Lightning. Can BitML also do this?

**Tags:** lightning-network


---

## 1 answers

### Answer by username_1 on 2019-11-07. Score: 2 | Accepted answer

In short, yes (kinda).

More in detail, Balzac can perform the operations required for HTLC transactions. The following transaction is redeemable by Alice providing the premimage of *h*, or by Bob after the timelock block 1550000 expires.

```
transaction T_BtoA {
    input = B_funds: sig(kA)
    output = 1 BTC:
        fun(x,s:string) . sha256(s) == h && versig(kApub;x)
            || checkBlock 1550000 : versig(kBpub;x)
}

```

So, Balzac can be used to express the transactions of an HTLC, or any payment channel.

BitML is designed to express contracts, and compiles to a set of Balzac transactions.
Thereby, it cannot be used to express arbitrary transactions.
Nonetheless, we can express a similar logic in BitML with the following contract ([full code](https://gist.github.com/username_1/e703afbd6e14befb6346e523a7f62065)):

```
(choice 
  (reveal (h) (withdraw "Alice"))
  (after 1550000 (withdraw "Bob")))

```

This contract compiles to three transactions, one similar to *T\_BtoA* above, and other two to move the bitcoin from the first transaction to either Alice or Bob.
Note that all transactions need to be signed by both participants when stipulating the contract, so they cannot be changed unilaterally.

While BitML can be used to express such transactions, at the moment it cannot express payment channels. With BitML you cannot design contract where the values of transactions are not known at compile time, or that require an unbound number of iterations. However, there is ongoing research to extend BitML with these features.


---

