# 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 four distinct parts:
- The first part declares the immutable parameters of the contract.
- The second part describes the contract’s constraint, which must be valid when the contract is deployed.
- The third part declares the mutable fields.
- The fourth part contains all
`transition`

and`procedure`

definitions.

```
(* Scilla contract structure *)
(***************************************************)
(* Scilla version *)
(***************************************************)
scilla_version 1
(***************************************************)
(* Associated library *)
(***************************************************)
library MyContractLib
(* Library code block follows *)
(***************************************************)
(* Contract definition *)
(***************************************************)
contract MyContract
(* Immutable contract parameters declaration *)
(vname_1 : vtype_1,
vname_2 : vtype_2)
(* Contract constraint *)
with
(* Constraint expression *)
=>
(* Mutable fields declaration *)
field vname_1 : vtype_1 = init_val_1
field vname_2 : vtype_2 = init_val_2
(* Transitions and procedures *)
(* Procedure signature *)
procedure firstProcedure (param_1 : type_1, param_2 : type_2)
(* Procedure body *)
end
(* Transition signature *)
transition firstTransition (param_1 : type_1, param_2 : type_2)
(* Transition body *)
end
(* Procedure signature *)
procedure secondProcedure (param_1 : type_1, param_2 : type_2)
(* Procedure body *)
end
transition secondTransition (param_1: type_1)
(* Transition body *)
end
```

### Immutable Contract Parameters¶

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

Immutable parameters are declared using the following syntax:

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

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

. Multiple parameter
declarations are separated by `,`

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

Note

In addition to the explicitly declared immutable parameters, a Scilla contract has the following implicitly declared immutable contract parameters

1.

`_this_address`

of type`ByStr20`

, which is initialised to the address of the contract when the contract is deployed.2.

`_creation_block`

of type`BNum`

, which is initialized to the block number at which the contract is / was deployed.

These parameters can be freely read within the implementation without having to
dereference it using `<-`

and cannot be modified with `:=`

.

### Contract Constraints¶

A contract constraint is a requirement placed on the contract’s immutable parameters. A contract constraint provides a way of establishing a contract invariant as soon as the contract is deployed, thus preventing the contract being deployed with nonsensical parameters.

A contract constraint is declared using the following syntax:

```
with
...
=>
```

The constraint must be an expression of type `Bool`

.

The constraint is checked when the contract is deployed. Contract
deployment only succeeds if the constraint evaluates to `True`

. If
it evaluates to `False`

, then the deployment fails.

Here is a simple example of using contract constraints to make sure a contract with a limited period of functioning is not deployed after that period:

```
contract Mortal(end_of_life : BNum)
with
builtin blt _creation_block end_of_life
=>
```

The snippet above uses the implicit contract parameter `_creation_block`

described in Immutable Contract Parameters.

Note

Declaring a contract constraint is optional. If no constraint is
declared, then the constraint is assumed to simply be `True`

.

### Mutable Fields¶

Mutable fields represent the mutable state (mutable variables) of the
contract. They are declared after the immutable parameters, 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 initialiser for the field in question. The definitions complete the initial state of the contract, at the time of creation. As the contract executes a transition, 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, measured in QA (1 ZIL = 1,000,000,000,000 QA). 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 fields and immutable parameters 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.

### Units¶

The Zilliqa protocol supports three basic tokens units - ZIL, LI (10^-6 ZIL) and QA (10^-12 ZIL).

The base unit used in Scilla smart contracts is QA. Hence, when using money variables, it is important to attach the trailing zeroes that are needed to represent it in QAs.

(* fee is 1 QA *) let fee = Uint128 1 (* fee is 1 LI *) let fee = Uint128 1000000 (* fee is 1 ZIL *) let fee = Uint128 1000000000000

### Transitions¶

Transitions are a way to define how the state of the contract may change. The transitions of a contract define the public interface for the contract, since transitions may be invoked by sending a message to the contract.

Transitions 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. In a chain call, this is the contract that sent the message invoking the current transition.`_origin : ByStr20`

: The account address that initiated the current transaction (which can possibly be a chain call). This is always a user address, since contracts can never initiate transactions.`_amount : Uint128`

: Incoming amount, in QA (see section above on the units), 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.

### Procedures¶

Procedures are another way to define now the state of the contract may change, but in contrast to transitions, procedures are not part of the public interface of the contract, and may not be invoked by sending a message to the contract. The only way to invoke a procedure is to call it from a transition or from another procedure.

Procedures are defined with the keyword `procedure`

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

keyword.

```
procedure 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 `,`

.

Once a procedure is defined it is available to be invoked from transitions and procedures in the rest of the contract file. It is not possible to invoke a procedure from transition or procedure defined earlier in the contract, nor is it possible for a procedure to call itself recursively.

Procedures are invoked using the name of the procedure followed by the actual arguments to the procedure:

```
v1 = ...;
v2 = ...;
foo v1 v2;
```

All arguments must be supplied when the procedure is invoked. A procedure does not return a result.

Note

The implicit transition parameters `_sender`

, `_origin`

and `_amount`

are
implicitly passed to all the procedures that a transition
calls. There is therefore no need to declare those parameters
explicitly when defining a procedure.

Note

Procedure parameters cannot be (or contain) maps. If a procedure needs to access a map, it is therefore necessary to either make the procedure directly access the contract field containing the map, or use a library function to perform the necessary computations on the map.

### 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 implementation of fst for an example.Note

Shadowing of type variables is not currently allowed. E.g.

`tfun 'T => tfun 'T => expr`

is not a valid expression.`@x T`

: Apply the type function`x`

to the type`T`

. This specialises the type function`x`

by instantiating the first type variable of`x`

to`T`

. Type applications are typically used when a library function is about to be applied. See the example application of fst for an example.`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 preceding 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`

.`p x y z`

: Invoke the procedure`p`

with the arguments`x`

,`y`

and`z`

. The number of arguments supplied must correspond to the number of arguments the procedure takes.`forall ls p`

: Invoke procedure`p`

for each element in the list`ls`

.`p`

should be defined to take exactly one argument whose type is equal to an element of the list`ls`

.`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 QA of the message that invoked the transition. The amount is automatically added to the`_balance`

field of the contract. If a message contains QA, but the invoked transition does not accept the money, the money is transferred back to the sender of the message. Not accepting the incoming amount (when it is non-zero) is not an error.`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 QA 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.

Note

To make it possible to transfer funds from a contract to both contracts and
user accounts, use a standard transition name as per ZRC-5, i.e.
`AddFunds`

. Please make sure to check if a contract to which you intend to
send funds is implemented in adherence with ZRC-5 convention.

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.

Here’s an example that sends multiple messages.

msg1 = { _tag : "setFoo"; _recipient : contractAddress1; _amount : Uint128 0; foo : Uint32 101 }; msg2 = { _tag : "setBar"; _recipient : contractAddress2; _amount : Uint128 0; bar : Uint32 100 }; msgs = let nil = Nil {Message} in let m1 = Cons {Message} msg1 nil in Cons msg2 m1 ; send msgs

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 (including during the execution of the procedures it invokes), 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 (including during the execution of the procedures it invokes), but the event will not be visible on the blockchain before the transition has completed.

### Run-time Errors¶

A contract can raise errors by throwing exceptions. Any error in the execution of a transition (including those due to thrown exceptions, out-of-gas errors and others such as integer overflows) results in the blockchain aborting the execution of the contract as well as aborting any other contracts that were executed before in that chain.

The syntax for raising errors is similar to that of events and messages.

```
e = { _exception : "InvalidInput"; <entry>_2; <entry>_3 };
throw e
```

Unlike that for `event`

or `send`

, The argument to `throw`

is optional
and can be omitted. An empty throw will result in an error that just conveys
the location of where the `throw`

happened without more information.

Note

We do not currently support catching exceptions and may add this in the future.

### Gas consumption in Scilla¶

Deploying contracts and executing transitions in them cost gas. The detailed cost mechanism is explained here.

The Nucleus Wallet page can be used to estimate gas costs for some transactions .

## 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. Exceptions are `pow`

whose second argument is always
`Uint32`

and `isqrt`

which takes in a single `UintX`

argument.

`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 isqrt i`

: Computes the integer square root of`i`

, i.e. the largest integer`j`

such that`j * j <= i`

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

.`builtin to_nat i1`

: Convert a value of type`Uint32`

to the equivalent value of type`Nat`

.`builtin to_(u)int32/64/128/256`

: Convert a`UintX`

/`IntX`

or a`String`

(that represents a decimal number) value to the result of`Option UintX`

or`Option IntX`

type. Returns`Some res`

if the conversion succeeded and`None`

otherwise. The conversion may fail when- there is not enough bits to represent the result;
- when converting a negative integer (or a string representing a negative integer) into a value of an unsigned type;
- the input string cannot be parsed as an integer.

Here is the list of concrete conversion builtins for better discoverability:

`to_int32`

,`to_int64`

,`to_int128`

,`to_int256`

,`to_uint32`

,`to_uint64`

,`to_uint128`

,`to_uint256`

.

Addition, subtraction, multiplication, pow, division and remainder operations may raise integer overflow, underflow and division_by_zero errors. This aborts the execution of the current transition and unrolls all the state changes made so far.

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`

.`s1`

and`s2`

must be of type`String`

.`builtin concat s1 s2`

: Concatenate string`s1`

with string`s2`

. Returns a`String`

.`builtin substr s idx len`

: Extract the substring of`s`

of length`len`

starting from position`idx`

.`idx`

and`len`

must be of type`Uint32`

. Character indices in strings start from`0`

. Returns a`String`

or fails with a runtime error if the combination of the input parameters results in an invalid substring.`builtin to_string x`

: Convert`x`

to a string literal. Valid types of`x`

are`IntX`

,`UintX`

,`ByStrX`

and`ByStr`

. Returns a`String`

. Byte strings are converted to textual hexadecimal representation.`builtin strlen s`

: Calculate the length of`s`

(of type`String`

). Returns a`Uint32`

.`builtin strrev s`

: Returns the reverse of the string`s`

.`builtin to_ascii h`

: Reinterprets a byte string (`ByStr`

or`ByStrX`

) as a printable ASCII string and returns an equivalent`String`

value. If the byte string contains any non-printable characters, a runtime error is raised.

### 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 and other cryptographic primitives,
including byte sequences. In the description
below, `Any`

can be of type `IntX`

, `UintX`

, `String`

, `ByStr20`

or
`ByStr32`

.

`builtin eq h1 h2`

: Is`h1`

equal to`h2`

? Both inputs are of the same type`ByStrX`

(or both are of type`ByStr`

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

.`builtin to_bystr h`

: Convert a value`h`

of type`ByStrX`

(for some known`X`

) to one of arbitrary length of type`ByStr`

.`builtin substr h idx len`

: Extract the sub-byte-string of`h`

of length`len`

starting from position`idx`

.`idx`

and`len`

must be of type`Uint32`

. Character indices in byte strings start from`0`

. Returns a`ByStr`

or fails with a runtime error.`builtin strrev h`

: Reverse byte string (either`ByStr`

or`ByStrX`

). Returns a value of the same type as the argument.`builtin to_bystrX h`

: (note that`X`

is a numerical paratemeter here and not a part of the builtin name, see the examples below)- if the argument
`h`

is of type`ByStr`

: Convert an arbitrary size byte string value`h`

(of type`ByStr`

) to a fixed sized byte string of type`ByStrX`

, with length`X`

. The result is of type`Option ByStrX`

in this case: the builtin returns`Some res`

if the length of the argument is equal to`X`

and`None`

otherwise. E.g.`builtin to_bystr42 bs`

returns`Some bs'`

if the length of`bs`

is 42. - if the argument
`h`

is of type`Uint(32/64/128/256)`

: Convert unsigned integers to their big endian byte representation, returning a`ByStr(4/8/16/32)`

value (notice it’s not an optional type in this case). For instance,`builtin to_bystr4 x`

(this only typechecks if`x`

has type`Uint32`

) or`builtin to_bystr16 x`

(this only typechecks if`x`

is of type`Uint128`

).

- if the argument
`builtin to_uint(32/64/128/256) h`

: Convert a fixed sized byte string value`h`

to an equivalent value of type`Uint(32/64/128/256)`

.`h`

must be of type`ByStrX`

for some known`X`

less than or equal to (4/8/16/32). A big-endian representation is assumed.`builtin schnorr_verify pubk data sig`

: Verify a signature`sig`

of type`ByStr64`

against a byte string`data`

of type`ByStr`

with the Schnorr public key`pubk`

of type`ByStr33`

.`builtin ecdsa_verify pubk data sig`

: Verify a signature`sig`

of type`ByStr64`

against a byte string`data`

of type`ByStr`

with the ECDSA public key`pubk`

of type`ByStr33`

.`builtin ecdsa_recover_pk data sig recid`

: Recover`data`

(of type`ByStr`

), having signature`sig`

(of type`ByStr64`

) and a`Uint32`

recovery integer`recid`

, whose value is restricted to be 0, 1, 2 or 3, the uncompressed public key, returning a`ByStr65`

value.`builtin concat h1 h2`

: Concatenate byte strings`h1`

and`h2`

.- If
`h1`

has type`ByStrX`

and`h2`

has type`ByStrY`

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

. - If the arguments are of type
`ByStr`

, the result is also of type`ByStr`

.

- If
`builtin strlen h`

: The length of byte string (`ByStr`

)`h`

. Returns`Uint32`

.`builtin bech32_to_bystr20 prefix addr`

. The builtin takes a network specific prefix (`"zil"`

/`"tzil"`

) of type`String`

and an input bech32 string (of type`String`

) and if the inputs are valid, converts it to a raw byte address (ByStr20). The return type is`Option ByStr20`

. On success,`Some addr`

is returned and on invalid inputs`None`

is returned.`builtin bystr20_to_bech32 prefix addr`

. The builtin takes a network specific prefix (`"zil"`

/`"tzil"`

) of type`String`

and an input`ByStr20`

address, and if the inputs are valid, converts it to a bech32 address. The return type is`Option String`

. On success,`Some addr`

is returned and on invalid inputs`None`

is returned.`builtin alt_bn128_G1_add p1 p2`

. The builtin takes two points`p1`

,`p2`

on the`alt_bn128`

curve and returns the sum of the points in the underlying group G1. The input points and the result point are each a`Pair {Bystr32 ByStr32}`

. Each scalar component`ByStr32`

of a point is a big-endian encoded number. Also see https://github.com/ethereum/EIPs/blob/master/EIPS/eip-196.md`builtin alt_bn128_G1_mul p s`

. The builtin takes a point`p`

on the`alt_bn128`

curve (as described previously), and a scalar`ByStr32`

value`s`

and returns the sum of the point`p`

taken`s`

times. The result is a point on the curve.`builtin alt_bn128_pairing_product pairs`

. This builtin takes in a list of pairs`pairs`

of points. Each pair consists of a point in group G1 (`Pair {Bystr32 ByStr32}`

) as the first component and a point in group G2 (`Pair {Bystr64 ByStr64}`

) as the second component. Hence the argument has type`List {(Pair (Pair ByStr32 ByStr32) (Pair ByStr64 ByStr64)) }`

. The function applies a pairing function on each point to check for equality and returns`True`

or`False`

depending on whether the pairing check succeeds or fails. Also see https://github.com/ethereum/EIPs/blob/master/EIPS/eip-197.md

### 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 (in some other programming
languages datatypes like Scilla’s `Map`

are called associative arrays, symbol
tables, or dictionaries). The type of map keys `kt`

may be any one of the
following *primitive* types: `String`

, `IntX`

, `UintX`

, `ByStrX`

,
`ByStr`

or `BNum`

. The type of values `vt`

may be any type except a
function type, this includes both builtin and user-defined algebraic datatypes.

Since compound types are not supported as map key types, the way to model, e.g.
association of pairs of values to another value is by using *nested* maps. For
instance, if one wants to associate with an account and a particular trusted
user some money limit the trusted user is allowed to spend on behalf of the
account, one can use the following nested map:

```
field operators: Map ByStr20 (Map ByStr20 Uint128)
= Emp ByStr20 (Map ByStr20 Unit)
```

The first and the second key are of type `ByStr20`

and represent accounts and
the trusted users correspondingly. We represent the money limits with the
`Uint128`

type.

Scilla supports a number of operations on map, which can be categorized as

*in-place*operations which modify*field*maps without making any copies, hence they belong to the imperative fragment of Scilla. These operations are efficient and recommended to use in almost all of the cases;*functional*map operations are intended to use in pure functions, e.g. when designing a Scilla library, because they never modify the original map they are called on. These operations may incur significant performance overhead as some of them create a new (modified) copy of the input map. Syntactically, the copying operations are all prefixed with`builtin`

keyword (see below). Note that to call the functional builtins on a field map one first needs to make a*copy*of the field map using a command like so:`map_copy <- field_map`

, which results in gas consumption proportional to the size of`field_map`

.

#### In-place map operations¶

`m[k] := v`

:*In-place*insert operation. It inserts a key`k`

bound to a value`v`

into a map`m`

. If`m`

already contains key`k`

, the old value bound to`k`

gets replaced by`v`

in the map.`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.`v <- m[k]`

:*In-place*fetch operation. It fetches the value associated with the key`k`

in the map`m`

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

.`b <- exists m[k]`

:*In-place*key existence check. If the key`k`

is associated with a value in the map`m`

then the result value`b`

(of type`Bool`

) will be`True`

; returns`b`

equals to`False`

otherwise.`m`

must refer to a contract field. 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`

.`delete m[k]`

:*In-place*remove operation. The operation removes a key`k`

and its associated value from the map`m`

. The identifier`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.

#### Functional map operations¶

`builtin put m k v`

: Insert a key`k`

bound to a value`v`

into a map`m`

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

but with`k`

associated with`v`

. If`m`

already contains key`k`

, the old value bound to`k`

gets replaced by`v`

in the result map. 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.`builtin 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.`builtin 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.`builtin 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. If`m`

does not contain key`k`

the`remove`

function simply returns a copy of`m`

with no indication that`k`

is missing. The`remove`

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

makes a copy of`m`

before removing the key-value pair.`builtin 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).`builtin size m`

: Return the number of bindings in map`m`

. The result type is`Uint32`

. Calling this builtin consumes a small*constant*amount of gas. But calling it directly on a*field*map is not supported, meaning that getting the size of field maps while avoiding expensive copying needs some more scaffolding, which you can find out about in Field map size section.

Note

Builtin functions `put`

and `remove`

return a new map, which is
a possibly modified copy of the original map. This may affect performance!

Note

Empty maps can be constructed using the `Emp`

keyword, specifying the key
and value types as its arguments. This is the way to initialise `Map`

fields to be empty. For example `field foomap : Map Uint128 String = Emp Uint128 String`

declares a `Map`

field with keys of type `Uint128`

and values of type
`String`

, which is initialized to be the empty map.

### 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 three 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 thought 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`

.`list_foldk: ('B -> 'A -> ('B -> 'B) -> 'B) -> 'B -> (List 'A) -> 'B`

: Recursively process the elements in a list according to a*folding function*, while keeping track of an*accumulator*.`list_foldk`

is a more general version of the left and right folds, which, by the way, can be both implemented in terms of it.`list_foldk`

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

and`'B`

:- The function describing the fold step. This function takes three
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 third argument represents the postponed recursive call (of type`'B -> 'B`

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

). The computation*terminates*if the programmer does not invoke the postponed recursive call. This is a major difference between`list_foldk`

and the left and right folds which process their input lists from the beginning to the end unconditionally. - The initial value of the accumulator
`z`

(of type`'B`

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

).

- The function describing the fold step. This function takes three
arguments. The first argument is the current value of the
accumulator (of type

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. For an example of `list_foldk`

see list_find.

1 2 3 4 5 6 7 8 9 10 11 12 | ```
let list_length : forall 'A. List 'A -> Uint32 =
tfun 'A =>
fun (l : List 'A) =>
let foldl = @list_foldl 'A Uint32 in
let init = Uint32 0 in
let one = Uint32 1 in
let iter =
fun (z : Uint32) =>
fun (h : 'A) =>
builtin add one z
in
foldl 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 variable 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
```

To apply `fst`

to one must first instantiate the type variables
`'A`

and `'B`

, which is done as follows:

```
p <- pp;
fst_specialised = @fst String Uint32;
p_fst = fst_specialised p
```

The value associated with the identifier `p_fst`

will be the string
`"Hello"`

.

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 two structural recursion primitives 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`

). Incidentally, the next number to be processed is the predecessor of the current number being processed. 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
`nat_foldk: ('A -> Nat -> ('A -> 'A) -> 'A) -> 'A -> Nat -> 'A`

: Recursively process the Peano numbers down to zero according to a*folding function*, while keeping track of an*accumulator*.`nat_foldk`

is a more general version of the left fold allowing for early termination. It takes three arguments, two depending on the type variable`'A`

.- The function describing the fold step. This function takes three
arguments. The first argument is the current value of the
accumulator (of type
`'A`

). The second argument is the predecessor of the Peano number being processed (of type`Nat`

). The third argument represents the postponed recursive call (of type`'A -> 'A`

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

). The computation*terminates*if the programmer does not invoke the postponed recursive call. Left folds inevitably process the whole list whereas`nat_foldk`

can differ in this regard. - The initial value of the accumulator
`z`

(of type`'A`

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

).

- The function describing the fold step. This function takes three
arguments. The first argument is the current value of the
accumulator (of type

To better understand `nat_foldk`

, we explain how `nat_eq`

works.
`nat_eq`

checks to see if two Peano numbers are equivalent. Below
is the program, with line numbers and an explanation.

1 2 3 4 5 6 7 8 9 10 11 12 13 14 | ```
let nat_eq : Nat -> Nat -> Bool =
fun (n : Nat) => fun (m : Nat) =>
let foldk = @nat_foldk Nat in
let iter =
fun (n : Nat) => fun (ignore : Nat) => fun (recurse : Nat -> Nat) =>
match n with
| Succ n_pred => recurse n_pred
| Zero => m (* m is not zero in this context *)
end in
let remaining = foldk iter n m in
match remaining with
| Zero => True
| _ => False
end
``` |

Line 2 specifies that we take two Peano numbers `m`

and `n`

.
Line 3 instantiates the type of `nat_foldk`

, we give it `Nat`

because we will be passing a `Nat`

value as the fold accumulator.

Lines 4 to 8 specify the fold description, this is the first argument
that `nat_foldk`

takes usually of type `'A -> Nat -> ('A -> 'A) -> 'A`

but we have specified that `'A`

is `Nat`

in this case. Our function
takes the accumulator `n`

and `ignore : Nat`

is the predecessor of
the number being processed which we don’t care about in this particular case.

Essentially, we start accumulating the end result from `n`

and iterate
at most `m`

times (see line 10), decrementing both `n`

and `m`

at each recursive step (lines 4 - 9).
The `m`

variable gets decremented implicitly because this is how `nat_foldk`

works under the hood.
And we explicitly decrement `n`

using pattern matching (lines 6, 7).
To continue iteratively decrement both `m`

and `n`

we use `recurse`

on line 7.
If the two input numbers are equal, we will get the accumulator (`n`

) equal to
zero in the end.
We call the final value of the accumulator `remaining`

on line 10.
At the end we will be checking to see if our accumulator
ended up at `Zero`

to say if the input numbers are equal.
The last lines, return `True`

when the result of the fold is `Zero`

and `False`

otherwise as described above.

In the case when accumulator `n`

reaches zero (line 8) while `m`

still has not been fully processed, we stop iteration
(hence no `recurse`

on that line) and return a non-zero natural number
to indicate inequality.
Any number (e.g. `Succ Zero`

) would do, but to make the code concise
we return the original input number `m`

because we know `iter`

gets called on `m`

only if it’s not zero.

In the symmetrical case when `m`

reaches zero while the accumulator `n`

is still strictly positive, we indicate inequality, because `remaining`

gets this final value of `n`

.

### 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 definition 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. Both the ADT and constructor names must begin with a capital letter
(‘A’ - ‘Z’). 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 game. 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
```

### Type identity for user-defined ADTs¶

Note

Due to a bug in the Scilla implementation the information in this section is only valid from Scilla version 0.10.0 and forwards. Contracts written in Scilla versions prior to 0.10.0 and which exploit this bug will have to be rewritten and redeployed, as they will no longer work from version 0.10.0 and onwards.

Each type declaration defines a unique type. In particular this means that even if two libraries both define identical types, the types are considered different.

As an example, consider the following two contracts:

```
library C1Lib
type T =
| C1 of Uint32
| C2 of Bool
contract Contract1()
field contract2_address : ByStr20 = 0x1234567890123456789012345678901234567890
transition Sending ()
c2 <- contract2_address;
x = Uint32 0;
out = C1 x;
msg = { _tag : "Receiving" ; _recipient : c2 ; _amount : Uint128 0 ;
param : out };
no_msg = Nil {Message};
msgs = Cons {Message} msg no_msg;
send msgs
end
(* ******************************* *)
(* Contract2 is deployed at address 0x1234567890123456789012345678901234567890 *)
library C2Lib
type T =
| C1 of Uint32
| C2 of Bool
contract Contract2()
transition Receiving (param : T)
match param with
| C1 v =>
| C2 b =>
end
end
```

Even though both contracts define identical types `T`

, the two types
are considered different in Scilla. In particlar this means that the
message sent from `Contract1`

to `Contract2`

will not trigger the
`Receiving`

transition, because the value sent as the `param`

message field has the type `T`

from `Contract1`

, whereas the type
`T`

from `Contract2`

is expected.

In order to pass a value of a user-defined ADT as a parameter to a transition, the type must be defined in a user-defined library, which both the sending and the receiving contract must import:

```
library MutualLib
type T =
| C1 of Uint32
| C2 of Bool
(* ******************************* *)
import MutualLib
library C1Lib
contract Contract1()
field contract2_address : ByStr20 = 0x1234567890123456789012345678901234567890
transition Sending ()
c2 <- contract2_address;
x = Uint32 0;
out = C1 x;
msg = { _tag : "Receiving" ; _recipient : c2 ; _amount : Uint128 0 ;
param : out };
no_msg = Nil {Message};
msgs = Cons {Message} msg no_msg;
send msgs
end
(* ******************************* *)
(* Contract2 is deployed at address 0x1234567890123456789012345678901234567890 *)
scilla_version 0
import MutualLib
library C2Lib
contract Contract2()
transition Receiving (param : T)
match param with
| C1 v =>
| C2 b =>
end
end
```

The section User-defined Libraries has more information on how to define and use libraries.

## More ADT examples¶

To further illustrate how ADTs can be used, we provide some more
examples and describe them in detail. Versions of 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.

### Computing a Left Fold¶

The function `list_foldl`

returns the result of a left fold given a function
`f : 'B -> 'A -> 'B`

, accumulator `z : 'B`

and list `xs : List 'A`

.
This can be implemented as a recursion primitive or a list utility function.

A left fold is a recursive application of an accumulator `z`

and next
list element `x : 'A`

with `f`

repetitively until there are no more list
elements. For example the left fold on `[1,2,3]`

using subtraction starting with
accumulator 0 would be `((0-1)-2)-3 = -6`

. The left fold is explained in
pseudocode below, note that the result is always the accumulator type.

1 2 | ```
list_foldl _ z [] = z
list_foldl f z (x:xs) = list_foldl f (f z x) xs
``` |

The same can be achieved with `list_foldk`

by partially applying a left fold
description; this avoids illegal direct recursion. Our fold description
`left_f : 'B -> 'A -> ('B -> 'B) -> 'B`

takes arguments accumulator,
next list element and recursive call. The recursive call will be supplied
by the `list_foldk`

function. An implementation is explained below.

1 2 3 4 5 6 7 8 | ```
let list_foldl : forall 'A. forall 'B. ( 'B -> 'A -> 'B) -> 'B -> List 'A -> 'B =
tfun 'A => tfun 'B =>
fun (f : 'B -> 'A -> 'B) =>
let left_f = fun (z: 'B) => fun (x: 'A) =>
fun (recurse : 'B -> 'B) => let res = f z x in
recurse res in
let folder = @list_foldk 'A 'B in
folder left_f
``` |

On line 1, we declare the name and type signature as according to the first
paragraph. On the second line, we say that the function takes two types as arguments
`'A`

and `'B`

. The third line says that we take some function `f`

to process the list element
and accumulator, as in paragraph two.

On line 4, we define the fold description using `f`

. The fold description does not
take a function but instead it should be implemented in terms of some function, as
according to the type signature, `left_f : 'B -> 'A -> ('B -> 'B) -> 'B`

.
`left_f`

takes arguments as described in paragraph two. We calculate the new
accumulator `f z x`

and call it `res`

. Then we recursively call with the new
accumulator.

On line 7, we instantiate an instance of `list_foldk`

that has the right types
for the job using a type application.

On line 8, we partially apply `folder`

with the left fold description.
. What is significant about `list_foldk`

is that when calling the description,
it provides a recursive call to itself, changing to the next element
in the list and respective tail each time. This results in a function that
just needs the user to provide the updated accumulator in the description.

### Computing a Right Fold¶

The function `list_foldr`

returns the result of a right fold given some
function `f : 'A -> 'B -> 'B`

, accumulator `z : 'B`

and
list `xs : List 'A`

. Like `list_foldl`

, this can be a recursion primitive
or a list utility function.

A right fold is similar to a left fold but is reversed in a way.
The right fold applies a function `f`

with an accumulator `z`

starting from
the end and then combines with the second last element, third last element,
etc… until it reaches the beginning. For example a right fold on
the list `[1,2,3]`

with subtraction starting with accumulator 0 would
be equal to `1-(2-(3-0)) = 2`

. It is listed below in pseudocode,
note that the result is always the accumulator type.

1 2 | ```
list_foldr _ z [] = z
list_foldr f z (x:xs) = f x (list_foldr f z xs)
``` |

Like before, the same can be achieved with `list_foldk`

by partially
applying a right fold description. The fold description takes arguments
accumulator `z : 'B`

, next list element `x : 'A`

and recursive call
`recurse : 'B -> 'B`

. The recursive call will be supplied by the
`list_foldk`

function. An implementation is explained below.

1 2 3 4 5 6 7 | ```
let list_foldr : forall 'A. forall 'B. ('A -> 'B -> 'B) -> 'B -> List 'A -> 'B =
tfun 'A => tfun 'B =>
fun (f : 'A -> 'B -> 'B) =>
let right_f = fun (z: 'B) => fun (x: 'A) =>
fun (recurse : 'B -> 'B) => let res = recurse z in f x res in
let folder = @list_foldk 'A 'B in
folder right_f
``` |

This is very similar to before. On line 1 we declare the name and type
signature, according to the first paragraph. On line 2, we take two
type arguments `'A`

and `'B`

. The third line says that we take some
function `f`

to process the list element `x : 'A`

and accumulator `z`

.
The argument order is necessarily different to that of a left fold.

Following that we write a fold description like before.
`list_foldk`

processes lists from left to right.
But we need `list_foldr`

to emulate the right-to-left traversal.
By calling `recurse z`

on line 5 as our first action, we postpone actual computation
with the combining function `f`

preserving the original accumulator until the very end.
Once the recursive call reaches an empty list it returns the original accumulator.
Then the function calls `f x res`

(line 5) will evaluate outwards combining
from the end to the beginning, see paragraph two.

The recursive call `recurse z`

on line 5 may seem to be the same each time but what is changing
is the list element we process.

On line 6, we instantiate `list_foldk`

by applying the types `'A`

and `'B`

to make
a type-specific function. The last line we partially apply `folder`

with the
right fold description. Like before what is special about `list_foldk`

is that it calls
this function with a recursive call to itself that each time slightly truncates the list;
this provides the recursion.

### 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 accumulator type `Bool`

. In
line 6 we set the initial accumulator 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
accumulator. If an element has been found which satisfies the
predicate, the accumulator 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.

### Finding the first occurrence satisfying a predicate¶

The function `list_find`

searches for the first occurrence in a
list that satisfies some predicate `p : 'A -> Bool`

. It takes
the predicate and the list, returning `Some {'A} x :: Option 'A`

if
`x`

is the first element such that `p x`

and `None {'A} :: Option 'A`

otherwise.

Below we have an implementation of `list_find`

that illustrates
how to use `list_foldk`

.

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 | ```
let list_find : forall 'A. ('A -> Bool) -> List 'A -> Option 'A =
tfun 'A =>
fun (p : 'A -> Bool) =>
let foldk = @list_foldk 'A (Option 'A) in
let init = None {'A} in
(* continue fold on None, exit fold when Some compare st. p(compare) *)
let predicate_step =
fun (ignore : Option 'A) => fun (x : 'A) =>
fun (recurse: Option 'A -> Option 'A) =>
let p_x = p x in
match p_x with
| True => Some {'A} x
| False => recurse init
end in
foldk predicate_step init
``` |

Like before, we take a type variable `'A`

on line 2 and take the predicate
on the next line. We begin by using this type variable to instantiate `foldk`

,
by giving it our processing type and return type. The processing type being
the list element type and the result type being `Option 'A`

. The next line
is our accumulator, we assume that at the start of the search there is no
satisfier.

On line 7, we write a fold description for `foldk`

. This embodies the order of
the recursion and conditions for recursion. `predicate_step`

has the
type `Option 'A -> 'A -> (Option 'A -> Option 'A) -> Option 'A`

.
The first argument is the accumulator, the second `x`

is the next element to
process and the third `recurse`

is the recursive call. We do not care what
the accumulator `ignore`

is since if it mattered we will have already
terminated.

On lines 10 to 12 check for `p x`

and if so return `Some {'A} x`

. In the case
that `p x`

does not hold, try again from scratch with the next element and
so on via recursion. `recurse init`

is in pseudo-code equal to
`λk. foldk predicate_step init k xs`

where `xs`

is the tail of our list of
to be processed elements.

With the final line we partially apply `foldk`

so that it just takes a list
argument and gives us our final answer. The first argument of `foldk`

gives
us the specific fold we want, for example if you wanted a left fold you
would replace `predicate_step`

with something else.

## 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 and procedures 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.

```
let int_list_eq = @list_eq Int64 in
let one = Int64 1 in
let two = Int64 2 in
let ten = Int64 10 in
let eleven = Int64 11 in
let nil = Nil {Int64} in
let l1 = Cons {Int64} eleven nil in
let l2 = Cons {Int64} ten l1 in
let l3 = Cons {Int64} two l2 in
let l4 = Cons {Int64} one l3 in
let f = int64_eq in
(* See if [2,10,11] = [1,2,10,11] *)
int_list_eq f l3 l4
```

`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_foldl_while : ('B -> 'A -> Option 'B) -> 'B -> List 'A -> 'B`

Given a function`f : 'B -> 'A -> Option 'B`

, accumulator`z : 'B`

and list`ls : List 'A`

execute a left fold when our given function returns`Some x : Option 'B`

using`f z x : 'B`

or list is empty but in the case of`None : Option 'B`

terminate early, returning`z`

.

```
(* assume zero = 0, one = 1, negb is in scope and ls = [10,12,9,7]
given a max and list with elements a_0, a_1, ..., a_m
find largest n s.t. sum of i from 0 to (n-1) a_i <= max *)
let prefix_step = fun (len_limit : Pair Uint32 Uint32) => fun (x : Uint32) =>
match len_limit with
| Pair len limit => let limit_lt_x = builtin lt limit x in
let x_leq_limit = negb limit_lt_x in
match x_leq_limit with
| True => let len_succ = builtin add len one in let l_sub_x = builtin sub limit x in
let res = Pair {Uint32 Uint32} len_succ l_sub_x in
Some {(Pair Uint32 Uint32)} res
| False => None {(Pair Uint32 Uint32)}
end
end in
let fold_while = @list_foldl_while Uint32 (Pair Uint32 Uint32) in
let max = Uint32 31 in
let init = Pair {Uint32 Uint32} zero max in
let prefix_length = fold_while prefix_step init ls in
match prefix_length with
| Pair length _ => length
end
```

`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 -> Uint32`

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`

.`nat_fold_while : ('T -> Nat -> Option 'T) -> 'T -> Nat -> 'T`

: Takes arguments`f : 'T -> Nat -> Option 'T`

,`z : `T`

and`m : Nat`

. This is`nat_fold`

with early termination. Continues recursing so long as`f`

returns`Some y`

with new accumulator`y`

. Once`f`

returns`None`

, the recursion terminates.`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.

```
let fst_strings = @fst String String in
let nick_name = "toby" in
let dog = "dog" in
let tobias = Pair {String String} nick_name dog in
fst_strings tobias
```

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

: Extract the second element of a Pair.

## User-defined Libraries¶

In addition to the standard library provided by Scilla, users are allowed
to deploy library code on the blockchain. Library files are allowed to only
contain pure Scilla code (which is the same restriction that in-contract
library code has). Library files must use the `.scillib`

file extension.

Below is an example of a user-defined library that defines a single function
`add_if_equal`

that adds to `Uint128`

values if they are equal and returns
`0`

otherwise.

```
import IntUtils
library ExampleLib
let add_if_equal =
fun (a : Uint128) => fun (b : Uint128) =>
let eq = uint128_eq a b in
match eq with
| True => builtin add a b
| False => Uint128 0
```

The structure of a library file is similar to the structure of the library part of a Scilla contract. A library file contains definitions of variables and pure library functions, but does not contain an actual contract definition with parameters, fields, transitions and so on.

Of particular importance is that a library cannot declare fields. Therefore, all libraries are stateless and can only contain pure code.

Similar to how contracts can import libraries, a library can import other libraries
(including user-defined libraries) too. The scope of variables in an imported library
is restricted to the immediate importer. So if `X`

imports library `Y`

which in
turn imports library `Z`

, then the names in `Z`

are not in scope in X`, but only
in `Y`

. Cyclic dependencies in imports are not allowed and flagged as errors
during the checking phase.

### Local Development with User-defined Libraries¶

To use variables and functions declared in an external (user-defined) library module,
the command line argument to the Scilla executables must include a `-libdir`

option,
along with a list of directories as an argument. If the Scilla file imports a library `ALib`

,
then the Scilla executable will search for a library file called `ALib.scillib`

in the directories provided. If more than one directory contains a file with the correct name,
then the directories are given priority in the same order as they are provided to the Scilla executable.
Alternatively, the environment variable `SCILLA_STDLIB_PATH`

can be set to a list of library directories.

`scilla-checker`

typechecks library modules in the same way as contract modules. Similarly,
`scilla-runner`

can deploy libraries. Note that `scilla-runner`

takes a `blockhain.json`

as
argument (the way it does for Contract Creation) to be command
line argument compatible with contract creation.

### User-defined Libraries on the Blockchain¶

While the Zilliqa blockchain is designed to provide the standard Scilla libraries to an executing contract, it must be provided with extra information to support user-defined libraries.

The `init.json`

of a library must include a `Bool`

entry named `_library`

, set to
`True`

. Additionally,
A contract or a library that imports user-defined libraries must include in its init.json
an entry named `_extlibs`

, of Scilla type `List (Pair String ByStr20)`

. Each entry in
the list maps an imported library’s name to its address in the blockchain.

Continuing the previous example, a contract or library that imports `Examplelib`

should have
the following entry in its `init.json`

:

```
[
...,
{
"vname" : "_library",
"type" : "Bool",
"value": { "constructor": "True", "argtypes": [], "arguments": [] }
}
{
"vname" : "_extlibs",
"type" : "List(Pair String ByStr20)",
"value" : [
{
"constructor" : "Pair",
"argtypes" : ["String", "ByStr20"],
"arguments" : ["ExampleLib", "0x986556789012345678901234567890123456abcd"]
},
...
]
}
]
```

### Namespaces¶

Import statements can be used to define separate namespaces for imported names.
To push the names from a library `Foo`

into the namespace `Bar`

, use the statement
`import Foo as Bar`

. Accessing a variable `v`

in Foo must now be done using the qualified
name `Bar.v`

. This is useful when importing multiple libraries that define the same name.

The same variable name must not be defined more than once in the same namespace, so if multiple imported libraries define the same name, then at most one of the libraries may reside in the default (unqualified) namespace. All other conflicting libraries must be pushed to separate namespaces.

Extending our previous example, shown below is a contract that imports `ExampleLib`

in namespace `Bar`

, to use the function `add_if_equal`

.

```
scilla_version 0
import ExampleLib as Bar
library MyContract
let adder = fun (a : Uint128) => fun (b : Uint128) =>
Bar.add_if_equal a b
contract MyContract ()
...
```

## 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 contract’s
transitions are invoked. This eases the process for the blockchain
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¶

In a sequence of contract calls (i.e, a contract transition execution resulting in the execution of one or more similar transition executions (of the same or other contracts), any kind of failure at one point will result in the entire set of executions to be discarded (except for the gas already consumed).

The total number of executions that can happen in a single chain call
sequence (starting from first execution that was triggered from a non-contract
account) is currently set at `10`

edges which includes both breadth and depth.
The number may be subjected to revision in the future.

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.