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).

1 Like