IELE：區塊鏈的一個新虛擬機器
本文由幣乎社群（bihu.com）內容支援計劃獎勵。
Runtime Verification (RV)很自豪的釋出了他們第一個版本的IELE，區塊鏈的一個新虛擬機器。
什麼是IELE？
IELE是 LLVM
的一個變種，專門用於在區塊鏈上執行智慧合約。它的設計、定義以及實現都是在最高的數學標準下完成的，遵循語義優先的方式，以驗證智慧合約為主要目標。具體來說，我們使用 K 架構定義了IELE正式的語法和語義，這不僅給我們提供了一系列的程式分析工具包括程式驗證器，還提供了一個可執行的參考模型。K 是由我們的團隊在過去15年中創建出來的，它將語言設計，語義和形式化方法融入了現代藝術。 IELE的設計是建立一定的經驗之上的，該經驗就是我們用 K 正式定義了
與基於棧的EVM不同，IELE是基於暫存器的機器，就像LLVM。它支援無限的暫存器以及無界整數。為了感受一下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 成為使用任何語言執行智慧合約的通用平臺。
-
在Cardano區塊鏈上部署IELE。
技術細節和下載
IELE擁有UIUC許可證（類似MIT許可證），它可以自由評論以及在Github上可以免費獲取：
除了上面提到的兩個IELE程式 erc20.iele和forwardingWallet.iele可以顯示IELE程式碼是人類可讀的之外，下面github倉庫的連結也可以讓你感受一下什麼是IELE以及它與EVM和LLVM的區別：
- iele.md—IELE語言完整的正式可執行語義
- Design.md—IELE設計原理，也是與LLVM和EVM比較的細節
- iele-gas.md—IELE的當前gas模型（在我們開發IELE編譯器的時候仍然需要調整）
進行參與
本著開源、社群主導的發展精神，我們將會在我們的渠道上進行所有的IELE討論：
我們鼓勵任何感興趣的人來找我們，提出問題、貢獻程式碼或使用我們的工具進行熟悉。我們也一直在尋找能夠處理文件的貢獻者，為新開發人員提供有效的安裝/快速啟動過程，以及更多的示例和測試。 我們正在招聘，並將保持對有幫助的貢獻者的留意。
我們也將會在我們新的Twitter頁@rv_inc發表我們的更新，希望任何感興趣的開發者follow我們以及互動。
讓我們一起為所有人建立一個更加安全的智慧合約。
致謝
我們熱烈地感謝IOHK對IELE和KEVM的慷慨資助。 尤其是IELE，如果沒有IOHK的支援，它的持續研究會議，以及與研究團隊的激烈技術討論，IELE將是不可能會實現的。
我們同樣感謝 K 團隊，他們定義了KEVM語義（參見技術報告）並驗證了ERC20合規性的智慧合約。他們在EVM層面的努力和不平凡的證明引導了尋求新的虛擬機器，能夠更好地支援智慧合同驗證的新虛擬機器。