Scilla by Example¶
HelloWorld¶
We start off by writing a classical HelloWorld.scilla
contract with the
following specification:
- It should have an immutable contract parameter
owner
to be initialized by the creator of the contract. The parameter is immutable in the sense that once initialized during contract deployment, its value cannot be changed.owner
will be of typeByStr20
(a hexadecimal Byte String representing a 20 byte address). - It should have a mutable field
welcome_msg
of typeString
initialized to""
. Mutability here refers to the possibility of modifying the value of a variable even after the contract has been deployed. - The
owner
and only her should be able to modifywelcome_msg
through an interfacesetHello
. The interface takes amsg
(of typeString
) as input and allows theowner
to set the value ofwelcome_msg
tomsg
. - It should have an interface
getHello
that welcomes any caller withwelcome_msg
.getHello
will not take any input.
Defining a Contract, its Immutable Parameters and Mutable Fields¶
A contract is declared using the contract
keyword that starts the scope of
the contract. The keyword is followed by the name of the contract which will be
HelloWorld
in our example. So, the following code fragment declares a
HelloWorld
contract.
contract HelloWorld
Note
In the current implementation, a Scilla contract can only contain a single
contract declaration and hence any code that follows the contract
keyword is part of the contract declaration. In other words, there is no
explicit keyword to declare the end of the contract definition.
A contract declaration is followed by the declaration of its immutable
parameters, the scope of which is defined by ()
. Each immutable parameter is
declared in the following way: vname: vtype
, where vname
is the
parameter name and vtype
is the parameter type. Immutable parameters are
separated by ,
. As per the specification, the contract will have only one
immutable parameter owner
of type ByStr20
and hence the following code
fragment.
(owner: ByStr20)
Mutable fields in a contract are declared through keyword field
. Each
mutable field is declared in the following way: field vname : vtype =
init_val
, where vname
is the field name, vtype
is its type and
init_val
is the value to which the field has to be initialized. The
HelloWorld
contract has one mutable field welcome_msg
of type String
initialized to ""
. This yields the following code fragment:
field welcome_msg : String = ""
At this stage, our HelloWorld.scilla
contract will have the following form
that includes the contract name, its immutable parameters and mutable fields:
contract HelloWorld
(owner: ByStr20)
field welcome_msg : String = ""
Defining Interfaces aka Transitions¶
Interfaces like setHello
are referred to as transitions in Scilla.
Transitions are similar to functions or methods in other languages. There is
an important difference, however, most languages allow their functions or
methods to be “interrupted” by a thread running in parallel, but Scilla won’t
let a transition to be interrupted ensuring there is no so-called reentrancy
issues.
Note
The term transition comes from the underlying computation model in Scilla which follows a communicating automaton. A contract in Scilla is an automaton with some state. The state of an automaton can be changed using a transition that takes a previous state and an input and yields a new state. Check the wikipedia entry to read more about transition systems.
A transition is declared using the keyword transition
. The end of a
transition scope is declared using the keyword end
. The transition
keyword is followed by the transition name, which is setHello
for our
example. Then follows the input parameters within ()
. Each input parameter
is separated by a ,
and is declared in the following format: vname :
vtype
. According to the specification, setHello
takes only one parameter
of name msg
of type String
. This yields the following code fragment:
transition setHello (msg : String)
What follows the transition signature is the body of the transition. Code for
the first transition setHello (msg : String)
to set welcome_msg
is
given below:
1 2 3 4 5 6 7 8 9 10 11 12 | transition setHello (msg : String)
is_owner = builtin eq owner _sender;
match is_owner with
| False =>
e = {_eventname : "setHello"; code : not_owner_code};
event e
| True =>
welcome_msg := msg;
e = {_eventname : "setHello"; code : set_hello_code};
event e
end
end
|
At first, the caller of the transition is checked against the owner
using
the instruction builtin eq owner _sender
in Line 2
. In order to compare
two addresses, we are using the function eq
defined as a builtin
operator. The operator returns a Boolean value True
or False
.
Note
Scilla internally defines some variables that have special semantics. These
special variables are often prefixed by _
. For instance, _sender
in
Scilla refers to the account address that called the current contract.
Depending on the output of the comparison, the transition takes a different path declared using pattern matching, the syntax of which is given in the fragment below.
match expr with
| pattern_1 => expr_1
| pattern_2 => expr_2
end
The above code checks whether expr
evaluates to a value that
matches pattern_1
or pattern_2
. If expr
evaluates to a
value matching pattern_1
, then the next expression to be evaluated
will be expr_1
. Otherwise, if expr
evaluates to a value
matching pattern_2
, then the next expression to be evaluated will
be expr_2
.
Hence, the following code block implements an if-then-else
instruction:
match expr with
| True => expr_1
| False => expr_2
end
The Caller is Not the Owner¶
In case the caller is different from owner
, the transition takes
the False
branch and the contract emits an event using the
instruction event
.
An event is a signal that gets stored on the blockchain for everyone to see. If a user uses a client application to invoke a transition on a contract, the client application can listen for events that the contract may emit, and alert the user.
More concretely, the output event in this case is:
e = {_eventname : "setHello"; code : not_owner_code};
An event is comprised of a number of vname : value
pairs delimited
by ;
inside a pair of curly braces {}
. An event must contain
the compulsory field _eventname
, and may contain other fields such
as the code
field in the example above.
Note
In our example we have chosen to name the event after the transition that emits the event, but any name can be chosen. However, it is recommended that you name the events in a way that makes it easy to see which part of the code emitted the event.
The Caller is the Owner¶
In case the caller is owner
, the contract allows the caller to set the
value of the mutable field welcome_msg
to the input parameter msg
.
This is done through the following instruction:
welcome_msg := msg;
Note
Writing to a mutable field is done using the operator :=
.
And as in the previous case, the contract then emits an event with
the code set_hello_code
.
Libraries¶
A Scilla contract may come with some helper libraries that declare
purely functional components of a contract, i.e., components with no
state manipulation. A library is declared in the preamble of a
contract using the keyword library
followed by the name of the
library. In our current example a library declaration would look as
follows:
library HelloWorld
The library may include utility functions and program constants using
the let ident = expr
construct. In our example the library will
only include the definition of error codes:
let not_owner_code = Uint32 1
let set_hello_code = Uint32 2
At this stage, our contract fragment will have the following form:
library HelloWorld
let not_owner_code = Uint32 1
let set_hello_code = Uint32 2
contract HelloWorld
(owner: ByStr20)
field welcome_msg : String = ""
transition setHello (msg : String)
is_owner = builtin eq owner _sender;
match is_owner with
| False =>
e = {_eventname : "setHello"; code : not_owner_code};
event e
| True =>
welcome_msg := msg;
e = {_eventname : "setHello"; code : set_hello_code};
event e
end
end
Adding Another Transition¶
We may now add the second transition getHello()
that allows client
applications to know what the welcome_msg
is. The declaration is
similar to setHello (msg : String)
except that getHello()
does
not take a parameter.
transition getHello ()
r <- welcome_msg;
e = {_eventname: "getHello"; msg: r};
event e
end
Note
Reading from a mutable field is done using the operator <-
.
In the getHello()
transition, we will first read from a mutable field, and
then we construct and emit the event.
Scilla Version¶
Once a contract has been deployed on the network, it cannot be changed. It is therefore necessary to specify which version of Scilla the contract is written in, so as to ensure that the behaviour of the contract does not change even if changes are made to the Scilla specification.
The Scilla version of the contract is declared using the keyword
scilla_version
:
scilla_version 0
The version declaration must appear before any library or contract code.
Putting it All Together¶
The complete contract that implements the desired specification is
given below, where we have added comments using the (* *)
construct:
(* HelloWorld contract *)
(***************************************************)
(* Scilla version *)
(***************************************************)
scilla_version 0
(***************************************************)
(* Associated library *)
(***************************************************)
library HelloWorld
let not_owner_code = Uint32 1
let set_hello_code = Uint32 2
(***************************************************)
(* The contract definition *)
(***************************************************)
contract HelloWorld
(owner: ByStr20)
field welcome_msg : String = ""
transition setHello (msg : String)
is_owner = builtin eq owner _sender;
match is_owner with
| False =>
e = {_eventname : "setHello"; code : not_owner_code};
event e
| True =>
welcome_msg := msg;
e = {_eventname : "setHello"; code : set_hello_code};
event e
end
end
transition getHello ()
r <- welcome_msg;
e = {_eventname: "getHello"; msg: r};
event e
end
A Second Example: Crowdfunding¶
In this section, we present a slightly more involved contract that runs a crowdfunding campaign. In a crowdfunding campaign, a project owner wishes to raise funds through donations from the community.
It is assumed that the owner (owner
) wishes to run the campaign
until a certain, predetermined block number is reached on the
blockchain (max_block
). The owner also wishes to raise a minimum
amount of QA (goal
) without which the project can not be
started. The contract hence has three immutable parameters owner
,
max_block
and goal
.
The immutable parameters are provided when the contract is deployed. At
that point we wish to add a sanity check that the goal
is a
strictly positive amount. If the contract is accidentally initialised
with a goal
of 0, then the contract should not be deployed.
The total amount that has been donated to the campaign so far is
stored in a field _balance
. Any contract in Scilla has an implicit
_balance
field of type Uint128
, which is initialised to 0 when
the contract is deployed, and which holds the amount of QA in the
contract’s account on the blockchain.
The campaign is deemed successful if the owner can raise the goal in the stipulated time. In case the campaign is unsuccessful, the donations are returned to the project backers who contributed during the campaign. The backers are supposed to ask for refund explicitly.
The contract maintains two mutable fields:
backers
: a field map from a contributor’s address (aByStr20
value) to the amount contributed, represented with aUint128
value. Since there are no backers initially, this map is initialized to anEmp
(empty) map. The map enables the contract to register a donor, prevent multiple donations and to refund back the money if the campaign does not succeed.funded
: a Boolean flag initialized toFalse
that indicates whether the owner has already transferred the funds after the end of the campaign.
The contract contains three transitions: Donate ()
that allows anyone to
contribute to the crowdfunding campaign, GetFunds ()
that allows only the
owner to claim the donated amount and transfer it to owner
and
ClaimBack()
that allows contributors to claim back their donations in case
the campaign is not successful.
Sanity check for contract parameters¶
To ensure that the goal
is a strictly positive amount, we use a
contract constraint:
with
let zero = Uint128 0 in
builtin lt zero goal
=>
The Boolean expression between with
and =>
above is evaluated during
contract deployment and the contract only gets deployed if the result of
evaluation is True
. This ensures that the contract cannot be deployed with a
goal
of 0 by mistake.
Reading the Current Block Number¶
The deadline is given as a block number, so to check whether the deadline has passed, we must compare the deadline against the current block number.
The current block number is read as follows:
blk <- & BLOCKNUMBER;
Block numbers have a dedicated type BNum
in Scilla, so as to not
confuse them with regular unsigned integers.
Note
Reading data from the blockchain is done using the operator
<- &
. Blockchain data cannot be updated directly from the
contract.
Reading and Updating the Current Balance¶
The target for the campaign is specified by the owner in the immutable
parameter goal
when the contract is deployed. To check whether the
target have been met, we must compare the total amount raised to the
target.
The amount of QA raised is stored in the contract’s account on the
blockchain, and can be accessed through the implicitly declared
_balance
field as follows:
bal <- _balance;
Money is represented as values of type Uint128
.
Note
The _balance
field is read using the operator <-
just like any other
contract field. However, the _balance
field can only be updated by
accepting money from incoming messages (using the instruction accept
), or
by explicitly transferring money to other account (using the instruction
send
as explained below).
Sending Messages¶
In Scilla, there are two ways that transitions can transmit data. One
way is through events, as covered in the previous example. The other
is through the sending of messages using the instruction send
.
send
is used to send messages to other accounts, either in order
to invoke transitions on another smart contract, or to transfer money
to user accounts. On the other hand, events are dispatched signals
that smart contracts can use to transmit data to client applications.
To construct a message we use a similar syntax as when constructing events:
msg = {_tag : ""; _recipient : owner; _amount : bal; code : got_funds_code};
A message must contain the compulsory message fields _tag
, _recipient
and _amount
. The _recipient
message field is the blockchain address (of
type ByStr20
) that the message is to be sent to, and the _amount
message
field is the number of QA to be transferred to that account.
The value of the _tag
message field is the name of the transition (of type
String
) that is to be invoked on the contract deployed at _recipient
address. If _recipient
is the address of a user account then the value of
_tag
is ignored, hence for simplicity we put ""
here.
Note
To make it possible to refund both contracts and user accounts (this is
useful if a backer used a wallet contract to donate), use a standard
transition name as per ZRC-5, i.e.
AddFunds
.
In addition to the compulsory fields the message may contain other
fields, such as code
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.
Sending a message is done using the send
instruction, which takes
a list of messages as a parameter. Since we will only ever send one
message at a time in the crowdfunding contract, we define a library
function one_msg
to construct a list consisting of one message:
let one_msg =
fun (msg : Message) =>
let nil_msg = Nil {Message} in
Cons {Message} msg nil_msg
To send out a message, we first construct the message, insert it into a list, and send it:
msg = {_tag : ""; _recipient : owner; _amount : bal; code : got_funds_code};
msgs = one_msg msg;
send msgs
Procedures¶
The transitions of a Scilla contract often need to perform the same small sequence of instructions. In order to prevent code duplication a contract may define a number of procedures, which may be invoked from the contract’s transitions. Procedures also help divide the contract code into separate, self-contained pieces which are easier to read and reason about individually.
A procedure is declared using the keyword procedure
. The end of a
procedure is declared using the keyword end
. The procedure
keyword is followed by the transition name, then the input parameters
within ()
, and then the statements of the procedure.
In our example the Donate
transition will issue an event in three
situations: An error event if the donation happens after the deadline,
another error event if the backer has donated money previously, and a
non-error event indicating a successful donation. Since much of the
event issuing code is identical, we decide to define a procedure
DonationEvent
which is responsible for issuing the correct event:
procedure DonationEvent (failure : Bool, error_code : Int32)
match failure with
| False =>
e = {_eventname : "DonationSuccess"; donor : _sender;
amount : _amount; code : accepted_code};
event e
| True =>
e = {_eventname : "DonationFailure"; donor : _sender;
amount : _amount; code : error_code};
event e
end
end
The procedure takes two arguments: A Bool
indicating whether the
donation failed, and an error code indicating the type of failure if a
failure did indeed occur.
The procedure performs a match
on the failure
argument. If the
donation did not fail, the error code is ignored, and a
DonationSuccess
event is issued. Otherwise, if the donation
failed, then a DonationFailure
event is issued with the error code
that was passed as the second argument to the procedure.
The following code shows how to invoke the DonationEvent
procedure with the arguments True
and 0
:
c = True;
err_code = Int32 0;
DonationEvent c err_code;
Note
The special parameters _sender
, _origin
and _amount
are available to
a procedure even though the procedure is invoked by a transition
rather than by an incoming message. It is not necessary to pass
these special parameters as arguments to the procedure.
Note
Procedures are similar to library functions in that they can be invoked from any transition (as long as the transition is defined after the procedure). However, procedures are different from library functions in that library functions cannot access the contract state, and procedures cannot return a value.
Procedures are similar to transitions in that they can access and change the contract state, as well as read the incoming messages and send outgoing messages. However, procedures cannot be invoked from the blockchain layer. Only transitions may be invoked from outside the contract, so procedures can be viewed as private transitions.
Putting it All Together¶
The complete crowdfunding contract is given below.
(***************************************************)
(* Scilla version *)
(***************************************************)
scilla_version 0
(***************************************************)
(* Associated library *)
(***************************************************)
import BoolUtils
library Crowdfunding
let one_msg =
fun (msg : Message) =>
let nil_msg = Nil {Message} in
Cons {Message} msg nil_msg
let blk_leq =
fun (blk1 : BNum) =>
fun (blk2 : BNum) =>
let bc1 = builtin blt blk1 blk2 in
let bc2 = builtin eq blk1 blk2 in
orb bc1 bc2
let get_funds_allowed =
fun (cur_block : BNum) =>
fun (max_block : BNum) =>
fun (balance : Uint128) =>
fun (goal : Uint128) =>
let in_time = blk_leq cur_block max_block in
let deadline_passed = negb in_time in
let target_not_reached = builtin lt balance goal in
let target_reached = negb target_not_reached in
andb deadline_passed target_reached
let claimback_allowed =
fun (balance : Uint128) =>
fun (goal : Uint128) =>
fun (already_funded : Bool) =>
let target_not_reached = builtin lt balance goal in
let not_already_funded = negb already_funded in
andb target_not_reached not_already_funded
let accepted_code = Int32 1
let missed_deadline_code = Int32 2
let already_backed_code = Int32 3
let not_owner_code = Int32 4
let too_early_code = Int32 5
let got_funds_code = Int32 6
let cannot_get_funds = Int32 7
let cannot_reclaim_code = Int32 8
let reclaimed_code = Int32 9
(***************************************************)
(* The contract definition *)
(***************************************************)
contract Crowdfunding
(* Parameters *)
(owner : ByStr20,
max_block : BNum,
goal : Uint128)
(* Contract constraint *)
with
let zero = Uint128 0 in
builtin lt zero goal
=>
(* Mutable fields *)
field backers : Map ByStr20 Uint128 = Emp ByStr20 Uint128
field funded : Bool = False
procedure DonationEvent (failure : Bool, error_code : Int32)
match failure with
| False =>
e = {_eventname : "DonationSuccess"; donor : _sender;
amount : _amount; code : accepted_code};
event e
| True =>
e = {_eventname : "DonationFailure"; donor : _sender;
amount : _amount; code : error_code};
event e
end
end
procedure PerformDonate ()
c <- exists backers[_sender];
match c with
| False =>
accept;
backers[_sender] := _amount;
DonationEvent c accepted_code
| True =>
DonationEvent c already_backed_code
end
end
transition Donate ()
blk <- & BLOCKNUMBER;
in_time = blk_leq blk max_block;
match in_time with
| True =>
PerformDonate
| False =>
t = True;
DonationEvent t missed_deadline_code
end
end
procedure GetFundsFailure (error_code : Int32)
e = {_eventname : "GetFundsFailure"; caller : _sender;
amount : _amount; code : error_code};
event e
end
procedure PerformGetFunds ()
bal <- _balance;
tt = True;
funded := tt;
msg = {_tag : ""; _recipient : owner; _amount : bal; code : got_funds_code};
msgs = one_msg msg;
send msgs
end
transition GetFunds ()
is_owner = builtin eq owner _sender;
match is_owner with
| False =>
GetFundsFailure not_owner_code
| True =>
blk <- & BLOCKNUMBER;
bal <- _balance;
allowed = get_funds_allowed blk max_block bal goal;
match allowed with
| False =>
GetFundsFailure cannot_get_funds
| True =>
PerformGetFunds
end
end
end
procedure ClaimBackFailure (error_code : Int32)
e = {_eventname : "ClaimBackFailure"; caller : _sender;
amount : _amount; code : error_code};
event e
end
procedure PerformClaimBack (amount : Uint128)
delete backers[_sender];
msg = {_tag : ""; _recipient : _sender; _amount : amount; code : reclaimed_code};
msgs = one_msg msg;
e = { _eventname : "ClaimBackSuccess"; caller : _sender; amount : amount; code : reclaimed_code};
event e;
send msgs
end
transition ClaimBack ()
blk <- & BLOCKNUMBER;
after_deadline = builtin blt max_block blk;
match after_deadline with
| False =>
ClaimBackFailure too_early_code
| True =>
bal <- _balance;
f <- funded;
allowed = claimback_allowed bal goal f;
match allowed with
| False =>
ClaimBackFailure cannot_reclaim_code
| True =>
res <- backers[_sender];
match res with
| None =>
(* Sender has not donated *)
ClaimBackFailure cannot_reclaim_code
| Some v =>
PerformClaimBack v
end
end
end
end