I want to share a DSL I am building for describing and running bitcoin contracts.
It is not another effort to write Script in a higher level language.
Instead, the DSL is a tool for describing transactions, sending them to bitcoin node, and running assertions on the state of the system - using a declarative syntax.
The easiest way to describe it is by using an example
The key features of the DSL are to provide a declarative syntax for the following:
Describe transactions with a high level descriptive syntax
Write locking using miniscript, descriptors and plain old Script
Write unlocking scripts with high level constructs again - the runtime automatically tracks witness programs for generating signatures
Execute multiple branches of contracts using system state transitions
Interact with bitcoin node
Assert system state
There is still some more things I want to build, for example, incorporate taproot constructions and making it easy for users to run experimental versions of bitcoin.
Being able to write the ARK and lightning contracts and execute them on regtest using a high level DSL has been fun for me. I hope others will find the DSL useful too.
Looking at the lightning examples, it seems like it would be helpful to have a reorg_chain command along the lines of “extend_chain” that combines invalidateblock and generate and potentially replaces some previously confirmed transactions.
You might consider differentiating keys and addresses – eg
Seeing if you can rewrite feature_block.py might be worth doing – then the test case could perhaps easily be run on other node implementations, and perhaps it might be easier to add other tests, or easier to understand what the existing tests do if your DSL is actually a better way to describe these things?
The address suggestion is neat. It can help break away from the sig: prefixed construction. I’ll have to see how we can translate that into plain Script usage, e.g. in situations where we do things like script_sig: 'sig:@alice ""', etc.
Writing features.py with this DSL will be a neat way to validate the expressiveness of the DSL, so I’ll try to do that. I do want to say that the goals of features.py and this DSL are slightly different. The goal here is to write contracts and system state transitions at a high level to facilitate clearer communication between developers and to quickly experiment with ideas.
reorg_chain is interesting idea too. I’ll definitely incorporate it. I have taken a slightly different approach until now and that is to reset the system state to run a different set of transitions, but I can see some situations and developers will benefit from a reorg_chain approach.
Makes a lot of sense to join forces. The DSL has to eventually incorporate advances in contract definitions you guys are pushing forward.
As I see it, the DSL can definitely help with some of the goals mentioned in the “advanced scripting” and “graph of transactions” parts. The only thing I am not sure of and need to figure out is state-fullness.
On the tooling part, I am close to shipping a jupyter notebook to build, share and run DSL scripts. That might be useful to BitVM too. Attached is a sneak peak
What’s the best place to connect with people working on BitVM? Have you started work on defining constant expressions, templates and opcode composition?
For me, the main difference I had in mind would be that if you reset the chain, you have to mine the funding transaction a second time, whereas if you do a reorg you can keep the block that included the funding tx, and be a little bit more sure that you don’t accidentally change the funding tx as part of the reset. If you accidently change the coinbase txs when reorging you’ll also change the funding tx (which presumably spends some coinbase), and the spends of that funding tx, all of which make for poor test cases if (as in lightning) your contract is meant to be able to be spent in multiple ways.
We currently use Rust macros at GitHub - BitVM/rust-bitcoin-script at script_macro to work with Rust Bitcoin’s Script.
New scripts and opcodes can be composed and there is some syntactic sugar like loops. Looks like this:
fn script_from_func() -> ScriptBuf {
return script! { OP_ADD };
}
let script = script! {
for i in 0..3 {
for k in 0..(3 as u32) {
OP_ADD
if k == i {
OP_SUB
} else {
script_from_func
}
{ i * 42 }
{ k + 42}
}
}
OP_ADD
};
This is very cool, thank you for working on it! I noticed on your personal website that you’ve also worked on using TLA+ PLA+ to verify the completeness of Bitcoin contract protocols (hat tip to @dgpv who has also done similar work). I’m wondering if there’s any planned overlap, for example an automated way to extract information from a comprehensive DSL to use with TLA+ PLA+?
TLA+ is a different beast from this DSL. The goals of the two systems are pretty different with TLA+ being just so much more powerful - but slightly harder to pick up.
TLA+
With TLA+ you define a system state and possible transitions. TLA+ can then run a “model checker” that goes off and explores all possible reachable states. Once all the possible states have been generated, it asserts that certain properties that we define remain valid in all reachable states. If in any state, our properties are not satisfied, it can produce a trace showing which state transitions lead to that bad state. As you can see, this really helps debug concurrent protocols - just like Bitcoin and LN. I really think specing LN network communication protocols in TLA+ will help a lot. Anyway, I digress.
Bitcoin DSL
In contrast, the DSL requires developers to write all state transitions themselves and script their execution - this is similar to writing unit/functional tests for any code. The plus side of the DSL is that it runs your code on regtest, so you really know your scripts will result in real world system transitions. Which I find really helpful personally. I also found it very helpful to learn about various contract constructions - the DSL could be a nice teaching aid.
I took a quick look at @dgpv’s atomic swap contract. It is pretty serious effort. It will be nice to decompose such contracts into multiple modules.
Bitcoin blockchain - this captures the chain state and state transitions possible. It is kind of on the back burner atm. I’ll get back to it soon.
A module of functions to help build contracts - this kind of explodes in complexity, but we can start small and write functions for the most common use cases.
Communication between parties - I believe this should be left to vanilla TLA+ or pluscal.
Minsc has some functional constructs for looping that might be interesting to check out.
You can use repeat($n, $script) for cases where you need to repeat a script fragment exactly N times. For example to create a rollFromAltStack function (for statically known N):
The fragment can also be constructed with a function if the index is needed, for example `0 repeat(3, |$i| repeat(5, |$k| `$i OP_ADD {$k+10} OP_SUB`))`
There’s also unrollLoop($max, $condition, $body) that runs a script fragment as long as a condition is met, up to $max times. For example, a simple countdown from a number on the stack (up to 50) down to 0:
Minsc focuses entirely on defining the (Mini)Script-level spending conditions and doesn’t deal with higher-level abstracts like Bitcoin DSL does, so perhaps they could somehow work together.
Note that the main https://min.sc website is outdated, the docs are lacking the (non-Miniscript) Script features and the playground runs an old version. A playground that matches the code on github is available at https://min.sc/next/. I don’t have updated docs but I did publish some more advanced examples using CTV and Liquid’s introspection opcodes.
I should really get this cleaned up and released properly I haven’t been working on this for some time but picking this back up has been on my mind.
