# Scilla in Depth¶

## Structure of a Scilla Contract¶

The general structure of a Scilla contract is given in the code fragment below:

- The contract starts with the declaration of
`scilla_version`

, which indicates which major Scilla version the contract uses. - Then follows the declaration of a
`library`

that contains purely mathematical functions, e.g., a function to compute the boolean`AND`

of two bits, or a function computing the factorial of a given natural number. - Then follows the actual contract definition declared using the
keyword
`contract`

. - Within a contract, there are then three distinct parts:
- The first part declares the immutable parameters of the contract.
- The second part declares the mutable fields.
- The third part contains all
`transition`

definitions.

```
(* Scilla contract structure *)
(***************************************************)
(* Scilla version *)
(***************************************************)
scilla_version 1
(***************************************************)
(* Associated library *)
(***************************************************)
library MyContractLib
(* Library code block follows *)
(***************************************************)
(* Contract definition *)
(***************************************************)
contract MyContract
(* Immutable fields declaration *)
(vname_1 : vtype_1,
vname_2 : vtype_2)
(* Mutable fields declaration *)
field vname_1 : vtype_1 = init_val_1
field vname_2 : vtype_2 = init_val_2
(* Transitions *)
(* Transition signature *)
transition firstTransition (param_1 : type_1, param_2 : type_2)
(* Transition body *)
end
transition secondTransition (param_1: type_1)
(* Transition body *)
end
```

### Immutable Variables¶

Immutable variables are the contract’s initial parameters whose values are defined when the contract is deployed, and cannot be modified afterwards.

Declaration of immutable variables has the following format:

```
(vname_1 : vtype_1,
vname_2 : vtype_2,
... )
```

Each declaration consists of a variable name (an identifier) and
followed by its type, separated by `:`

. Multiple variable
declarations are separated by `,`

. The initialization values for
variables are to be specified when the contract is deployed.

Note

In addition to the explicitly declared immutable fields, a Scilla
contract has an implicitly declared mutable field `_this_address`

of type `ByStr20`

, which is initialised to the address of the
contract when the contract is deployed. This field can be
freely read within the implementation, but cannot be modified.

### Mutable Variables¶

Mutable variables represent the mutable state of the contract. They are also
called fields. They are declared after the immutable variables, with each
declaration prefixed with the keyword `field`

.

```
field vname_1 : vtype_1 = expr_1
field vname_2 : vtype_2 = expr_2
...
```

Each expression here is an initializer for the field in question. The definitions complete the initial state of the contract, at the time of creation. As the contract goes through transitions, the values of these fields get modified.

Note

In addition to the explicitly declared mutable fields, a Scilla contract
has an implicitly declared mutable field `_balance`

of
type `Uint128`

, which is initialised to 0 when the contract is
deployed. The `_balance`

field keeps the amount of funds held by
the contract. This field can be freely read within the
implementation, but can only modified by explicitly transferring
funds to other accounts (using `send`

), or by accepting money
from incoming messages (using `accept`

).

Note

Both mutable and immutable variables must be of a *storable*
type:

- Messages, events and the special
`Unit`

type are not storable. All other primitive types like integers and strings are storable. - Function types are not storable.
- Complex types involving uninstantiated type variables are not storable.
- Maps and ADT are storable if the types of their subvalues are storable. For maps this means that the key type and the value type must both be storable, and for ADTs this means that the type of every constructor argument must be storable.

### Transitions¶

Transitions define the change in the state of the contract. These are
defined with the keyword `transition`

followed by the parameters to
be passed. The definition ends with the `end`

keyword.

```
transition foo (vname_1 : vtype_1, vname_2 : vtype_2, ...)
...
end
```

where `vname : vtype`

specifies the name and type of each parameter and
multiple parameters are separated by `,`

.

Note

In addition to the parameters that are explicitly declared in the definition, each transition has the following implicit parameters:

`_sender : ByStr20`

: The account address that triggered this transition. If the transition was called by a contract account instead of a user account, then`_sender`

is the address of the contract that called this transition.`_amount : Uint128`

: Incoming amount of ZILs sent by the sender. To transfer the money from the sender to the contract, the transition must explicitly accept the money using the`accept`

instruction. The money transfer does not happen if the transition does not execute an`accept`

.

Note

Transition parameters must be of a *serialisable* type:

- Messages, events and the special
`Unit`

type are not serialisable. All other primitive types like integers and strings are serialisable. - Function types and map types are not serialisable.
- Complex types involving uninstantiated type variables are not serialisable.
- ADT are serialisable if the types of their subvalues are serialisable. This means that the type of every constructor argument must be serialisable.

### Expressions¶

Expressions handle pure operations. Scilla contains the following types of expressions:

`let x = f`

: Give`f`

the name`x`

in the contract. The binding of`x`

to`f`

is**global**and extends to the end of the contract. The following code fragment defines a constant`one`

whose values is`1`

of type`Int32`

throughout the contract.let one = Int32 1

`let x = f in expr`

: Bind`f`

to the name`x`

within expression`expr`

. The binding here is**local**to`expr`

only. The following example binds the value of`one`

to`1`

of type`Int32`

and`two`

to`2`

of type`Int32`

in the expression`builtin add one two`

, which adds`1`

to`2`

and hence evaluates to`3`

of type`Int32`

.let sum = let one = Int32 1 in let two = Int32 2 in builtin add one two

`{ <entry>_1 ; <entry>_2 ... }`

: Message or event expression, where each entry has the following form:`b : x`

. Here`b`

is an identifier and`x`

a variable, whose value is bound to the identifier in the message.`fun (x : T) => expr`

: A function that takes an input`x`

of type`T`

and returns the value to which expression`expr`

evaluates.`f x`

: Apply the function`f`

to the parameter`x`

.`tfun T => expr`

: A type function that takes`T`

as a parametric type and returns the value to which expression`expr`

evaluates. These are typically used to build library functions. See the section on Pairs below for an example.`@x T`

: Apply the type function`x`

to the type`T`

.`builtin f x`

: Apply the built-in function`f`

on`x`

.`match`

expression: Matches a bound variable with patterns and evaluates the expression in that clause. The`match`

expression is similar to the`match`

expression in OCaml. The pattern to be matched can be an ADT constructor (see ADTs) with subpatterns, a variable, or a wildcard`_`

. An ADT constructor pattern matches values constructed with the same constructor if the subpatterns match the corresponding subvalues. A variable matches anything, and binds the variable to the value it matches in the expression of that clause. A wildcard matches anything, but the value is then ignored.match x with | pattern_1 => expression_1 ... | pattern_2 => expression_2 ... | _ => (*Wildcard*) expression ... end

Note

A pattern-match must be exhaustive, i.e., every legal (type-safe) value of

`x`

must be matched by a pattern. Additionally, every pattern must be reachable, i.e., for each pattern there must be a legal (type-safe) value of`x`

that matches that pattern, and which does not match any pattern preceeding it.

### Statements¶

Statements in Scilla are operations with effect, and hence not purely mathematical. Scilla contains the following types of statements:

`x <- f`

: Fetch the value of the contract field`f`

, and store it into the local variable`x`

.`f := x`

: Update the mutable contract field`f`

with the value of`x`

.`x`

may be a local variable, or another contract field.`x <- & BLOCKNUMBER`

: Fetch the value of the blockchain state variable`BLOCKNUMBER`

, and store it into the local variable`x`

.`v = e`

: Evaluate the expression`e`

, and assign the value to the local variable`v`

.`match`

: Pattern-matching at statement level:match x with | pattern_1 => statement_11; statement_12; ... | pattern_2 => statement_21; statement_22; ... | _ => (*Wildcard*) statement_n1; statement_n2; ... end

`accept`

: Accept the ZILs of the message that invoked the transition. The amount is automatically added to the`_balance`

field of the contract. If a message contains ZILs, but the invoked transition does not accept the money, the money is transferred back to the sender of the message.`send`

and`event`

: Communication with the blockchain. See the next section for details.In-place map operations : Operations on contract fields of type

`Map`

. See the Maps section for details.

A sequence of statements must be separated by semicolons `;`

:

```
transition T ()
statement_1;
statement_2;
...
statement_n
end
```

Notice that the final statement does not have a trailing `;`

, since
`;`

is used to separate statements rather than terminate them.

### Communication¶

A contract can communicate with other contract and user accounts
through the `send`

instruction:

`send msgs`

: Send a list of messages`msgs`

.The following code snippet defines a

`msg`

with four entries`_tag`

,`_recipient`

,`_amount`

and`param`

.(*Assume contractAddress is the address of the contract being called and the contract contains the transition setHello*) msg = { _tag : "setHello"; _recipient : contractAddress; _amount : Uint128 0; param : Uint32 0 };

A message passed to `send`

must contain the compulsory fields
`_tag`

, `_recipient`

and `_amount`

.

The `_recipient`

field (of type `ByStr20`

) is the blockchain
address that the message is to be sent to, and the `_amount`

field
(of type `Uint128`

) is the number of ZIL to be transferred to that
account.

The `_tag`

field (of type `String`

) is only used when the value of
the `_recipient`

field is the address of a contract. In this case,
the value of the `_tag`

field is the name of the transition that is
to be invoked on the recipient contract. If the recipient is a user
account, the `_tag`

field is ignored.

In addition to the compulsory fields the message may contain other
fields (of any type), such as `param`

above. However, if the message
recipient is a contract, the additional fields must have the same
names and types as the parameters of the transition being invoked on
the recipient contract.

Note

The Zilliqa blockchain does not yet support sending multiple
messages in the same transition. This means that the list given as
an argument to `send`

must contain only one message, and that a
transition may perform at most one `send`

instruction each time
the transition is called.

A contract can also communicate to the outside world by emitting events. An event is a signal that gets stored on the blockchain for everyone to see. If a user uses a client application invoke a transition on a contract, the client application can listen for events that the contract may emit, and alert the user.

`event e`

: Emit a message`e`

as an event. The following code emits an event with name`e_name`

.

e = { _eventname : "e_name"; <entry>_2 ; <entry>_3 }; event e

An emitted event must contain the compulsory field `_eventname`

(of
type `String`

), and may contain other entries as well. The value of
the `_eventname`

entry must be a string literal. All events with the
same name must have the same entry names and types.

Note

A transition may send a message at any point during execution, but the recipient account will not receive the message until after the transition has completed. Similarly, a transition may emit events at any point during execution, but the event will not be visible on the blockchain before the transition has completed.

## Primitive Data Types & Operations¶

### Integer Types¶

Scilla defines signed and unsigned integer types of 32, 64, 128, and
256 bits. These integer types can be specified with the keywords
`IntX`

and `UintX`

where `X`

can be 32, 64, 128, or 256. For
example, the type of an unsigned integer of 32 bits is `Uint32`

.

The following code snippet declares a variable of type `Uint32`

:

```
let x = Uint32 43
```

Scilla supports the following built-in operations on integers. Each
operation takes two integers `IntX`

/`UintX`

(of the same type) as
arguments, except for `pow`

whose second argument is always
`Uint32`

`builtin eq i1 i2`

: Is`i1`

equal to`i2`

? Returns a`Bool`

.`builtin add i1 i2`

: Add integer values`i1`

and`i2`

. Returns an integer of the same type.`builtin sub i1 i2`

: Subtract`i2`

from`i1`

. Returns an integer of the same type.`builtin mul i1 i2`

: Integer product of`i1`

and`i2`

. Returns an integer of the same type.`builtin div i1 i2`

: Integer division of`i1`

by`i2`

. Returns an integer of the same type.`builtin rem i1 i2`

: The remainder of integer division of`i1`

by`i2`

. Returns an integer of the same type.`builtin lt i1 i2`

: Is`i1`

less than`i2`

? Returns a`Bool`

.`builtin pow i1 i2`

:`i1`

raised to the power of`i2`

. Returns an integer of the same type as`i1`

.`builtin to_nat i1`

: Convert a value of type`Uint32`

to the equivalent value of type`Nat`

.`builtin to_(u)int(32/64/128/256)`

: Convert a`UintX/IntX`

value to the equivalent`UintX/IntX`

value. Returns`Some IntX/UintX`

if the conversion succeeded,`None`

otherwise.

Addition, subtraction, multiplication, pow, division and reminder operations may raise integer overflow, underflow and division_by_zero errors.

Note

Variables related to blockchain money, such as the `_amount`

entry
of a message or the `_balance`

field of a contract, are of type
`Uint128`

.

### Strings¶

`String`

literals in Scilla are expressed using a sequence of
characters enclosed in double quotes. Variables can be declared by
specifying using keyword `String`

.

The following code snippet declares a variable of type `String`

:

```
let x = "Hello"
```

Scilla supports the following built-in operations on strings:

`builtin eq s1 s2`

: Is`s1`

equal to`s2`

? Returns a`Bool`

.`builtin concat s1 s2`

: Concatenate`s1`

with`s2`

. Returns a`String`

.`builtin substr s1 i1 i2`

: Extract the substring of`s1`

of length`i2`

starting from position`i1`

with length.`i1`

and`i2`

must be of type`Uint32`

. Character indices in strings start from 0. Returns a`String`

.`builtin to_string x1`

: Convert`x1`

to a string literal. Valid types of`x1`

are`IntX`

,`UintX`

,`ByStrX`

and`ByStr`

. Returns a`String`

.`strlen s`

: Calculate the length of`s`

(of type`String`

). Returns a`Uint32`

.

### Crypto Built-ins¶

A hash in Scilla is declared using the data type `ByStr32`

. A
`ByStr32`

represents a hexadecimal byte string of 32 bytes (64
hexadecimal characters). A `ByStr32`

literal is prefixed with
`0x`

.

The following code snippet declares a variable of type `ByStr32`

:

```
let x = 0x123456789012345678901234567890123456789012345678901234567890abff
```

Scilla supports the following built-in operations on hashes. In the description
below, `Any`

can be of type `IntX`

, `UintX`

, `String`

, `ByStr20`

or
`ByStr32`

.

`builtin eq h1 h2`

: Is`h1`

equal to`h2`

? Returns a`Bool`

.`builtin sha256hash x`

: Convert`x`

of`Any`

type to its SHA256 hash. Returns a`ByStr32`

.`builtin keccak256hash x`

: Convert`x`

of`Any`

type to its Keccak256 hash. Returns a`ByStr32`

.`builtin ripemd160hash x`

: Convert`x`

of`Any`

type to its RIPEMD-160 hash. Returns a`ByStr16`

.`builtin to_byStr x`

: Convert a hash`x`

of type`ByStrX`

(for some known`X`

) to one of arbitrary length of type`ByStr`

.`builtin to_uint256 x`

: Convert a hash`x`

to the equivalent value of type`Uint256`

.`x`

must be of type`ByStrX`

for some known`X`

less than or equal to 32.`builtin schnorr_verify pubk x sig`

: Verify a signature`sig`

of type`ByStr64`

against a hash`x`

of type`ByStr32`

with the Schnorr public key`pubk`

of type`ByStr33`

.`concat x1 x2`

: Concatenate the hashes`x1`

and`x2`

. If`x1`

has type`ByStrX`

and`x2`

has type`ByStrY`

, then the result will have type`ByStr(X+Y)`

.

### Maps¶

A value of type `Map kt vt`

provides a key-value store where `kt`

is the type of keys and `vt`

is the type of values. `kt`

may be
any one of `String`

, `IntX`

, `UintX`

, `ByStrX`

or
`ByStr`

. `vt`

may be any type except a function type.

Scilla supports the following built-in operations on maps:

`put m k v`

: Insert a key`k`

and a value`v`

into a map`m`

. Returns a new map which is a copy of the`m`

but with`k`

associated with`v`

. The value of`m`

is unchanged. The`put`

function is typically used in library functions. Note that`put`

makes a copy of`m`

before inserting the key-value pair.`m[k] := v`

:*In-place*insert operation, i.e., identical to`put`

, but without making a copy of`m`

.`m`

must refer to a contract field. Insertion into nested maps is supported with the syntax`m[k1][k2][...] := v`

. If the intermediate key(s) does not exist in the nested maps, they are freshly created along with the map values they are associated with.`get m k`

: Fetch the value associated with the key`k`

in the map`m`

. Returns an optional value (see the`Option`

type below) – if`k`

has an associated value`v`

in`m`

, then the result is`Some v`

, otherwise the result is`None`

. The`get`

function is typically used in library functions.`v <- m[k]`

:*In-place*fetch operation, i.e, identical to`get`

.`m`

must refer to a contract field. Returns an optional value (see the`Option`

type below) – if`k`

has an associated value`v`

in`m`

, then the result is`Some v`

, otherwise the result is`None`

. Fetching from nested maps is supported with the syntax`v <- m[k1][k2][...]`

. If one or more of the intermediate key(s) do not exist in the corresponding map, the result is`None`

.`contains m k`

: Is the key`k`

associated with a value in the map`m`

? Returns a`Bool`

. The`contains`

function is typically used in library functions.`b <- exists m[k]`

:*In-place*existence check, i.e., identical to`contains`

.`m`

must refer to a contract field. Returns a`Bool`

. Existence checks through nested maps is supported with the syntax`v <- exists m[k1][k2][...]`

. If one or more of the intermediate key(s) do not exist in the corresponding map, the result is`False`

.`remove m k`

: Remove a key`k`

and its associated value from the map`m`

. Returns a new map which is a copy of`m`

but with`k`

being unassociated with a value. The value of`m`

is unchanged. The`remove`

function is typically used in library functions. Note that`remove`

makes a copy of`m`

before removing the key-value pair.`delete m[k]`

:*In-place*remove operation, i.e., identical to`remove`

, but without making a copy of`m`

.`m`

must refer to a contract field. Removal from nested maps is supported with the syntax`delete m[k1][k2][...]`

. If any of the specified keys do not exist in the corresponding map, no action is taken. Note that in the case of a nested removal`delete m[k1][...][kn-1][kn]`

, only the key-value association of`kn`

is removed. The key-value bindings of`k`

to`kn-1`

will still exist.`to_list m`

: Convert a map`m`

to a`List (Pair kt vt)`

where`kt`

and`vt`

are key and value types, respectively (see the`List`

type below).

### Addresses¶

An address in Scilla is declared using the data type
`ByStr20`

. `ByStr20`

represents a hexadecimal byte string of 20
bytes (40 hexadecimal characters). A `ByStr20`

literal is prefixed
with `0x`

.

Scilla supports the following built-in operations on addresses:

`eq a1 a2`

: Is`a1`

equal to`a2`

? Returns a`Bool`

.

### Block Numbers¶

Block numbers have a dedicated type `BNum`

in Scilla. Variables of
this type are specified with the keyword `BNum`

followed by an
integer value (for example `BNum 101`

).

Scilla supports the following built-in operations on block numbers:

`eq b1 b2`

: Is`b1`

equal to`b2`

? Returns a`Bool`

.`blt b1 b2`

: Is`b1`

less than`b2`

? Returns a`Bool`

.`badd b1 i1`

: Add`i1`

of type`UintX`

to`b1`

of type`BNum`

. Returns a`BNum`

.`bsub b1 b2`

: Subtract`b2`

from`b1`

, both of type`BNum`

. Returns an`Int256`

.

## Algebraic Datatypes¶

An algebraic datatype (ADT) is a composite type used commonly in
functional programming. Each ADT is defined as a set of
**constructors**. Each constructor takes a set of arguments of certain
types.

Scilla is equipped with a number of built-in ADTs, which are described below. Additionally, Scilla allows users to define their own ADTs.

### Boolean¶

Boolean values are specified using the type `Bool`

. The `Bool`

ADT
has two constructors `True`

and `False`

, neither of which take any
arguments. Thus the following code fragment constructs a value of type
`Bool`

by using the constructor `True`

:

```
x = True
```

### Option¶

Optional values are specified using the type `Option t`

, where `t`

is some type. The `Option`

ADT has two constructors:

`Some`

represents the presence of a value. The`Some`

constructor takes one argument (the value, of type`t`

).`None`

represents the absence of a value. The`None`

constructor takes no arguments.

The following code snippet constructs two optional values. The first
value is an absent string value, constructed using `None`

. The
second value is the `Int32`

value 10, which, because the value is
present, is constructed using `Some`

:

```
let none_value = None {String}
let some_value =
let ten = Int32 10 in
Some {Int32} ten
```

Optional values are useful for initialising fields where the value is not yet known:

```
field empty_bool : Option Bool = None {Bool}
```

Optional values are also useful for functions that might not have a
result, such as the `get`

function for maps:

```
getValue = builtin get m _sender;
match getValue with
| Some v =>
(* _sender was associated with v in m *)
v = v + v;
...
| None =>
(* _sender was not associated with a value in m *)
...
end
```

### List¶

Lists of values are specified using the type `List t`

, where `t`

is some type. The `List`

ADT has two constructors:

`Nil`

represents an empty list. The`Nil`

constructor takes no arguments.`Cons`

represents a non-empty list. The`Cons`

constructor takes two arguments: The first element of the list (of type`t`

), and another list (of type`List t`

) representing the rest of the list.

All elements in a list must be of the same type `t`

. In other
words, two values of different types cannot be added to the same list.

The following example shows how to build a list of `Int32`

values. First we create an empty list using the `Nil`

constructor. We then add four other values one by one using the
`Cons`

constructor. Notice how the list is constructed backwards by
adding the last element, then the second-to-last element, and so on,
so that the final list is `[11; 10; 2; 1]`

:

```
let one = Int32 1 in
let two = Int32 2 in
let ten = Int32 10 in
let eleven = Int32 11 in
let nil = Nil {Int32} in
let l1 = Cons {Int32} one nil in
let l2 = Cons {Int32} two l1 in
let l3 = Cons {Int32} ten l2 in
Cons {Int32} eleven l3
```

Scilla provides two structural recursion primitives for lists, which can be used to traverse all the elements of any list:

`list_foldl: ('B -> 'A -> 'B) -> 'B -> (List 'A) -> 'B`

: Recursively process the elements in a list from front to back, while keeping track of an*accumulator*(which can be though of as a running total).`list_foldl`

takes three arguments, which all depend on the two type variables`'A`

and`'B`

:- The function processing the elements. This function takes two
arguments. The first argument is the current value of the
accumulator (of type
`'B`

). The second argument is the next list element to be processed (of type`'A`

). The result of the function is the next value of the accumulator (of type`'B`

). - The initial value of the accumulator (of type
`'B`

). - The list of elements to be processed (of type
`(List 'A)`

).

The result of applying

`list_foldl`

is the value of the accumulator (of type`'B`

) when all list elements have been processed.- The function processing the elements. This function takes two
arguments. The first argument is the current value of the
accumulator (of type
`list_foldr: ('A -> 'B -> 'B) -> 'B -> (List 'A) -> 'B`

: Similar to`list_foldl`

, except the list elements are processed from back to front. Notice also that the processing function takes the list element and the accumulator in the opposite order from the order in`list_foldl`

.

Note

When an ADT takes type arguments (such as `List 'A`

), and occurs
inside a bigger type (such as the type of `list_foldl`

), the ADT
and its arguments must be grouped using parentheses `( )`

. This
is the case even when the ADT occurs as the only argument to
another ADT. For instance, when constructing an empty list of
optional values of type `Int32`

, one must instantiate the list
type using the syntax `Nil {(Option Int32)}`

.

To further illustrate the `List`

type in Scilla, we show a small
example using `list_foldl`

to count the number of elements in a
list.

1 2 3 4 5 6 7 8 9 10 11 12 | ```
let list_length =
tfun 'A =>
fun (l : List 'A) =>
let folder = @list_foldl 'A Uint32 in
let init = Uint32 0 in
let iter =
fun (z : Uint32) =>
fun (h : 'A) =>
let one = Uint32 1 in
builtin add one z
in
folder iter init l
``` |

`list_length`

defines a function that takes a type argument `'A`

,
and a normal (value) argument `l`

of type `List 'A`

.

`'A`

is a *type variable* which must be instantiated by the code
that intends to use `list_length`

. The type varible is specified in
line 2.

In line 4 we instantiate the types for `list_foldl`

. Since we are
traversing a list of values of type `'A`

, we pass `'A`

as the
first type argument to `list_foldl`

, and since we are calculating
the length of the list (a non-negative integer), we pass `Uint32`

as
the accumulator type.

In line 5 we define the initial value of the accumulator. Since an
empty list has length 0, the initial value of the accumulator is 0 (of
type `Uint32`

, to match the accumulator type).

In lines 6-10 we specify the processing function `iter`

, which takes
the current accumulator value `z`

and the current list element
`h`

. In this case the processing function ignores the list element,
and increments the accumulator by 1. When all elements in the list
have been processed, the accumulator will have been incremented as
many times as there are elements in the list, and hence the final
value of the accumulator will be equal to the length of the list.

In line 12 we apply the type-instantiated version of `list_foldl`

from line 4 to the processing function, the initial accumulator, and
the list of values.

Common utilities for the `List`

type (including `list_length`

) are
provided in the `ListUtils`

library as part of the standard library
distribution for Scilla.

### Pair¶

Pairs of values are specified using the type `Pair t1 t2`

, where
`t1`

and `t2`

are types. The `Pair`

ADT has one constructor:

`Pair`

represents a pair of values. The`Pair`

constructor takes two arguments, namely the two values of the pair, of types`t1`

and`t2`

, respectively.

Note

`Pair`

is both the name of a type and the name of a constructor
of that type. An ADT and a constructor typically only share their
names when the constructor is the only constructor of the ADT.

A `Pair`

value may contain values of different types. In other
words, `t1`

and `t2`

need not be the same type.

Below is an example where we declare a field `pp`

of type ```
Pair
String Uint32
```

, which we then initialise by constructing a pair
consisting of a value of type `String`

and a value of type
`Uint32`

:

```
field pp: Pair String Uint32 =
let s1 = "Hello" in
let num = Uint32 2 in
Pair {String Uint32} s1 num
```

Notice the difference in how we specify the type of the field as
`Pair A' B'`

, and how we specify the types of values given to the
constructor as `Pair { A' B' }`

.

We now illustrate how pattern matching can be used to extract the
first element from a `Pair`

. The function `fst`

shown below
is defined in the `PairUtils`

library of the Scilla standard library.

```
let fst =
tfun 'A =>
tfun 'B =>
fun (p : Pair ('A) ('B)) =>
match p with
| Pair a b => a
end
```

Note

Using `Pair`

is generally discouraged. Instead, the programmer
should define an ADT which is specialised to the particular
type of pairs that is needed in the particular use case. See the
section on User-defined ADTs below.

### Nat¶

Peano numbers are specified using the type `Nat`

. The `Nat`

ADT
has two constructors:

`Zero`

represents the number 0. The`Zero`

constructor takes no arguments.`Succ`

represents the successor of another Peano number. The`Succ`

constructor takes one argument (of type`Nat`

) which represents the Peano number that is one less than the current number.

The following code shows how to build the Peano number corresponding to the integer 3:

```
let three =
let zero = Zero in
let one = Succ zero in
let two = Succ one in
Succ two
```

Scilla provides one structural recursion primitive for Peano numbers,
which can be used to traverse all the Peano numbers from a given
`Nat`

down to `Zero`

:

`nat_fold: ('A -> Nat -> 'A) -> 'A -> Nat -> 'A`

: Recursively process the succession of numbers from a`Nat`

down to`Zero`

, while keeping track of an accumulator.`nat_fold`

takes three arguments, two of which depend on the type variable`'A`

:- The function processing the numbers. This function takes two
arguments. The first argument is the current value of the
accumulator (of type
`'A`

). The second argument is the next Peano number to be processed (of type`Nat`

). The result of the function is the next value of the accumulator (of type`'A`

). - The initial value of the accumulator (of type
`'A`

). - The first Peano number to be processed (of type
`Nat`

).

The result of applying

`nat_fold`

is the value of the accumulator (of type`'A`

) when all Peano numbers down to`Zero`

have been processed.- The function processing the numbers. This function takes two
arguments. The first argument is the current value of the
accumulator (of type

### User-defined ADTs¶

In addition to the built-in ADTs described above, Scilla supports user-defined ADTs.

ADT definitions may only occur in the library parts of a program, either in the library part of the contract, or in an imported library. An ADT definiton is in scope in the entire library in which it is defined, except that an ADT definition may only refer to other ADT definitions defined earlier in the same library, or in imported libraries. In particular, an ADT definition may not refer to itself in an inductive/recursive manner.

Each ADT defines a set of constructors. Each constructor specifies a number of types which corresponds to the number and types of arguments that the constructor takes. A constructor may be specified as taking no arguments.

The ADTs of a contract must have distinct names, and the set of all
constructors of all ADTs in a contract must also have distinct
names. However, a constructor and an ADT may have the same name, as is
the case with the `Pair`

type whose only constructor is also called
`Pair`

.

As an example of user-defined ADTs, consider the following type declarations from a contract implementing a chess-like game called Shogi or Japanese Chess (https://en.wikipedia.org/wiki/Shogi). When in turn, a player can choose to either move one of his pieces, place a previously captured piece back onto the board, or resign and award the victory to the opponent.

The pieces of the game can be defined using the following type
`Piece`

:

```
type Piece =
| King
| GoldGeneral
| SilverGeneral
| Knight
| Lance
| Pawn
| Rook
| Bishop
```

Each of the constructors represents a type of piece in the games. None of the constructors take any arguments.

The board is represented as a set of squares, where each square has two coordinates:

```
type Square =
| Square of Uint32 Uint32
```

The type `Square`

is an example of a type where a constructor has
the same name as the type. This usually happens when a type has only
one constructor. The constructor `Square`

takes two arguments, both
of type `Uint32`

, which are the coordinates (the row and the column)
of the square on the board.

Similar to the definition of the type `Piece`

, we can define the
type of direction of movement using a constructor for each of the
legal directions as follows:

```
type Direction =
| East
| SouthEast
| South
| SouthWest
| West
| NorthWest
| North
| NorthEast
```

We are now in a position to define the type of possible actions that a user may choose to perform when in turn:

```
type Action =
| Move of Square Direction Uint32 Bool
| Place of Piece Square
| Resign
```

If a player chooses to move a piece, she should use the constructor
`Move`

, and provide four arguments:

- An argument of type
`Square`

, indicating the current position of the piece she wants to move. - An argument of type
`Direction`

, indicating the direction of movement. - An argument of type
`Uint32`

, indicating the distance the piece should move. - An argument of type
`Bool`

, indicating whether the moved piece should be promoted after being moved.

If instead the player chooses to place a previously captured piece
back onto the board, she should use the constructor `Place`

, and
provide two arguments:

- An argument of type
`Piece`

, indicating which piece to place on the board. - An argument of type
`Square`

, indicating the position the piece should be placed in.

Finally, if the player chooses to resign and award the victory to her
opponent, she should use the constructor `Resign`

. Since `Resign`

does not take any arguments, no arguments should be provided.

To check which action a player has chosen we use a match statement or a match expression:

```
transition PlayerAction (action : Action)
...
match action with
| Resign =>
...
| Place piece square =>
...
| Move square direction distance promote =>
...
end;
...
end
```

## More ADT examples¶

To further illustrate how ADTs can be used, we provide two more
examples and describe them in detail. Both the functions described
below can be found in the `ListUtils`

part of the Scilla standard
library.

### Computing the Head of a List¶

The function `list_head`

returns the first element of a list.

Since a list may be empty, `list_head`

may not always be able to
compute a result, and thus should return a value of the `Option`

type. If the list is non-empty, and the first element is `h`

, then
`list_head`

should return `Some h`

. Otherwise, if the list is
empty, `list_head`

should return `None`

.

The following code snippet shows the implementation of `list_head`

,
and how to apply it:

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 | ```
let list_head =
tfun 'A =>
fun (l : List 'A) =>
match l with
| Cons h t =>
Some {'A} h
| Nil =>
None {'A}
end
let int_head = @list_head Int32 in
let one = Int32 1 in
let two = Int32 2 in
let three = Int32 3 in
let nil = Nil {Int32} in
let l1 = Cons {Int32} three nil in
let l2 = Cons {Int32} two l1 in
let l3 = Cons {Int32} one l2 in
int_head l3
``` |

Line 2 specifies that `'A`

is a type parameter to the function,
while line 3 specifies that `l`

is a (value) parameter of type
`List 'A`

. In other words, lines 1-3 specify a function
`list_head`

which can be instantiated for any type `'A`

, and which
takes as an argument a value of type `List 'A`

.

The pattern-match in lines 4-9 matches on the value of `l`

. In line
5 we match on the list constructor `Cons h t`

, where `h`

is the
first element of the list, and `t`

is the rest of the list. If the
list is not empty then the match is successful, and we return the
first element as an optional value `Some h`

. In line 7 we match on
the list constructor `Nil`

. If the list is empty then the match is
successful, and we return the optional value `None`

indicating that
there was no head element of the list.

Line 11 instantiates the `list_head`

function for the type
`Int32`

, so that `list_head`

can be applied to values of type
`List Int32`

. Lines 13-20 build a list of type `List Int32`

, and
line 21 invokes the instantiated `list_head`

function on the list
that was built.

### Checking for Existence in a List¶

The function `list_exists`

takes a predicate function and a list,
and returns a value indicating whether the predicate holds for at
least one element in the list.

A predicate function is a function returning a boolean value, and since we want to apply it to elements in the list, the argument type of the function should be the same as the element type of the list.

`list_exists`

should return either `True`

(if the predicate holds
for at least one element) or `False`

(if the predicate does not hold
for any element in the list), so the return type of `list_exists`

should be `Bool`

.

The following code snippet shows the implementation of
`list_exists`

, and how to apply it:

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 | ```
let list_exists =
tfun 'A =>
fun (f : 'A -> Bool) =>
fun (l : List 'A) =>
let folder = @list_foldl 'A Bool in
let init = False in
let iter =
fun (z : Bool) =>
fun (h : 'A) =>
let res = f h in
match res with
| True =>
True
| False =>
z
end
in
folder iter init l
let int_exists = @list_exists Int128 in
let f =
fun (a : Int128) =>
let three = Int128 3 in
builtin lt a three
(* build list l3 similar to the previous example *)
...
(* check if l3 has at least one element satisfying f *)
int_exists f l3
``` |

As in the previous example `'A`

is a type variable to the
function. The function takes two arguments:

- A predicate
`f`

, i.e., a function that returns a`Bool`

. In this case,`f`

will be applied to elements of the list, so the argument type of the predicate should be`'A`

. Hence,`f`

should have the type`'A -> Bool`

. - A list of elements
`l`

of type`List 'A`

, so that the type of the elements in the list matches the argument type of`f`

.

To traverse the elements of the input list `l`

we use
`list_foldl`

. In line 5 we instantiate `list_foldl`

for lists with
elements of type `'A`

and for the accummulator type `Bool`

. In
line 6 we set the initial accummulator value to `False`

to indicate
that no element satisfying the predicate has yet been seen.

The processing function `iter`

defined in lines 7-16 tests the
predicate on the current list element, and returns an updated
accummulator. If an element has been found which satisfies the
predicate, the accummulator is set to `True`

and remains so for the
rest of the traversal.

The final value of the accumulator is either `True`

, indicating that
`f`

returned `True`

for at least one element in the list, or
`False`

, indicating that `f`

returned `False`

for all elements
in the list.

In line 20 we instantiate `list_exists`

to work on lists of type
`Int128`

. In lines 21-24 we define the predicate, which returns
`True`

if its argument is less than 3, and returns `False`

otherwise.

Omitted in line 27 is building the same list `l3`

as in the previous
example. In line 30 we apply the instantiated `list_exists`

to the
predicate and the list.

## Standard Libraries¶

The Scilla standard library contains five libraries:
`BoolUtils.scilla`

, `IntUtils.scilla`

, `ListUtils.scilla`

,
`NatUtils.scilla`

and `PairUtils.scilla`

. As the names suggests
these contracts implement utility operations for the `Bool`

,
`IntX`

, `List`

, `Nat`

and `Pair`

types, respectively.

To use functions from the standard library in a contract, the relevant
library file must be imported using the `import`

declaration. The
following code snippet shows how to import the functions from the
`ListUtils`

and `IntUtils`

libraries:

```
import ListUtils IntUtils
```

The `import`

declaration must occur immediately before the
contract’s own library declaration, e.g.:

```
import ListUtils IntUtils
library WalletLib
... (* The declarations of the contract's own library values and functions *)
contract Wallet ( ... )
... (* The transitions of the contract *)
```

Below, we present the functions defined in each of the library.

### BoolUtils¶

`andb : Bool -> Bool -> Bool`

: Computes the logical AND of two`Bool`

values.`orb : Bool -> Bool -> Bool`

: Computes the logical OR of two`Bool`

values.`negb : Bool -> Bool`

: Computes the logical negation of a`Bool`

value.`bool_to_string : Bool -> String`

: Transforms a`Bool`

value into a`String`

value.`True`

is transformed into`"True"`

, and`False`

is transformed into`"False"`

.

### IntUtils¶

`intX_eq : IntX -> IntX -> Bool`

: Equality operator specialised for each`IntX`

type.`uintX_eq : UintX -> UintX -> Bool`

: Equality operator specialised for each`UintX`

type.`intX_lt : IntX -> IntX -> Bool`

: Less-than operator specialised for each`IntX`

type.`uintX_lt : UintX -> UintX -> Bool`

: Less-than operator specialised for each`UintX`

type.`intX_neq : IntX -> IntX -> Bool`

: Not-equal operator specialised for each`IntX`

type.`uintX_neq : UintX -> UintX -> Bool`

: Not-equal operator specialised for each`UintX`

type.`intX_le : IntX -> IntX -> Bool`

: Less-than-or-equal operator specialised for each`IntX`

type.`uintX_le : UintX -> UintX -> Bool`

: Less-than-or-equal operator specialised for each`UintX`

type.`intX_gt : IntX -> IntX -> Bool`

: Greater-than operator specialised for each`IntX`

type.`uintX_gt : UintX -> UintX -> Bool`

: Greater-than operator specialised for each`UintX`

type.`intX_ge : IntX -> IntX -> Bool`

: Greater-than-or-equal operator specialised for each`IntX`

type.`uintX_ge : UintX -> UintX -> Bool`

: Greater-than-or-equal operator specialised for each`UintX`

type.

### ListUtils¶

`list_map : ('A -> 'B) -> List 'A -> : List 'B`

.Apply`f : 'A -> 'B`

to every element of`l : List 'A`

, constructing a list (of type`List 'B`

) of the results.(* Library *) let f = fun (a : Int32) => builtin sha256hash a (* Contract transition *) (* Assume input is the list [ 1 ; 2 ; 3 ] *) (* Apply f to all values in input *) hash_list_int32 = @list_map Int32 ByStr32; hashed_list = hash_list_int32 f input; (* hashed_list is now [ sha256hash 1 ; sha256hash 2 ; sha256hash 3 ] *)

`list_filter : ('A -> Bool) -> List 'A -> List 'A`

.Filter out elements on the list based on the predicate`f : 'A -> Bool`

. If an element satisfies`f`

, it will be in the resultant list, otherwise it is removed. The order of the elements is preserved.(*Library*) let f = fun (a : Int32) => let ten = Int32 10 in builtin lt a ten (* Contract transition *) (* Assume input is the list [ 1 ; 42 ; 2 ; 11 ; 12 ] *) less_ten_int32 = @list_filter Int32; less_ten_list = less_ten_int32 f l (* less_ten_list is now [ 1 ; 2 ]*)

`list_head : (List 'A) -> (Option 'A)`

.Return the head element of a list`l : List 'A`

as an optional value. If`l`

is not empty with the first element`h`

, the result is`Some h`

. If`l`

is empty, then the result is`None`

.`list_tail : (List 'A) -> (Option List 'A)`

.Return the tail of a list`l : List 'A`

as an optional value. If`l`

is a non-empty list of the form`Cons h t`

, then the result is`Some t`

. If`l`

is empty, then the result is`None`

.`list_append : (List 'A -> List 'A -> List 'A)`

.Append the first list to the front of the second list, keeping the order of the elements in both lists. Note that`list_append`

has linear time complexity in the length of the first argument list.`list_reverse : (List 'A -> List 'A)`

.Return the reverse of the input list. Note that`list_reverse`

has linear time complexity in the length of the argument list.`list_flatten : (List List 'A) -> List 'A`

.Construct a list of all the elements in a list of lists. Each element (which has type`List 'A`

) of the input list (which has type`List List 'A`

) are all concatenated together, keeping the order of the input list. Note that`list_flatten`

has linear time complexity in the total number of elements in all of the lists.`list_length : List 'A -> Int32`

Count the number of elements in a list. Note that`list_length`

has linear time complexity in the number of elements in the list.`list_eq : ('A -> 'A -> Bool) -> List 'A -> List 'A -> Bool`

.Compare two lists element by element, using a predicate function`f : 'A -> 'A -> Bool`

. If`f`

returns`True`

for every pair of elements, then`list_eq`

returns`True`

. If`f`

returns`False`

for at least one pair of elements, or if the lists have different lengths, then`list_eq`

returns`False`

.`list_mem : ('A -> 'A -> Bool) -> 'A -> List 'A -> Bool`

.Checks whether an element`a : 'A`

is an element in the list`l : List'A`

.`f : 'A -> 'A -> Bool`

should be provided for equality comparison.(* Library *) let f = fun (a : Int32) => fun (b : Int32) => builtin eq a b (* Contract transition *) (* Assume input is the list [ 1 ; 2 ; 3 ; 4 ] *) keynumber = Int32 5; list_mem_int32 = @list_mem Int32; check_result = list_mem_int32 f keynumber input; (* check_result is now False *)

`list_forall : ('A -> Bool) -> List 'A -> Bool`

.Check whether all elements of list`l : List 'A`

satisfy the predicate`f : 'A -> Bool`

.`list_forall`

returns`True`

if all elements satisfy`f`

, and`False`

if at least one element does not satisfy`f`

.`list_exists : ('A -> Bool) -> List 'A -> Bool`

.Check whether at least one element of list`l : List 'A`

satisfies the predicate`f : 'A -> Bool`

.`list_exists`

returns`True`

if at least one element satisfies`f`

, and`False`

if none of the elements satisfy`f`

.`list_sort : ('A -> 'A -> Bool) -> List 'A -> List 'A`

.Sort the input list`l : List 'A`

using insertion sort. The comparison function`flt : 'A -> 'A -> Bool`

provided must return`True`

if its first argument is less than its second argument.`list_sort`

has quadratic time complexity.let int_sort = @list_sort Uint64 in let flt = fun (a : Uint64) => fun (b : Uint64) => builtin lt a b let zero = Uint64 0 in let one = Uint64 1 in let two = Uint64 2 in let three = Uint64 3 in let four = Uint64 4 in (* l6 = [ 3 ; 2 ; 1 ; 2 ; 3 ; 4 ; 2 ] *) let l6 = let nil = Nil {Uint64} in let l0 = Cons {Uint64} two nil in let l1 = Cons {Uint64} four l0 in let l2 = Cons {Uint64} three l1 in let l3 = Cons {Uint64} two l2 in let l4 = Cons {Uint64} one l3 in let l5 = Cons {Uint64} two l4 in Cons {Uint64} three l5 (* res1 = [ 1 ; 2 ; 2 ; 2 ; 3 ; 3 ; 4 ] *) let res1 = int_sort flt l6

`list_find : ('A -> Bool) -> List 'A -> Option 'A`

.Return the first element in a list`l : List 'A`

satisfying the predicate`f : 'A -> Bool`

. If at least one element in the list satisfies the predicate, and the first one of those elements is`x`

, then the result is`Some x`

. If no element satisfies the predicate, the result is`None`

.`list_zip : List 'A -> List 'B -> List (Pair 'A 'B)`

.Combine two lists element by element, resulting in a list of pairs. If the lists have different lengths, the trailing elements of the longest list are ignored.`list_zip_with : ('A -> 'B -> 'C) -> List 'A -> List 'B -> List 'C )`

.Combine two lists element by element using a combining function`f : 'A -> 'B -> 'C`

. The result of`list_zip_with`

is a list of the results of applying`f`

to the elements of the two lists. If the lists have different lengths, the trailing elements of the longest list are ignored.`list_unzip : List (Pair 'A 'B) -> Pair (List 'A) (List 'B)`

.Split a list of pairs into a pair of lists consisting of the elements of the pairs of the original list.`list_nth : Uint32 -> List 'A -> Option 'A`

.Return the element number`n`

from a list. If the list has at least`n`

elements, and the element number`n`

is`x`

,`list_nth`

returns`Some x`

. If the list has fewer than`n`

elements,`list_nth`

returns`None`

.

### NatUtils¶

`nat_prev : Nat -> Option Nat`

: Return the Peano number one less than the current one. If the current number is`Zero`

, the result is`None`

. If the current number is`Succ x`

, then the result is`Some x`

.`is_some_zero : Nat -> Bool`

: Zero check for Peano numbers.`nat_eq : Nat -> Nat -> Bool`

: Equality check specialised for the`Nat`

type.`nat_to_int : Nat -> Uint32`

: Convert a Peano number to its equivalent`Uint32`

integer.`uintX_to_nat : UintX -> Nat`

: Convert a`UintX`

integer to its equivalent Peano number. The integer must be small enough to fit into a`Uint32`

. If it is not, then an overflow error will occur.`intX_to_nat : IntX -> Nat`

: Convert an`IntX`

integer to its equivalent Peano number. The integer must be non-negative, and must be small enough to fit into a`Uint32`

. If it is not, then an underflow or overflow error will occur.

### PairUtils¶

`fst : Pair 'A 'B -> 'A`

: Extract the first element of a Pair.`snd : Pair 'A 'B -> 'B`

: Extract the second element of a Pair.

## Scilla versions¶

### Major and Minor versions¶

Scilla releases have a major version, minor version and a patch
number, denoted as `X.Y.Z`

where `X`

is the major version,
`Y`

is the minor version, and `Z`

the patch number.

- Patches are usually bug fixes that do not impact the behaviour of existing contracts. Patches are backward compatible.
- Minor versions typically include performance improvements and feature additions that do not affect the behaviour of existing contracts. Minor versions are backward compatible until the latest major version.
- Major versions are not backward compatible. It is expected that miners have access to implementations of each major version of Scilla for running contracts set to that major version.

Within a major version, miners are advised to use the latest minor revision.

The command `scilla-runner -version`

will print major, minor and patch versions
of the interpreter being invoked.

### Contract Syntax¶

Every Scilla contract must begin with a major version declaration. The syntax is shown below:

```
(***************************************************)
(* Scilla version *)
(***************************************************)
scilla_version 0
(***************************************************)
(* Associated library *)
(***************************************************)
library MyContractLib
...
(***************************************************)
(* Contract definition *)
(***************************************************)
contract MyContract
...
```

When deploying a contract the output of the interpreter contains the
field `scilla_version : X.Y.Z`

, to be used by the blockchain code to
keep track of the version of the contract. Similarly,
`scilla-checker`

also reports the version of the contract on a
successful check.

### The `init.json`

file¶

In addition to the version specified in the contract source code, it
is also required that the contract’s `init.json`

specifies the same
version when the contract is deployed and when the contracts
transitions are invoked. This eases the process for the blockhain
code to decide which interpreter to invoke.

A mismatch in the versions specified in `init.json`

and the source code
will lead to a gas-charged error by the interpreter.

An example `init.json`

:

```
[
{
"vname" : "_creation_block",
"type" : "BNum",
"value" : "1"
},
{
"vname" : "_scilla_version",
"type" : "Uint32",
"value" : "1",
}
]
```

### Chain Invocation Behaviour¶

Contracts of different Scilla versions may invoke transitions on each other.

The semantics of message passing between contracts is guaranteed to be backward compatible between major versions.