ILLUM: an Intermediate-Level Language for the UTXO Model

The project implements a compiler from the HeLLUM contract language to the ILLUM intermediate language. HeLLUM is a subset of Solidity that is suitable to be executed on UTXO blockchains like Cardano.

For example, the following is an Auction contract in HeLLUM:

contract Auction {
    uint deadline;
    uint min_bid;
    address winner;  
    address seller;

    constructor(address a, uint d, uint m) {
        seller = a;
        deadline = d;
        min_bid = m;
    }
    
    function bid(uint v, address a) input(v:T) {
        require v >= min_bid;
        require v > balance(T);     // the current bid is greater than the previous ones 
        require a != address(0);
        
        // the previous maximum bid is returned to the previous winner
        winner.transfer((balance(T)-v):T);
        
        // the new winner is set to the current (highest) bidder
        winner = a;
    }
        
    function close()
        auth(seller) 
        after(deadline) 
    {
        seller.transfer(balance(T):T);
    }
}

HeLLUM contracts

The repository includes a benchmark of common Solidity smart contracts, implemented in HeLLUM:

• Crowdfund
• Auction
• Payment splitter
• Vault
• Automated Market Maker
• Voting
• Vesting wallet
• Escrow
• King of the Hill
• Blind auction
• Lending pool
• Lottery

Installation and setup

We give below minimal instructions to setup a local installation of OCaml on Linux. See here for instructions on other OSs.

First, install opam, the OCaml official package manager:

sudo apt install opam

Then, you must initialize opam. This installs OCaml and creates a default switch:

opam init --bare -a -y

Here we assume you will work on the default switch. To check that a switch actually exists:

opam switch list

In case the previous command shows an empty list, you must manually create a switch:

opam switch create illum ocaml-base-compiler.4.14.0

The following command updates environment variables, to make OCaml commands available on the current switch:

eval $(opam env)

Finally, we need a few extra OCaml packages:

opam install -y dune ocaml-lsp-server odoc ocamlformat menhir ppx_inline_test digestif

In particular, this installation includes:

• dune, a build system for OCaml projects, similar to make;
• Menhir, a parser generator;
• ppx_inline_test, a tool for writing in-line tests in OCaml;
• digestif, for cryptographic hashes.

Running the ILLUM compiler

After cloning the repository, you can run a collection of tests through the following command, launched from the illum-lang directory:

dune test 

If everything is ok, the command will produce no output.

To run the HeLLUM compiler:

dune exec illum hllc test/auction.hll

If successful, the command produces a set of ILLUM clauses. For example, the clauses resulting from the compilation of the Auction contract are:

clause constructor_run(deadline,min_bid,winner,seller,bal_T; a,d,m) {
  precond_wallet: bal_T:T
  precond_if: true
  process: 
    call constructor_next(d,m,winner,a,bal_T)
}
clause constructor_next(deadline,min_bid,winner,seller,bal_T; ) {
  precond_wallet: bal_T:T
  precond_if: true
  process: 
    call bid(deadline,min_bid,winner,seller,bal_T)
    auth(seller) afterAbs(deadline) : call close(deadline,min_bid,winner,seller,bal_T)
}
clause bid_run(deadline,min_bid,winner,seller,bal_T; v,a) {
  precond_wallet: bal_T+v:T
  precond_if: (v>=min_bid && (v>bal_T+v)) && a!=address(0)
  process: 
    call( Pay(winner,(bal_T+v)-v,T) | bid_next(deadline,min_bid,a,seller,(bal_T+v)-bal_T) )
}
clause bid_next(deadline,min_bid,winner,seller,bal_T; ) {
  precond_wallet: bal_T:T
  precond_if: true
  process: 
    call bid(deadline,min_bid,winner,seller,bal_T)
    auth(seller) afterAbs(deadline) : call close(deadline,min_bid,winner,seller,bal_T)
}
clause close_run(deadline,min_bid,winner,seller,bal_T; ) {
  precond_wallet: bal_T:T
  precond_if: true
  process: 
    call( Pay(seller,bal_T,T) | close_next(deadline,min_bid,winner,seller,0) )
}
clause close_next(deadline,min_bid,winner,seller,bal_T; ) {
  precond_wallet: bal_T:T
  precond_if: true
  process: 
    call bid(deadline,min_bid,winner,seller,bal_T)
    auth(seller) afterAbs(deadline) : call close(deadline,min_bid,winner,seller,bal_T)
}
clause Pay(a,v,t; ) {
  precond_wallet: v:t
  precond_if: true
  process: 
    send(v:t -> a)
}
clause Check(b; ) {
  precond_wallet: 
  precond_if: b
  process: 
    send()
}