A Smart Contract Development Stack

Better Abstractions for Correct Smart Contracts

Blockchains and Smart Contracts are one of the most intense hypes I have ever encountered, a close number two right after micro services :-) Even the IHK Stuttgart, the local industry association, recently organised a Blockchain Camp, and around 200 people attended, many of them with no computer science background.

Two Aspects of Smart Contracts

For me, the topic conceptually splits into two aspects. One is the non-functional properties provided by the Blockchain technology, such as trustworthiness and non-repudiability, as a consequence of the distributed nature of block processing and the involved math. Even though it builds on many established ideas and technologies (such as public key crypto), the approach is fundamentally new and interesting. Some of the particular technologies definitely need to change to approaches that are way less wasteful of energy though; Algorand looks very interesting, as well as Ethereum’s native work on proof-of-stake in the context of Casper.

The other aspects is the idea that non-programmers can specify, analyse, simulate and ultimately execute contracts. And I really mean contracts, i.e., processes where multiple involved parties make (a sequence of) decisions over time. The non-functional properties of blockchains can be beneficialhere, but are not necessary — if you trust a central entity, you can delegate the execution of the contract to that entity and use crypto to control who is allowed to do what as part of a contract. This second aspect is very much in line with the computerification of other non-technical domains such as computational law or computational governance. It is probably not a surprise to you, dear reader, that I consider this a very good use case for DSLs.

Ethereum and Solidity

The preeminent platform for executing smart contracts is Ethereum. Except for the energy issue, it is very suitable for providing the non-functional properties of blockchains I mentioned above. However, it falls short in the second aspect. The primary programming language for the Ethereum VM (EVM) is Solidity. It is essentially a general-purpose programming language with support for the specifics of programs that run on the blockchain. For example, running code on the distributed EVM costs money (Ether), and developers can limit the processing time used by a particular program in order to not run out of money. And every method that’s called on a contract implicitly carries information about the sender (more specifically, their account number) so that the fee for a transaction can be paid by this account; the ID can also be used for authorisation of operations defined in the contract. However, Solidity (and the other Ethereum languages I have seen so far) does not provide first-class support for the typical patterns found in smart contracts that run on the blockchain, i.e., programs where a group of parties collaboratively make decisions and run processes. This is interesting, since the community has identified typical “contract patterns” that are a good starting point for reification into language abstractions.

An Architecture for Smart Contract Development

The following picture shows an overview of how I imagine a Smart Contract development environment to look like. Let’s walk through the parts.

The first realisation is that the overall problem can be broken down into the development of contracts and into its execution.

Contract Execution

Considering that blockchain technology exists (and ignoring the energy challenge), execution is almost the simpler problem. Once you have implemented a contract correctly (!), you can deploy it to the blockchain and execute it there, benefiting from the guarantees provided by the blockchain (and maybe also suffering from some of its limitations, such as relatively low throughput, at least for now). Several different blockchain technologies exist; for example, in a business context, it seems that Hyperledger might be(come) more important than Ethereum. It doesn’t have exactly the same properties or guarantees, but that is good: users can choose the properties they need. Notice, however, the exclamation point behind the “correctly” above. That is the crux!

It is of course necessary that the infrastructure itself provides correctness guarantees. This is why various projects are under way to formally verify the virtual machine or enhance the solidity compiler to support advanced checking through integration with a solver. However, you can still implement the wrong behavior in your contract (which is then correctly executed by a verified VM). This is where the importance of the right contract development languages and tools come in.

Contract Development

It’s almost funny how often I have heard statements like, “Well, contracts have to be correct, because, in contrast to other software, money is involved, and you don’t want to lose that.” True, of course, but if you’re the developer of pace makers, you don’t want to kill people because of bugs in your software. And if you develop satellites, you don’t want it to die from a software bug on day two of the mission. So, ensuring the correctness of a program is relevant outside of smart contracts, too. And we should take a look at what those communities do, and not reinvent the wheel (a gentle hint at the formal methods booklet :-)). More generally, this means that the development of (correct) contracts must also be supported by the overall toolchain. Here is how I envision this to work.

Contract development should rely on a language stack. At the core of this stack, I expect a functional programming language. Functional languages are useful because they are (relatively) easy to verify, and can also relatively easily support (in-memory) transactions (as I have discussed in this previous post), which is useful for contract-style programs. On top of the functional core, I expect a couple of language extensions that directly support the above mentioned contract patterns, such as decisions, auctions, agreements and resource allocations. Each of those can be broken down into a whole range of configuration options (think: domain analysis, variability, feature model), that determine the specific behavior. The Executable Multi-Party Contract Language (EMPCL) in the above picture contains language constructs for these typical Smart Contract building blocks. It also support state machines, since most non-trivial contracts are in effect state machines. I will return to this idea below when we look at example code.

On top of EMPCL, I see languages (or EMPCL-extensions) that are closely aligned with domains such as logistics or finance. Each of those has their own idiomatic contract constructs, and the language extensions should support those directly.

Why language extensions and not just frameworks or libraries? Because they make it easier to write correct code (once they are stable). Two reasons. First, by using language constructs at an appropriate level of abstraction, many lower-level mistakes cannot be made in the first place. The contract is, to some degree, correct-by-construction. In addition, a language that makes semantically relevant things first-class citizens makes verification of the not-correct-by-construction things much easier (again, a hint at the formal methods booklet :-)); good IDE support can also be provided more easily. It’s also just less code one has to write, so it’s easier to understand and review. Even better, by providing an interpreter, one can interactively play with the contracts and explore their behavior, and write test cases that are executed immediately. Finally, at least for those DSLs that are aligned with particular domains (those above EMPCL), there’s a realistic chance that non-programmer domain experts can read or write the code. Really, this is the “usual DSL story” that has been proven to work over and over again, and it will also work here.

Contracts also have a couple of very specific risks that go beyond functional safety-style verification that result from their game theoretic nature, for example sybil attacks or timing problems. For now, dealing with those is outside of what I am looking at.

Prototypical Implementation

I have implemented some aspects of this language stack in MPS. In particular, I have started building a language that could become EMPCL. At this point I have not yet implemented verification tools, and I don’t yet translate to any blockchain technology for execution. But some of the core abstractions are available, and this illustrates how and why they are useful. I will explain them in detail below. Make sure you have read the post on Dealing with Mutable State in KernelF, because I rely on it heavily.

The Multi-Party Boolean Decision

The core abstraction I have implemented is the multi-party boolean decision, i.e., a process which lets a group of parties make a yes/no decision. It’s the simplest process one can think of in the context of contracts. We had performed an initial domain analysis for decisions, and based on this, I have derived the following set of configuration options.

First, who are the parties involved in making the decision. In the example above, bernd and markus are references to global variables of type party. Optionally, the set of parties can be dynamic, which means that, as the process executes, additional parties can be made members of the decision process. If the parties are dynamic, an additional check box shows up that allows support for sealing the parties: once the process is sealed, no new parties can be added anymore. The remaining options concern the actual decision process. The procedure determines how the final decision is made, e.g., by simple majority, by unanimous agreement or by a custom algorithm. The turnout determines whether a minimum number of parties have to actually make a decision. The time limit requires the decision to be made within a given timeframe, and the revokable flag determines whether a party can revoke their decision once they have made it.

The decisions are an example of a process, i.e., a language construct that can be stimulated by executing commands, and it can be observed by reading values. Based on the configuration of the process, different commands and values are available. Since this is a language extension and not just a library, the IDE knows about these and can provide support, i.e., help ensure some degree of correctness by construction. A few examples are shown below.

For example, once a turnout is configured, a non-vote cannot be interpreted as a “no” vote, so the system has to explicitly support voteFor and voteAgainst commands. Similarly, although not shown, the decision value is now an opt<boolean> instead of a boolean because, until the turnout has been achieved, no decision has been taken (and none is returned). Also, all the commands to add parties are only offered if dynamic is selected.

Playing with Decisions — the REPL

Processes have this nice property of uniform interaction: send in commands, observe values. The KernelF Read-Eval-Print-Loop, or REPL, has special support for such values through the live() expression. Applied to a process (such as the MultipartyBooleanDecision), it provides code completion for the commands that are currently allowed. In fact, it even looks at the current state of the process and only supports those commands that are allowed at the current execution state. The REPL also supports a nice, readable rendering for the values of processes. For a sequence of steps, it even highlights the changes in blue, so it’s easy to observe how a process evolved as users issue comm. The next screenshot shows a REPL session on a MultipartyBooleanDecision with a dynamic set of parties and sealing enabled. Check out how the internal state changes based on the commands issued.

Because all of this is based on a generic, reflective API, one can imagine other UIs. In particular, we will build a “simulator” where there are buttons for each command and UI widgets for each value. This will allow non-programmers to creatively play with a contract and thus better understand how it behaves.

Of course, one can also script tests and execute them directly in the IDE, based on the same interpreter that also drives the REPL.

Combining Decisions with State Machines

The decision described above supports basic, multi-party decisions. Over time, we will also add support for auctions, agreements and other contract patterns. However, a contract will also always have specific behavior that cannot easily be expressed declaratively. However, there’s no reason to “fall down” to imperative programming just yet. State machines are a much better abstraction for many of these behaviors, especially when combined with the processes. Consider the following set of requirements:

We have a set of products, each can potentially be sold. First, a
predefined group of stakeholders has to make a decision for each of the
products whether it should indeed be sold or not. Everybody has to vote, and the
decision is by majority. There is a limited time by which the vote has
to have taken place. Once that decision has been made for all products,
each products can be sold to somebody; a product can only be sold once,
and the price must be the same or higher as the one specified in the
offer, and the offer must not have been sold before. All sales are
recorded. Once all sellable products have been successfully sold, the
contract terminates.

This is a realistic, and not totally simplistic example of a contract. Let’s look at its implementation based on declarative decision processes, state machines and a couple of helper functions. We also need a couple of data types; we start with those, they should be rather obvious:

Next, we define a few helper functions, the comments in the code explain what they do.

The remaining implementation consists of one decision process and a state machine (with a few more embedded functions). We show the code next, and then discuss it in some detail:

The state machine serves as the “top level” interface for the contract. Its API are the two events defined in it. The first one, vote, expresses that the party who votes for or against (expressed through the Boolean parameter) selling the product with the given ID. The second event, buy, expresses that a particular party wants to buy a product for a given price.

The next line is crucial. Remember that we want to make a separate sell/no-sell decision for every product/offer. So the salesDecisions variable is initialized to a map that contains an instance of the ShouldWeSell process associated with each product ID.

Let’s now move on to the initial state decideOnSelling. If the vote event comes in, we react by checking whether the shouldWeSell flag is true. If so, we retrieve the sales decision process for the respective product and voteForit. Otherwise we voteAgainst. If, for all sales decisions, the turnout has been achieved we transition to the selling state.

In the selling state, we expect the buy event (any other event leads to a failure of the operation). If it comes in, and the decision to sell the particular product has been positive (check out the shouldBeSold function), we retrieve the box that contains the offer and call tryToBuy. Otherwise we ignore the event. Once all to-be-sold products have been sold, we move to the endedstate.

The final piece of the puzzle is the tryToBuy function. If the product/offer has already been sold it does nothing; otherwise it checks if the price paid by the buyer is greater or equal to the price stated in the offer, and if so, sets the offer’s sold flag to true and adds the corresponding sale to the list of sales.

Another Example

This final example is one where several decision processes interact and processes are started dynamically by the coordinating state machine. It’s similar to the (in-)famous DAO in the sense that the set of decision makers changes dynamically. In particular, the requirements are:

We’re an online community that has to continuously maintain a (selling)
decision; it can be revoked or granted over time. The group of
individuals, called the deciders, can vote (and revoke) this sales
decision. The vote has to be unanimous. In addition, additional people
can be voted into the group of deciders. The existing deciders vote for
new candidates, by simple majority, but with a time limit. Once voted
into the group of deciders, the new member can participate in the
sell/no-sell decision. Multiple member approval processes can go on at
the same time. While a member request is pending, the sales decision cannot
be changed.

At the core are two decision processes. Sale runs “forever” and manages the group decision. It’s membership can change over time. The other process, AccessControl, manages the join request and the voting for a potential new guy. It is started, dynamically, for each join request. The key is that whenever a join request for a new guy finishes successfully, it’s join process is terminated, and the new guy is added to the parties of the Sale process. Check out the code, as well as the REPL session below.

The REPL session is a bit longish, but it does illustrate the point.

Wrap up and Outlook

It should be obvious from these examples that the ability to declaratively specify contracts based on a mix of state machines and (a growing) set of declarative decision, auction, agreement and resource allocation processes provides a solid foundation for efficiently implementing Smart Contracts. Many low-level mistakes cannot be made, and stakeholders can experiment with the contract by playing with it in the REPL and a future simulator. Tests can be written an executed.

It’s probably worth mentioning that the whole contract, state machines and decision processes, are transactional (as discussed in that previous post). So if anything goes wrong (e.g., an event is posted when there is no transition that handles it), the machine fails and the transaction, if one has been started before, is rolled back.

In the future, we will implement functional verification of contracts based on an integration with model checkers and SMT solvers; but don’t expect a post that too soon, this is quite a bit of work.

Finally, we also need a deployment story. We are working on a Java generator for KernelF and all the rest, so a plain Java (Enterprise) deployment is not too far away. We are also working on a generator to Ethereum to exploit its non-functional properties as well. But again, these things will take some time. My goal with this work, and this post, was to play with better abstractions for Smart Contracts; let me know if I succeeded.