Landing
Github
VS code extension
What is Archetype
Getting started
Usage
Reference
Archetype language
Contract library
Governance
Digital Assets
Escrow
Auction
Finance
Insurance
IoT
Framework examples
Powered by GitBook

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 val_address
  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

  • address : account address

  • bool : boolean values

  • bytes : bytes sequence

  • chain_id: chain id value

  • date : date values

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

  • int : integer values

  • key : key value

  • key_hash : key hash value

  • nat : positive integers

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

  • signature : signature value

  • string : string of characters

  • tez : Tezos currency

  • unit : unit 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> = []

  • big_map declares a big map from a non-composite builtin type to any type.

variable assoc : big_map<int, string> = []

  • set declares a set of non-composite builtin type values.

variable poll : set<address> = []

  • or declares a or type

variable ls : or<nat, string> = left<string>(1)
variable lc : or<nat, string> = left<nat, string>(1)
variable rs : or<nat, string> = right<nat>("mystr")
variable rc : or<nat, string> = right<nat, string>("mystr")

  • record declares a record structure.

record r {
   s : string;
   i : int;
}

  • lambda declares a lambda type

variable vlambda : lambda<nat, int> = lambda<int>((x : nat) -> x - 1)

  • 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
enum t =
| A of nat
| B of string
| C

It is then possible to declare variables:

variable c : color = Green
variable v : t = A(0)

  • contract is the type of contract entry point signature.

variable b : option<contract<nat>> = entrypoint<nat>("%getValue", selfaddress)

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).

​

Other type

  • operation

var e   : contract<unit> = @tz1Lc2qBKEWCBeDU8npG6zCeCqpmaegRi6Jg;
var op  : operation = mkoperation(0tz, e, ());

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
  }
}
archetype expr_control_match_list
​
variable res : nat = 0
​
entry exec() {
  var l : list<nat> = [1];
  res :=
  match l with
  | hd::t -> hd
  | []    -> 0
  end
}
archetype expr_control_match_option
​
variable res : nat = 0
​
entry exec() {
  var o : option<nat> = some(3);
  res :=
  match o with
  | some(v) -> v
  | none -> 0
  end
}
archetype expr_control_match_or
​
variable a : nat = 0
variable b : int = 0
​
entry exec() {
  var l : or<nat, int> = left<int>(2);
  a :=
  match l with
  | left(v)  -> v
  | right(v) -> 0
  end;
​
  var r : or<nat, int> = right<nat>(3i);
  b :=
  match r with
  | left(v)  -> 0i
  | right(v) -> v
  end
}
archetype enum_with_args
​
enum t =
| A of nat
| B of nat
| C
​
variable res : nat = 0
​
entry exec() {
  var o : t = A(1);
​
  match o with
  | A v | B v -> res := v
  | C -> res := 0
  end
}

  • for in do done iterates over a collection.

 var res = 0;
 for a in an_asset do
   res += an_asset[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 subnat

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); // see abs below
var nlsr = 2 |>> 1; // 4
var nlsl = 2 <<| 1; // 1
var n7 = sub_nat(5,6); // fails
var n8 = sub_nat(6,5); // 1

int

constant i : int = 1i
constant j : int = -42;

  • + - * div %

  • < > = <> <= >=

  • min max

  • abs

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
constant p0 : rational = 1%
constant p1 : rational = 1.1%

  • + - * /

  • < > = <> <= >=

  • 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

  • = <>

  • contract_address key_address (converts contract and key to address)

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

  • date_from_timestamp

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;
var d3 = date_from_timestamp(1609372800i) // int to date

bytes

constant bl : bytes = 0x12f12354356a

  • slice

  • length

  • concat

  • = <>

  • blake2b sha256 sha512 keccak sha3

  • 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 h4 = keccak(0x050100000009617263686574797065);
var h5 = sha3(0x050100000009617263686574797065);
var b3 = pack("archetype");
var s : string option = unpack<string>(0x050100000009617263686574797065);

option

constant op1 : option<nat> = none
constant op2 : option<nat> = some(0)

  • issome

  • isnone

  • opt_get

  • require_some

  • match ... with | some(v) -> ... | none -> ... end

effect {
    var t1 : bool = isnone(none);
    var t2 : bool = issome(some(1));
    var i  : nat  = opt_get(some(1)); /* i = 1 */
    var i  : nat  = require_some(none, "some is required"); /* will fail ... */
}

list

  • 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<nat> = [0; 1 ; 2; 3];
    var new_set2 : set<nat> = add(my_set, 4);
    var new_set3 : set<nat> = 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, nat> = [ ("k0", 3) ;
                                      ("k1", 2) ;
                                      ("k2", 1) ;
                                      ("k3", 0) ];
    var new_map1 : map<string, nat> = put(my_map, "k4", 4);
    var new_map2 : map<string, nat> = remove(my_map, "k0");
    var new_map3 : option<nat>      = my_map["k0"];
    var new_map4 : nat              = getopt(my_map, "k0");
    var map_c    : bool             = contains(my_map, "k0");
    var map_l    : nat              = length(my_map);
}

record

record can be shaped with as, like below:

record my_record {
  a: int;
  b: nat;
  c: string;
} as (((x, %_), z))
​
variable r : my_record = {1i; 2; "mystr"}

generates in michelson :

storage (pair (pair (int %x) nat) (string %z))

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);
  }
}

blockchain operations

  • set_delegate

  • implicit_account

var kh : key_hash       = "tz1aazS5ms5cbGkb6FN1wvWmN7yrMTTcr6wB";
var op : operation      = set_delegate(some(kh));
var c  : contract<unit> = implicit_account(kh);

see https://tezos.gitlab.io/michelson-reference/#instr-SET_DELEGATE and https://tezos.gitlab.io/michelson-reference/#instr-IMPLICIT_ACCOUNT for more detail

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;

  • unit

variable u0 : unit = ()
variable u1 : unit = Unit

  • operations is the list of operation returned after effect execution of an entry

entry exec(op  : operation) {
  operations := prepend(operations, op);
}

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 expressions in effect are available in the 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 : address = @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);
Previous
Usage
Next
Archetype language
Last updated 3 weeks ago
Edit on GitHub
Contents
Declarations
Builtin types
Composite types
Other type
Effect
Declaration
Assignment
Effects on asset collection
Control
Expressions
bool
nat
int
rational
string
tez
address
duration
date
bytes
option
list
set
map
record
asset
blockchain operations
Constants
Verification
Specification
Expression
Asset expression
Extra asset collection
Security predicate