Cardano KEVM／IELE Testnet 相關參考資料

Cardano KEVM／IELE Testnet 相關參考資料：

（1）Cardano Testnet 官網：

KEVM：https://testnet.iohkdev.io/goguen/kevm/
IELE：https://testnet.iohkdev.io/goguen/iele/

註：IELE 以 LLVM 為模型：https://en.wikipedia.org/wiki/LLVM

（2）Faucet

KEVM Testnet Faucet：
a、https://testnet.iohkdev.io/goguen/kevm/faucet/
b、$ curl -X POST https://kevm-testnet.iohkdev.io:8099/faucet?address=0x00000000000000000000000000000000000001
c、mallet> requestFunds('0x00000000000000000000000000000000000001')

IELE Testnet Faucet：
a、https://testnet.iohkdev.io/goguen/iele/faucet/

（3）Mallet 指令列錢包下載
https://github.com/input-output-hk/mallet/releases

a、連線至 KEVM：

$ cd $HOME/mallet
$ ./mallet kevm

b、連線至 IELE：

$ cd $HOME/mallet
$ ./mallet iele

c、連線至私人網路：

$ cd $HOME/mallet
$ ./mallet https://kevm-testnet.iohkdev.io:8546
$ ./mallet https://iele-testnet.iohkdev.io:8546

（4）Mantis 下載
https://github.com/input-output-hk/mantis/releases

（5）Block Explorer

KEVM Testnet：https://testnet.iohkdev.io/goguen/kevm/explorer/
IELE Testnet：https://testnet.iohkdev.io/goguen/iele/explorer/

（6）Smart Contract Compiler 智能合約編譯器

KEVM Testnet：
https://remix.ethereum.org
https://github.com/runtimeverification/solidity/releases

IELE Testnet：
https://iele-testnet.iohkdev.io/remix
https://github.com/runtimeverification/solidity/tree/sol2iele/help

（7）其他資源：

Cardano Smart Contracts & VMs Explained：
IOHK | Research; Prof. Philip Wadler, Smart Contracts.：
IOHK | IELE Testnet - Smart Contracts in IELE：

（8）意思解釋（翻譯自官網）：

a、K：

．The KEVM testnet is based on the K framework, a system for specifying languages and virtual machines and then deriving tools for these languages such as interpreters, type checkers, equivalence checkers, and debuggers. It can be used to create both static and dynamic analysis tools.
．K Framework 是一個用於指定語言和指定 VM 的系統，然後成為這些語言的產生工具。如 Interpreter 解譯器，類型檢查器，等價檢查器和調試器。它也可用於創建靜態和動態分析工具。

．The K specification defines the formal semantics for elements such as the configuration and transition rules of EVM. The K framework provides the platform within which to work and also provides an executable.
．K 定義了元素的形式語義，例如 EVM 以太坊虛擬機的配置和轉換規則。K Framework 則提供了工作的平台，並提供了可執行的檔案。

．Semantics-based compilation (SBC) is one of the most challenging components of the K framework. Its goal is to automatically generate a correct by construction compiler by applying the semantics of a language to a program written in that language. The result is a new semantics that is a synthesis of the original semantics of the language but specialized for that particular program. The new semantics is simpler, faster to execute and easier to understand.
．基於語義的編譯器（SBC）是 K Framework 中最具挑戰性的組件之一。它的目標是透過將語言的語義應用至用該語言所撰寫的程式，自動生成構造編譯器。結果會是一種新的語義，它是語言原始語義的組合，但專門用於特定程式。新語義更簡單，執行更快，且更易於理解。

．The K framework has been developed by Grigore and Runtime Verification over 15 years. It is used in mission-critical applications – this is software that cannot afford to fail. To this end, Runtime Verification has worked with companies including Nasa, Boeing, and Toyota. His collaboration with IOHK began after he was contacted by Charles Hoskinson. The IOHK chief executive had spotted that the software vulnerabilities that had resulted in many hacks on blockchains and the draining of cryptocurrencies worth hundreds of millions of dollars, could have been prevented using the formal methods developed by Runtime Verification.
．K Framework 由 Grigore 和 Runtime Verification 開發超過 15 年。它用於任務關鍵型應用程式 - 這是一個無法承受失敗的軟體。為此，Runtime Verification 與包括美國宇航局，波音公司和豐田公司在內的公司合作。在與 Charles Hoskinson 聯繫後，便與 IOHK 開始合作。IOHK 首席執行官發現，使用執行時驗證開發的正式方法，可防止區塊鏈上的許多駭客攻擊，以及導致價值數億美元的加密貨幣耗盡的軟體漏洞。

b、Mallet：

．Mallet, the minimal wallet, is the command line interface used to send transactions, deploy smart contracts, and interact with the IELE and KEVM testnets.
．Mallet 是最小錢包，是用於發送事務，部署智能合約，以及與 IELE Testnets 和 KEVM Testnets 互動的指令列界面。

．On Linux and Mac, you will require Node.js 10.4.0, or the latest version, and the Git tools. For Windows, you will also need the Windows Subsystem for Linux (WSL).
．在 Linux 和 Mac 上，您將需要 Node.js 10.4.0 或最新版本以及 Git 工具。對於 Windows，您還需要 Windows 的 Linux 子系統（WSL）。

．There are two ways to interact with the IELE testnet and VM. One is the Remix integrated development environment (IDE), and the other is to use Mallet, the command line wallet program. Both connect to the IELE testnet and the Solidity compiler, and are functionality equivalent. The main difference is that Remix can be accessed through your web browser so there is no need to install anything on your computer, while Mallet and the compiler are text-based and need to be installed.
．有兩種方法可以與 IELE Testnet 和 VM 進行互動。一個是 Remix 集成開發環境（IDE），另一個是使用指令列錢包程序 Mallet。兩者都需連接到 IELE Testnet 和 Solidity 編譯器，並且功能相同。主要區別在於，Remix 可以透過 Web 瀏覽器訪問，因此無需在電腦上額外安裝任何軟體；而 Mallet 和編譯器則是基於 Text-Based 的，則需要額外安裝。

c、Mantis：

．The Mantis client creates the blockchain records in conjunction with the KEVM itself. This node is the base node from which the chain records are created.
．Mantis 客戶端節點與 KEVM 本身一起創建區塊鏈紀錄。此節點是創建區塊鏈紀錄中的基本節點。

．By default, the blockchain and all other files that are created by the Mantis node are stored in the user’s home folder under a sub folder called .mantis. This setting is found in the storage.conf file.
．預設情況下，Mantis 節點創建的區塊鏈和所有其他檔案都儲存在用戶主資料夾中，一個名為 .mantis 的子資料夾內。而設置則位於 storage.conf 檔案中。

．The KEVM testnet is implemented on Mantis, the standards-compliant Ethereum Classic client designed within the specification of the K framework.
．KEVM Testnet 在 Mantis上實現，Mantis 是符合標準的 Ethereum Classic 客戶端，在 K Framework 規範中設計出來。

．The Mantis client has been tested extensively on Ethereum Classic small instances with 2G of RAM. This is sufficient to run the client and the miner.
．Mantis 客戶端已經在具有 2G RAM 的 Ethereum Classic 以太坊經典小型實例上進行了廣泛測試。這足以運行客戶端和挖礦。

d、KEVM Testnet：

．The KEVM testnet is based on the K framework, a system for specifying languages and virtual machines and then deriving tools for these languages such as interpreters, type checkers, equivalence checkers, and debuggers. It can be used to create both static and dynamic analysis tools.
．KEVM Testnet 基於 K Framework。K Framework 是一個用於指定語言和指定 VM 的系統，然後成為這些語言的產生工具。如 Interpreter 解譯器，類型檢查器，等價檢查器和調試器。它也可用於創建靜態和動態分析工具。

．KEVM is a specification of the EVM (Etherium Virtual Machine) in K.
．KEVM 是 K 中對 EVM（Etherium VM）的規範。

．KEVM is also an interpreter for EVM, automatically derived from the KEVM specification. You could say that the K specification of EVM is the “source code” for the interpreter. But it is much more than that.
．KEVM 也是 EVM 的 Interpreter 解譯器，EVM 自動從 KEVM 規範中產生。您可以說 EVM 的 K 是 Interpreter 解譯器的「來源程式碼」。但 K 遠不止於此。

．KEVM can be used to prove that smart contracts are correct. This is done by specifying a contract’s desired properties in K, combining the contract with the KEVM specification, and then using the K framework to verify those properties.
．KEVM 可用於證明智能合約是正確的。這是透過在 K 中指定合約的所需屬性，將合約與 KEVM 規範相結合，然後使用 K Framework 來驗證這些屬性來完成的。

．KEVM can be used to check for errors such as integer over and under flows, stack over and under flows, out-of-gas, and other contract generic properties. You can also verify more targeted properties for specific contracts.
．KEVM 可用於檢查錯誤，例如整數變數的溢位和欠位（低於可顯示的最小值），堆疊的溢位和欠位，Gas 手續費不足，以及其他合約內的通用變數錯誤。您還可以驗證特定合約的更多目標變數。

．When you run a smart contract on the testnet using the testnet wallet, the testnet will send the contract to the KEVM interpreter to be executed. This interpreter is the only part of the testnet that is based on the K framework. But because the interpreter is generated from the K specification, you can use K (and KEVM) to verify your smart contracts before you send them to the testnet. In this sense, testnet is related to the entire K framework.
．當您使用 Testnet 錢包在 Testnet 上執行智能合約時，Testnet 會將合約發送到 KEVM Interpreter 解譯器用以執行合約。這個 Interpreter 是基於 K Framework 中 Testnet 的唯一部分。但是因為 Interpreter 是從 K 生成的，所以在將它們發送到 Testnet 之前，可以使用 K（和 KEVM）來驗證智能合約。從這個意義上講，Testnet 與整個 K Framework 相關。

．The KEVM is a high quality, formally-verified smart contract virtual machine. The KEVM testnet is implemented on Mantis, the standards-compliant Ethereum Classic client designed within the specification of the K framework. The K specification defines the formal semantics for elements such as the configuration and transition rules of EVM. The K framework provides the platform within which to work and also provides an executable.
．KEVM 是一種高質量，經過正式驗證的智能合約 VM。KEVM Testnet 在 Mantis上實現，Mantis 是符合標準的 Ethereum Classic 以太坊經典客戶端，在 K Framework 規範中設計。K 定義了元素的形式語義，例如 EVM 以太坊虛擬機的配置和轉換規則。K Framework 則提供了工作的平台，並提供了可執行的檔案。

．The KEVM is a stack-based machine, as opposed to a register-based machine. The primary difference between these two architectures is in the way in which operands and their results are stored and retrieved.
．KEVM 是 Stack-Based 基於堆疊的機器，而不是 Register-Bbased 基於寄存器的機器。這兩種體系結構之間的主要區別，在於作業數量及其結果的儲存和檢索方式。

．A Java Virtual Machine (JVM) is needed to run the client. The version must be 1.8.x. The client has not been tested with JVM 1.9.
．執行 KEVM 客戶端需要 Java 虛擬機（JVM）。版本必須是 1.8.x. 客戶端，目前則尚未使用 JVM 1.9 進行測試。

．64 bit output.
．KEVM 需要 64 位元輸出。

．Appropriate disk space: enough space will be needed for the blockchain to grow. An SSD of at least 35G is recommended.
．KEVM 需要適當的磁磁空間：區塊鏈需要足夠的空間來增長。建議使用至少 35G 的 SSD 硬碟。

e、IELE Testnet：

．IELE is a dedicated virtual machine that provides a foundation for the Cardano blockchain protocol. It executes and verifies smart contracts as well as providing a human-readable language for blockchain developers.
．IELE是一個專用的 VM，為 Cardano 區塊鏈協議奠定了基礎。它執行並驗證智能合約，並為區塊鏈開發人員提供人類可讀的語言。

．IELE was designed using formal methods to address security and correctness concerns inherent in writing Solidity smart contracts in Ethereum.
．IELE 採用正式方法設計，以解決在 Ethereum 以太坊中編寫 Solidity 智能合約所固有的安全性和正確性問題。

．When you write a smart contract in IELE, it is more secure and is easier to verify for correctness. You benefit from an easy-to-use and readable language structure - and the overall performance is improved.
．當您在 IELE 中編寫智能合約時，它更安全，更容易驗證是否正確。您可以從易於使用且易讀的語言結構中受益 - 並且整體性能得到改善。

．The IELE testnet provides better performance and is register-based, which means it can make use of a wider array of analyses and optimizations than a stack-based virtual machine such as KEVM. This leads to more accurate gas cost predictions, as well as lower gas cost for contracts.
．IELE Testnet 提供了更好的性能並且 Register-Bbased 基於寄存器，這意味著它可以使用比 Stack-Based 基於堆疊的 VM（如 KEVM）更廣泛的分析和優化。這樣可以更準確地預測 Gas 手續費成本，並降低合約的 Gas 手續費成本。

．IELE is a human-readable language that resembles the LLVM intermediate representation. This makes it easy to code directly to IELE, as well as to understand contracts and how they are deployed in the blockchain.
．IELE 是一種類似於 LLVM 中介表示的人類可讀語言。這樣可以輕鬆直接編寫 IELE 程式碼，以及了解合約和如何在區塊鏈中部署合約。

．IELE is designed to make formal verification of smart contracts easier. This includes writing specifications that smart contracts must obey as well as helping develop automated techniques that prove smart contracts are mathematically correct. For example, pushing a possibly computed number on to the stack and then jumping to it as an address makes verification hard, and thus security weaker, with current smart contract paradigms. IELE avoids this problem. It has named labels and jumps can only be made to those labels. Also, avoiding the use of a bounded stack and eliminating stack or arithmetic overflow helps the specification and verification of smart contracts.
．IELE 旨在簡化智能合約的正式驗證。這包括編寫智能合約必須遵守的規範，以及幫助開發自動化技術，證明智能合約在數學上是正確的。例如，當前的智能合約會將可能計算的數字推送到堆疊然後作為地址跳轉到它，這將使得驗證變得困難，因此安全性較弱。IELE 則避免了這個問題，它具有命名標籤，只能對這些標籤進行跳轉。此外，也避免了使用有界堆疊，並消除堆疊或算術溢位，這也有助於智能合約的規範和驗證。

．Debugging contracts is easier because IELE has a different status error code for each of the exceptions that can occur while executing the functions within a contract. The sender of a transaction that calls a function receives a status code as a return value in addition to the normal return values of the account call.
．調試合約更容易，因為 IELE 對於在合約中執行函數時可能發生的每個異常，都有不同的狀態錯誤代碼。除了帳戶呼叫的正常返回值之外，調用函數的事務發送方還會接收到狀態代碼作為返回值。

．That turns out not to be true. As a result, virtual machines are now widely used. For example, it was a natural choice for the Ethereum Foundation to create a virtual machine tailored to smart contracts. IELE represents a next stage in VM technology. The problem with VMs is that they’re written by people working from an informal specification. Or, often, the specification isn’t written down until after the VM is finished. That leads to mismatches between what the VM should do and what it does do. (That is: bugs.) Even where the VM is correct, informal specifications encourage misinterpretation by the implementors of higher-level languages, leading to bugs in their compilers.
．VM 現在被廣泛使用。例如，以太坊基金會創建一個為智能合約量身定制的 VM 是一個自然的選擇。IELE 代表了 VM 技術的下一個階段。VM 的問題在於它們是由非正式規範的人員編寫的。或者，通常，直到 VM 完成後才會記錄規範。這導致什麼 VM 應該做，什麼之間的不匹配不會做。（即：臭蟲）即使 VM 正確，非正式規範也會鼓勵高級語言的實現者誤解，從而導致編譯器出現錯誤。

．IELE is a virtual machine developed in a different way. The specification was written first, and it was written in a formal (extremely precise) language. Then, using a suite of tools called the K framework, the virtual machine was generatedfrom the formal specification, rather than being implemented by people. While a bug in the generator could still produce a bug in the VM, the chances of that are much, much lower than from a human implementation.
．IELE 是以不同方式開發的 VM。該規範首先編寫，並以正式（非常精確）的語言編寫，然後，使用一套稱為 K Framework 的工具。VM 是從正式規範生成的，而不是由人們實現的。雖然生成器中的錯誤仍然可能在 VM 中產生錯誤，但這種錯誤遠遠低於人工實現。此外，錯誤在於決定 VM 應該做什麼（即規範中的錯誤）方面的影響要小得多。您只需重新生成整個 VM，而不是強制人們重寫相應的 VM 代碼。因此，製作一台複雜的以太坊 VM 的工作 VM 的整個過程只有十個人月。

．However, the IELE VM is only an order of a magnitude slower than the Ethereum virtual machine. That sounds scary but it’s sufficient for the specialized domain of smart contracts. Just as with Java, which has gone from “fast enough that it’s a viable competitor for C for web work” to “fast enough for all but specialized applications”, we can expect further generations of IELE to speed up.
．IELE VM 只比 Ethereum VM 慢一個數量級。這聽起來很可怕，但對智能合約的專業領域來說已經足夠了。就像 Java 一樣，它已經從「足夠快，它可以成為 C 網路工作的可行競爭對手」到「除了專業應用程序以外的所有應用程序」，我們可以期待更多代的 IELE 加速。

．IELE is designed to support machine analysis. Specifically, Cardano will enable high-value contracts to be evaluated like this: "What the contract must do is stated in a precise language, separately from the code.", "The contract source code is compiled into IELE’s underlying language, which has been specified with great precision.", "Formal verification techniques are used to (in effect) explore all possible values. So the case where the ether sender is the same as the ether receiver will automatically be checked.".
．IELE 旨在支持機器分析。具體來說，Cardano 將使高價值合約能夠像這樣進行評估：「合約必須做的是用精確的語言陳述，與代碼分開。」、「合約源代碼被編譯成 IELE 的基礎語言，該語言已經非常精確地指定。」、「正式驗證技術用於（實際上）探索所有可能的值。因此，將自動檢查以太發送器與以太接收器相同的情況。」。

．The IELE virtual machine’s instruction set is modelled after that of LLVM. LLVM is an open source technology that’s widely used, most notably in Apple’s toolset for building iPhone and Mac apps. Over the eighteen years LLVM has been in development, many optimization and analysis techniques have been applied to its instruction set. Going forward, Cardano can adapt the best of them rather than having to invent new ones.
．IELE 虛擬機的指令集以 LLVM 的模型為模型。LLVM 是一種廣泛使用的開源技術，最著名的是 Apple 用於構建 iPhone 和 Mac 應用程序的工具集。在過去的 18 年中，LLVM 一直在開發中，許多優化和分析技術已應用於其指令集。展望未來，Cardano 可以適應其中最好的而不是發明新的。

．IELE is modelled on LLVM and follows a semantics-based approach to deliver a more secure, more reliable platform that gives developers an easier way to verify their smart contracts.
．IELE 以 LLVM 為模型，遵循 Semantics-Based 基於語義的方法，提供更安全，更可靠的平台，使開發人員能夠更輕鬆地驗證其智能合約。

．For IELE, this means that now we can write smart contracts in any programming language and have a correct by construction compiler to IELE.
．現在我們可以用任何編程語言編寫智能合約，並通過構造編譯器對 IELE 進行編譯。

．A Java Virtual Machine (JVM) is needed to build the client, as with the KEVM testnet. The version must be 1.8.x. The client has not been tested with JVM 1.9.
．與 KEVM testnet 一樣，構建客戶端需要 Java 虛擬機（JVM）。版本必須是 1.8.x. 客戶端，尚未使用 JVM 1.9 進行測試。

．230 disk space and 10MB of RAM are recommended.
．建議使用 230 個磁盤空間和 10MB RAM。

（9）示意圖：