Bitcoin
$3,302.04
-131.28
Ethereum
$86.16
-4.37
Litecoin
$23.40
-0.71
DigitalCash
$61.25
-3.54
Monero
$42.78
-0.6
Nxt
$0.03
0
Ethereum Classic
$3.80
-0.12
Dogecoin
$0.00
-0

Scilla – The Code Behind Zilliqa

Zilliqa is planning to become the next-generation, scalable, smart contract platform. In order to power their smart contracts, they are creating their own smart contract language called Scilla or Smart Contract Intermediate-Level LAnguage. The main issue that Scilla is looking to solve is smart contract security.

So, before we take a look into how Scilla works, let’s see the security problems that the current smart contracts are facing.

The Current State of Smart Contract Security

Back in 2016, everyone was excited about The DAO. It was basically a complex smart contract which was going to be a decentralized venture capital fund for future Dapp development. However, that dream soon came crashing down, when a vulnerability in their smart saw a hacker siphon away $50 million dollars worth of Ethereum. This incident caused such a cataclysmic pandemonium, that the entire Ethereum community got split into Ethereum Classic and Ethereum.

The scary part is that this is not a one-off situation.

Smart contract security is a huge cause of concern for prospective investors. In order to gain mainstream adoption, smart contracts and cryptocurrencies must earn the unwavering faith of the public.

This begs the question, what exactly is stopping smart contracts from gaining complete security?

Firstly, as you may know, blockchains and smart contracts are inherently immutable by nature. Meaning, once you enter something into the blockchain, you can’t tamper with it anymore. While this is definitely a big plus point, the fact remains this has an undesirable flipside as well. Once a smart contract has been executed, you can’t go back and fix a bug! Basically, if you want to avoid a hard fork, then you better be 100% sure that your smart contract is absolutely faultless.

Obviously, that is an unreasonable thing to ask and this why the crypto space right now is riddled with faulty smart contracts. As Ethereum Foundation’s Martin Swende puts it, “This is Disneyland for hackers.”

Secondly, one must keep in mind that these solidity contracts are running on gas consumption. So, whenever a developer presents a smart contract for execution, they must specify a gas limit as well. Since each and every line of the contract code consumes gas, the specified limit should be enough to cover the entire contract.

This is why, it is doubly important to make sure that the contract isn’t buggy. A bug may simply siphon away all the gas in the contract mid-execution. Also, we can’t simply let a buggy contract float around in the ecosystem, because the whole process is being executed in a Byzantine network where we are assuming that each and every node is malicious and trying to take advantage of a vulnerability.

Ok, so what is the solution here?

Let’s look at what two of the most important cryptocurrencies in the world are doing.

Bitcoin is using a simple scripting language to take care of their transactions. The language is simple for entry-level participants to understand and take part in. However, it is not that flexible and only allows for relatively simplistic transactions.

On the other hand, Ethereum is using the Turing complete solidity. Meaning, if given enough time and resources, it should be, theoretically, able to compute anything. So, while this affords developers a lot of flexibility, it is a simple language and can lead to disasters if not coded properly.

This why Zilliqa chose to create an intermediate-level language. Scilla hopes to be both simple-to-understand and flexible enough for real-world applications. One thing to keep in mind, while Scilla is being designed in the context of Zilliqa, it is not agnostic to the underlying blockchain platform and hence can be used with any other blockchain.

How Does Scilla Work?

So, how does Scilla achieve this balance between flexibility and simplicity without compromising on security? By separating various programming concerns, namely:

  • Between computation and communication
  • Between effectful and pure computations
  • Between invocation and continuation

Computation and Communication

There are tons of computations that take place during smart contract execution like balance changing, value computation of a function etc. These computations are implemented as standalone, atomic transitions which are self-sufficient and don’t require involvement from other parties.

However, there may be instances during the contract execution when such an involvement will be required (e.g. when you need to transfer the control of a particular mechanism to another party). In instances such as these, the program demands explicit communication between the parties via message sending and receiving.

This property allows the smart contract to:

  • Compute without outside interference.
  • Make sure that concrete and efficient communication is maintained when another party needs to get involved in the operations.

Effectful and Pure Computations

Smart contracts need to have an in-built halting property. Every computation that is taking place within the contract has to be terminable. Also, these must have a predictable effect on the overall state of the contract. This property ensures that contract execution remains under control and doesn’t behave in unforeseen ways.

Invocation and Continuation

The contracts in Scilla are structured as communication automata which provides a computational model, known as continuation-passing style (CPS), where a call to an external function is made in the last line of instruction.

So, what exactly is the advantage of this model?

Calling an external function mid-execution can lead to a plethora of problems, like the re-entrancy attack. In fact, it was the re-entrancy attack that caused the DAO attack.

How is a Scilla Contract Framed?

The following is what a simple Scilla contract looks like:

(* Scilla contract structure *)

(***************************************************)

(*               Associated library                *)

(***************************************************)

library MyContractLib

(* Library code block follows *)

(***************************************************)

(*             Contract definition                 *)

(***************************************************)

contract MyContract

(* Immutable fields declaration *)

(vname_1 : vtype_1,

vname_2 : vtype_2)

(* Mutable fields declaration *)

field vname_1 : vtype_1 = init_val_1

field vname_2 : vtype_2 = init_val_2

(* Transitions *)

(* Transition signature *)

transition firstTransition (param_1 : type_1, param_2 : type_2)

 (* Transition body *)

end

transition secondTransition (param_1: type_1)

 (* Transition body *)

end

NOTE: Code taken from Scilla docs.

As you can see, the contract starts with library declaration. The libraries contain simple mathematical functions like a function to compute the boolean and of two bits or computing factorial of a given natural number.

The contact that you see above has three parts to it:

  • Declaring immutable variables of the contract
  • Declare the mutable fields
  • Transition definitions

Part #1: Immutable Variables

The immutable variables are declared in this part of the contract:

vname_1 : vtype_1,

vname_2 : vtype_2

The immutable variables (or contract parameters) have their values defined at the time of contract creation and cannot be tampered with later on. These variables are specified at the beginning of the contract, right after the contract name is defined.

Each declaration has:

  • A variable name and its type. Both of those are separated by a “:”
  • If multiple declarations are required, then they are separated by a “,”
  • They must be initialized at the time of contract creation

Part #2: Mutable Fields

Following are the mutable fields in the contract:

field name1 : type1 = expr1

field name2 : type2 = expr2

This part of the contract represents the state that is not set in stone. It presents the mutable and changeable part of the contract which is subject to state transition. In other words, the value of these fields gets modified as the contract goes through various transitions.

Part #3: Transitions

The “Transitions” section of the contract defines the change in the state of the contract. The follow section shows the two transition states that our contract are going through:

transition firstTransition (param_1 : type_1, param_2 : type_2)

 (* Transition body *)

end

transition secondTransition (param_1: type_1)

 (* Transition body *)

end

As you can see, these transitions are defined by the keyword “transition”, followed by the name and parameters to be passed. The transition function ends with the “end” keyword.

Now, let’s look at what is happening inside the parameters.

(param_1 : type_1, param_2 : type_2)

  • param_1 is the name of the parameter
  • type_1 is the type of parameter param_1
  • The param_1 and type_1 are separated by a “:”
  • Multiple parameters are separated by a “,”

Ok, so we have seen how the parameters are declared within the transition function. However, what about the “transition” keyword itself? Turns out, each transition has the following implicit parameters available to it:

  • _sender : ByStr20 = This is the account of the sender of the message, i.e. the one that triggered this transition
  • _amount : Uint128 = This is the incoming amount of ZIL tokens. These must be accepted explicitly by the “accept” statement. Remember, when we told you that explicit messaging is required in Scilla whenever an outside party gets involved? This is an example of that. The money transfer doesn’t take place if the transition function doesn’t execute “accept”.

Standard Libraries

The concept of libraries is nothing new in programming. They are just a bunch of precompiled routines that a developer can use in their contract instead of coding everything from scratch. Think of it like this, if you want to make a sandwich, which of the following will be more convenient?

  • Order bread from the store
  • Baking the bread from scratch

Using libraries is sort of like ordering bread from the store.

Scilla has four standard library contract which you can call into your smart contract:

  • BoolUtils.scilla
  • ListUtils.scilla
  • NatUtils.scilla
  • PairUtils.scilla

BoolUtils.scilla

The BoolUtils.scilla library implements operations on Boolean data types. Boolean data types takes only two inputs, “True” and “False”. Boolean is declared using the keyword “Bool”.

ListUtils.scilla

The ListUtils.scilla library uses the List arithmetic data type (ADT). List provides users a structure to contain a list of values of the same type.

List is specified by using the “List” keyword and has two constructors:

  • Nil: This creates an empty list and is declared like this: Nil{A}. This creates an empty list of type A
  • Cons: This constructor adds an element to the existing list. The syntax is like this:

    Cons {A} h l.

    In the above case, “A” is a type variable, “h” is an element of type A and it is inserted at the head of list “l”. 

The ListUtils.scilla library includes various common List utilities such as list_length.

NatUtils.scilla

The Nat ADT works with natural numbers. A natural number is either a 0 or a positive integer.

PairUtils.scilla

PairUtils.scilla is a library which includes Pair ADTs.

Pair ADTs are used to specifically contain a pair of values of possibly different types. These pair variables are declared by using the Pair keyword and can be created by using the constructor Pair {‘A ‘B} a b here ‘A and ‘B are type variables, and a and b are variables of type ‘A and ‘B respectively.

Let’s see how that works in program execution. Let’s construct a Pair of Int32 values:

let one = 1 in

let two = 2 in

let p = Pair {Int32 Int32} one two in

“fst” is among the many functions that the PairUtils library has. “fst” enables users to utilize pattern matching to extract the first element from a Pair.

let fst =

 tfun ‘A =>

 fun (p : Pair ‘A ‘A) =>

 match p with

 | Pair {‘A ‘A} a b =>

     a

 end

 

let p = Pair {Int32 Int32} one two in

let fst_int = @fst Int32 in

let a = fst_int p in

 … (* a = one *) …

The Classic HelloWorld Contract

Let’s take a look at how the classic “Hello World” contract works in Scilla.

library HelloWorld

let one_msg =

    fun (msg : Message) =>

    let nil_msg = Nil {Message} in

    Cons {Message} msg nil_msg

 

let not_owner_code  = Int32 1

let set_hello_code  = Int32 2

 

contract HelloWorld

(owner: ByStr20)

 

field welcome_msg : String = “”

transition setHello (msg : String)

  is_owner = builtin eq owner _sender;

  match is_owner with

  | False =>

    msg = {_tag : “Main”; _recipient : _sender; _amount : Uint128 0; code : not_owner_code};

    msgs = one_msg msg;

    send msgs

  | True =>

    welcome_msg := msg;

    msg = {_tag : “Main”; _recipient : _sender; _amount : Uint128 0; code : set_hello_code};

    msgs = one_msg msg;

    send msgs

  end

end

Alright, so let’s breakdown sections of this contract and see what is going on.

Section #1: Libraries

library HelloWorld

let one_msg =

fun (msg : Message) =>

let nil_msg = Nil {Message} in

Cons {Message} msg nil_msg

let not_owner_code  = Int32 1

let set_hello_code  = Int32 2

A library is declared right in the beginning of the smart contract. This HelloWorld contract code has a function one_msg in the library and two global constants.

Section #2: Mutable and Immutable Variables

contract HelloWorld

(owner: Address)

field welcome_msg : String = “”

Like we have mentioned before, Scilla contracts have two kinds of state variables:

  • Mutable
  • Immutable

In this HelloWorld contract, “owner” is the immutable variable. Throughout the execution of this contract, the owner’s address won’t change.

On the other hand, the variable “welcome_msg” is a mutable variable whose state adn value will change through the contract execution.

Section #3: Transitions

transition setHello (msg : String)

is_owner = builtin eq owner _sender;

match is_owner with

| False =>

  msg = {_tag : “Main”; _recipient :  _sender; _amount : Uint128 0; code : not_owner_code};

  msgs = one_msg msg;

  send msgs

| True =>

  welcome_msg := msg;

  msg = {_tag : “Main”; _recipient :  _sender; _amount : Uint128 0; code : set_hello_code};

  msgs = one_msg msg;

  send msgs

end

end

transition getHello ()

  r <- welcome_msg;

  msg = {_tag : “Main”; _recipient : _sender; _amount : Uint128 0; msg : r};

  msgs = one_msg msg;

  send msgs

end

We have two transition functions here which can change the value of the mutable variables and engage in inter-contract communication. What are these two transition functions?

  • setHello(): This transition function takes a String as input, updates welcome_msg and informs the caller about the success/failure of the operation 
  • getHello(): This function simply sends the current value of welcome_msg to the caller.

Where to Execute Scilla?

Scilla is under active development and as right now there are two platforms where you can try out Scilla:

  • Blockchain IDE
  • Interpreter IDE

Blockchain IDE

Currently, the simplest way to experiment with Scilla is via the Scilla Blockchain IDE. This Integrated Development Environment or IDE is connected to the Zilliqa blockchain through the Zilliqa testnet wallet and a block explorer.

In other words, it comes with nearly all the features that are needed to run a Scilla contract in a real blockchain environment.

How does one get to access the Blockchain IDE?

By holding on to Testnet ZIL tokens aka the tokens that are used to operate Zilliqa’s blockchain infrastructure. These testnet ZIL tokens are needed to pay for gas fees to run these smart contracts. These tokens are distributed time-to-time for free.

So, what are the gas rates like?

  • Each regular payment from a non-contract account to a non-contract account corresponds to 1 unit of gas
  • Contract creation costs around 50 units of gas
  • A call from a non-contract account to contract account and contract account to contract account will both cost 10 units of gas.

Interpreter IDE

For developers who want to roll their sleeves back and get down and dirty with Scilla coding, the Interpreter IDE is a good alternative. The Scilla Interpreter IDE is a standalone environment to test Scilla contracts.

While the interpreter runs in the backend, it is not linked to any blockchain network. As a result, it doesn’t maintain a persistent state and is free from any blockchain wide-parameters such as current block number. In other words, it is the ideal sandbox.

On the flipside, since the interpreter is not up-to-date with the latest blockchain state, developers will need to mimic and manually provide certain data inputs to get more realistic results. Unlike the Blockchain IDE, Interpreter doesn’t require any testnet ZIL tokens.

Design Challenges

Before we explain the design challenges that Scilla creators are facing, you should familiarize yourself with the term “correctness”. In simple terms, if the algorithm is consistently producing the expected results when given a specific input, it is said to have a high degree of correctness.

So, what are the design challenges that the Scilla creators are facing?

  • Each smart contract comes with its own unique criteria of correctness. In other words, it is infeasible to come up with the exact set of properties which indicates “wrong correctness”. 
  • A big reason as to why that is difficult to do is because behavior that is considered wrong in one contract, might actually be extremely desirable in another. Zeroing in on a universal set of desired contract properties requires immense formal specification 
  • Currently, they need to find a common ground between clean and straightforward contract semantics and contract-expression flexibility. According to them, “we consider our mission to provide semantic foundations, as well as a logical vocabulary for making it possible to formulate and prove all reasonable contract properties, giving Scilla programmers a toolset to implement, specify, and mechanically verify the contracts with respect to correctness conditions of interest.” 
  • They also are planning to prototype their contract language by encoding the programs and the semantics in a state-of-the-art language with dependent types and a support for formal machine-assisted proofs. This will enable a large degree of correctness during program execution itself 
  • Another scenario that they want to avoid is something similar to the “Landin’s knot”.

    Basically, the ability to implement potentially non-terminating computations by making a contract call itself, directly or indirectly, via a message passing mechanism or explicit continuations. This can happen because the developer failed to specify stack length or gas bounds.

    This goes against the communication automata model that has been envisioned for Scilla. So, to be able to detect such scenarios before the transaction is even executed, they need to implement a careful analysis to deliver precise parameterized cost boundaries on transition executions.

Conclusion

If Zilliqa can pull off their product then they may very well open the floodgates to truly scalable Dapps. However, before they do that, it is extremely important that they nail Scilla. The main people working in this project are Head of Research Amrit Kumar, Lead Language Designer Ilya Sergey, and Zilliqa advisor Aquinas Hobor. Let’s hope that they nail this project for the overall betterment of the entire crypto space.

Leave A Reply

Your email address will not be published.