IELEVM

The IELE VM

• ☐ Compatible with the EVM?
• ☐ What kind of languages can be compiled to its bytecode?

The IELE VM is a process virtual machine designed to run SmartContracts and is currently the VM best supported by the Elrond Node.

IELE VM was created using the K Framework, a software project that automatically generates execution environments according to the formal definitions of a language. In other words, the source code of IELE VM has only been partially written by hand, because most of it (?) was generated by running the K Framework on the formal definition of the IELE bytecode. The result of this process is the Go package that builds into the IELE VM. For more details, see Creating the IELE VM.

The K Framework

According to its project page, the K Framework is "a rewrite-based executable semantic framework in which programming languages, type systems and formal analysis tools can be defined using configurations, computations and rules."

In simpler words, one generates an interpreter for their new programming language by defining it using K's formal rules, which K then uses to generate the source code of the interpreter. Note that the K Framework does not execute anything; instead, it is used to create the interpreter that executes code written in the desired programming language. Therefore, once the formal definition of the desired programming language has been written, the K Framework is used only once to generate the interpreter. Afterwards, one uses the generated interpreter only and must not be concern themselves with whether the interpreter was created by a source code generator or was written by hand.

Creating the IELE VM using K

In order to generate interpreters from formal definitions of programming languages, the K Framework needs to be able to write some source code itself. To do this, the K Framework has multiple backends, which are components that can write source code in a target progamming language. Elrond has created a backend for K that can generate Go source code from any formal definition.

The K Framework allows defining very complex languages. For example, one could write the formal rules that define a universal assembly language. When generating the interpreter from its definition, the K Framework effectively produces a Virtual Machine for us. A developer could then write programs in this low-level assembly language. Or better yet, write a program in a high-level language like C++, Solidity or JavaScript, which is then compiled to the low-level assembly language. The interpreter generated by K can then be used to execute the compiled form of the program. This is, in fact, what IELE VM is: an interpreter generated by K that executes a low-level assembly-like code, which was originally defined as formal rules.

As stated earlier, Elrond has developed a Go backend for the K Framework. The motivation for this effort was to use K to generate the IELE VM source code in the Go programming language, in order to make it easy to integrate with the Elrond Node, which is itself written in Go.