基于一种专门用于在区块链上执行智能合约的IELE虚拟机介绍

Runtime Verification （RV）很自豪的发布了他们第一个版本的IELE，区块链的一个新虚拟机。

什么是IELE？

IELE是 LLVM 的一个变种，专门用于在区块链上执行智能合约。它的设计、定义以及实现都是在最高的数学标准下完成的，遵循语义优先的方式，以验证智能合约为主要目标。具体来说，我们使用 K 架构定义了IELE正式的语法和语义，这不仅给我们提供了一系列的程序分析工具包括程序验证器，还提供了一个可执行的参考模型。K 是由我们的团队在过去15年中创建出来的，它将语言设计，语义和形式化方法融入了现代艺术。 IELE的设计是建立一定的经验之上的，该经验就是我们用 K 正式定义了几十种语言，特别是用 K 语言正式定义了两种其他虚拟机的近期经验，即：

KEVM，我们 EVM 的语义

KLLVM，我们 LLVM 的语义；LLVM语义的最新版本会在LLVM完成并发布后公布，不过早期版本在这里可获取

与基于栈的EVM不同，IELE是基于寄存器的机器，就像LLVM。它支持无限的寄存器以及无界整数。为了感受一下IELE程序看起来是什么样子的，这里有两个程序（这些还没有被验证，可能会改变）：

erc20.iele — 一个ERC20代币 IELE的实现

forwardingWallet.iele — 一个可以创建和调用其他合约的钱包实现

设计原理

以下是推动 IELE设计的因素：

想成为将高级语言的智能合约翻译并执行的统一、低级平台。合约可以使用ABI的方法进行交互。ABI是IELE的核心元素，而不仅仅只是个公约。无界整数和无限的寄存器应该可以让高级语言的编译更加的直接和优雅，并且看看LLVM的成功，从长远来看更加的高效。事实上，LLVM的很多优化将会继续下去。因此，IELE会尽可能的跟随LLVM的设计选择和表现。团队还包括了来自Illinois大学（LLVM的创造地）的LLVM专家。

为所有语言提供一个统一的gas模型。IELE中gas计算的一般思想是“没有限制，但是你消耗多少就需要支付多少”。例如，一个IELE程序使用的寄存器越多，gas消耗的也会越多。或者在运行期计算的数字越大，消耗的gas越多。使用的内存越多，根据位置和存储在位置上数据的大小，消耗的gas也越多，等等。

为了让编写安全的智能合约更加的简单。这包括编写智能合约必须要遵守的需求规范，同样也使得开发自动化技术更加的容易，该自动化技术以数学方式验证/证明智能合约就此类规范是正确的。例如，在当前智能合约的规范下，将一个可能计算的数字压入栈中，然后跳转到它的地址，这样让验证变得非常的困难，从而也使得安全性变弱。IELE和LLVM一样，命名了标签，跳转语句只能跳转到这些标签。而且，它还避免了使用有界的堆栈，因此就不用担心堆栈和算术溢出问题，这让智能合约的规范和验证变得容易了很多。

就像 KEVM 一样，我们之前定义的EVM的正式语义，是使用 K 架构进行验证和评估的，IELE的设计也同样使用 K 架构且基于语义的风格。加上目前还在开发的快速执行 K 后端，预计从IELE语义中自动获得的解释器将会成为IELE实现的有效参考。

下一步是什么？

为了充分发挥 IELE的潜力，我们计划下一步该做的事情：

K 的高效后端。然后是 K 的语义，包括IELE，都可以在一个可接收的性能下被执行。正如我们在KEVM白皮书讨论的那样，当前版本的 K 可以执行EVM的语义，性能与C++实现的EVM参考的性能在一个数量级之内。如果能做到的话，那么就没有动机以特殊的方式来实现IELE：K 可执行的IELE语义也会成为它的实现，所以它的构建是正确的，因此VM本身的实现缺点就不能被利用了。并且，IELE本身会更容易维护一点，未来版本也更容易部署一点。

从Solidity和Plutus到IELE的编译器/翻译器。直接在IELE中编写智能合约比直接在EVM中编写智能合约的可行性要稍微高一点，因为 IELE是跟随LLVM IR的，LLVM IR的设计是人类可读的，但是 IELE 的代码仍然是低级语言的，因此容易出错。为了正确的测试IELE并获得对其整体设计和功能的信心，我们将会实现一个从Solidity到IELE的编译器/翻译器，也是使用K。因为Plutus在智能合约的函数式编程语言中成为明星，而且我们也定义了Plutus正式语义，所以Plutus到IELE 的编译器会在Solidity之后立即开发。

基于语义的编译。除了提升 K 的性能之外，我们还计划实现一个工具，该工具建立在 K 之上，我们称它为基于语义的编译器。请看我们前一篇博客文章了解更多细节。它的思想就是使用一个编程语言语义L和用L编程的程序P，然后生成（使用大量符号执行）一个新的语言语义L’，L‘就是P的专用L。我们预期性能至少有一个数量级的增加。更重要的是，这会让我们拥有一个统一的机制将任何拥有K语义的程序语言的任何程序翻译成IELE，因此让IELE和 K 成为使用任何语言执行智能合约的通用平台。