CertiK is proud to announce version 1.0 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 compiler is now complete enough to support practical smart contracts. Second, in addition to Ethereum 1.0 and the CertiK Chain, we have added experimental support for compiling to Ethereum 2.0 style WebAssembly.
Basic feature set complete
In January we released a “pre-alpha preview” of the compiler, which could compile programs but had some gaps left, and a language manual which described the planned basic feature set. In this release we have completed those outstanding items (e.g. events, keccak hashes, reading calldata…), so we finally support the entire language as described in the manual.
This is by no means the final version of the language, and we will continue to improve it, but this version can now be used to write some useful programs. For example, one of our example programs, Olive.ds, was inspired by a real ERC20 contract which was used to manage the coin offering of the Olive live streaming platform. We selected this example because it is one of the more complex ERC20 contracts that CertiK has audited, so the fact that DeepSEA supports the same functionality shows that it can handle most token contracts.
CertiK is proud to announce version 1.0 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 compiler is now complete enough to support practical smart contracts. Second, we have added two new compilation targets. In addition to Ethereum and the CertiK Chain, we now support writing contracts for Ant Financial’s AntChain, and have experimental support for compiling to Ethereum-flavored WebAssembly.
Basic feature set complete
In January we released a “pre-alpha preview” of the compiler, which could compile programs but had some gaps left, and a language manual which described the planned basic feature set. In this release we have completed those outstanding items (e.g. events, keccak hashes, reading calldata…), so we finally support the entire language as described in the manual.
This is by no means the final version of the language, and we will continue to improve it, but this version can now be used to write some useful programs. For example, one of our example programs, Olive.ds, was inspired by a real ERC20 contract which was used to manage the coin offering of the Olive live streaming platform. We selected this example because it is one of the more complex ERC20 contracts that CertiK has audited, so the fact that DeepSEA supports the same functionality shows that it can handle most token contracts.
For another example, CertiK is internally developing many smart contracts to support our Chain and security offerings, and we find that many of them are fully supported by the features that DeepSEA provides.
Future plans for the DeepSEA compiler
We will continue to add more language features to the compiler. In upcoming releases we will also add more target platforms to the backend, and provide support for loading contracts into an interactive theorem prover to prove them secure.
WebAssembly support
WebAssembly (WASM) has been trending in the blockchain industry for a while now. It seems likely to be the platform used by most smart contract languages in the future.
WASM first appeared in 2015 as a lightweight low-level language running in browser engines, and it has extensive tool support. Furthermore, WASM is designed with formal methods in mind: it has a formally defined execution semantics and a sound type system (validation rules). The type system ensures that if a WebAssembly program passes compilation, it will not exhibit any type errors or memory safety issues. The clearly-defined semantics make it easy to build verification frameworks and formally proven compilers, which makes WebAssembly an ideal target language for high-security smart contracts. Current WebAssembly blockchain users include Ethereum Foundation, Parity Technologies, Cosmos, and Hyperledger.
DeepSEA support for Ethereum WebAssembly
This release of DeepSEA introduces support for compiling to Ethereum WebAssembly (eWasm), the style of WASM used in the Ethereum 2.0 project. The difference between eWasm and the regular WASM we see in web browsers is that eWasm contracts follow a specific interface: they only export the memory section and a main function serving as the multiplexer for function calling, and they import the Ethereum External Interface (EEI) for Ethereum-specific features such as transfer, storage, events, etc. For other features like gas metering or hash functions (keccak256), eWasm uses a pre-compiled system contract deployed to a fixed address.
Because Ethereum 2.0 is still under development, the eWasm testnet and the keccak256 system contract are not available yet. Therefore, as of this moment, the DeepSEA eWasm backend cannot handle contracts that use hashing, which implies that features that make use of hashing do not work, (e.g. structs, mappings, and arrays).
The DeepSEA Wasm support is work in progress. Future releases will complete the eWasm implementation, and also add support for other Wasm flavors used by other blockchains.
Running a WebAssembly contract
To execute a WebAssembly contract, you only need to download the DeepSEA compiler and then use the `ewasm` option. Detailed information about usage is included in the DeepSEA reference manual. Here, we demonstrate a simple example, First, install the WebAssembly Binary Toolkit (WABT) by following the instructions on the WABT github repo. (If you are on MacOS, you can just type `brew install wabt`.) Then, we use DeepSEA to compile contracts. In this example, we compile a simple multiplication contract:
and run it on a Javascript virtual machine:
The contract calling convention is the same as Ethereum 1.0, where you pass the first 4 bytes of the keccak256-hash of the function you want to call. Here, we hard code the hash in JS script for simplicity. When compiling a custom contract, you can always change the hash for the function and fill in the right parameters.
AntChain support
Differences between the Ethereum and AntChain version
AntChain is compatible with EVM and Solidity, which lets us use the verified DeepSEA EVM backend to compile code for it. However, one important difference is the format of cryptographic identifiers. In Ethereum, users are identified by “addresses”, which are derived by first hashing an ECDSA public key using the Keccak-256 hash function (which is not standardized), and then truncating the result to 20 bytes. AntChain uses a different set of cryptographic primitives, and instead creates “identifiers” which are 32 bytes.
To handle this, we have created a new version of the DeepSEA compiler which lets the programmer use the keywordidentityinstead ofaddress, and treats these as 32 bytes instead of 20 bytes. The compiler can be downloaded from the DeepSEA preview repository [insert link here]. This release also includes an example contract and the javascript code to deploy it.
Running a contract on the AntChain
In order to deploy contracts to the AntChain testnet, users must have an enterprise level Alipay account. More information about how to apply for testnet access can be found in the Ant documentation [https://tech.antfin.com/docs/2/147534] (in Chinese).
Once you have access, one can use the AntChain SDK to deploy the contract. In this DeepSEA preview release we include an example deployment script and the user manual has detailed instructions for how to use it. We start by downloading the DeepSEA compiler preview from github.
Next, we go to the contracts/token_ant folder, which contains an example contract called token.ds and an example deployment script called token.js. We run the deepsea compiler on the contract to produce two files token.bytecode and token.abi.
We then use the token.js deployment script to deploy the contract to the chain. It needs to be edited by the user to put in their account information, and it’s also possible to edit it to experiment with calls to the contract. The key part of the script is the following lines, which takes the bytecode file produced above and sends it to the AntChain.
The console.log statement prints out a data object which contains msg_type, txhash, receipt and so on. We can record the txhash and later use that in AntChain explorer.
Moreover, inside the callback function, we can make calls to the contract. For example, a single call to the contract method totalsupply() would be like the code snippet below
As a final step, we can confirm that our contract was successfully deployed using the AntChain explorer. We log in to the BaaS platform of Ant and find the explorer search bar at the top-right.
Of course, this is only a simple example, and the Ant SDK provides further APIs to interact with the contract. [https://tech.antfin.com/docs/2/107127]
Future plans for DeepSEA/Ant support
Compiling contracts via EVM is only a first step. Although the AntChain is backwards compatible with EVM, the recommended way of deploying programs is by using the Ant-developed MYVM which offers better performance.
In the coming months, CertiK will develop a version of the DeepSEA compiler supporting the MYVM directly. Developing it involves developing a formal specification for the semantics of the MYVM virtual machine, and a backend generating MYVM code. So not only can third-parties use the DeepSEA language directly to write completely verified contracts, but programming language developers can reuse the backend to compile other programming languages in a secure way, and developers of verification tools can refer to the formalized semantics.
and run it on a Javascript virtual machine:
The contract calling convention is the same as Ethereum 1.0, where you pass the first 4 bytes of the keccak256-hash of the function you want to call. Here, we hard code the hash in JS script for simplicity. When compiling a custom contract, you can always change the hash for the function and fill in the right parameters.
