Blockchain: How to write safe and verifiable smart contracts

Zilliqa, the public blockchain exploring sharding to increase transaction throughput, has also released Scilla, an intermediate-level language for verified smart contracts.

This new approach provides a clean separation between the communication aspect of smart contracts on a blockchain, and the programming component which is amenable to formal verification.

In the context of Ethereum's Solidity, the semantics of the language doesn't distinguish between things like transferring funds or calling another contract, and computations that the contract itself performs as a program.

To enable a clean separation, Scilla creates several independent language contexts that make it easier to reason about the behavior of a contract.

Ilya Sergey, an Assistant Professor at University College London and one of the authors of the Scilla white paper, explained: "When we reason about the way the contract performs a task, we abstract from the fact that it transfers funds or communicates with other contracts.

"This makes it possible to state high level properties that span the entire lifetime of the contract execution."

A useful example would be making sure money can be retrieved from the contract (called the liveness property) as in Kickstarter when a crowdfunded campaign fails to meet its target.

Scilla, which uses the Coq proof assistant to reason about smart contracts, can formally establish the baked in liveness properties in all contracts.

Coq in this sense can be considered as an extension of functional programming languages like OCaml to make formal statements about a program, in the same way as proving facts about mathematical functions.

Unlike programs written in Java and C, purely functional languages don't express things like objects and state. So would it be possible to have a contract that is represented by function?

"The answer is yes and no," said Sergey. "Functional languages differ in whether they are so called pure, and impure.

"Mathematical functions, like an exponent are pure in the sense that they don't have memory, whereas any reasonable program has state. So you run a program on your computer and it writes certain things to the hard drive of the computer, so you could run it later on and it would pick it up. That's why the state is important.

"Anything that has to do with fewer reproducible computations can be implemented in a purely functional language. But anything that has to with storing the state, storing information, cannot.

"Actually, it goes slightly beyond functional programming; you can still write programs like that in OCaml, but they are a bit more difficult to reason about. Because in addition to reasoning about the program as a function, you need to reason about the effect of this function.

"This is precisely what we model in Scilla. In Scilla all pure computations that just compute a value are functional. So they are very much the same as they would be in the pure component of an account without any state.

"But a contract also maintains a state. Imagine something like an ICO, an ERC 20 token which involves a kind of book-keeping, regarding who bought how many tokens. For that we need a state, and for that we need certain specifications; how this state is going to be changed, how it's going to evolve over time.

"Our goal with Scilla was to develop a better smart contract language that could eliminate known issues with smart contracts and help prove strong guarantees about the correctness of a contract."

Sharding

Scilla is not a necessary component of Zilliqa's sharding architecture, but any language that helps prove strong properties is going to be useful.

Amrit Kumar, Crypto Lead, Zilliqa, said: "Running a smart contract whether written in Solidity or Scilla on a sharded architecture, brings its own set of challenges.

"Look at how normal transfer transactions work currently on a sharded architecture, they can be processed on different shards in parallel without requiring too much of cross-shard communication. The only issue to worry about is double spends that can be easily handled within a shard.

"When you have smart contracts, things become slightly more complicated because they have a common state which is being manipulated by different shards at the same time; one shard has to know in some way what's happening in the other shard.

"There are a number of challenges here, and you might need something like cross-shard communication or some language support that's going to help you solve that problem," he said.

Zilliqa is solving network sharding or transaction sharding, which is really a subset of the problem Ethereum is tackling with state sharding.

Zilliqa's transaction sharding involves every node storing the entire state; every single account and its corresponding balance. Ethereum is attempting to solve a harder problem, not only to shard the network and process transactions in parallel, but also to shard the state. Not every shard is going to store the entire state of the blockchain so there can be light client implementations and so on.

"We think network and transaction sharding is complicated enough in its own right. State sharding is the next level. So we want to take baby steps before taking a giant step," said Kumar.