IELE’s gas model? Compilation process? Eight questions developers might be asking about Cardano’s smart contracts

Already working or planning to, on the IELE testnet? You might have some questions about gas model, compilation, languages supported, process of formal verification among other general questions.

Answered by Sebastien Guillemot, EMURGO Technical Manager.

Twitter: @SebastienGllmt

1. KEVM

Does KEVM use its own version of Solidity? Will all language compilers generated by K have their own specific version of the language assuming they already have hand-written compilers?

Solidity on the KEVM is meant to be backwards compatible with Solidity on the EVM. The compiler for Solidity should be the same as the bytecode is the same. However the gas costs between the two is different so you have to be careful.

2. Uniformed gas model

What does a “uniform gas model” mean? If a language has a compiler for IELE does this mean the cost of gas for each operation in that language can be defined in IELE?

It means the gas cost is defined in terms of the IELE Intermediate Representation. Any language you make that compiles down to IELE will use the IELE IR and therefore use the same gas model.

3. GAS price

In examples shown on Solidity on the IELE testnet the gas price was in ether, e.g. https://www.youtube.com/watch?v=jz5gu4keU9U

If we wanted to use Ada instead would we have to use a specific language, say Plutus? Or will it just depend on how the gas model is defined in IELE? Are there specific tie ins between certain languages and cryptocurrencies used for gas prices, e.g. Solidity and ether, Plutus and Ada?

The testnet runs on ETC because it is easier to setup that way. In the future it will run on the mainnet and use ADA.

4. Compiler

If we write a compiler to compile a language to LLVM intermediate representation (IR) and then write an analysis & optimization layer for different architectures such as x86, ARM, etc., when we write another compiler for a different language to compile to LLVM IR would we be able to use the same analysis & optimization layer? Or would we somewhat have to tweak it to adapt it to the new language?

It would be the same.

5. Difference in Syntax of Plutus and Plutus core

How different is the syntax of Plutus from Plutus Core? What was the reason Plutus was not made to compile directly to IELE but to another intermediate representation layer (Plutus Core)?

Plutus Core supports a very minimal syntax but the full details aren’t decided/published yet. With Plutus Core you can update Plutus quicker without having to modify other languages that may depend on the much simpler Plutus Core.

6. IELE testnet and how it can be compiled

Is Solidity compiled to Plutus Core or directly to IELE when using the IELE testnet? Is Plutus Core geared toward functional languages only?

Plutus and Plutus core aren’t done yet. Solidity compiles straight to IELE. It is not the same Solidity as in the EVM though as in IELE some opcodes are not the same (changed or removed) and therefore Solidity had to be modified also.

7. LLVM

Which project is working on building the IELE representation to run on LLVM? Is it an IOHK or a Runtime Verification (RV) project?

It’s a RV project. They are building a LLVM backend for the K-Framework which is what is used to generate IELE.

8. Process of formal verification

Formally verifying smart contracts to find security and functional correctness flaws seems like a non-trivial exercise (runtime verification commercializes it). Would it be true if we said that by running Solidity smart contracts on KEVM or IELE (correct by construction virtual machines) there are still no guarantees about the correctness of the contract unless it went to some type of formal verification process? In what other aspects would it be more secure or have better assurance than running it on the EVM?

KEVM removes some ambiguity in the yellow paper of Ethereum and less likely to have any bugs so it is safer in that regard.

IELE removes some dangerous constructs that were present in the EVM so it should remove a lot of common bugs (like integer overflow, calling library contracts, etc).

However, it is true that in general you will need extra work to verify your smart contract. Even if you don’t want to spend the time/money verifying your own smart contract, you can still benefit by complying to known standards that are verified. For example, you could run your contract against the formal specification of an ERC-20 smart contract.

Author: Sebastien Guillemot