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

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

2 Likes
CHIP 2021-05 Bounded Looping Operations
#17

Loops (OP_BEGIN / OP_UNTIL) have now been added to the 2026 VM and DSL. A few other language constructs were also added, and some optimizations were performed to the VM and examples.

3 Likes
CHIP-2025-08 Functions (Takes 2 & 3)
#18

Initial support for OP_DEFINE / OP_INVOKE has been added to the 2026 VM and DSL. Both functions (global namespace) and lambdas were added based on this construct. The OP_EVAL based lambdas were removed but may be added back later (as experimental) for mutable “closure like” support.

3 Likes
#19

Work was continued on the albaDsl secp256k1 EC multiply demo which also lead to some improvements to the albaVm efficiency. Steps were taken to optimize the EC code: VM2026 functions were introduced to compress the code and the algorithm was changed to use Jacobian coordinates. Current code size is ~1300 bytes. Since loops are now used instead of recursion, execution fits within current stack limits. On albaVm multiplying G by n - 1 (where n is the curve order) now takes around 40 ms (20x that of a straightforward native Haskell implementation). The EC algorithm/implementation can be improved further to bring down the execution time and code size.

3 Likes
#20

The VM 2026 function support in albaDsl was revamped somewhat. VM 2026 functions are now managed in the same way as macros and can thus be more easily grouped into Haskell modules and referenced without fuss. During compilation albaDsl will collect all functions into a function table at the beginning of the program (using OP_DEFINE). Slots are assigned to functions based on how frequently they are used. The function breakdown for the EC multiplication demo can be seen below. Program size is now around 900 bytes and execution time on albaVm is ~33ms.

Module                                   Line  Function                  Ops   Slot  Sites
------------------------------------------------------------------------------------------
DslDemo.EllipticCurve.Field              44    primeModulus              1     0     57
DslDemo.EllipticCurve.Field              47    modulo                    20    1     9
DslDemo.EllipticCurve.Jacobian           37    ecMul                     6     2     7
DslDemo.EllipticCurve.JacobianAdd        18    ecDoubleJ                 147   3     2
DslDemo.EllipticCurve.Jacobian           40    ecMulJ                    70    4     1
DslDemo.EllipticCurve.Jacobian           73    toJacobian                58    5     1
DslDemo.EllipticCurve.Jacobian           89    fromJacobian              177   6     1
DslDemo.EllipticCurve.JacobianAdd        65    ecAddJ                    335   7     1
2 Likes
CHIP-2025-08 Functions (Takes 2 & 3)
#21

The EC multiply code is now 600 bytes. The function table can be seen below. Note that some functions are quite small but called frequently.

Module                                   Line  Function                  Slot  Ops   Sites
------------------------------------------------------------------------------------------
DslDemo.EllipticCurve.Field              27    feMul                     0     4     36   
DslDemo.EllipticCurve.Field              24    feSub                     1     20    9    
DslDemo.EllipticCurve.Field              33    feCube                    2     6     5    
DslDemo.EllipticCurve.JacobianPoint      44    makeIdentity              3     15    4    
DslDemo.EllipticCurve.JacobianPoint      61    getX                      4     5     4    
DslDemo.EllipticCurve.JacobianPoint      66    getY                      5     5     4    
DslDemo.EllipticCurve.JacobianPoint      71    getZ                      6     4     4    
DslDemo.EllipticCurve.Field              45    primeModulus              7     1     3    
DslDemo.EllipticCurve.JacobianPoint      25    makePoint                 8     18    3    
DslDemo.EllipticCurve.JacobianPoint      58    getTag                    9     4     3    
DslDemo.EllipticCurve.Field              39    feInv                     10    41    2    
DslDemo.EllipticCurve.JacobianAdd        19    ecDoubleJ                 11    75    2    
DslDemo.EllipticCurve.JacobianPoint      76    getField                  12    7     2    
DslDemo.EllipticCurve.Jacobian           38    ecMul                     13    48    1    
DslDemo.EllipticCurve.Jacobian           70    toJacobian                14    29    1    
DslDemo.EllipticCurve.Jacobian           81    fromJacobian              15    57    1    
DslDemo.EllipticCurve.JacobianAdd        40    ecAddJ                    16    183   1    
Functions total: 17
3 Likes
CHIP-2025-08 Functions (Takes 2 & 3)
#22

A feature was added to albaVm to export execution logs to HTML. And a feature to albaDsl for sharing information about the function table with albaVm. This way, the function definitions & calls in the HTML can be decorated/annotated. This can be used to illustrate what I think is the key feature of the Functions CHIP: functions provide a means of abstraction.

As an example we will evaluate this albaDsl program which uses a mini-language of functions (‘feMul’, ‘feAdd’, ‘feSub’, and ‘feCube’) to perform modular arithmetic on field elements (integers):

progAbstraction :: FN s (s > TBool)
progAbstraction =
  begin
    # int 3 # int 7 # feMul # int 1 # feAdd # int 12 # feSub # feCube
    # int 1000 # opNumEqual

The functions definitions are not shown here. In this example, the integer arguments are much smaller than the modulus so the results of the function applications are the same as the corresponding arithmetic operators.

Log #1 shows the execution for when functions are not used. I.e. ‘feMul’ etc. are defined as macros. Execution log #2 shows the result when they are defined as functions and the logs have been annotated with the function names.

In log #1 it is hard to see the overall structure of the program and how it ties back to the source code. There is lots of repeated code which one has to continually re-read while trying to grasp what is going on. With functions, the repetition is factored out (log #2). We can read the code at a higher abstraction level and not worry about the underlying details. If we are interested in the details we can expand the function calls by clicking on the respective row. The logging annotation framework hides the OP_INVOKES so that the functions can be read as higher-level opcodes (user defined words in Forth lingo).

I think it is a strength of Bitcoin that the opcode language is readable and not just seen as a compilation target. The functions CHIP greatly improves readability by adding structure and removing repetition. And with functions there can be a one-to-one correspondence between source language constructs and opcode level constructs.

Note how functions in some cases are just a few opcodes long. It is important that the function mechanism is very lightweight for this to be feasible.

3 Likes
CHIP-2025-08 Functions (Takes 2 & 3)
2026 Layla Upgrade Lock-in CHIP Endorsements Thread
#23

I implemented a simple windowed version of Elliptic Curve point multiplication. It improves performance and also shows how OP_DEFINE/OP_INVOKE can be used to implement dynamically computed lookup tables.

My previous changes to reduce the code size using functions came with a performance regression to ~38 ms. But the windowed version of EC multiply brings that down to 26 ms (a ~30% improvement). The code size for table setup and multiply comes to 723 bytes.

The following code shows how to use the windowed EC multiply:

test :: FN s (s > TPoint > TPoint)
test =
  begin
    # gTable # g # setupTable
    # gTable # nat 100_000_000_000 # ecMul
    # gTable # nat 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFEBAAEDCE6AF48A03BBFD25E8CD0364140 # ecMul
  where
    gTable = nat 100

    g = <generator point>

In this case we will calculate n*G where G is the generator point. But we could have used any other point on the curve. We first initialize a table for G. It starts at function slot 100 and will stretch to slot 115. The table contains entries for n’*G where n’ goes from 0…15. Each entry is 100 bytes long. We then use the precomputed table in two point multiplications. First with a small scalar and then with a large scalar.

The algorithm works by first breaking down ‘n’ into a string of nibbles. To store these a bytestring on the stack is used: each nibble is stored in a byte and then OP_CATed together. I refer to these as vectors. The algorithm then OP_SPLITs off one nibble at a time from the vector, and uses it as an index into the lookup table to get a point value that is then used in the rest of the computation.

The lookup table could have been stored in a vector too, but OP_INVOKE based lookups are more efficient (especially for random access as here). Vectors have the benefit that they don’t consume the limited slot resource. So this is a trade-off. A combination of vectors and OP_DEFINE/OP_INVOKE probably gives best results.

3 Likes
2026 Layla Upgrade Lock-in CHIP Endorsements Thread
CHIP-2025-08 Functions (Takes 2 & 3)