lamtez

KO | EN

gitlite — search

#typescript #go #machine-learning #rust #deep-learning #docker #java #awesome #cli #kubernetes #pytorch #mcp #ios #open-source

(★ 21)

An ML-inspired smart contract language, compiling to Tezos' Michelson VM

lamtez Latest Version Download

Download Latest Version (.zip)

// repository documentation

Was this content helpful?

★ 0 (0 ratings)

lamtez: a typed lambda-calculus compiling to Tezos Michelson VM
================================================================

Lamtez is Domain-Specific Language for smart contracts, and its compiler to
Michelson, [Tezos](http://www.tezos.ch)' virtual machine for smart contracts
execution.

It is released under the MIT license, with no guaranty of any kind (among other,
there's no proof that it compiles to sound nor correct Michelson code). I'm
interested in feedbacks anyway, if you experiment with it.

## Building

The compiler is written in OCaml; the build process relies on `ocamlbuild`,
and it depends on the parser generator [menhir](http://gallium.inria.fr/~fpottier/menhir/).
If [opam](https://opam.ocaml.org/) is installed on your system, `opam install
ocamlbuild menhir` should be enough to get a building environment. If you
compiled Tezos from sources, Lamtez requirements are a subset of Tezos'.

## Examples

If you would rather look at source code examples first, before reading the
fine manual, you can go and check
[EXAMPLES.md](https://github.com/fab13n/lamtez/blob/master/EXAMPLES.md). It reimplements
contract exmaples from [http://michelson-lang.com] and
[the Michelson specification](https://github.com/tezos/tezos/blob/master/src/proto/alpha/docs/language.md).

## Cheat sheet

For a quick summary of the language syntax and main features, a PDF two-pages
summary is available as https://github.com/fab13n/lamtez/raw/master/CHEAT-SHEET.pdf.

## General considerations on the language

The language is strongly influenced by ML dialects OCaml and Haskell: mostly
functional, relying heavily on sum-types and product-types, statically typed
with type inference. It also composes with some limitations in Michelson. Most
of the limitations in Michelson language follow from the following
assumptions:

* Most useful smart contracts will be rather simple, commpared to typical
  programs written be profesionnal developers in general-purpose languages;

* A very high level of confidence in contracts correctness will be required.
  Given how finding and exploiting bugs in smart contracts can be turned into
  tokens and actual money, every contract handling significant amounts of
  money will be thoroughly reviewed and attacked by black-het hackers, several
  of them smarter than the contract's author and white-hat reviewers.

* Tezos being self-amending, it's better to start with a very limited language
  and progressively add empirically needed features, rather than start with
  many bells and whistles: some of them might prove less secure than
  anticipated, or not as useful as it first seemed, but each of them making
  formal proofs more tedious or complicated to produce.

Michelson closely ressembles a simply-typed lambda calculus, without native
recursivity nor proper closures; drastic limitations also exist on the ability
for a contract to call other contracts.

Compared to hand-written Michelson, Lamtez contracts offer higher-level
features:

* Sum and product types of arbitrary size and with arbitrary field/case names.
  In Michelson, sums with more than two alternatives and products with more
  than two fields have to be encoded with nested alternatives and pairs, thus
  quickly becoming hard to read for humans.

* lexically scoped variables: keeping track of what is at which level of the
  stack is cumbersome when writing a program, and it makes reading someone
  else's contracts dreadful. Being able to name things rather than shuffling
  them on a stack greatly improves contract readability.

* Limited support for closures: a function can use variables declared
  outside of it. It is done by either compiling functions as a pair of
  a `LAMBDA` with a tuple capturing its environment from the stack,
  by beta-reducing the closures when possible, or by reimplementing
  `MAP` and `REDUCE` operations with `LOOP` when the function needs
  its environment. Some cases remain, though, where Lamtez is not able
  to compile a closure.

* type inference: as most ML dialects, lamtez uses a variant of the W
  algorithm to guess types with very little user annotations. However,
  contrary to ML, it expects the final contract not to be polymorphic, as
  Michelson doesn't support it. So you might get some "Add more type
  annotations" errors. Annotating function parameters is sufficient, although
  often not necessary, to ensure a monomorphic contract type. (inner
  polymorphic functions are technically possible, but NOT YET IMPLEMENTED)

* storage management: instead of manually managing the storage, variables
  prefixed with `@` are declared and stored in it, and can be updated
  in the contract through a simple and readable syntax (under some conditions).
  An option is provided to declare and extract an initial storage value
  from the contract source file.

* `TRANSFER_TOKEN`, the act of calling another contract, can only be
  done under very strict conditions in Michelson (the stack must be empty).
  This restriction is partially lifted in Lamtez: it will dedicate a field
  in the storage to save the stack before calling, and restore it after
  it returns.

(note: currently, the stack is saved rather naively: a big sum type is
reserved in the storage, one per invocation of `TRANSFER_TOKEN`, and
the whole stack is saved in it. First the  stack could be pruned before
saving, as some slots won't be used after the contract call anymore,
and two invocations with the same stack types above them should share
their slot)

Lamtez is mostly functional. It has two kinds of side effects: storage updates
and calls to other contracts. Normally, functional programming languages will
only let you touch side effects with a ten foot pole. They typically call that
pole a "monad"; wielding a monad towards unfamiliar developers scares them
about as much as doing so with an actual ten foot pole.

Lamtez doesn't explicitly supports monads, but it enforces some (coarser)
constraints about where side effects are accepted. Namely, these operations
can't happen in an inner function (we couldn't keep track of them without
monads then), nor in places where evaluation order isn't intuitively obvious:
not in tuples/products, not in function arguments.

Whitespaces are not significant except to separate tokens, indentation is not
significant, comments start with a `#` sign and run until the end of the
current line.

Lamtez is not proved correct in any way; the proper way to ensure any
correctness property is by working directly on the generated Michelson code.
It is annotated and commented, among other with the stack's state after each
instruction, in order to help analysis.

## Anatomy of a contract

A contract is composed of:

* a series of _type declarations_: it creates type structures, with
  arbitrary sizes, arbitrary labelled fields and alternative cases.

* a series of _stored variables_: those variables, starting with a
  `@` symbol, are kept between contract calls in the blockchain's
  storage. They can optionally be given an initial value; if all
  stored variables in the contract have an initial value, then one
  can extract a data initialization value from the contract, which
  can be directly passed to the tezos client.
  (In the future it will be possible to compile storage values from
  separate files; but the contract's type declarations are needed to
  properly encode sum and product values).

* a function, taking a parameter and returning a result. This function
  can also, under controlled conditions, perform two kinds of effects:
  calling other contracts, and updating the content of stored variables.

## Expression Syntax

### Functions and function applications

In languages inspired by lambda calculus, functions are introduced by
a $\lambda$ sign; In Lamtez as in ML we represent it with the `fun`
keyword; we tolerate also the backslash `\\`, visually more similar,
used by Haskell, more concise, but which might make the code look more
cryptic at first sight.

The complete syntax for a function is `fun x: body`. Parameters can be
annotated with types, through the `::` infix operator: `fun x :: nat:
body`. The result type can also be specified, although it can normally
be inferred by the compiler: `fun x :: nat :: unit: body`.

Lamtez supports multi argument functions, but contrary to ML-inspired
languages, they are encoded through tuples rather than through
currying (nested functions returning functions, a standard idiom in
λ-calcullus inspired languages). Currying is mainly useful for partial
applications, and their usefulness is not demonstrated for Tezos smart
contracts. They can always be encoded through eta-expansion if needed.
Finally, currying leads to cumbersome code at best, in a target
language that doesn't support closures.

Functions are syntactically applied the ML/λ-calculus way, by putting
the arguments after the function, without parentheses nor separating
commas, i.e. what's written `f(x, y)` in C-inspired syntaxes is
written `f x y`, and equivalent to `f(x, y)`, the application of
function `f` to the pair `(x, y)`. Parentheses are still needed for
nested function applications, e.g. what would be written `f(g(x),
g(y))` in C would give `f (g x) (g y)` in Lamtez, as in most ML
dialects.

Lamtez performs type inference, i.e. if there are enough hints in the
code, it will correctly guess the types which the user omitted to
write. However, unlike most other ML-family languages, polymorphism is
not allowed, because the underlying Michelson VM doesn't support it
(TODO: inner lambdas could be polymorphic, as long as it doesn't show
on the outside type. Not sure hwo useful that would be in
practice). So if the type inference algorithm determines that a
function's best type is, say, `∀a: list a -> nat`, the compiler will
emit an error and demand more type annotations rather than accepting

Examples:

fun x: x
    fun x y: x + y
    fun x :: nat, y ::nat: x - y
    fun x :: nat, y: x * y
    fun parameter: ((), map-update parameter (Some self-amount) @store)

For instance, the simplest contract, identity, which does nothing, just takes
a unit parameter and returns a unit result, is written below:

fun p :: unit: p

The barely more interesting one, which adds one to its parameter, is:

fun p :: nat: p + 1

### Literals

Lamtez supports the same literals as Michelson:

* to distinguish naturals from positive integers, the later have to be
  prefixed with a `+` sign, so `42` is a natural number and `+42` is typed as
  an integer. Beware therefore that `f+1` is the application of function `f`
  to signed integer `+1`, and not an addition to number `f`.

* dates are represented with the ISO format, without surrounding quotes:
  `2017-08-22T22:00:00Z`, `2017-08-22T22:00:00+01:00`

* Tez amounts are represented with a `tz` prefix and optional cents: `tz1`,
  `tz1.00`, `tz.05` (TODO: support `_` characters). If there are cents, they
  must be two digits long: `tz0.`, `tz0.1` or `tz.100` are illegal.

* Signatures are represented with a `sig:` prefixing the base58 hash.

* Key hashes are written directly, without surrounding quotes; they are by
  their `tz1` followed by a base58 hash.

### Variables

Variable names must start with a lowercase letter or an underscore;
they are allowed to contain a `-`: this is currently used to sort
primitive functions into pseudo-namespaces. As a result, it's important to
leave spaces around `-` when used as a substraction infix operator.

Examples: `foo, bar0, contract-call, _foo, foo_bar, fooBar`

(In the future I might get rid of dashes in names, if there's a decent
namespace system instead)

### Let: local variables

ML-style local variables, `let x=a; b` evaluates `b` with `x` set to `a`.
Equivalent, execution-wise, to `(\x:b) a`.

Example:

let x = 32;
    let y = 10;
    x + y

Lamtez being mostly functional, you can't update the value stored in a
variable; however, and as often done in ML dialect, you can shadow a variable
with a new variable of the same name:

let x = 10;
    let x = 20;  # From here you can't refer to the first `x` variable anymore
    do_stuff_with x

### Tuples (unlabelled cartesian products)

Whereas Michelson supports pairs, Lamtez supports tuples of length bigger than
2 (and encodes them as nested pairs). Contrary to many ML dialects, tuples are
mandatorily surrounded with parentheses to avoid misleading precedence issues;
elements are separated with commas.

Elements are extracted from a tuple with the suffix `.n`, where `n` is a
litteral positive integer, 0-indexed. The extractor suffix binds tighter than
function application (same as most ML-family languages).

Tuples are encoded as balanced trees, i.e. so that the length of paths in
`n`-products grows as `log2(n)`. This can easily be changed if desired
(left-folded or right-folded accessors have `o(n)` access and update times,
but might lead to simpler proofs).

Example:

let triplet = (32, 5, 5);
    triplet.0 + triplet.1 + triplet.2

### (labelled) Cartesian products

For larger composite structures, it's easier to refer to individual elements
by user-given names, rather than by number. This requires to declare a product
type before using it. Labels are like identifiers except that they start with
a capital letter.

Type declarations happen at the beginning of the contract (cf. infra);
labelled product types are sequences of labels and types separated by `*`
    symbols.

Litteral product types are sequences of labels and types, separated by commas
and surrounded by braces.

Access to product fields are made with a `.Label` suffix, which binds as
tightly as unlabelled product accessors.

Finally, one can generate a product from another: a product which is equal to
`p` except that field `F` has value `42` can be created through the syntax
`p <- F: 42`.

Example:

type coordinates = Latitude: int * Longitude: int

let p = {Latitude: 43500, Longitude: 1500 };
    let i_miss_trigonometry = p.Latitude * p.Latitude + p.Longitude * p.Longitude;

let p_2_degrees_north = p.Latitude <- p.Latitude+2;
    let p_south_west =
      p <- Latitude: p.Latitude - 1
        <- Longitude: p.Longitude + 1;

(p, p_2_degrees_north, p_south_west)

### Sum types

Equivalent of labelled unions, they are a generalization of the
`Left|Right` Michelson operators with an arbitrary number of labels,
freely named.

Types have to be declared; they are declared the same way as products,
except that cases are separated with `+` instead of `*`.

A label can only belong to one sum type; for instance, it's illegal to
have both `type a = A: int + B: string` and `type b = A: int + C:
bool`.

Each case has one and only one associated value type. Make it a `unit`
if you don't use it, make it a tuple or a product if you need several
values.  Syntactically, unit arguments can be omitted, though.

Sum expressions are built with a label followed by an expression. It
binds as tightly as a function application.

Sum accessors, equivalent to ML's `match/with` or Michelson `IF_LEFT`,
are of the form `case expression | Label_0 v_0: e_0 |... | Label_n
v_n: e_n end`. the variables `v_n` can be omitted when they're not
used in the corresponding `e_n`. In sum cases, unit values can be
omitted too.

Booleans are encoded as `type bool = False unit | True unit`, so
if/then/else operations can be encoded as sum accessors, as shown
in the example below.

Option types `Some x + None`, binary alternatives `Left/Right` and
list constructors `Nil/Cons` are also predeclared as sum types.

Examples:

type operation = Withdrawal tez + GetBalance unit + Deposit tez
    fun amount operation storage:
      case operation
      | Withdrawal a: (None, storage - a)
      | GetBalance:   (Some storage, storage)
      | Deposit:      (None, storage + a)
      end

self-now > date ? True: "OK" | False: "Not yet"

Some syntax sugar is proposed for boolean cases, which allows to chain several
`if / then / else if * / else` statements:

* `if <cond>: <body0> end` is equivalent to
  `case <cond> | True: <body0> | False: () end`.

* `if <cond>: <body0> | else: <body1> end` is equivalent to
  `case <cond> | True: <body0> | False: <body1> end`.

* `if <cond_0>: <body_0> | ... | <cond_n>: <body_n> else: <body_e> end`
  is equivalent to nested if/then/elseif statements:

### Binary and unary operators

TODO

### Composite values

There are native syntaxes to enter lists, sets and maps:

l = (list 1 2 3 4)
    s = (set "a" "b" "c" "d")
    m = (map 1 "one" 2 "two" 3 "three")

Lists can also be built out of `Cons` and `Nil` sum types.

### Type annotations

Expressions can be annotated with their types, with the `::` infix operator.
It serves several purposes: compiler-checked hint for contract readers,
helping the compiler resolve a polymorphic type, or helping it produce a more
precise error message when facing an unsound program.

### Storage

Michelson contracts have a storage value; it is stored on the blockchain,
passed as a parameter to contracts when they execute, and contracts return an
updated storage object which is stored back on the blockchain.

As non-trivial programs often store multiple values, the store is generally a
product type. Since Lamtez might need to store additional fields in the store,
contract developpers are expected to declare and use the field they need
through a dedicated `@` syntax:

* a sequence of `@name :: type` declarations after type declarations declare
  every storage field type and name;

* optionally, a value can be associated, e.g. `@n :: nat = 42`. If all stored
  values have such an initial value, a data initializer can be extracted from
  the contract, and passed to the tezos client.

* in the code, `@name` returns the current content of field `name`.

* fields can be updated with the syntax `@name <- expr`.

Storage fields cannot be updated anywhere: you can't update them inside
functions, in tuple or product elements, in function arguments.

If you want to update them inside a function, make the function return the
updated value and perform the update from outside:

@n :: int

let f = fun x :: int: @n <- x + 1; () # Illegal
    f 3

let f = fun x :: int: x + 1;
    @n <- f 3 # Legal

Instead of performing storage updates in function arguments or products,
perform them before in a `let` expression.

### Loops

(NOT IMPLEMENTED)

Loops are not very functional; however, in a languge that doesn't
fully support closures and doesn't support contract calls from inside
lambdas, access to the `LOOP` Michelson primitive is
necessary. Although this isn't implemented, my intention is to
introduce a syntax of the form `loop (<var*>) = (<expr*>) while
<condition> else (<expr*>)`:

* the `<expr*>` and `<var*>` lists have the same sizes;
* at step 0, the variables are assigned the values after the `else`;
* as long as `<condition>` is true, an iteration of the loop is performed:
    * the expressions before the `while` are evaluated, with the current
      assignments for `<var*>`;
    * the result is assigned to `<var*>`, before a new condition checking,
      and maybe iteration, is performed.

As an example, here's what factorial would look like with the loop operator:

let fact = fun n:
      let loop (acc, i) = (1, n) then (acc*i, i-1) while i > 0

Some syntactic permissiveness might be granted for the order in which `loop`,
`while` and `else` elements are ordered:

fun n: let (fact, _) = loop (acc, i) = (acc*i, i-1) while i > 0 else (1, n)
    fun n: let (fact, _) = while i > 0 loop (acc, i) = (acc*i, i-1) else (1, n)
    fun n: let (fact, _) = else (1, n) while i > 0 loop (acc, i) = (acc*i, i-1)

The first and second versions seem more naturally readable, the last
one follows "natural evaluation order" more closely.

It might also be sensible to accept `let loop (vars) = XXX while C else X0`
as a shortcut for `let (vars) = loop (vars) = XXX while C else X0`

### Type syntax

Types can be created at the beginning of the contract file. We've
already seen the syntax to create labelled product types `type name =
Label_0 field_type_0 * ... * Label_n field_type_n`, and sum types
`type name = Label_0: case_type_0 * ... * Label_n: case_type_n`. Type
aliases can also be created, with the notation `type name = type`.

Type can be polymorphic, i.e. take type parameters. Beware, however,
that since Michelson is not polymorphic, some valid Lamtez programs
will be rejected by the compiler. Type parameters are passed between
the name and the `=` sign. Lists are encoded that way in Lamtez.

Examples:

type option a = None unit + Some a  # Actually predeclared
    type pair a b = (a * b)  # Actually predeclared
    type assoc_list k v = list (pair k v)

Type annotations can be the following:

* an identifier, i.e. the name of an alias, a sum type, a product type or a
  primitive.

* if an identifier is polymorphic, as the `option` example above, it must
  receive the corresponding number of parameters after it. For instance, `nat`
  is a valid type, so is `list int` or `list (pair string int)`, but `list` or
  `pair int` are not valid.

* Tuples are represented as types, separated with `*` and surrounded by
  parentheses, e.g. `(int * int)` or `(int*list a*tez)`.

* functions types are denoted `parameter_type -> result_type`. The arrow is
  right associative, and multi-parameter functions are encoded as curried
  (nested) lambda terms. For instance, a function from two ints to a string
  has type `int -> int -> string`.

### Contracts

A contract with parameter type `p`, and result type `r` is represented in a
file as a sequence of type declarations, then a sequence of store field
declarations, then an expression of type `p -> r`. The

Example:

type operation = Withdrawal tez + GetBalance unit + Deposit tez

@store :: tez

fun amount operation:
      case operation
      | Withdrawal a: @store <- @store - a; None
      | GetBalance:   Some storage
      | Deposit:      @store <- @store + self-amount
      end

### Semantics

TODO

### Primitives

The primitives are listed here, with their corresponding Michelson
opcode as a title.

#### TRANSFER TOKENS

`contract-call` is the equivalent of `TRANSFER_TOKEN`, and as this
opcode, it can only be called within very specific constraints,
enforced by Michelson to make some classes of error harder to write:
It cannot be in a function, and no variable existing before the call
canbe used after.

contract-call: ∀ param result: contract param result → param → tez  → result

#### Other primitives TODO

type zero     = (+)
    type unit     = (*)
    type option a = None+Somea
    type bool     = False + True
    type list a   = Nil + Cons (a * (list a))
    type account  = (contract unit unit)

val contract-call           :: ∀ param result:
        contract param result -> param -> tez -> result
    val contract-create         :: ∀ param storage result:
        key -> option key -> bool -> bool -> tez ->
        (param * storage) -> (result * storage) -> storage -> contract param result
    val contract-create-account :: key -> option key -> bool -> tez -> account
    val contract-get            :: key -> account
    val contract-manager        :: ∀ param storage: contract param storage -> key

val crypto-check :: key -> sig -> string -> bool
    val crypto-hash  :: ∀ a: a -> string

val fail :: fail

val list-map    :: ∀ a b: list a -> (a -> b) -> list b
    val list-reduce :: ∀ a acc: list a -> acc -> (a -> acc -> acc) -> acc

val map-get    :: ∀ k v: k -> map k v -> option v
    val map-map    :: ∀ k v0 v1: map k v0 -> (k -> v0 -> v1) -> map k v1
    val map-mem    :: ∀ k v: k -> map k v -> bool
    val map-reduce :: ∀ k v acc: map k v -> acc -> (k -> v -> acc -> acc) -> acc
    val map-update :: ∀ k v: k -> option v -> map k v -> map k v

val self-amount         :: tez
    val self-balance        :: tez
    val self-contract       :: ∀ param result: contract param result
    val self-now            :: time
    val self-source         :: ∀ param result: contract param result
    val self-steps-to-quota :: nat

val set-map    :: ∀ a b: set a -> (a -> b) -> set b
    val set-mem    :: ∀ elt: set elt -> elt -> bool
    val set-reduce :: ∀ elt acc: set elt -> acc -> (elt -> acc -> acc) -> acc
    val set-update :: ∀ elt: elt -> bool -> set elt

lamtez

lamtez Latest Version Download

Today's picks

Was this content helpful?

Recent Feedback

lamtez

lamtez Latest Version Download

Today's picks

Was this content helpful?

Recent Feedback

Download README