An archetype contract is composed of declarations, entry points and optionally specification for formal verification.
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_rolerequire {r1 : arg2 > 0}failif {f1 : arg2 > 10}effect {// ...}}
An entry with just an effect section may omit the effect section syntax:
variable val : nat = 0entry 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| Failtransition confirm () {from Createdto Confirmedwhen { 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 Confirmedto Failwhen { ... }}
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
*
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).
An entry's effect is composed of instructions separated by a semi-colon.
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;
:=
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 * 2d += 3w; // d := i + 3w, date d is now previous d plus 3 weeks
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' examplean_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 fieldan_asset.clear();
See Assets section for details.
;
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_matchwithenum t =| C1| C2| C3| C4| C5variable res : int = 0entry exec () {specification {s0: res = 1;}effect {var x : t = C3;match x with| C1 | C2 -> res := 0| C3 -> res := 1| _ -> res := 2end}}
for in do done
iterates over a collection.
var res = 0;for a in an_asset dores += a.a_val;done;
iter to do done
iterates over a sequence of integer values (starting from 1).
var res = 0iter i to 3 do // iterates from 1 to 3 includedres += 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");
constant x : bool = trueconstant 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;
constant i : nat = 1constant 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);
constant i : int = 1iconstant 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);
constant f : rational = 1.1constant g : rational = -1.1constant r : rational = 2 / 6constant 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 1var i2 = floor(-5 / 3); // int -2var i3 = ceil(5 / 3); // int 2var i4 = ceil(-5 / 3); // int -1
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)
constant ctz : tez = 1tzconstant cmtz : tez = 1mtzconstant 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;
constant a : address = @tz1Lc2qBKEWCBeDU8npG6zCeCqpmaegRi6Jg
=
<>
var b1 = @tz1Lc2qBKEWCBeDU8npG6zCeCqpmaegRi6Jg <> @tz1bfVgcJC4ukaQSHUe1EbrUd5SekXeP9CWk;
// duration of 3 weeks 8 days 4 hours 34 minutes 18 secondsconstant d : duration = 3w8d4h34m18s
+
-
<
>
=
<>
<=
>=
min
max
var b1 = 1h > 2h;var b2 = 1h >= 2h;var d1 = 1h + 2s;var d2 = 1h - 2s; /* absolute value */
constant date0 : date = 2019-01-01constant date1 : date = 2019-01-01T01:02:03constant date2 : date = 2019-01-01T01:02:03Zconstant date3 : date = 2019-01-01T00:00:00+01:00constant 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;
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);
constant op1 : option<int> = noneconstant 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 */}
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");}
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);}
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);}
contains
count
nth
head
tail
select
sort
sum
archetype expr_method_asset_containsasset my_asset identified by id {id : string;value : int;} initialized by {{"id0"; 0i};{"id1"; 1i};{"id2"; 2i}}variable res : bool = falseentry 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);}}
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_statestates =| First| Second| Thirdtransition mytr () {from Firstto Secondwith effect {require (state = First)}}
chainid
var v : chain_id = chainid;
Here is a full example with all sections of an entry specification
archetype contract_with_full_specificationasset 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 = 0shadow effect {myvar := 3}assert a1 {x = yinvariant for myloop {x = 0;y = 0}}postcondition s1 {x = yinvariant for myloop {x = 0;y = 0}}}effect {var x : int = 0;var y : int = 0;for : myloop c in col1 dorequire(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 = yinvariant for myloop {x = 0;y = 0}}
invariant
invariant for myloop {x = 0;y = 0}
postcondition
postcondition s1 {x = yinvariant 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}
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;
subsetof
archetype expr_formula_asset_method_subsetasset 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_isemptyasset 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)}}
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 {trueinvariant for loop {iterated.isempty()}}}effect {var res : int = 0;for:loop i in my_asset dores += 1;done}}
toiterate
entry exec () {specification {postcondition p1 {trueinvariant for loop {toiterate.isempty()}}}effect {var res : int = 0;for:loop i in my_asset dores += 1;done}}
archetype lang_securityconstant admin : role = @tz1aazS5ms5cbGkb6FN1wvWmN7yrMTTcr6wBasset 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);