An archetype contract is composed of declarations, actions (aka entry points) and optionally specification for formal verification.
constantandvariablesdeclare global variables. A constant value cannot be modified in the contract's actions.
constant rate : rational = 0.2variable price : tez = 10tzstatesdeclares contract's possible states. It is then possible to use transitions to change the contract states (see below)
states =
| Created initial
| Confirmed
| Canceled
| Success
| Failinitial is used to declare the initial state value of the contract.
actiondeclares an entry point of the contract. An action has the following sections:specification(optional) to provide the post conditions the action is supposed to haveaccept transfer(optional) to specify that transfer of tez is acceptedcalled by(optional) to declare which role may call this actionrequire(optional) to list the necessary conditions for the action to be executedfailif(optional)to list the conditions which prevent from executioneffectis the code to execute by the action
action an_action_1 (arg1 : string, arg2 : int) {
specification {
// see 'specification' section below
}
called by a_role
require {
r1 : arg2 > 0
}
failif {
f1 : arg2 > 10
}
effect {
// ...
}
}transitiondeclares an entry point of the contract that changes the state of the contract. A transition has the same sections as an action (excepteffect, see above) plus:fromto specify the states the transition starts fromtoto specify the states after the transitionwhen(optional) to specify the transition conditionwith effectto specify the effect of the transition
states
| Created initial
| Confirmed
| Canceled
| Success
| Fail
transition confirm {
from Created
to Confirmed
when { transferred > 10 tz }
with effect {
transfer 1tz to @tz1RNB9PXsnp7KMkiMrWNMRzPjuefSWojBAm
}
}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 fail {
from Created or Confirmed
to Fail
when { ... }
}bool: boolean valuesint: integer valuesrational: floating value that can be expressed as the quotient or fraction of two integersaddress: account addressrole: an address that can be used in action's called by sectiondate: date valuesduration: duration values (in second, minute, hour, day, week)string: string of characterstez: Tezos currencybytes: bytes sequence
*declares a tuple made of other types.
constant pair : int * string = (1, "astr")optiondeclares an option of type.
constant value : int option = nonelistdeclares a list of any type (builtin or composed)
variable vals : string list = []assetdeclares a collection of asset 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;
}enumdeclares an enumeration value. It is read with amatch ... withcommand (see below).
enum color =
| White
| Red
| Green
| BlueIt is then possible to declare a variable of type color:
variable c : color = Greencontractdeclares the signature of another existing contract to call in actions.
contract called_contract_sig {
action set_value (n : int)
action add_value (a : int, b : int)
}It is then possible to declare a contract value of type called_contract_sig and set its address:
constant c : called_contract_sig = @KT1RNB9PXsnp7KMkiMrWNMRzPjuefSWojBAmcollectiondeclares an asset field as a collection of another asset.
asset an_asset identified by id {
id : string;
a_val : int;
asset_col : another_asset collection
}partitiondeclares an asset field as a collection of another asset. The difference withcollectionis 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 identified by id {
id : string;
asset_part : partitioned_asset partition;
}As a consequence of the partition, a partitioned asset cannot be straightforwardly added or removed to its global collection with add and remove (see operation below). This has to be done via a partition field:
my_partitioning_asset.asset_part.add(a_new_partitioned_asset)An action's effect is composed of instructions separated by a semi-colon.
vardeclares 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 * 2
d += 3w; // d := i + 3w, date d is now previous d plus 3 weeksaddenables to add an asset to an asset collection. It fails if the asset key is already present in the collection.
an_asset.add({ id = "RJRUEQDECSTG", asset_col = [] }); // see 'collection' exampleupdateenables to update an existing asset; it takes as arguments the id of the asset to update and the list of effects on the asset. It fails if the id is not present in the asset collection.
an_asset.update("RJRUEQDECSTG", { a_value += 3 });addupdateis similar to update except that it adds the asset if its identifier is not present in the collection.
an_asset.addupdate("RJRUEQDECSTG", { a_value += 3 });removeremoves a an asset from its collection.
an_asset.remove("RJRUEQDECSTG");removeifenables removing assets under a condition.
an_asset.removeif(a_val > 10); // "a_val" is an asset fieldclearclears an asset collection.
an_asset.clear();;sequence
res := 1;
res := 2;
res := 3;if thenandif then elseare the conditional branchings instructions.
if i > 0 then (
// (* effect when i > 0 *)
) else (
// (* effect when i <= 0 *)
);match ... with ... endFIXME
archetype effect_control_matchwith
enum t =
| C1
| C2
| C3
| C4
| C5
variable res : int = 0
action 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 doneiterates over a collection.
var res = 0;
for a in an_asset do
res += a.a_val;
done;iter to do doneiterates 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 6transfertransfers an amount of tez to an address or a contract.
transfer 2tz to @tz1RNB9PXsnp7KMkiMrWNMRzPjuefSWojBAm;With the contract keyword presented above, it is possible to transfer to a contract and call an entry point. In the example below, the entry point set_value of contract c is called and 2tz is transferred.
contract contract_called_sig {
action set_value (n : int)
action add_value (a : int, b : int)
}
constant c : called_contract_sig = @KT1RNB9PXsnp7KMkiMrWNMRzPjuefSWojBAm
action update_value(n : int) {
effect {
transfer 2tz to c call set_value(n);
}
}failaborts the execution. It prevents from deploying the contract on the blockchain. As a consequence the storage is left unchanged when executed.
fail("a message");requireandfailiffail if the argument condition is respectively false and true.require(t)is sugar forif t then fail("").
require(val > 0);
failif(val <= 0);boolean
constant x : bool = true
constant y : bool = falseinteger
constant i : int = 1
constant j : int = -42rational
constant f : rational = 1.1
constant g : rational = -1.1
constant r : rational = 2 div 6
constant t : rational = -2 div 6string
constant s : string = "hello world"tez
constant ctz : tez = 1tz
constant cmtz : tez = 1mtz
constant cutz : tez = 1utzaddress/role
constant a : address = @tz1Lc2qBKEWCBeDU8npG6zCeCqpmaegRi6Jgduration
// duration of 3 weeks 8 days 4 hours 34 minutes 18 seconds
constant d : duration = 3w8d4h34m18s 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 list
constant mylist : int list = [1; 2; 3]option
constant op1 : int option = none
constant op2 : int option = some(0)bytes
constant bl : bytes = 0x12f12354356a andoperator of logical conjunction
var bool_bool_and : bool = (true and false);oroperator of logical disjunction
var bool_bool_or : bool = (true or false);notoperator of logical negation
var bool_bool_not : bool = not true;=FIXME
var int_int_eq : bool = 1 = 2;
var rat_int_eq : bool = (1 div 2) = 2;
var int_rat_eq : bool = 1 = (2 div 3);
var rat_rat_eq : bool = (1 div 3) = (2 div 3);
var tez_tez_eq : bool = 1tz = 2tz;
var dur_dur_eq : bool = 1h = 2h;
var date_date_eq : bool = 2020-01-01 = 2020-12-31;
var bool_bool_eq : bool = true = false;
var addr_addr_eq : bool = @tz1Lc2qBKEWCBeDU8npG6zCeCqpmaegRi6Jg = @tz1bfVgcJC4ukaQSHUe1EbrUd5SekXeP9CWk;
var str_str_eq : bool = "a" = "b";<>FIXME
var int_int_ne : bool = 1 <> 2;
var rat_int_ne : bool = (1 div 2) <> 2;
var int_rat_ne : bool = 1 <> (2 div 3);
var rat_rat_ne : bool = (1 div 2) <> (2 div 3);
var tez_tez_ne : bool = 1tz <> 2tz;
var dur_dur_ne : bool = 1h <> 2h;
var date_date_ne : bool = 2020-01-01 <> 2020-12-31;
var bool_bool_ne : bool = true <> false;
var addr_addr_ne : bool = @tz1Lc2qBKEWCBeDU8npG6zCeCqpmaegRi6Jg <> @tz1bfVgcJC4ukaQSHUe1EbrUd5SekXeP9CWk;
var str_str_ne : bool = "a" <> "b";<FIXME
var int_int_lt : bool = 1 < 2;
var rat_int_lt : bool = (1 div 2) < 2;
var int_rat_lt : bool = 1 < (2 div 3);
var rat_rat_lt : bool = (1 div 2) < (2 div 3);
var tez_tez_lt : bool = 1tz < 2tz;
var dur_dur_lt : bool = 1h < 2h;
var date_date_lt : bool = 2020-01-01 < 2020-12-31;<=FIXME
var int_int_le : bool = 1 <= 2;
var rat_int_le : bool = (1 div 2) <= 2;
var int_rat_le : bool = 1 <= (2 div 3);
var rat_rat_le : bool = (1 div 2) <= (2 div 3);
var tez_tez_le : bool = 1tz <= 2tz;
var dur_dur_le : bool = 1h <= 2h;
var date_date_le : bool = 2020-01-01 <= 2020-12-31;>FIXME
var int_int_gt : bool = 1 > 2;
var rat_int_gt : bool = (1 div 2) > 2;
var int_rat_gt : bool = 1 > (2 div 3);
var rat_rat_gt : bool = (1 div 2) > (2 div 3);
var tez_tez_gt : bool = 1tz > 2tz;
var dur_dur_gt : bool = 1h > 2h;
var date_date_gt : bool = 2020-01-01 > 2020-12-31;>=FIXME
var int_int_ge : bool = 1 >= 2;
var rat_int_ge : bool = (1 div 2) >= 2;
var int_rat_ge : bool = 1 >= (2 div 3);
var rat_rat_ge : bool = (1 div 2) >= (2 div 3);
var tez_tez_ge : bool = 1tz >= 2tz;
var dur_dir_ge : bool = 1h >= 2h;
var date_date_ge : bool = 2020-01-01 >= 2020-12-31;+FIXME
var int_int_plus : int = 1 + 2;
var rat_rat_plus : rational = 1.1 + 1.2;
var int_rat_plus : rational = 1 + 1.2;
var rat_int_plus : rational = 1.1 + 2;
var dur_dur_plus : duration = 1h + 2s;
var date_dur_plus : date = 2020-01-01 + 1d;
var dur_date_plus : date = 1d + 2020-01-01;
var str_str_plus : string = "str1" + "str2"; (* concat *)
var tez_tez_plus : tez = 2tz + 1tz;-FIXME
var int_int_minus : int = 1 - 2;
var rat_rat_minus : rational = 1.1 - 1.2;
var int_rat_minus : rational = 1 - 1.2;
var rat_int_minus : rational = 1.1 - 2;
var date_date_minus : duration = 2020-01-01 - 2019-12-31; (* absolute value *)
var dur_dur_minus : duration = 1h - 2s; (* absolute value *)
var date_dur_minus : date = 2020-01-01 - 1d;
var tez_tez_minus : tez = 2tz - 1tz;*FIXME
var int_int_mult : int = 1 * 2;
var rat_rat_mult : rational = 1.1 * 1.2;
var int_rat_mult : rational = 1 * 1.2;
var rat_int_mult : rational = 1.1 * 2;
var int_dur_mult : duration = 2 * 1h;
var int_tez_mult : tez = 1 * 1tz;
var rat_tez_mult : tez = 1.1 * 1tz;/FIXME
var int_int_div : int = 1 / 2;
var rat_rat_div : rational = 1.1 / 1.2;
var int_rat_div : rational = 1 / 1.2;
var rat_int_div : rational = 1.1 / 2;
var dur_int_div : duration = 1h / 2;%FIXME
var int_int_modulo : int = 1 % 2;callerFIXME
var v : address = caller; (* SENDER *)sourceFIXME
var v : address = source; (* SOURCE *)balanceFIXME
var v : tez = balance; (* BALANCE *)transferredFIXME
var v : tez = transferred; (* AMOUNT *)nowFIXME
var v : date = now; (* NOW *)stateFIXME
archetype sample_state
states =
| First
| Second
| Third
transition mytr () {
from First
to Second
with effect {
require (state = First)
}
}minFIXME
var int_int_min : int = min(1, 2);
var rat_int_min : rat = min(1 div 2, 1);
var int_rat_min : rat = min(2, 1 div 3);
var rat_rat_min : rat = min(1 div 2, 1 div 3);
var date_date_min : date = min(2020-01-01, 2020-12-31);
var dur_dur_min : dur = min(1h, 1s);
var tez_tez_min : tez = min(1tz, 2tz);maxFIXME
var int_int_max : int = max(1, 2);
var rat_int_max : rat = max(1 div 2, 1);
var int_rat_max : rat = max(2, 1 div 3);
var rat_rat_max : rat = max(1 div 2, 1 div 3);
var date_date_max : date = max(2020-01-01, 2020-12-31);
var dur_dur_max : dur = max(1h, 1s);
var tez_tez_max : tez = max(1tz, 2tz);absFIXME
var int_abs : int = abs(-1);
var rat_abs : rat = abs(-1 div 2);containsFIXME
archetype expr_list_contains
variable res : bool = false
action exec () {
specification {
s0: res = true;
}
effect {
var l : string list = ["1"; "2"; "3"];
res := contains(l, "2")
}
}countFIXME
archetype expr_list_count
variable res : int = 0
action exec () {
specification {
s0: res = 3;
}
effect {
var l : string list = ["1"; "2"; "3"];
res := count(l)
}
}nthFIXME
archetype expr_list_nth
variable res : string = ""
action exec () {
specification {
s0: res = "2";
}
effect {
var l : string list = ["1"; "2"; "3"];
res := nth(l, 1)
}
}prependadds an element to a list at the first position.
archetype expr_list_prepend
variable res : string list = []
action exec () {
specification {
s0: res = ["0"; "1"; "2"; "3"];
}
effect {
var l : string list = ["1"; "2"; "3"];
res := prepend(l, "0");
}
}containsFIXME
archetype expr_method_asset_contains
asset my_asset identified by id {
id : string;
value : int;
} initialized by {
{"id0"; 0};
{"id1"; 1};
{"id2"; 2}
}
variable res : bool = false
action exec () {
specification {
s0: res = true;
}
effect {
res := my_asset.contains("id0")
}
}countFIXME
archetype expr_method_asset_count
asset my_asset identified by id {
id : string;
value : int;
} initialized by {
{"id0"; 0};
{"id1"; 1};
{"id2"; 2}
}
variable res : int = 0
action exec () {
specification {
s0: res = 3;
}
effect {
res := my_asset.count()
}
}getFIXME
archetype expr_method_asset_get
asset my_asset identified by id {
id : string;
value : int;
} initialized by {
{"id0"; 0};
{"id1"; 1};
{"id2"; 2}
}
variable res : int = 0
action exec () {
specification {
s0: res = 1;
}
effect {
var a = my_asset.get("id1");
res := a.value
}
}nthFIXME
archetype expr_method_asset_nth
asset my_asset identified by id {
id : string;
value : int;
} initialized by {
{"id0"; 0};
{"id1"; 1};
{"id2"; 2}
}
variable res : int = 0
action exec () {
specification {
s0: res = 1;
}
effect {
var a = my_asset.nth(1);
res := a.value
}
}headFIXME
archetype expr_method_asset_head
asset my_asset identified by id {
id : string;
value : int;
} initialized by {
{"id0"; 4};
{"id1"; 3};
{"id2"; 2}
}
variable res : int = 0
action exec () {
specification {
s0: res = 3;
}
effect {
var l = my_asset.head(2);
var a = l.nth(1);
res := a.value
}
}tailFIXME
archetype expr_method_asset_tail
asset my_asset identified by id {
id : string;
value : int;
} initialized by {
{"id0"; 0};
{"id1"; 1};
{"id2"; 2}
}
variable res : int = 0
action exec () {
specification {
s0: res = 1;
}
effect {
var l = my_asset.tail(2);
var a = l.nth(0);
res := a.value
}
}selectFIXME
archetype expr_method_asset_select
asset my_asset identified by id {
id : string;
value : int;
} initialized by {
{"id0"; 0};
{"id1"; 1};
{"id2"; 2}
}
variable res : int = 0
action exec () {
specification {
s0: res = 2;
}
effect {
var l = my_asset.select(the.id = "id2");
var a = l.nth(0);
res := a.value
}
}sortFIXME
archetype expr_method_asset_sort
asset my_asset identified by id {
id : string;
value : int;
} initialized by {
{"id0"; 3};
{"id1"; 2};
{"id2"; 1}
}
variable res : int = 0
action exec () {
specification {
s0: res = 1;
}
effect {
var l = my_asset.sort(value);
var a = l.nth(0);
res := a.value
}
}you can also sort with several criteria
archetype multi_sort
asset my_asset identified by id {
id : string;
v1 : int;
v2 : int;
v3 : int;
} initialized by {
{"id0"; 1; 2; 7};
{"id1"; 1; 3; 9};
{"id2"; 1; 3; 8};
{"id3"; 1; 2; 6}
}
action exec () {
effect {
var res = my_asset.sort(v1, asc(v2), desc (v3))
(* res = ["id0"; "id3", "id1", "id2"] *)
}
}sumFIXME
archetype expr_method_asset_sum
asset my_asset identified by id {
id : string;
value : int;
} initialized by {
{"id0"; 0};
{"id1"; 1};
{"id2"; 2}
}
variable res : int = 0
action exec () {
specification {
s0: res = 3;
}
effect {
res := my_asset.sum(value)
}
}Here is a full example with all sections of an action specification
archetype contract_with_full_specification
asset myasset {
id: string;
val: bool;
}
asset col1 {
id1 : string;
}
asset col2 {
id2 : string;
}
action 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
}
}definitionFIXME
definition mydef {
x : myasset | forall y in col1, x.id = y.id1
}predicateFIXME
predicate mypredicate (a : int) {
forall x in col1, forall y in col2, x.id1 = y.id2
}variableFIXME
variable myvar : int = 0shadow effectFIXME
shadow effect {
myvar := 3
}assertFIXME
assert a1 {
x = y
invariant for myloop {
x = 0;
y = 0
}
}invariantFIXME
invariant for myloop {
x = 0;
y = 0
}postconditionFIXME
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 invariantFIXME
contract invariant c1 {
true <> false
}All expression in effect are available in formula part.
foralluniversal quantifier
q1: forall x : int, x = x;
q2: forall x in my_asset, x.value = x.value;existsexistential 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;subsetofFIXME
archetype expr_formula_asset_method_subset
asset my_asset identified by id {
id : string;
value : int;
} initialized by {
{"id0"; 0};
{"id1"; 1};
{"id2"; 2}
}
action exec () {
specification {
s: my_asset.subsetof(my_asset);
}
effect {
require (true)
}
}isemptyFIXME
archetype expr_formula_asset_method_isempty
asset my_asset identified by id {
id : string;
value : int;
} initialized by {
{"id0"; 0};
{"id1"; 1};
{"id2"; 2}
}
action exec () {
specification {
s: my_asset.isempty();
}
effect {
require (true)
}
}beforeFIXME
s1: before.my_asset.isempty();atFIXME
s2: at(lbl).my_asset.isempty();unmovedFIXME
s3: my_asset.unmoved.isempty();addedFIXME
s4: my_asset.added.isempty();removedFIXME
s5: my_asset.removed.isempty();iteratedFIXME
action exec2 () {
specification {
postcondition p1 {
true
invariant for loop {
iterated.isempty()
}
}
}
effect {
var res : int = 0;
for:loop i in my_asset do
res += 1;
done
}
}toiterateFIXME
action exec3 () {
specification {
postcondition p1 {
true
invariant for loop {
toiterate.isempty()
}
}
}
effect {
var res : int = 0;
for:loop i in my_asset do
res += 1;
done
}
}archetype lang_security
constant admin : role = @tz1aazS5ms5cbGkb6FN1wvWmN7yrMTTcr6wB
asset my_asset identified by id {
id : string;
value : int;
}
action exec () {
effect {
require true
}
}
security {
s00 : only_by_role (anyaction, admin);
s01 : only_in_action (anyaction, exec);
s02 : only_by_role_in_action (anyaction, admin, exec);
s03 : not_by_role (anyaction, admin);
s04 : not_in_action (anyaction, exec);
s05 : not_by_role_in_action (anyaction, admin, exec);
s06 : transferred_by (anyaction);
s07 : transferred_to (anyaction);
s08 : no_storage_fail (anyaction);
}only_by_roleFIXME
s00 : only_by_role (anyaction, admin);only_in_actionFIXME
s01 : only_in_action (anyaction, exec);only_by_role_in_actionFIXME
s02 : only_by_role_in_action (anyaction, admin, exec);not_by_roleFIXME
s03 : not_by_role (anyaction, admin);not_in_actionFIXME
s04 : not_in_action (anyaction, exec);not_by_role_in_actionFIXME
s05 : not_by_role_in_action (anyaction, admin, exec);transferred_byFIXME
s06 : transferred_by (anyaction);transferred_toFIXME
s07 : transferred_to (anyaction);no_storage_failFIXME
s08 : no_storage_fail (anyaction);