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 proven on a language fragment, 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
opam update

  2. Then, install using opam:

    opam install coq-albert

Through Docker

Albert can also be run through Docker. The following sets up an alias that runs the latest version of Albert:

:::bash alias albert_c=’docker run -v “$PWD:$PWD” -w “$PWD” registry.gitlab.com/nomadic-labs/albert:latest’

and then use the Albert compiler as below.

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

Publications

Albert, an intermediate smart-contract language for the Tezos blockchain.

Bruno Bernardo, Raphaël Cauderlier, Basile Pesin, and Julien Tesson

4th Workshop on Trusted Smart Contracts, February 2020 (pdf)

Tezos is a smart-contract blockchain. Tezos smart contracts are written in a low-level stack-based language called Michelson. In this article we present Albert, an intermediate language for Tezos smart contracts which abstracts Michelson stacks as linearly typed records. We also describe its compiler to Michelson, written in Coq, that targets Mi-Cho-Coq, a formal specification of Michelson implemented in Coq.

Further reading

Contact us

For any questions or inquiries:

References

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