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 n
th 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:
-
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
-
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:
- auction.alb: An auction contract
- multisig.alb: The Albert version of the multisig contract
- vote.alb: The voting contract demonstrated above
- simple.alb: A
noop
-function
And a series of test contracts demonstrating the features of Albert:
- string.alb: Tests on strings
- update.alb: Tests on updates
- variant.alb: Tests of variant types
- compare.alb: Tests on comparisons
- fail.alb: Tests
failwith
- functions.alb: Tests on functions
- list.alb: Tests on lists
- loop.alb: Tests on loops
- map.alb: Tests on maps
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
- Basile Pesin’s internship report on the design and compilation Albert and associated slides
- The formal specification of Albert
- Albert Gitlab Repo
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.