本文由幣乎社區(qū)（bihu.com）內(nèi)容支持計(jì)劃獎(jiǎng)勵(lì)十酣。
Runtime Verification (RV)很自豪的發(fā)布了他們第一個(gè)版本的IELE寻拂，區(qū)塊鏈的一個(gè)新虛擬機(jī)佛南。
什么是IELE晃酒？
IELE是 LLVM 的一個(gè)變種故源，專門用于在區(qū)塊鏈上執(zhí)行智能合約。它的設(shè)計(jì)账千、定義以及實(shí)現(xiàn)都是在最高的數(shù)學(xué)標(biāo)準(zhǔn)下完成的侥蒙，遵循語(yǔ)義優(yōu)先的方式，以驗(yàn)證智能合約為主要目標(biāo)蕊爵。具體來(lái)說(shuō)辉哥，我們使用 K 架構(gòu)定義了IELE正式的語(yǔ)法和語(yǔ)義，這不僅給我們提供了一系列的程序分析工具包括程序驗(yàn)證器攒射，還提供了一個(gè)可執(zhí)行的參考模型醋旦。K 是由我們的團(tuán)隊(duì)在過去15年中創(chuàng)建出來(lái)的，它將語(yǔ)言設(shè)計(jì)会放，語(yǔ)義和形式化方法融入了現(xiàn)代藝術(shù)饲齐。 IELE的設(shè)計(jì)是建立一定的經(jīng)驗(yàn)之上的，該經(jīng)驗(yàn)就是我們用 K 正式定義了幾十種語(yǔ)言咧最，特別是用 K 語(yǔ)言正式定義了兩種其他虛擬機(jī)的近期經(jīng)驗(yàn)捂人，即：
與基于棧的EVM不同捣鲸，IELE是基于寄存器的機(jī)器瑟匆，就像LLVM。它支持無(wú)限的寄存器以及無(wú)界整數(shù)栽惶。為了感受一下IELE程序看起來(lái)是什么樣子的愁溜，這里有兩個(gè)程序（這些還沒有被驗(yàn)證，可能會(huì)改變）：
- erc20.iele — 一個(gè)ERC20代幣 IELE的實(shí)現(xiàn)
- forwardingWallet.iele — 一個(gè)可以創(chuàng)建和調(diào)用其他合約的錢包實(shí)現(xiàn)
設(shè)計(jì)原理
以下是推動(dòng) IELE設(shè)計(jì)的因素：
想成為將高級(jí)語(yǔ)言的智能合約翻譯并執(zhí)行的統(tǒng)一外厂、低級(jí)平臺(tái)冕象。合約可以使用ABI的方法進(jìn)行交互。ABI是IELE的核心元素汁蝶，而不僅僅只是個(gè)公約渐扮。無(wú)界整數(shù)和無(wú)限的寄存器應(yīng)該可以讓高級(jí)語(yǔ)言的編譯更加的直接和優(yōu)雅，并且看看LLVM的成功，從長(zhǎng)遠(yuǎn)來(lái)看更加的高效墓律。事實(shí)上意荤，LLVM的很多優(yōu)化將會(huì)繼續(xù)下去。因此只锻，IELE會(huì)盡可能的跟隨LLVM的設(shè)計(jì)選擇和表現(xiàn)。團(tuán)隊(duì)還包括了來(lái)自Illinois大學(xué)（LLVM的創(chuàng)造地）的LLVM專家紫谷。
為所有語(yǔ)言提供一個(gè)統(tǒng)一的gas模型齐饮。IELE中g(shù)as計(jì)算的一般思想是“沒有限制，但是你消耗多少就需要支付多少”艺挪。例如赴邻，一個(gè)IELE程序使用的寄存器越多舅柜，gas消耗的也會(huì)越多∞嗥В或者在運(yùn)行期計(jì)算的數(shù)字越大，消耗的gas越多崇裁。使用的內(nèi)存越多匕坯，根據(jù)位置和存儲(chǔ)在位置上數(shù)據(jù)的大小，消耗的gas也越多拔稳，等等葛峻。
為了讓編寫安全的智能合約更加的簡(jiǎn)單。這包括編寫智能合約必須要遵守的需求規(guī)范巴比，同樣也使得開發(fā)自動(dòng)化技術(shù)更加的容易术奖，該自動(dòng)化技術(shù)以數(shù)學(xué)方式驗(yàn)證/證明智能合約就此類規(guī)范是正確的。例如轻绞，在當(dāng)前智能合約的規(guī)范下采记，將一個(gè)可能計(jì)算的數(shù)字壓入棧中，然后跳轉(zhuǎn)到它的地址政勃，這樣讓驗(yàn)證變得非常的困難唧龄，從而也使得安全性變?nèi)酢ELE和LLVM一樣稼病，命名了標(biāo)簽选侨，跳轉(zhuǎn)語(yǔ)句只能跳轉(zhuǎn)到這些標(biāo)簽。而且然走，它還避免了使用有界的堆棧援制，因此就不用擔(dān)心堆棧和算術(shù)溢出問題，這讓智能合約的規(guī)范和驗(yàn)證變得容易了很多芍瑞。
就像 KEVM 一樣晨仑，我們之前定義的EVM的正式語(yǔ)義，是使用 K 架構(gòu)進(jìn)行驗(yàn)證和評(píng)估的，IELE的設(shè)計(jì)也同樣使用 K 架構(gòu)且基于語(yǔ)義的風(fēng)格洪己。加上目前還在開發(fā)的快速執(zhí)行 K 后端妥凳，預(yù)計(jì)從IELE語(yǔ)義中自動(dòng)獲得的解釋器將會(huì)成為IELE實(shí)現(xiàn)的有效參考。
下一步是什么答捕？
為了充分發(fā)揮 IELE的潛力逝钥，我們計(jì)劃下一步該做的事情：
K 的高效后端。然后是 K 的語(yǔ)義拱镐，包括IELE艘款，都可以在一個(gè)可接收的性能下被執(zhí)行。正如我們?cè)贙EVM白皮書討論的那樣沃琅，當(dāng)前版本的 K 可以執(zhí)行EVM的語(yǔ)義哗咆，性能與C++實(shí)現(xiàn)的EVM參考的性能在一個(gè)數(shù)量級(jí)之內(nèi)。如果能做到的話益眉，那么就沒有動(dòng)機(jī)以特殊的方式來(lái)實(shí)現(xiàn)IELE：K 可執(zhí)行的IELE語(yǔ)義也會(huì)成為它的實(shí)現(xiàn)晌柬，所以它的構(gòu)建是正確的，因此VM本身的實(shí)現(xiàn)缺點(diǎn)就不能被利用了郭脂。并且年碘，IELE本身會(huì)更容易維護(hù)一點(diǎn)，未來(lái)版本也更容易部署一點(diǎn)朱庆。
從Solidity和Plutus到IELE的編譯器/翻譯器盛泡。直接在IELE中編寫智能合約比直接在EVM中編寫智能合約的可行性要稍微高一點(diǎn)，因?yàn)?IELE是跟隨LLVM IR的娱颊，LLVM IR的設(shè)計(jì)是人類可讀的傲诵，但是 IELE 的代碼仍然是低級(jí)語(yǔ)言的，因此容易出錯(cuò)箱硕。為了正確的測(cè)試IELE并獲得對(duì)其整體設(shè)計(jì)和功能的信心拴竹，我們將會(huì)實(shí)現(xiàn)一個(gè)從Solidity到IELE的編譯器/翻譯器，也是使用K剧罩。因?yàn)?a target="_blank" rel="nofollow">Plutus在智能合約的函數(shù)式編程語(yǔ)言中成為明星栓拜，而且我們也定義了Plutus正式語(yǔ)義，所以Plutus到IELE 的編譯器會(huì)在Solidity之后立即開發(fā)惠昔。
基于語(yǔ)義的編譯幕与。除了提升 K 的性能之外，我們還計(jì)劃實(shí)現(xiàn)一個(gè)工具镇防，該工具建立在 K 之上啦鸣，我們稱它為基于語(yǔ)義的編譯器。請(qǐng)看我們前一篇博客文章了解更多細(xì)節(jié)来氧。它的思想就是使用一個(gè)編程語(yǔ)言語(yǔ)義L和用L編程的程序P诫给，然后生成（使用大量符號(hào)執(zhí)行）一個(gè)新的語(yǔ)言語(yǔ)義L'香拉，L‘就是P的專用L。我們預(yù)期性能至少有一個(gè)數(shù)量級(jí)的增加中狂。更重要的是凫碌，這會(huì)讓我們擁有一個(gè)統(tǒng)一的機(jī)制將任何擁有K語(yǔ)義的程序語(yǔ)言的任何程序翻譯成IELE，因此讓IELE和 K 成為使用任何語(yǔ)言執(zhí)行智能合約的通用平臺(tái)胃榕。
在Cardano區(qū)塊鏈上部署IELE盛险。
技術(shù)細(xì)節(jié)和下載
IELE擁有UIUC許可證（類似MIT許可證），它可以自由評(píng)論以及在Github上可以免費(fèi)獲妊帧：
除了上面提到的兩個(gè)IELE程序 erc20.iele和forwardingWallet.iele可以顯示IELE代碼是人類可讀的之外枉层，下面github倉(cāng)庫(kù)的鏈接也可以讓你感受一下什么是IELE以及它與EVM和LLVM的區(qū)別：
- iele-syntax.md—IELE語(yǔ)言完整的正式語(yǔ)義
- iele.md—IELE語(yǔ)言完整的正式可執(zhí)行語(yǔ)義
- Design.md—IELE設(shè)計(jì)原理，也是與LLVM和EVM比較的細(xì)節(jié)
- iele-gas.md—IELE的當(dāng)前gas模型（在我們開發(fā)IELE編譯器的時(shí)候仍然需要調(diào)整）
進(jìn)行參與
本著開源赐写、社區(qū)主導(dǎo)的發(fā)展精神，我們將會(huì)在我們的渠道上進(jìn)行所有的IELE討論：
我們鼓勵(lì)任何感興趣的人來(lái)找我們膜赃，提出問題挺邀、貢獻(xiàn)代碼或使用我們的工具進(jìn)行熟悉。我們也一直在尋找能夠處理文檔的貢獻(xiàn)者跳座，為新開發(fā)人員提供有效的安裝/快速啟動(dòng)過程端铛，以及更多的示例和測(cè)試。 我們正在招聘疲眷，并將保持對(duì)有幫助的貢獻(xiàn)者的留意禾蚕。
我們也將會(huì)在我們新的Twitter頁(yè)@rv_inc發(fā)表我們的更新，希望任何感興趣的開發(fā)者follow我們以及互動(dòng)狂丝。
讓我們一起為所有人建立一個(gè)更加安全的智能合約换淆。
致謝
我們熱烈地感謝IOHK對(duì)IELE和KEVM的慷慨資助。 尤其是IELE几颜，如果沒有IOHK的支持倍试，它的持續(xù)研究會(huì)議，以及與研究團(tuán)隊(duì)的激烈技術(shù)討論蛋哭，IELE將是不可能會(huì)實(shí)現(xiàn)的县习。
我們同樣感謝 K 團(tuán)隊(duì)，他們定義了KEVM語(yǔ)義（參見技術(shù)報(bào)告）并驗(yàn)證了ERC20合規(guī)性的智能合約谆趾。他們?cè)贓VM層面的努力和不平凡的證明引導(dǎo)了尋求新的虛擬機(jī)躁愿，能夠更好地支持智能合同驗(yàn)證的新虛擬機(jī)。
翻譯作者: 許莉
原文地址: IELE: A New Virtual Machine for the Blockchain
