DeepSEA Version 1.1 Release

Originally published
October 21, 2020

Here at CertiK everybody is excited for the mainnet launch, which will happen in only a few days on Oct. 24 (10:24am ET). But before that, we have one more announcement for you: version 1.1 of the DeepSEA compiler. You can download the executable and examples from the github releases page.

There are two major improvements in this release. First, the WebAssembly backend is now complete, with all of DeepSEA’s language features supported. Second, the backend part of the compiler is now a stand-alone library that you can use in your own projects.

Ethereum 2.0 Style WebAssembly Full Support on CertiK Chain

In DeepSEA’s 1.0 release, the Ethereum WebAssembly support was limited to operations that do not involve hashing (i.e., all operations excluding arrays, structs, keccak256 direct calls, events). In this release, we are completing those features. We have also integrated DeepSEA’s WebAssembly backend to CertiK Chain’s CVM (by supporting a majority of the Ethereum Environment Interfaces as host functions). You can now deploy a DeepSEA WebAssembly contract to the Shentu testnet by using the `--ewasm` flag in `certikcli deploy` command. Additionally, you can use the `--runtime` flags to indicate if the contract you are deploying contains any initialization code.

Below is an example of running a multi-layer contract in DeepSEA with Ethereum 2.0 type WebAssembly:

Stand-alone Compiler Backend

The other exciting improvement is we now release the DeepSEA compiler backend as a separate software component which can be used to create compilers for other programming languages. Like many other compilers, the DeepSEA implementation is divided into a front-end and a back-end. The front-end handles parsing, type checking, mapping from abstract data types to concrete representations, and DeepSEA-specific concepts like objects and layers. It translates the program into a simpler intermediate language which we call MiniC. The backend then translates the MiniC program into either EVM or eWasm. 

While DeepSEA is designed in a quite opinionated way, based on our ideas about how to do formal verification, the MiniC language is much more conventional. As the name suggests it is similar to a simplified version of the C programming language, and it should be quite suitable for compiling all kinds of languages. Using the DeepSEA backend is much easier than directly generating EVM bytecode, and because it is formally verified, compilers based on it are less likely to have bugs and the users can be more confident that it works correctly.

The DeepSEA 1.1 release includes two versions of the backend. First, there is a stand-alone program to compile MiniC programs from the command line. Second, we provide the same backend as a set of OCaml files which can be directly linked into any OCaml program, which is convenient if your compiler is written in OCaml. For more details about the MiniC language and how to use the compiler backend, please see the Reference Manual.

Finally, as an example of using the backend, we include a new programming language for writing Ethereum smart contracts called OpenSC. This language was created as a group project in an introduction to compilers class at Columbia University, and the students graciously allowed us to publish it. As you can see from reading the documentation, OpenSC is completely different from DeepSEA, and yet the implementation is able to use the DeepSEA backend. We hope that this can be an inspiration for people everywhere who are interested in writing their own blockchain programming languages---it’s not hard to get started.