In which I explore various ways to speed-up smart-contract execution on Tezos and the tradeoffs involved… All of these ideas come from interacting with different developers in the Tezos ecosystem, I am merely summarizing a series of discussions in one place.
Rationale
Michelson is an interpreted language instrumented for gas metering. This makes it incur a large overhead and speed penalty over a native program performing the same computation. The penalty varies depending on what the contract exactly does. For instance, there is little penalty to call functions that verify signatures or hash data. Not only are these merely calls to an efficient external library, but they are also CPU intensive which means the overhead is relatively insignificant. In contrast a program which mostly performs a large amount of stack manipulation incurs a high penalty. One of the most extreme example of a program incurring a high penalty would be one that simply loops through the first billion integers. As a point of reference, such a contract is about three orders of magnitude slower when interpreted and gas metered in Michelson than when compiled as a C program. Note that this is an extreme example. Much of what a contract does is read and write data to the context and the cost of that is dominated by I/O speed, not by the interpreter.
Also note that performance is not the only goal and should not be blindly pursued at all costs. Security, proper gas metering, and determinism are all extremely important. Nonetheless the current overhead is such that some gains can clearly be gained without sacrificing too many other aspects. I explore a few possibilities below.
Optimizing the Michelson interpreter
A few simple optimization to today’s Michelson interpreter can speed it up about 2x. This is displayed in MR#158 by Gabriel (LIGO), then generalized with MR#157 and MR#165 by Ilias and Mehdi (Nomadic Labs). These consist in replacing systematic calls through the LWT concurrency library which do not serve a real purpose in there and in simplifying the gas accounting at each operation. These patches are part of some upcoming protocol proposals for a tentative next version of the protocol.
While cutting in half compute time is not something to sneer at, it’s only scratching the surface. The Michelson interpreter is currently impleted using so called “big-step semantic”. This is done to facilitate its implementation using the OCaml GADT which offers a high-level of confidence that the implementation is correct, at least in so far as types are concerned. If we relax the need to implement the interpreter in a GADT, a “small-step semantic” intepreter can be written. Such an interpreter can have a more efficient implementation than the big-step semantic interpeter by separating instructions which are purely computational (CAR/CDR) from the one that are effectful (CREATE_CONTRACT/BIG_MAP_GET) and have to be wrapped in a monad. A quick and dirty PoC of this (by Gabriel) can be found here.
Going beyond this transformation, the interpreter could be written to work direclty on the byte level as opposed to trying to represent the various data structure in Michelson programs as OCaml values.
These optimizations could yield a one or two order of magnitude gains, but they come at the cost of an interpreter who doesn’t have the GADT, which makes excluding impossible code branches harder to do in a provably type-safe manner.
Optimizing gas metering
Much of the overhead comes not from interpreting contracts but from computing the gas as the contract is executed. It may not sound like much, but a simple SWAP operation which should take merely a few CPU cycles involves at least one addition in order to take its gas cost into account and a comparison to ensure that the spent gas remains below the limit.
In comparison, metering the gas for a computing intensive operation like CHECK_SIGNATURE does not introduce much overhead, relatively speaking as the operation itself takes much longer than an addition and a comparison.
Introduce compound opcodes
Creating keyhold optimizations such as having an UNPAIR opcode (as opposed to DUP; CDR; SWAP; CAR) can save on gas metering costs. Likewise, the introduction of DIG and DUG in Babylon (by Suzanne from LIGO) permits some stack operation to happen much faster.
More opcodes are being introduced by Gabriel in MR#167, in particular opcodes dealing with records and sum types to quickly destructure and reform them.
Precompute gas costs
It may be possible to statically determine gas costs. For instance if a long stretch of Michelson code without any branching involved only operation costing a constant amount of gas, this can be detected at origination time, the contract can be annotated internally to reflect these computations. This would let the interpreter execute many operations in a row without having to count the gas at each step.
Prove a bound on gas metering cost at origination time
Zen protocol has a cool technique for handling gas cost. Rather than meter the cost of gas when executing a contract, it is required that any contract originated comes with a gas cost function which computes a bound on the contract’s executing time, given the inputs passed to the contract. What’s more, the contract must come with a formal proof that the gas cost function executes under a given gas bound and that the
contract itself will execute in a time bounded by the gas cost function. Zen Protocol does this all in F*, albeit in a slightly clunky way that requires compiling and loading libraries on the fly.
The approach however has many benefits: it completely dispenses from metering gas when contracts are executed which means they can be executed as fast as the hardware will tolerate. It can also dispense users from having to estimate the amount of gas they migh need. There are two main downsides: first, this requires every contract to come up with a formal proof which can be tedious. Second, a bound that can be statically proven to hold will always be more conservative than one computed dynamically.
One solution to the first issue is to propose a compiler which automatically weaves gas instrumentation inside of the contrat itself and uses that instrumentation to prove a bound (for example by having the contract choose to abort when it consummes more than a certain amount of gas). While this approach does completely address the first issues, it’s a bit of a cop out. If all users end up relying on adding instrumentation as part of the contract code itself to generate their proof, the overhead might be worse than if the instrumentation were handled by an interpreter!
Introduce a more efficiently interpreted VM
Another approach and a departure from the idea behind Michelson would be to introduce a more efficiently interpeted, lower-level virtual machine. Th obvious choice for this approach is WASM which is quickly becoming somewhat of a de facto standard across different projects in this space (NEAR, Polkadot, ETH 2.0, etc). WASM is designed to be largely deterministic and to be efficient to run, there are toolchains to compile to WASM, large sums of money are being spent every year by large tech companies to produce very fast and efficient interpreters, etc. If one is going to go the route of a low level VM, it’s the natural choice.
However, it is by no means obvious that this route worth taking (nor is it obvious that it shouldn’t be taken). A few important things could be lost by using such a VM. Michelson is high-level enough that reasonable proofs can be done about the behavior of programs written in it, even when the code is the output of a compiler such as LIGO or a language like SmartPy. By contrast, the analysis of contracts executing in WASM would have to be done based not on the code that actually lives on the chain but on the code it was compiled from. This is not necessarily an issue but this would require compilers to be deterministic and, ideally certified.
To place this in context, Ethereum has had the habit of linking the Solidity code (hosted on some service) to smart-contracts deployed on-chain alongside with the compiler version used. In theory it’s possible to check that the code on the chain matches the source code published by using the same compiler and comparing the output. However this only works if the compiler is deterministic that is, if it always produce the same output given the same input. This may sound trivial but very few compilers actually achieve this. In practice when the DAO hack happened, it was very hard to find out which version of the DAO was actually running on the Ethereum chain as the Solidity compiler at the time was not deterministic. Even then, it’s not necessarily sufficient to be comfortable that the code was indeed compiled from a correct program, one would generally want to know that the code on the chain has the exact same semantic as the one expressed in the high-level program — in other words, we want to be highly confident that the compiler does not introduce its own bugs in the code. This is what a certified compiler achieves. Certified compilers have been built before, but it’s no small task!
Assuming having a WASM target is desirable, there are different ways in which a WASM VM could be integrated in Tezos.
Replace the Michelson interpreter altogether
In this approach, a Michelson to WASM compiler (ideally a certified compiler) would port all existing Michelson contracts to WASM and replace them on the chain on the fly through a protocol upgrade. At that points, contracts could be deployed directly using WASM code (including some “system” calls to access the context for example). Michelson would then take on a new life not as a VM but as compiled language. It’s the most radical, least “iterative” option but it’s also a clean cut.
Maintain interpeters side by side
The Michelson interpeter could be maintained as is but it would be possible to also originate contracts in WASM. Typed interfaces between contracts would be maintained to ensure interoperability. In this scenario, a Michelson to WASM compiler can also be introduced but would not be necessary though some compiler from some language would be necessary.
Sander (LIGO) is exploring those alternatives, and has written about it on this post.
Introduce WASM code in lambdas
In this approach, Michelson is kept as is, but it becomes possible to create lambda values by providing a piece of wasm code. This maintains everything intact but a contract designer could choose to keep Michelson only “at the edges” while implementing much of the logic inside lambdas constructed from compiled WASM code. This last approach is a total platypus, but it’s also a safer, if more cumbersome, way to experiment with WASM.
I thank Gabriel, Benjamin, and many others for discussions on the matter.
