區(qū)塊鏈的一個新虛擬機“IELE”可執(zhí)行智能合約

Runtime Verification （RV）很自豪的發(fā)布了他們第一個版本的IELE，區(qū)塊鏈的一個新虛擬機。

什么是IELE？

IELE是 LLVM 的一個變種，專門用于在區(qū)塊鏈上執(zhí)行智能合約。它的設(shè)計、定義以及實現(xiàn)都是在最高的數(shù)學標準下完成的，遵循語義優(yōu)先的方式，以驗證智能合約為主要目標。具體來說，我們使用 K 架構(gòu)定義了IELE正式的語法和語義，這不僅給我們提供了一系列的程序分析工具包括程序驗證器，還提供了一個可執(zhí)行的參考模型。K 是由我們的團隊在過去15年中創(chuàng)建出來的，它將語言設(shè)計，語義和形式化方法融入了現(xiàn)代藝術(shù)。 IELE的設(shè)計是建立一定的經(jīng)驗之上的，該經(jīng)驗就是我們用 K 正式定義了幾十種語言，特別是用 K 語言正式定義了兩種其他虛擬機的近期經(jīng)驗，即：

KEVM，我們 EVM 的語義

KLLVM，我們 LLVM 的語義；LLVM語義的最新版本會在LLVM完成并發(fā)布后公布，不過早期版本在這里可獲取

與基于棧的EVM不同，IELE是基于寄存器的機器，就像LLVM。它支持無限的寄存器以及無界整數(shù)。為了感受一下IELE程序看起來是什么樣子的，這里有兩個程序（這些還沒有被驗證，可能會改變）：

erc20.iele — 一個ERC20代幣 IELE的實現(xiàn)

forwardingWallet.iele — 一個可以創(chuàng)建和調(diào)用其他合約的錢包實現(xiàn)

設(shè)計原理

以下是推動 IELE設(shè)計的因素：

想成為將高級語言的智能合約翻譯并執(zhí)行的統(tǒng)一、低級平臺。合約可以使用ABI的方法進行交互。ABI是IELE的核心元素，而不僅僅只是個公約。無界整數(shù)和無限的寄存器應該可以讓高級語言的編譯更加的直接和優(yōu)雅，并且看看LLVM的成功，從長遠來看更加的高效。事實上，LLVM的很多優(yōu)化將會繼續(xù)下去。因此，IELE會盡可能的跟隨LLVM的設(shè)計選擇和表現(xiàn)。團隊還包括了來自Illinois大學（LLVM的創(chuàng)造地）的LLVM專家。

為所有語言提供一個統(tǒng)一的gas模型。IELE中g(shù)as計算的一般思想是“沒有限制，但是你消耗多少就需要支付多少”。例如，一個IELE程序使用的寄存器越多，gas消耗的也會越多?；蛘咴谶\行期計算的數(shù)字越大，消耗的gas越多。使用的內(nèi)存越多，根據(jù)位置和存儲在位置上數(shù)據(jù)的大小，消耗的gas也越多，等等。

為了讓編寫安全的智能合約更加的簡單。這包括編寫智能合約必須要遵守的需求規(guī)范，同樣也使得開發(fā)自動化技術(shù)更加的容易，該自動化技術(shù)以數(shù)學方式驗證/證明智能合約就此類規(guī)范是正確的。例如，在當前智能合約的規(guī)范下，將一個可能計算的數(shù)字壓入棧中，然后跳轉(zhuǎn)到它的地址，這樣讓驗證變得非常的困難，從而也使得安全性變?nèi)酢ELE和LLVM一樣，命名了標簽，跳轉(zhuǎn)語句只能跳轉(zhuǎn)到這些標簽。而且，它還避免了使用有界的堆棧，因此就不用擔心堆棧和算術(shù)溢出問題，這讓智能合約的規(guī)范和驗證變得容易了很多。

就像 KEVM 一樣，我們之前定義的EVM的正式語義，是使用 K 架構(gòu)進行驗證和評估的，IELE的設(shè)計也同樣使用 K 架構(gòu)且基于語義的風格。加上目前還在開發(fā)的快速執(zhí)行 K 后端，預計從IELE語義中自動獲得的解釋器將會成為IELE實現(xiàn)的有效參考。

下一步是什么？

為了充分發(fā)揮 IELE的潛力，我們計劃下一步該做的事情：

K 的高效后端。然后是 K 的語義，包括IELE，都可以在一個可接收的性能下被執(zhí)行。正如我們在KEVM白皮書討論的那樣，當前版本的 K 可以執(zhí)行EVM的語義，性能與C++實現(xiàn)的EVM參考的性能在一個數(shù)量級之內(nèi)。如果能做到的話，那么就沒有動機以特殊的方式來實現(xiàn)IELE：K 可執(zhí)行的IELE語義也會成為它的實現(xiàn)，所以它的構(gòu)建是正確的，因此VM本身的實現(xiàn)缺點就不能被利用了。并且，IELE本身會更容易維護一點，未來版本也更容易部署一點。

從Solidity和Plutus到IELE的編譯器/翻譯器。直接在IELE中編寫智能合約比直接在EVM中編寫智能合約的可行性要稍微高一點，因為 IELE是跟隨LLVM IR的，LLVM IR的設(shè)計是人類可讀的，但是 IELE 的代碼仍然是低級語言的，因此容易出錯。為了正確的測試IELE并獲得對其整體設(shè)計和功能的信心，我們將會實現(xiàn)一個從Solidity到IELE的編譯器/翻譯器，也是使用K。因為Plutus在智能合約的函數(shù)式編程語言中成為明星，而且我們也定義了Plutus正式語義，所以Plutus到IELE 的編譯器會在Solidity之后立即開發(fā)。

基于語義的編譯。除了提升 K 的性能之外，我們還計劃實現(xiàn)一個工具，該工具建立在 K 之上，我們稱它為基于語義的編譯器。請看我們前一篇博客文章了解更多細節(jié)。它的思想就是使用一個編程語言語義L和用L編程的程序P，然后生成（使用大量符號執(zhí)行）一個新的語言語義L’，L‘就是P的專用L。我們預期性能至少有一個數(shù)量級的增加。更重要的是，這會讓我們擁有一個統(tǒng)一的機制將任何擁有K語義的程序語言的任何程序翻譯成IELE，因此讓IELE和 K 成為使用任何語言執(zhí)行智能合約的通用平臺。

在Cardano區(qū)塊鏈上部署IELE。

技術(shù)細節(jié)和下載

IELE擁有UIUC許可證（類似MIT許可證），它可以自由評論以及在Github上可以免費獲取：

Github上IELE的倉庫

除了上面提到的兩個IELE程序 erc20.iele和forwardingWallet.iele可以顯示IELE代碼是人類可讀的之外，下面github倉庫的鏈接也可以讓你感受一下什么是IELE以及它與EVM和LLVM的區(qū)別：

iele-syntax.md—IELE語言完整的正式語義

iele.md—IELE語言完整的正式可執(zhí)行語義

Design.md—IELE設(shè)計原理，也是與LLVM和EVM比較的細節(jié)

iele-gas.md—IELE的當前gas模型（在我們開發(fā)IELE編譯器的時候仍然需要調(diào)整）

進行參與

本著開源、社區(qū)主導的發(fā)展精神，我們將會在我們的渠道上進行所有的IELE討論：

#IELE:matrix.org on Riot

runtimeverification/iele-semantics on Gitter

我們鼓勵任何感興趣的人來找我們，提出問題、貢獻代碼或使用我們的工具進行熟悉。我們也一直在尋找能夠處理文檔的貢獻者，為新開發(fā)人員提供有效的安裝/快速啟動過程，以及更多的示例和測試。 我們正在招聘，并將保持對有幫助的貢獻者的留意。

我們也將會在我們新的Twitter頁@rv_inc發(fā)表我們的更新，希望任何感興趣的開發(fā)者follow我們以及互動。

讓我們一起為所有人建立一個更加安全的智能合約。