AlbaDsl & albaVm: Haskell based DSL and VM for Bitcoin Cash 2025 contract programming

Technical
#1

I’m exploring what Bitcoin Cash contract development in a Haskell DSL could look like and this is the, work in progress, result. Although this is op-code level script programming, Haskell’s abstraction mechanisms, strong typing, property based testing, and tooling such as the Language Server Protocol, makes it into a beast of its own. The project also provides a VM supporting the BCH 2025 features, which can be used to test arbitrary BCH bytecode. This is alpha software.

albaDsl

AlbaDsl is a shallowly embedded Domain Specific Language (DSL) for programming Bitcoin Cash Script (2025) in Haskell. It uses Haskell’s type system to statically enforce the type of the input and output stacks of a given program. Stack items can be assigned names for easier reference. Haskell functions can be used as a form of statically typed parameterized macros. Collections of such macros can be grouped into libraries and complex contracts can be built from them. Standard Haskell tooling such as syntax highlighting, code formatting, and Language Server Protocol (LSP) can be used. When using the Haskell Language Server, it gives immediate feedback about type errors such as mismatched stack element types.

Bitcoin Cash contracts written in albaDsl can be assembled into transactions and serialized into byte strings for publishing to the network using, for example, Bitcoin Cash Node.

albaVm

AlbaVm is a Bitcoin Cash virtual machine written in Haskell. It supports the BCH 2025 instruction set (including tokens, BigInts, and VM limits). It passes the Libauth 2025 standard and non-standard “success vectors”, and part of the non-standard and invalid “failure vectors” (correct failure reasons yet to be verified). AlbaVm can be used to evaluate arbitrary BCH byte code, and specifically albaDsl programs during development and testing.

Combining albaDsl & albaVm to verify contracts

Given an albaDsl program ‘p’, the albaDsl compiler ‘compile’ and the albaVm evaluator ‘eval’, it is possible to combine them into a function ‘g = eval (compile p)’. This function can be used to calculate the result of applying ‘p’ to arbitrary input stacks. Thus it can be used to write unit tests for the program. Such tests can make use of automatic property based testing via Haskell’s QuickCheck. Possibly, the LiquidHaskell program verifier can also be used for verification.

The example contracts in this repository (transferWithTimeout and lastWill) illustrate how contracts can be built and tested.

8 Likes
#2

Welcome to BCH Research!

How long have you been working on this? Is there any specific inspiration for the name “Alba”, was it related to ABLA?

I don’t know much about Haskell, but if I understand correctly this basically lets people write BCH scripts and transactions in Haskell which is very cool. I assume there must be online Haskell communities, have you tried showing this to them & what was their reaction?

2 Likes
#3

Amazing stuff, mate! Super excited to see what comes of this!

#4

Thanks!

It has been in the works since about last Bliss. And the name is a reference to that :slight_smile:

This is not really targeted at the Haskell community — to which a shallowly embedded DSL is not very novel. This is more to demonstrate to the BCH community that you can achieve something like a statically typed Forth by piggy backing on another high-level language. This won’t be a replacement for CashScript and Spedn anytime soon. But it might appeal to a small number of people (perhaps just me) who think that programming contracts Forth-style actually could be of interest, especially if you get the abstraction mechanisms and typing that Haskell can provide.

I plan to record a demo of what programming in this DSL looks like.

2 Likes
#5

Thanks! I plan to port over some more complex contracts. Also want to explore if LiquidHaskell can be used in proving contract correctness. And add in the proposed 2026 opcodes.

2 Likes
#6

@Jonathan_Silverblood will be thrilled to hear it.

I look forward to seeing it! Especially if it doubles as making some kind of new or cool BCH contract in a usable MVP app!

3 Likes
#7

I have uploaded a demo video (mp4) to GitHub in the form of a release:

This demo illustrates:

  • How to write a simple program in albaDsl.
  • How the Haskell LSP flags type errors in the program.
  • How to compile the program to bytecode.
  • How to evaluate the bytecode and view an execution log.
  • How changes in the albaDsl code affects the function signature.
  • How a function signature pins what an albaDsl function (macro) can do to the stack.
  • How to factor out code into a macro for readability.
  • How to use a macro defined in a separate library.
  • How to use QuickCheck to verify an albaDsl program.
  • How to name arguments on the stack.
  • How to use BigInt arithmetic.

In this demo we use the Haskell REPL to interact with the albaDsl & albaVm “tools”. You can of course also use these tools from compiled code (see the example contracts).

Also, a simplified API to the tools is presented. In reality they are slightly more complex (see DemoPrelude.hs).

3 Likes
#8

The albaDsl project has been updated with an initial version of the BCH 2026 VM & DSL that supports OP_EVAL. The DSL introduces a new type (TLambda) for a byte string on the stack that represents a compiled anonymous function. TLambda holds the type of the function it represents, so that the Haskell compiler can ensure correct stack item types at invocation sites. A parameterized typed macro ‘f’ can be turned into a TLambda with ‘lambda f’.

To support recursion in the Dsl a less strongly typed lambda (TLambdaUntyped) had to be introduced. To illustrate the power of recursion a few recursive functions where implemented: the factorial function, integer exponentiation, and merge sort on short ASCII strings (current implementation quickly runs into the max control stack depth for longer strings).

[https://github.com/albaDsl/alba-dsl/blob/282bd1ca27006f9323e4ea82ee1656f75cdbc42d/test/TestEval.hs#L97]
[https://github.com/albaDsl/alba-dsl/blob/main/test/Exponentiation.hs]
[https://github.com/albaDsl/alba-dsl/blob/main/test/MergeSort.hs]

3 Likes
#9

This sounds like a really cool playground. Are you generally pro or against OP_EVAL as a proposal or undecided? Do you expect this will enable us to either demonstrate its safety or problems?

#10

I’m for OP_EVAL as formulated by Jason. It is an immense boost to the expressiveness of the language while still being fully contained by the VM limits. Combined with the loops proposal I believe we are getting to a point where all the key features of an expressive language are in place. Having an expressive and well understood core language reduces the need for custom opcodes etc. in the future, and thus reduces risk overall by allowing the VM to stabilize.

I plan to continue to demonstrate the value that OP_EVAL (and loops) bring using this DSL. I also want to better understand the concerns that some people have, so may join the OP_EVAL discussion thread later.

5 Likes
#11

There were concerns regarding analyzability and auditing of contracts using Eval, check out the alternative: https://github.com/bitjson/bch-functions/tree/functions

It’s pretty much functionally equivalent to Eval, but better behaved in that it’s natural to use it in a way that makes it obvious what the program does. Trade-off is that MAST-like or other one-off constructions need to use 3 bytes more, e.g. these 2 are equivalent:

  • OP_DUP OP_HASH256 <hash> OP_EQUALVERIFY OP_0 OP_DEFINE OP_0 OP_INVOKE vs
  • OP_DUP OP_HASH256 <hash> OP_EQUALVERIFY OP_EVAL
3 Likes
#12

Very cool project @albaDsl, thanks for sharing! Have you thought about or experimented with getting more efficient stack scheduling in the compiled output?

2 Likes
#13

Thanks! Only thought about it so far as to include part of the CashScript optimization rules:

[https://github.com/albaDsl/alba-dsl/blob/main/src/Alba/Dsl/V1/Common/CashScriptOptimizerRules.hs]

Since it is a opcode level DSL some of the responsibility also falls on the developer using e.g. “roll” over “pick” in the right places etc. But I’m sure there is a lot more the tool can do.

Also, some contract developers may perhaps choose to sacrifice efficiency and byte size in order to get a one-to-one correspondence between the source code and the compiled output.

In the contract examples I have provided I haven’t focused on bytecode efficiency, just on quickly getting something that solves the problem.

1 Like
#14

Makes sense! I’d be curious how you might apply Haskell to the next level of optimization, even just limited to optimizing sequences of contiguous stack juggling operations like this tool (simply patched for BCH – note this optimizes for opCount though, the old blocker before 2025 limits): https://github.com/bitjson/bch-wizard

(Edit: and then with type awareness, it seems likely that the DSL could identify the input/output patterns of the business logic between such sequences, allowing it to work one level higher at suggesting better orderings of business logic blocks. Not sure how far you can go with tracking specific output → input requirements of that business logic. Is there a path all the way to “represent blocks of constraints as a DAG and reschedule an optimal, provably-equivalent program”?)

#15

With “efficient stack scheduling” what else do you have in mind than op count reduction? I’m thinking that shuffling code blocks to, for example, avoid deep stack references all boils down to reducing the op code count (byte size).

Making the right data layout choices in byte arrays (records) also would have large impact.

#16

Yep! For most use cases, contract length reduction is the key metric – between two equivalent contracts (equivalent functionality, safety, audit quality, etc.), compiled length is what impacts real user experiences (TX fees).

Though if you want the compiler to always be able to minimize ultimate TX sizes, you also need an op-cost minimizing “mode” to switch into when the contract’s worst case(s) exceed its budget. E.g. there are cost-prioritized and length-prioritized emulations for various bitwise ops right now, and picking the right one matters a lot for ultimate contract length if a naive length-focused compilation exceeds the op-cost budget. (The compiler can also add a <variable_length_garbage> [...] OP_DROP area to give some spend-time op-cost flexibility if the budget is too close or can’t be proven safe in all cases.)

1 Like