æternity was building a blockchain on the BEAM, in Erlang, and needed a virtual machine to run smart contracts on it. We ended up designing two things: Sophia, a language for writing contracts, and FATE, the machine that runs them. This post covers what we found in the existing designs, what we chose instead, and what those choices cost.
How the work started
Happi Hacking was approached by æternity, and we were invited to meet the development team in Sofia, Bulgaria, two weeks later. Neither Tobias nor I knew anything about blockchains at the time. So I sat down with the Ethereum "yellow paper" (sic) to learn the technology, and to really understand the Ethereum Virtual Machine I implemented a version of it in Erlang over those two weeks. I called it AEVM, the æternity Ethereum Virtual Machine.
We went to Sofia expecting to learn blockchain from the team. After a few days of discussion it was apparent that the field was young. Nobody knew much about how to implement these systems, or even which features to implement. When I showed the team the AEVM implementation we ended up in a central position in the core team, and for the next two years Tobias and I led many of the technical decisions and wrote much of the æternity core. Once the main blockchain features were in place we turned to the question of how a virtual machine for a blockchain should be designed.
What a contract actually needs
We started from the properties we wanted out of contract execution. Contracts should run in a short and predictable time. They should be deterministic, since every node has to reach the same result. They should be reusable, and they should be easy to read and to verify, because a contract that nobody can check is a contract nobody should trust with money. They should also reach æternity's own features, the oracles, contracts, and state channels, without ceremony.
The EVM gave us a useful counterexample. It was modeled after a computer, with stack slots, memory addresses, a fixed word length, and arithmetic that could overflow or fail silently. Those properties made sense for hardware, where they describe something real. On a chain they describe nothing, and they carry costs. A contract is a program about money, and money arithmetic that silently wraps around tends to produce expensive bugs. Solidity inherited the model, and through AEVM so did we.
Sophia
Sophia is the language we designed in response. It is statically typed, it allows parallelism between contracts, and it avoids concurrency inside one, which keeps execution simple to follow. Failures produce defined errors with something useful in them. æternity's features are reachable from the language directly, and data has one defined way of being serialized and stored. Where a design choice traded convenience against safety, we took safety, and that accounts for most of the distance between Sophia and Solidity.
FATE
FATE is the machine underneath. It is typed, and it is built for one language on one chain, which is what let us take the decisions below.
Gas is the only resource bound. There is no memory limit, so a contract that needs to compute something large pays for it and proceeds. Every operation costs gas and the total decides the price of the call, which keeps expensive code from monopolizing a node and gives contract authors a cost model they can reason about.
Execution is deterministic, and most of the design follows from that one requirement. A contract runs sequentially, so parallelism comes from running independent contracts or transactions at the same time. There are no floating point numbers, since rounding differences between implementations would put nodes into disagreement. Data has one defined byte representation, for the same reason. A blockchain is a machine for making thousands of computers agree on a number, and every ambiguity in the VM is a way for them to disagree.
Sophia is type checked at compile time, so errors surface before a contract is deployed. FATE checks types again at runtime, whatever compiler produced the bytecode, and a violation reverts the call. The machine does not trust its compiler. The types it knows about are part of the machine language:
-- Fate types
Integer -- signed arbitrary precision integers
Boolean -- (true | false)
Address -- A pointer into the state tree
Contract | Oracle | Oracle_query | Channel
String -- utf8 encoded byte arrays
Bytes
Tuple (), ('a), ('a, 'b, ...)
List -- Cons cells (‘a) | Nil (Ʇ)
Map (‘a, ‘b) -- (Key: ‘a -> Value: ‘b) ‘a not a map
Variant (| [Sizes] | Tag | Elements |)
Bits
TypeRep
Failures are defined too. A contract that fails returns a specific error, and the author can tell from it what went wrong. Oracles, contracts, and state channels are instructions in the machine, so the chain's own features need no library code reimplementing them on top of a general purpose VM.
Removing the machine model
We decided to have no memory addresses in FATE, so that the VM cannot be tricked into executing the wrong code. This is the structure that replaced them:
- Basic blocks. Code is organized into basic blocks, sequences of instructions that run without interruption. Control flow moves between blocks.
- No instruction addresses. There is nothing to compute a jump target from, so arbitrary jumps into the middle of code cannot be expressed.
- One code object per function. Each function in a contract has its own code, which keeps calls and resource accounting structured.
- No fixed data size. Integers are arbitrary precision, which removes overflow bugs and the attacks built on them.
- No word size. Nothing in the instruction set assumes a machine word, so the implementation is free to pick a representation.
- Flexible storage. FATE defines behavior and leaves layout to the implementation, which can then pick data structures that fit the platform.
- No byte addressed memory. Memory is not addressable from a contract, which decouples the semantics from any hardware model.
The pattern behind these decisions is to remove everything a contract author does not need, especially the parts inherited from a machine model that no longer applies. What is left is easier to reason about and harder to attack.
What this looks like in practice
The difference shows up in something as small as an identity function. Here it is in Solidity, the default language of Ethereum and the EVM.
// Solidity
pragma solidity ^0.5.11;
contract Identity {
function id(int256 X) public pure returns (int256) {
return X;
}
}
Here is the same contract in Sophia.
// Sophia
contract Identity = payable entrypoint main (x:int) = x
The Sophia version is one line, and it never asks you to pick a word size for your integer. Solidity does.
Compiling the Solidity identity contract to EVM assembly gives a fairly large program:
PUSH1 0x80 PUSH1 0x40 MSTORE CALLVALUE DUP1 ISZERO
PUSH1 0xF JUMPI PUSH1 0x0 DUP1 REVERT JUMPDEST POP
PUSH1 0xAB DUP1 PUSH2 0x1E PUSH1 0x0 CODECOPY PUSH1 0x0
RETURN INVALID PUSH1 0x80 PUSH1 0x40 MSTORE CALLVALUE
DUP1 ISZERO PUSH1 0xF JUMPI PUSH1 0x0 DUP1 REVERT
JUMPDEST POP PUSH1 0x4 CALLDATASIZE LT PUSH1 0x28
JUMPI PUSH1 0x0 CALLDATALOAD PUSH1 0xE0 SHR DUP1
PUSH4 0x1A94D83E EQ PUSH1 0x2D JUMPI JUMPDEST
PUSH1 0x0 DUP1 REVERT JUMPDEST PUSH1 0x56 PUSH1 0x4
DUP1 CALLDATASIZE SUB PUSH1 0x20 DUP2 LT ISZERO
PUSH1 0x41 JUMPI PUSH1 0x0 DUP1 REVERT JUMPDEST DUP2
ADD SWAP1 DUP1 DUP1 CALLDATALOAD SWAP1 PUSH1 0x20 ADD
SWAP1 SWAP3 SWAP2 SWAP1 POP POP POP PUSH1 0x6C JUMP
JUMPDEST PUSH1 0x40 MLOAD DUP1 DUP3 DUP2 MSTORE
PUSH1 0x20 ADD SWAP2 POP POP PUSH1 0x40 MLOAD DUP1
SWAP2 SUB SWAP1 RETURN JUMPDEST PUSH1 0x0 DUP2 SWAP1
POP SWAP2 SWAP1 POP JUMP INVALID LOG2 PUSH6
0x627A7A723158 KECCAK256 0xc2 0xb9 0xdf 0xb0 0xc8
0xdf 0xf6 SWAP14 SWAP14 0xe9 0x46 0xcd PUSH17
0x1D21108C0786A26266D0F114ADBF024CDE 0x4b 0xd1
PUSH5 0x736F6C6343 STOP SDIV SIGNEXTEND STOP ORIGIN
Compiling the Sophia identity contract to AEVM gives slightly smaller bytecode:
PUSH3 0, 0, 100 PUSH3 0, 0, 132 SWAP2 DUP1 DUP1 DUP1
MLOAD PUSH32 185, 201, 86, 242, 139, 49, 73, 169, 245,
152, 122, 165, 5, 243, 218, 27, 34, 9, 204, 87, 57, 35,
64, 6, 43, 182, 193, 189, 159, 159, 153, 234 EQ PUSH3 0,
0, 192 JUMPI POP DUP1 MLOAD PUSH32 104, 242, 103, 99,
56, 255, 80, 136, 57, 171, 164, 119, 73, 239, 250, 139,
232, 126, 242, 132, 242, 7, 251, 61, 153, 152, 112, 28,
213, 56, 135, 197 EQ PUSH3 0, 0, 175 JUMPI POP PUSH1 1
NOT MLOAD STOP JUMPDEST PUSH1 0 NOT MSIZE PUSH1 32 ADD
SWAP1 DUP2 MSTORE PUSH1 32 SWAP1 SUB PUSH1 3 DUP2 MSTORE
SWAP1 MSIZE PUSH1 0 MLOAD MSIZE MSTORE PUSH1 0 MSTORE
PUSH1 0 RETURN JUMPDEST PUSH1 0 DUP1 MSTORE PUSH1 0
RETURN JUMPDEST MSIZE MSIZE PUSH1 32 ADD SWAP1 DUP2
MSTORE PUSH1 32 SWAP1 SUB PUSH1 0 NOT MSIZE PUSH1 32 ADD
SWAP1 DUP2 MSTORE PUSH1 32 SWAP1 SUB PUSH1 3 DUP2 MSTORE
DUP2 MSTORE SWAP1 JUMP JUMPDEST PUSH1 32 ADD MLOAD MLOAD
MSIZE POP DUP1 SWAP2 POP POP DUP1 SWAP1 POP SWAP1 JUMP
JUMPDEST POP POP DUP3 SWAP2 POP POP PUSH3 0, 0, 140 JUMP
Compiling the Sophia identity contract to FATE gives:
FUNCTION init() : {tuple,[]}
;; BB : 0
STORE store1 ()
RETURNR ()
FUNCTION main(integer) : integer
;; BB : 0
RETURNR arg0
That is the actual FATE assembler output, and it is short enough to read in one sitting.
What the trade came to
Most of the EVM output above implements a calling convention and a memory layout that the contract author never asked for. FATE removes that layer, so the bytecode stays close to the source and the gas cost follows the operations in the source. The type system rules out another class of bugs before deployment.
The cost is a machine tied to one language and one chain. FATE is not a general compilation target, and running Solidity on it was never a goal. For æternity that trade was worth making. For a project that needs to run existing Ethereum contracts, it would not be.
These decisions also turned out to be permanent. Once a chain launches, its instruction encodings, opcodes, and gas costs are fixed by consensus. I traced what that did to the FATE instruction table in An Instruction Table Is History.
What the work covered
The VM was one part of it. We started by building AEVM in two weeks to show that a virtual machine for æternity was feasible, and stayed for two years inside the development team. Besides Sophia and FATE we worked on Merkle Patricia tries, oracles, state channels, names, accounts, Bitcoin.NG, and proof of work. Tobias and I reviewed code, mentored the more junior developers, ran many of the daily stand ups, and helped the project manager steer the work above the code.
We may come back with another article on the lessons from implementing a blockchain from scratch. Patricia Merkle tries deserve one of their own.
We were not alone in this project. Thank you to the whole team, you know who you are.