Reference

An archetype contract is composed of declarations, entry points and optionally specification for formal verification.

Declarations

  • constant and variables declare global variables. A constant value cannot be modified in the contract's entry points.

constant rate : rational = 0.2
variable price : tez = 10tz
  • states declares contract's possible states. It is then possible to use transitions to change the contract states (see below)

states =
| Created initial
| Confirmed
| Canceled
| Success
| Fail

initial is used to declare the initial state value of the contract.

  • entry declares an entry point of the contract. An entry has the following sections:

    • specification (optional) to provide the post conditions the entry is supposed to have

    • accept transfer (optional) to specify that transfer of tez is accepted

    • called by (optional) to declare which role may call this entry

    • require (optional) to list the necessary conditions for the entry to be executed

    • failif (optional) to list the conditions which prevent from execution

    • effect is the code to execute by the entry

entry an_entry_1 (arg1 : string, arg2 : int) {
specification {
// see 'specification' section below
}
called by a_role
require {
r1 : arg2 > 0
}
failif {
f1 : arg2 > 10
}
effect {
// ...
}
}

An entry with just an effect section may omit the effect section syntax:

variable val : nat = 0
entry add(v : nat) {
val += v;
}
  • transition declares an entry point of the contract that changes the state of the contract. A transition has the same sections as an entry (except effect, see above) plus:

    • from to specify the states the transition starts from

    • to to specify the states after the transition

    • when (optional) to specify the transition condition

    • with effect to specify the effect of the transition

states =
| Created initial
| Confirmed
| Canceled
| Success
| Fail
transition confirm () {
from Created
to Confirmed
when { transferred > 10tz }
with effect {
transfer 1tz to @tz1Lc2qBKEWCBeDU8npG6zCeCqpmaegRi6Jg
}
}

It is possible to specify several to ... when .... with effect ... sections in a transition. It is possible to specify a list of original states for the transition to start from:

transition to_fail () {
from Created or Confirmed
to Fail
when { ... }
}

Builtin types

  • bool : boolean values

  • int : integer values

  • nat : positive integers

  • rational : floating value that can be expressed as the quotient or fraction of two integers

  • address : account address

  • role : an address that can be used in entry's called by section

  • date : date values

  • duration : duration values (in second, minute, hour, day, week)

  • string : string of characters

  • tez : Tezos currency

  • bytes : bytes sequence

  • key : key value

  • signature : signature value

  • key_hash : key hash value

  • chain_id : chain id value

Composite types

  • * is the type of tuples.

constant pair : int * string = (1, "astr")
  • option is the type of optional value.

constant value : option<int> = none
  • list declares a list of any type (builtin or composed)

variable vals : list<string> = []
  • map declares a map from a non-composite builtin type to any type.

variable assoc : map<int, string> = []
  • set declares a set of non-composite builtin type values.

variable poll : set<address> = []
  • record declares a record structure.

record r {
s : string;
i : int;
}
  • asset declares a collection of assets and the data an asset is composed of. For example, the following declares a collection of real estates described by an address, a location, and an owner:

asset real_estate identified by addr {
addr : string;
xlocation : string;
ylocation : string;
owner : address;
}
  • enum declares an enumeration value. It is read with a match ... with command (see below).

enum color =
| White
| Red
| Green
| Blue

It is then possible to declare a variable of type color:

variable c : color = Green
  • contract is the type of contract entry point signature.

variable b : option<contract<nat>> = entrypoint(anaddress, "getbalance")

It is then possible to declare a contract value of type called_contract_sig and set its address:

constant c : called_contract_sig = @KT1RNB9PXsnp7KMkiMrWNMRzPjuefSWojBAm
  • aggregate declares an asset field as an aggregate of another asset.

asset an_asset {
id : string;
a_val : int;
col : aggregate<another_asset>;
}
  • partition declares an asset field as a collection of another asset. The difference with aggregate is that a partition ensures at compilation that every partitioned asset (i.e. element of the partition) belongs to one and only partitioning asset.

asset partitioning_asset {
id : string;
part : partition<partionned_asset>;
}

As a consequence of the partition, a partitioned asset cannot be straightforwardly added or removed to its global collection with add and remove (see Partitions, Reference section).

Effect

An entry's effect is composed of instructions separated by a semi-colon.

Declaration

  • var declares a local variable with its value. While possible, it is not necessary to declare the type a local variable. Local variables' identifier must be unique (no name capture in Archetype).

var i = 0;

Assignment

  • := enables to assign a new value to a global or local variable.

i := 1;
  • += , -= , *= and /= enable to respectively increment and decrement an integer variable (local or global).

i *= 2; // i := i * 2
d += 3w; // d := i + 3w, date d is now previous d plus 3 weeks

Effects on asset collection

  • add : adds an asset to an asset collection (fails if the asset key is already present in the collection)

  • update : updates an asset (fails if the id is not present in the asset collection)

  • addupdate is similar to update except that it adds the asset only if its identifier is not present in the collection

  • remove removes an asset from its collection (does not fail).

  • removeif enables removing assets under a condition

  • clear clears an asset collection

an_asset.add({ id = "RJRUEQDECSTG", asset_col = [] }); // see 'collection' example
an_asset.update("RJRUEQDECSTG", { a_value += 3 });
an_asset.addupdate("RJRUEQDECSTG", { a_value += 3 });
an_asset.remove("RJRUEQDECSTG");
an_asset.removeif(a_val > 10); // "a_val" is an asset field
an_asset.clear();

See Assets section for details.

Control

  • ; sequence

res := 1;
res := 2;
res := 3;
  • if then and if then else are the conditional branchings instructions.

if i > 0 then (
// (* effect when i > 0 *)
) else (
// (* effect when i <= 0 *)
);
  • match ... with ... end

archetype effect_control_matchwith
enum t =
| C1
| C2
| C3
| C4
| C5
variable res : int = 0
entry exec () {
specification {
s0: res = 1;
}
effect {
var x : t = C3;
match x with
| C1 | C2 -> res := 0
| C3 -> res := 1
| _ -> res := 2
end
}
}
  • for in do done iterates over a collection.

var res = 0;
for a in an_asset do
res += a.a_val;
done;
  • iter to do done iterates over a sequence of integer values (starting from 1).

var res = 0
iter i to 3 do // iterates from 1 to 3 included
res += i;
done; // res is 6
  • transfer transfers an amount of tez to an address or a contract.

transfer 2tz to @tz1RNB9PXsnp7KMkiMrWNMRzPjuefSWojBAm;
  • fail aborts the execution. It prevents from deploying the contract on the blockchain. As a consequence the storage is left unchanged when executed.

fail("a message");
  • dorequire and dofailif fail if the argument condition is respectively false and true. dorequire(t, msg) is sugar for if t then fail(msg).

dorequire(val > 0, "KO");
dofailif(val <= 0, "KO");

Expressions

bool

constant x : bool = true
constant y : bool = false
  • and

  • or

  • not

  • =

  • <>

  • xor

var b1 = (true and false);
var b2 = (true or false);
var b3 = not true;
var b4 = true = false;
var b5 = true <> false;
var b6 = true xor false;

nat

constant i : nat = 1
constant j : nat = 42
  • + - * div %

  • < > = <> <= >=

  • min max

  • abs

var n1 = 1 + 2;
var i1 : int = 1 - 2; /* difference of nats return an integer value */
var n2 = 3 * 4;
var n3 = 45 div 2; /* 22 (euclidean division) */
var n4 = 45 % 2; /* 1 (modulo) */
var n5 = min(5, 6);
var n6 = abs(-6);

int

constant i : int = 1i
constant j : int = -42
  • + - * div %

  • < > = <> <= >=

  • min max

var a : int = 1i;
var b : int = 2i;
var c : int = 3i;
var d : int = 4i;
var i1 = a + b;
var i2 = b - a;
var i3 = c * d;
var i4 = d div c;
var n1 = d % c;
var i5 = max(6i, 8i);

rational

constant f : rational = 1.1
constant g : rational = -1.1
constant r : rational = 2 / 6
constant t : rational = -2 / 6
  • + - * /

  • < > = <> <= >=

  • min max abs floor ceil

var b1 = (1 / 2) <> 2;
var b2 = 1 <> (2 / 3);
var b3 = (1 / 2) = (2 / 4);
var b4 = (1 / 2) < (2 / 4);
var r1 = (4 / 5) + (7 / 6);
var r2 = 3 + (1 / 2);
var r3 = (4 / 3) * (3 / 4);
var r4 = (8 / 9) / (3 / 7);
var i1 = floor(5 / 3); // int 1
var i2 = floor(-5 / 3); // int -2
var i3 = ceil(5 / 3); // int 2
var i4 = ceil(-5 / 3); // int -1

string

constant s : string = "hello world"
  • concat +

  • slice

  • length

  • < > = <> <= >=

  • to_string

var s1 = "str1" + "str2"; /* concat */
var s2 = slice("abcdef", 1, 2);
var l = length("archetype");
var b1 = "a" <> "b";
var b2 = "a" < "b";
var s = to_string(42)

tez

constant ctz : tez = 1tz
constant cmtz : tez = 1mtz
constant cutz : tez = 1utz
  • +

  • < > = <> <= >=

  • min max

var b1 = 1tz <= 2tz;
var b2 = 1tz < 2tz;
var b3 = 1tz <> 2tz;
var t1 = 1tz + 1tz;
var t2 = 2 * 4tz;
var t3 = 1/2 * 8tz;

address

constant a : address = @tz1Lc2qBKEWCBeDU8npG6zCeCqpmaegRi6Jg
  • = <>

var b1 = @tz1Lc2qBKEWCBeDU8npG6zCeCqpmaegRi6Jg <> @tz1bfVgcJC4ukaQSHUe1EbrUd5SekXeP9CWk;

duration

// duration of 3 weeks 8 days 4 hours 34 minutes 18 seconds
constant d : duration = 3w8d4h34m18s
  • + -

  • < > = <> <= >=

  • min max

var b1 = 1h > 2h;
var b2 = 1h >= 2h;
var d1 = 1h + 2s;
var d2 = 1h - 2s; /* absolute value */

date

constant date0 : date = 2019-01-01
constant date1 : date = 2019-01-01T01:02:03
constant date2 : date = 2019-01-01T01:02:03Z
constant date3 : date = 2019-01-01T00:00:00+01:00
constant date4 : date = 2019-01-01T00:00:00-05:30
  • < > = <> <= >=

  • min max

var b1 = 2020-01-01 > 2020-12-31;
var b2 = 2020-01-01 >= 2020-12-31;
var d1 = 2020-01-01 + 1d;
var d2 = 2020-01-01 - 1d;

bytes

constant bl : bytes = 0x12f12354356a
  • slice

  • length

  • concat

  • = <>

  • blake2b sha256 sha512

  • pack unpack

var b1 = concat(0x12, 0xef);
var b2 = slice(0xabcdef01, 1, 2);
var h1 = blake2b(0x050100000009617263686574797065);
var h2 = sha256(0x050100000009617263686574797065);
var h3 = sha512(0x050100000009617263686574797065);
var b3 = pack("archetype");
var s : string option = unpack<string>(0x050100000009617263686574797065);

option

constant op1 : option<int> = none
constant op2 : option<int> = some(0)
  • issome

  • isnone

  • opt_get

effect {
var t1 : bool = isnone(none);
var t2 : bool = issome(some(1));
var i : int = opt_get(some(1i)); /* i = 1 */
}

list

  • head_tail

  • contains

  • length

  • nth

  • prepend

effect {
var l : list<string> = ["1"; "2"; "3"];
var ht = head_tail(l);
var t1 = contains(l, "2");
var t2 = length(l);
var n = nth(l);
var p = prepend(l,"0");
}

set

  • add

  • remove

  • contains

  • length

effect {
var my_set : set<int> = [0; 1 ; 2; 3];
var new_set2 : set<int> = add(my_set, 4);
var new_set3 : set<int> = remove(my_set, 0);
var set_c : bool = contains(my_set, 2);
var c : nat = length(my_set);
}

map

  • put

  • remove

  • []

  • getopt

  • contains

  • length

effect {
var my_map : map<string, int> = [ ("k0", 3) ;
("k1", 2) ;
("k2", 1) ;
("k3", 0) ];
var new_map1 : map<string, int> = put(my_map, "k4", 4);
var new_map2 : map<string, int> = remove(my_map, "k0");
var new_map3 : option<int> = my_map["k0"];
var new_map4 : int = getopt(my_map, "k0");
var map_c : bool = contains(my_map, "k0");
var map_l : nat = length(my_map);
}

asset

  • contains

  • count

  • nth

  • head

  • tail

  • select

  • sort

  • sum

archetype expr_method_asset_contains
asset my_asset identified by id {
id : string;
value : int;
} initialized by {
{"id0"; 0i};
{"id1"; 1i};
{"id2"; 2i}
}
variable res : bool = false
entry exec () {
specification {
s0 : res = true;
}
effect {
var t = my_asset.contains("id0");
var c = my_asset.count();
var n = my_asset.nth(1);
var l1 = my_asset.head(3);
var l2 = my_asset.tail(2);
var l3 = my_asset.select(the.id < "id2");
var l4 = my_asset.sort(value);
var l5 = my_asset.sort(v1, asc(v2), desc (v3));
var s = my_asset.sum(value);
}
}

Constants

  • caller

var v : address = caller; /* the address calling the contract */
  • source

var v : address = source; /* the address at the origin of the call */
  • balance

var v : tez = balance; /* the contract's balance in tez */
  • transferred

var v : tez = transferred; /* the amount of tez that comes with the call */
  • now

var v : date = now; /* the date at execution */
  • state

archetype sample_state
states =
| First
| Second
| Third
transition mytr () {
from First
to Second
with effect {
require (state = First)
}
}
  • chainid

var v : chain_id = chainid;

Verification

Specification

Here is a full example with all sections of an entry specification

archetype contract_with_full_specification
asset myasset {
id : string;
val: bool;
}
asset col1 {
id1 : string;
}
asset col2 {
id2 : string;
}
entry exec () {
specification {
definition mydef {
x : myasset | forall y in col1, x.id = y.id1
}
predicate mypredicate (a : int) {
forall x in col1, forall y in col2, x.id1 = y.id2
}
variable myvar : int = 0
shadow effect {
myvar := 3
}
assert a1 {
x = y
invariant for myloop {
x = 0;
y = 0
}
}
postcondition s1 {
x = y
invariant for myloop {
x = 0;
y = 0
}
}
}
effect {
var x : int = 0;
var y : int = 0;
for : myloop c in col1 do
require(true)
done;
assert a1
}
}
  • definition

definition mydef {
x : myasset | forall y in col1, x.id = y.id1
}
  • predicate

predicate mypredicate (a : int) {
forall x in col1, forall y in col2, x.id1 = y.id2
}
  • variable

variable myvar : int = 0
  • shadow effect

shadow effect {
myvar := 3
}
  • assert

assert a1 {
x = y
invariant for myloop {
x = 0;
y = 0
}
}
  • invariant

invariant for myloop {
x = 0;
y = 0
}
  • postcondition

postcondition s1 {
x = y
invariant for myloop {
x = 0;
y = 0
}
}

One specification section is available at the top of the contract. But there is neither shadow effect nor postcondition, which is replaced by contract invariant for the last one.

  • contract invariant

contract invariant c1 {
true <> false
}

Expression

All expression in effect are available in formula part.

  • forall universal quantifier

q1: forall x : int, x = x;
q2: forall x in my_asset, x.value = x.value;
  • exists existential quantifier

q3: exists x : int, x = x;
q4: exists x in my_asset, x.value = x.value;
  • -> imply

o1: true -> true;
  • <-> equivalence

o2: true <-> true;

Asset expression

  • subsetof

archetype expr_formula_asset_method_subset
asset my_asset identified by id {
id : string;
value : int;
} initialized by {
{"id0"; 0};
{"id1"; 1};
{"id2"; 2}
}
entry exec () {
specification {
s: my_asset.subsetof(my_asset);
}
effect {
require (true)
}
}
  • isempty

archetype expr_formula_asset_method_isempty
asset my_asset identified by id {
id : string;
value : int;
} initialized by {
{"id0"; 0};
{"id1"; 1};
{"id2"; 2}
}
entry exec () {
specification {
s: my_asset.isempty();
}
effect {
require (true)
}
}

Extra asset collection

  • before

s1: before.my_asset.isempty();
  • at

s2: at(lbl).my_asset.isempty();
  • unmoved

s3: unmoved.my_asset.isempty();
  • added

s4: added.my_asset.isempty();
  • removed

s5: removed.my_asset.isempty();
  • iterated

entry exec () {
specification {
postcondition p1 {
true
invariant for loop {
iterated.isempty()
}
}
}
effect {
var res : int = 0;
for:loop i in my_asset do
res += 1;
done
}
}
  • toiterate

entry exec () {
specification {
postcondition p1 {
true
invariant for loop {
toiterate.isempty()
}
}
}
effect {
var res : int = 0;
for:loop i in my_asset do
res += 1;
done
}
}

Security predicate

archetype lang_security
constant admin : role = @tz1aazS5ms5cbGkb6FN1wvWmN7yrMTTcr6wB
asset my_asset identified by id {
id : string;
value : int;
}
entry exec () {
effect {
()
}
}
security {
s00 : only_by_role (anyentry, admin);
s01 : only_in_entry (anyentry, exec);
s02 : only_by_role_in_entry (anyentry, admin, exec);
s03 : not_by_role (anyentry, admin);
s04 : not_in_entry (anyentry, exec);
s05 : not_by_role_in_entry (anyentry, admin, exec);
s06 : transferred_by (anyentry);
s07 : transferred_to (anyentry);
s08 : no_storage_fail (anyentry);
}
  • only_by_role

s00 : only_by_role (anyentry, admin);
  • only_in_entry

s01 : only_in_entry (anyentry, exec);
  • only_by_role_in_entry

s02 : only_by_role_in_entry (anyentry, admin, exec);
  • not_by_role

s03 : not_by_role (anyentry, admin);
  • not_in_entry

s04 : not_in_entry (anyentry, exec);
  • not_by_role_in_entry

s05 : not_by_role_in_entry (anyentry, admin, exec);
  • transferred_by

s06 : transferred_by (anyentry);
  • transferred_to

s07 : transferred_to (anyentry);
  • no_storage_fail

s08 : no_storage_fail (anyentry);