Albert 🔦

Intermediate smart contract programming language for the Tezos blockchain

Albert is an intermediate smart contract programming language compiled to Michelson, the language for the Tezos blockchain. The name of the language was chosen in honor of the physicist Albert Michelson.

Albert is an imperative language with variables and records, abstracting the Michelson stack. The intent of Albert is to serve as a compilation target for high-level smart contract programming languages. The linear type system1 of Albert ensures that an Albert program, compiled to the stack-based Michelson language, properly consumes all stack values.

The Albert language is formally specified in the Ott semantic framework. The compiler, type checker, and parser of Albert are written in the Coq proof assistant. Progression and subject reduction of the typing rules have been proved, intuitively ensuring that well-typed programs do not go wrong. The current priority for the Albert project is to certify the compiler. That is, proving that the Albert compiler preserves the semantics of the compiled program.

Examples

The following program implements a vote. The storage contains a threshold, which is the cost of casting a vote, and the current tally in the field votes.

type storage_ty = { threshold : mutez; votes: map string nat }

def assert_some : { opt : option nat } -> { res : nat } =
    match opt with
    None n -> failwith "None"
    | Some n -> res = n
    end

def vote :
  { param : string ; store : storage_ty } ->
  { operations : list operation ; out_storage : storage_ty } =

    (store0, store1) = dup store;
    threshold = store1.threshold;
    (threshold, threshold_copy) = dup threshold;
    am = amount;
    ok = am >= threshold;
    match ok with
      False f ->
             failwith "you are so cheap!"
      | True t -> drop t;
             state = store0.votes ;
             (state0, state1) = dup state;
             (param0, param1) = dup param;
             prevote_option = state1[param1];
             { res = prevote } = assert_some { opt = prevote_option };
             one = 1;
             postvote = prevote + one;
             postvote = (Some : [ None : unit | Some : nat ]) postvote;
             final_state =  {| state0 with param0 |-> postvote |};
             out_storage = {threshold = threshold_copy; votes = final_state};
             operations = ([] : list operation)
    end

Here is the compiled program to Michelson:

parameter string;
storage (pair mutez (map string nat));
code { DUP;
       CAR;
       DIP 1 {CDR};
       DIG 1; DUP; PAIR; DUP; CAR;
       DIP 1 {CDR};
       DUG 2; CAR; DUP; PAIR; DUP; CAR;
       DIP 1 {CDR};
       DUG 3; DUG 3; AMOUNT; DIG 3; DIG 1;
       COMPARE;
       GE;
       IF { DIG 1; CDR; DUP; PAIR; DUP; CAR;
            DIP 1 {CDR};
            DUG 2; DUG 2; DUP; PAIR; DUP; CAR;
            DIP 1 {CDR};
            DIG 3; DIG 2; GET;
            IF_NONE {PUSH unit Unit; PUSH string "None"; FAILWITH} {};
            DUG 1; PUSH nat 1; DIG 2; ADD; SOME;
            DUG 1; DIG 2; DIG 2; DIG 2; UPDATE; DIG 1;
            PAIR;
            NIL operation
          }
          {PUSH unit Unit; PUSH string "you are so cheap!"; FAILWITH};
       PAIR
     }

For comparison, consider the same program hand-written in Michelson. The hand-written version is shorter, but arguably less readable due to the lack of variable names.

storage (map string int %candidates);
parameter string %chosen;
code { AMOUNT; PUSH mutez 5000000; COMPARE; GT;
       IF { PUSH string "you are so cheap!"; FAILWITH } {};
       DUP; DIP { CDR; DUP }; CAR; DUP;
       DIP {
             GET; ASSERT SOME;
             PUSH int 1; ADD; SOME
           };
       UPDATE; NIL operation; PAIR
     }

Features

Functions

Albert features non-recursive, simply typed functions. They are compiled through inlining. A function can take any number of input and output parameters. The following example defines a function that takes an integer, and returns its magnitude in m and sign in s.

def magnitude_sign : { i : int } -> { m : nat ; s : bool } =
    (i0, i) = dup i;
    m = abs i0;
    v = +0;
    s = i >= v

Variables

Albert programs abstract the stack through variables. The following function calculates the nth number in the Fibonacci sequence:

def fib : { n : nat } -> { f1 : nat } =
   f1 = 1 ;
   f2 = 1 ;
   (n0, n) = dup n ;
   z = 0;
   b = n0 > z ;
   loop b do
      (f1d, f1) = dup f1 ;
      f1 = f1 + f2 ;
      f2 = f1d ;
      o = 1;
      n1 = n - o ;
      n = abs n1;
      (n0, n) = dup n ;
      z = 0;
      b = n0 > z
   done;
   drop n; drop f2

Note the explicit variable duplication through the dup keyword and the explicit variable destructions through the drop instruction. The linear typing system of Albert enforces a variable usage that respect the stack semantics of the target language Michelson. Consequently, whenever a variable is used twice, it must be duplicated explicitly through dup. Conversely, all produced values must be eventually consumed (explicitly by drop if necessary).

Record and variant types

Albert programs can define non-recursive, simply typed records and variant types. Such types are compiled to nested pairs and sums in Michelson.

The following program demonstrates how a record and variants can represent geometrical forms. The function area employs pattern matching on the variant type form to calculate the area using the formula corresponding to the form.

type point = { x : int ; y : int }

def translate : { p1 : point ; p2 : point } -> { p : point } =
    { x = p1x ; y = p1y } = p1;
    { x = p2x ; y = p2y } = p2;
    xn = p1x + p2x;
    yn = p1y + p2y;
    p = { x = xn ; y = yn }

type square = { lower_left : point ; side : int }
type rectangle = { lower_left : point ; upper_right : point }

type form = [Square : square | Rectangle : rectangle]

def area : { f : form } -> { a : nat } =
   match f with
   Square s -> side = s.side ;
               (s, s1) = dup side ;
               a = s * s1;
               a = abs a
   | Rectangle r ->
      { upper_right = ur ; lower_left = ll } = r;
      { x = urx ; y = ury } = ur;
      { x = llx ; y = lly } = ll;
      dx = urx - llx ;
      dx = abs dx ;
      dy = ury - lly ;
      dy = abs dy ;
      a = dx * dy
   end

Formalized and mechanized type system and semantics in Ott

The type system and semantics of Albert are fully specified using Ott. The rendered PDF version of the static and dynamic semantics is available here.

How to get it

Albert can be installed using opam in the following manner:

  1. First, add the Coq opam repositories:

    opam repo add coq-released https://coq.inria.fr/opam/released
opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev

  2. Then, obtain the Albert sources:

    git clone git@gitlab.com:nomadic-labs/albert.git

  3. Finally, install using opam:

    cd albert/
opam install .

How to use it

The compiler is installed as the albert_c binary. For usage details, try albert_c -help. For example, running

albert_c -entrypoint vote examples/albert.alb

compiles the Albert program examples/vote.alb to Michelson. The output is written to examples/vote.tz. Note that the entrypoint parameter, specifying the Albert function that defines the contract, is obligatory to obtain a full Michelson contract.

Examples

The Albert repository contains a series of examples, including:

And a series of test contracts demonstrating the features of Albert:

Roadmap

  • Package for opam
  • Certify the compiler

Further reading

Footnotes

1 Wadler, Philip. “Linear types can change the world!.” Programming concepts and methods. Vol. 3. No. 4. 1990.