The IELE and K team Mathematical rigor and good design of programming languages and underlying virtual machines are critical for the success of blockchain technologies and applications. Indeed, decades of accumulated evidence show that formal techniques and their early adoption in the design of computing systems can significantly increase the safety, security and dependability of such systems. Moreover, when paired with good user interfaces that hide the mathematical complexity, such techniques can also increase the effectiveness, elegance and quality of code development. A good example is the recent success of functional programming languages and of automated theorem provers or constraint solvers.

Runtime Verification, a University of Illinois start-up founded by computer science Professor Grigore Rosu, has been recently awarded a research and development contract by IOHK to design a next generation virtual machine and a universal language framework to be used as core infrastructure for future blockchain technologies. The formal analysis and verification technology employed in this project was initiated by Prof. Rosu and his collaborators back in 2001, when he was a NASA scientist, and has been improved over more than 15 years of research and development both in his Formal System Laboratory (FSL) at the University of Illinois at Urbana-Champaign and at Runtime Verification, with generous funding of more than $10M from organisations including NSF, NASA, DARPA, NSA, Boeing, Microsoft, Toyota, and Denso. It is about time that aircraft grade, software analysis technology used for mission critical software gets deployed to smart contracts, the blockchain and cryptocurrencies. The project will be executed by a team of Runtime Verification experts led by Prof Rosu, who will work closely with students at the University of Illinois – also funded by IOHK – and with the IOHK research and development team.

IELE – A Register-Based Virtual Machine for the Blockchain

Based on learnings from defining KEVM, our semantics of EVM in K, we will design and define a new VM, which we call IELE (after the Mythological Iele). Unlike the EVM, which is a stack-based machine, IELE will be a register-based machine, like LLVM. It will have an unbounded number of registers and will also support unbounded integers. There are some tricky but manageable aspects with respect to gas calculation, a critical part of the design.

Here are the forces that will drive the design of IELE:

1. To serve as a uniform, lower-level platform for translating and executing smart contracts from higher-level languages, which can also interact with each other by means of an ABI (Application Binary Interface). The ABI will be a core element of IELE, and not just a convention on top of it. Also, unbounded integers and an unbounded number of registers will make compilation from higher-level languages more straightforward and elegant and, looking at the success of LLVM, more efficient in the long term. Indeed, many of the LLVM optimizations are expected to carry over. For that reason, IELE will follow the design choices and representation of LLVM as much as possible. The team includes an advanced PhD student from Vikram Adve’s lab at the University of Illinois, where LLVM was created, and who is an expert in LLVM.

2. To provide a uniform gas model, across all languages. The general design philosophy of gas calculation in IELE is “no limitations, but pay for what you consume”. For example, the more registers a IELE program uses, the more gas it consumes. Or the larger the numbers computed at runtime, the more gas it consumes. The more memory it uses, in terms of both locations and size of data stored at locations, the more gas it consumes. And so on.

3. To make it easier to write secure smart contracts. This includes writing requirements specifications that smart contracts must obey as well as making it easier to develop automated techniques that mathematically verify/prove smart contracts correct wrt to such specifications. For example, pushing a possibly computed number on the stack and then jumping to it regarded as an address makes verification hard, and thus security weaker, with current smart contract paradigms. We will have actual labels in IELE, like in LLVM, and structured jumps to those labels. Also, avoiding the use of a bounded stack and not having to worry about stack or arithmetic overflow will make specification and verification of smart contracts significantly easier.

Like KEVM, the formal semantics of EVM that we previously defined, validated and evaluated using the K framework, the design of IELE will also be done in a semantics-based style, using K. Together with a fast (LLVM-based) execution backend for K, it is expected that the interpreter obtained automatically from the semantics of IELE will be sufficiently efficient to serve as a reference implementation of IELE.

K as a Universal Language for the Blockchain

Besides EVM, several languages have been given a complete formal semantics in K, including C, Java, and JavaScript. Several others will be given K semantics as part of this project, including IELE itself, Solidity and Plutus. We want to allow all these languages, and possibly more as they are given K semantics, to be used for writing smart contracts. For that, we need to enhance the capabilities and implementation of the K platform itself, which will increase the practicality of all new and existing K semantics. We will implement several performance improvements not yet taken beyond proofs of concept, and develop production-quality implementations of analysis features such as the K symbolic execution engine, the semantics-based compiler (SBC), and the program verifier, which currently have only prototype-quality implementations in the academic K project.

Faster Execution

We plan to develop a concrete execution backend to K that will be at least one order of magnitude faster than the current one. The current one is based on translation to OCaml; we plan on translating to LLVM and specializing the pattern matcher to the specific patterns that occur in semantics. We believe it will be possible to execute programs against our KEVM semantics as efficiently as the reference C++ EVM implementation(!). If that will indeed be the case, and we strongly believe it will, then this will mark an unprecedented moment in the history of programming languages, when a language implementation automatically derived from a formal semantics of the language can serve as a realistic implementation of that language. While this was proved as a concept with toy languages, it has never been proven to work with real languages in practice. The K technology has reached a point where this is possible now. And not only to execute programs, or smart contracts, but also to reason about them, because a formal semantics, unlike an interpreter, can also be used for formal verification.

Semantics-Based Compilation

One of the most challenging components of the K framework that will be built in this project is what we call semantics-based compilation. The following picture shows how SBC works:

We have implemented a rough prototype and were able to make it work with a simple imperative language, which we call IMP. Here is an example:

The program to the left is transformed, using the semantics, into a much simpler program that looks like an abstract machine. The four states represent the “instructions” of the new language L’, and the edges are the new semantic rules of L’. As seen, the semantics of the various sequences of instructions has been symbolically summarized, so that the amount of computation that needs to be done at runtime is minimized and everything that can be done statically is hardwired in the new semantics of L’, so all done before the program is executed. Preliminary experiments are encouraging, confirming our strong belief that the resulting SBC programs will execute one order of magnitude, or more, faster:

These improvements to the K framework will not only yield a reasonably efficient prototype of executing smart contracts on IELE, but, more importantly, will give us an approach to write smart contracts in any programming languages that have a formal semantics in K.

We, the K team at RV and at UIUC, are very excited to pursue this new project with IOHK. This gives us a unique chance to demonstrate that the K technology is ready to transit to the real world, in a space where security and trust in computation are paramount. It almost feels like smart contracts are the opportunity that K was waiting for all along, like what it was designed and implemented for.

Why do we need transaction fees?

There are two main reasons why transaction fees are needed for a cryptocurrency like Cardano:

People who run full Cardano nodes spend time, money and effort to run the protocol, for which they should be compensated and rewarded. In contrast to Bitcoin, where new currency is created with each mined block, in Cardano, transaction fees are the only source of income for participants in the protocol.

The second reason for transaction fees is the prevention of DDoS (Distributed Denial of Service) attacks. In a DDoS attack, an attacker tries to flood the network with dummy transactions, and if he has to pay a sufficiently high fee for each of those dummy transactions, this form of attack will become prohibitively expensive for him.

How do transaction fees work?

Whenever somebody wants to transfer an amount of Ada, some minimal fees are computed for that transaction. In order for the transaction to be valid, these minimal fees have to be included (although the sender is free to pay higher fees if he so wishes). All transaction fees are collected in a virtual pool and then later distributed amongst participants in the Cardano protocol.

How are the minimal transaction fees calculated?

The minimal fees for a transaction are calculated according to the formula

a + b × size,

where 'a' and 'b' are constants and 'size' is the size of the transaction in Bytes. At the moment, the constants 'a' and 'b' have the values

a = 0.155381 ADA,
b = 0.000043946 ADA/Byte.

This means that each transaction costs at least 0.155381 ADA, with an additional cost of 0.000043946 ADA per Byte of transaction size. For example, a transaction of size 200 Byte (a fairly typical size) costs

0.155381 ADA + 0.000043946 ADA/Byte × 200 Byte = 0.1641702 ADA.

Why did we pick this particular formula? The reason for having parameter 'a' is the prevention of DDoS attacks mentioned above: even a very small dummy transaction should cost enough to hurt an attacker who tries to generate many thousands of them. Parameter 'b' has been introduced to reflect actual costs: storing larger transactions needs more computer memory than storing smaller transactions, so larger transactions should be more expensive than smaller ones.

In order to arrive at the particular values for parameters 'a' and 'b', we had to answer questions like:

• How expensive is one byte of computer memory?
• How many transactions will there be on average per second?
• How large will a transaction be on average?
• How much does it cost to run a full node?

We had to estimate the answers to those questions, but now that Cardano is up and running, we will be able to gather statistics to find more accurate answers. This means that 'a' and 'b' will probably be adjusted in future to better reflect actual costs.

We even plan to eventually come up with a scheme that will adjust those constants dynamically in a market driven way, so that no human intervention will be needed to react to changes in traffic and operational costs. How to achieve this is one focus of our active research.

How are fees distributed?

All transaction fees of a given "epoch" are collected in a virtual pool, and the idea is to then redistribute the money from that pool amongst people who were elected "slot leaders" by the proof of stake algorithm during that epoch and who created blocks.

At this stage of Cardano, where all blocks are created by nodes operated by IOHK and our partners, fees are already collected (to prevent DDoS attacks), but they will not be distributed and instead will be burnt.

As soon as Cardano enters its next, fully decentralized stage, fees will be distributed as described above.

What next?

Coming up with a solid scheme for fee distribution is a challenging mathematical problem: How do we incentivize "good" behavior and promote efficiency while punishing "bad" behavior and attacks? How do we make sure that people who participate in the protocol receive their fair reward, while also ensuring that the best way to earn money with Cardano is to make the system as reliable and efficient as possible? The trick is to align incentives for node operators with the "common good", so that rewards are highest when the system is running at optimal performance.

These are questions studied by the mathematical discipline called Game Theory, and we are proud to have prominent game theorist and Gödel Award laureate Prof. Elias Koutsoupias of the University of Oxford working with us on finding solutions to this problem.

IOHK received both Bitcoin and Ada for its contract to work on the Cardano project. IOHK converted most of its Bitcoin at the time of receiving it to fiat in order to ensure project stability. With respect to IOHK's holdings of Ada, IOHK does not expect a need to liquidate any of its Ada to cover immediate costs related to the Cardano project until 2019. However, like most ventures in the cryptocurrency space, we have made certain payroll commitments in Ada to several IOHK personnel, contractors and third party firms.

Therefore, IOHK will voluntarily adopt the following vesting schedule for its Ada. A third of IOHK's Ada holdings will be immediately available to IOHK. A third will be made available after June 1st of 2018. The final third of IOHK's Ada will be made available after June 1st of 2019.

Charles Hoskinson will not receive any Ada until the final third of supply unlocks in June of 2019. When the computation layer of Cardano is released next year, IOHK will move its total Ada supply into a custom vesting contract to reflect the above policy.

In the spirit of full disclosure, IOHK's initial Ada address is:

As for Emurgo and the Cardano Foundation, we have requested both partners to make a similar statement about use of funds. As they are independent businesses, they will do so at a time and manner of their choosing.

The technology was conceived in an Osaka restaurant more than two years ago and from that small beginning Cardano has been built into a leading cryptocurrency. The project has amassed a team of experts in countries around the world, has generated more than 67,000 lines of code, and has a strong and growing community in countries across Asia and beyond. Along the way, Cardano has set new standards for cryptocurrencies with best practices such as peer review and high assurance methods of software engineering. The official launch was held in the district of Shibuya in Tokyo on Saturday October 14 for an audience of about 500 people, who had each won a ticket through a lottery held on social media. Excited cryptocurrency enthusiasts, Ada holders and business people from across Japan queued to get Cardano t-shirts and souvenir physical Ada coins, before going into the main hall to hear about how Cardano was created and the vision for its future. "The first thing we did when we knew the project was real was to build great partnerships," Charles Hoskinson, founder and CEO of IOHK, told the audience. "Our chief scientist is based at University of Edinburgh, it is a wonderful place, where they built the heart of Cardano. We have a lot of wonderful people at the University of Athens, they are rigorous, making sure that the theory works. And we have people at Tokyo Tech who work on multi party computation and look to the future, and work out how to make Cardano last a long time." The vision for Cardano, Hoskinson said, was that it would pull together academic research and bright ideas from computer science to produce a cryptocurrency capable of much more than its predecessors.

This "third generation" cryptocurrency would be able to scale to a billion users, using a proof of stake algorithm, Ouroboros, which avoided the huge energy consumption of proof of work cryptocurrencies. Features that would be added to Cardano to help it scale included sidechains, trusted hardware, and RINA, or recursive internetwork architecture. Sustainability would be part of the design by way of a treasury system to fund development indefinitely, allowing stakeholders to vote on proposed changes to the protocol. Meanwhile, the computation layer of the technology, would be innovative in using a tool called K Framework to allow developers to write smart contracts in the programming language of their choice, he said. Security is paramount to cryptocurrency because flaws in code increase the risk of hacks and the loss of coin holder funds, unfortunately witnessed too often. With that in mind, Duncan Coutts, head of engineering at IOHK, explained how the company approaches software development: cryptography research papers are translated into code using the technique of formal specification. This involves a series of mathematical steps that progressively take the cryptography closer to the code that the developers write, a process that allows checks to be made that the specifications are indeed correct.

Duncan Coutts, IOHK Director of Engineering, presenting at the Cardano launch event

"I’m passionate about bringing clever ideas from computer science and using them in Cardano," Coutts said. "And I’m obsessive about software quality. Beautiful software is like beautiful mathematics or poetry." Aside from engineering, the other twin pillar of IOHK is research, and Bernardo David went on stage to talk about the rigour supporting the papers that IOHK produces. David is an assistant professor at Tokyo Tech where IOHK has a research partnership, and was one of the team that produced Ouroboros, a provably secure proof of stake algorithm. On the question of whether people should accept the quality of the research, he pointed to the paper’s peer review through its acceptance to Crypto 2017, the annual cryptography conference held in California. "This is the first proof of stake paper that was published in a big conference so you can trust the largest and most respected cryptography conference in the world," he said. "You don’t have to take my word, you can trust all the other cryptographers."

Michael Parsons, Chairman of Cardano, speaking at the Cardano launch event

The launch event introduced the other important organisations supporting Cardano, such as the Cardano Foundation. The Swiss-based standards body acts as the guardian of the protocol and its duties include providing information to the community and working with governments to shape regulation. Michael Parsons, chairman, announced that Ada holders would be able to store their coins in the Ledger hardware wallet and integration was being worked on. Plans for the future included working with a respected London think-tank to produce blockchain research. Thanking the community, he said: "Cardano is a blockchain protocol with integrity. We are dedicated to helping it derive its full potential and make the world a better place. You supported us to help make Cardano what it is, so thank you." The third organisation supporting Cardano is Emurgo, which is based in Japan and extends support and advice to anyone wishing to build applications on the software.

Ken Kodama, CEO of Emurgo, emphasised the advantages of Cardano’s technology over older cryptocurrencies, and said: "Emurgo sees a bright future that Cardano will provide a more trustable way of identifying individuals and also a reasonable, and faster payment method to people who don't have them now. Emurgo will play an important role in plugging developers and startups to the Cardano ecosystem." Kodama, along with Darren Camas, senior adviser to Emurgo, spoke about how a network was being established in other Asian countries to support its growth. Camas said: "The question for us is how do we help Ada become the fuel that powers financial technology, not only in the developed world but in Malaysia, Vietnam, Argentina, Nigeria… How do we bring more people from across the globe to transact in the Cardano ecosystem?"

After the presentation crowds formed outside the hall to have their photos taken with the Cardano team. Some people who came along were longstanding supporters of the project, such as Naomi Nisiguchi, from Mie Prefecture. She works as a manager in the construction industry and has had an interest in cryptocurrency for four years. "Around two years ago I heard about Ada and that Charles Hoskinson was involved," she said. "I’ve been following the news on Facebook and I’m very interested to learn how the project will move on."

Ken Kodama, CEO of Emurgo, speaking at the Cardano launch event

Many people had plans regarding Cardano. Takashi Kawaguchi set up Fintech Academia last month to give Japanese people information about cryptocurrencies, and came along because he believes Cardano has the potential to rise up and be on par with Bitcoin and Ethereum. His website would provide educational resources that would help people understand and trust crypto, he said, and learn that it wasn’t an enemy, but represented the future.

Other people at the event were planning business interests, such as Nobuyoshi Hayashi from Tochigi prefecture, who owns a consultancy and wants to begin offering cryptocurrency advisory services. The launch itself is only the beginning for Cardano, with many new features to be added during the next three years that will cement its position as the leading cryptocurrency. Mario Larangeira, specially appointed associate professor at Tokyo Tech, was in the audience, and said it was a great time to be working in cryptography. "To be part of this project is challenging, complex but also very exciting," he said. "Now we are working on multi party computation and putting even more cryptography into Cardano, for example with Kaleidoscope, new research that is being produced at Tokyo Tech with Bernardo David and Rafael Dowsley."

Bernardo David, IOHK Research Fellow, speaking at the Cardano launch event

There was much hard work ahead, agreed Charles Hoskinson, and holding an event in Tokyo with Cardano partners was a very special occasion. "This is a really fun event," he said. "Cardano has its largest community here in Japan and we felt it was so important to have a launch event to thank the community for being so supportive, loyal and patient. The point of this event has been to talk about where we came from and where we plan on going, and meet some new people and make new friends."

The launch of Cardano brings to an end an exciting first phase of development for us at IOHK, after more than a year spent planning and developing the technology. Now we’ve handed the product over to users and they are getting to know how it works. Using new software can be tricky – some people won’t need any help, but there will be those who need a little assistance. To make sure that people know how to use the software and aren’t experiencing any problems, IOHK and Cardano Foundation organised a help desk tour around Japan. As far as we know, this is the first time there has been a customer service tour for a cryptocurrency.

Over two weeks, starting from the end of September, the team visited five cities in Japan: Osaka, Nagoya, Hiroshima, Fukuoka and Tokyo, where we are holding three days of seminars. To figure out where we should go, the Cardano Foundation had previously sent out a questionnaire to find out who needed our help, and what kinds of questions people had. This helped us plan the tour accordingly.

We started out on a Saturday at the end of September in Osaka before moving on to Nagoya and making our way around Japan. Being able to meet and talk to the community of Ada holders was a really good experience. People were excited, eager to learn and had lots of positive comments and feedback. There was a mix of different ages, with the youngest people aged about 20 and the very oldest about 70. There were men and women, and there was a good turn out – sessions were nearly always just about full. Kondo, aged 45, heard about Cardano through Facebook and joined the online community to learn more. "I think Cardano’s future is very bright," Kondo said at a help desk seminar. "I brought my PC today and managed to redeem my Ada. I don’t think I could’ve done that without the staff’s help. I’m glad that everything’s solved."

Some people came along to meet other members of the community. New "crypto friends" swapped details so they could use talk about cryptocurrency using Line. Others were excited and wanted to share their thanks with the team and good wishes for the future of Cardano. Each Cardano help desk programme lasted a full day, over which we ran several sessions. The most popular presentation was on exchanges, and explained cryptocurrency markets and Bittrex, the exchange that Ada launched on. That session included a demonstration of how to use Bittrex, given by Daniel Friedman, a Japanese speaking IOHK staff member based in Osaka, and Toshiaki Miyatake, a Cardano community moderator from Tokyo, and the presentation was followed by a question and answer session. Aside from making sure that people had no technical problems, another objective of the help desk tour was to inform and educate. Cardano has attracted many people who are discovering an interest in cryptocurrency, so we want to help them get started by providing them with high quality resources and information.

Another presentation covered the Daedalus wallet. This wallet is where Ada is stored, and where users send and receive Ada. Step by step, we walked people through using Daedalus, including showing them how to store their private keys, how to add their Ada to the wallet and send it to the exchange. This session included offering one-to-one technical help, for anyone who needed personal assistance. People brought their laptops and we had memory sticks to install Daedalus for them if they hadn’t installed it already. There was also a popular presentation for people who wanted to join the growing Cardano community on social media. Miyatake showed people the Twitter accounts, the official Facebook group and how to join the conversation taking place in channels on Slack, with both Japanese and English language accounts available to join. Meeting Cardano users was enjoyable and hopefully provided them with all the help they needed, but it was also helpful for us too.

IOHK founder Jeremy Wood at the help desk tour

During the course of the sessions and meeting and talking to so many users, we uncovered a couple of small bugs in Daedalus, which our developers could begin work on fixing. Some of the bugs or issues we discovered were:

• Using Japanese characters when naming the wallet could cause the wallet to crash. A fix for this is due to be made soon.
• Daedalus now requires Windows users to synchronise the clock on their PC to the time on the internet.
• Windows users may find that when they try to connect to the network for a second time after quitting the application, they are stuck connecting to the network. Developers are looking into issue, which can sometimes can be fixed by restarting the computer.
• For a small number of people, transactions may not seen in the wallet despite being registered on the blockchain when they try to make a withdrawal from Bittrex. A fix for this is being worked on by developers.
• We have had reports that Daedalus may be wrongly identified as malware by the machine leaning algorithms used in some anti virus software. With time, this should change. Please be cautious if you are unsure and file a bug report. If you have a problem, first make sure your wallet is backed up, then download Daedalus again and reinstall it on your computer.
• Windows users may not be able to use a tablet and instead should use a desktop computer.

It was a busy but rewarding two weeks, now finishing up in Tokyo, where high demand means we had three full days booked at TKP Garden City in Shibuya. Now that Cardano is in the hands of the community there will be a special event in Tokyo this week to mark the successful launch. All three partners who are responsible for Cardano – IOHK as its developers, the Cardano Foundation as the standards body and guardian, and Emurgo, the venture builder for decentralised applications – will come together to talk about what users can expect to see with Cardano over the next three years. For coverage of the event, and to join the community, follow our social channels on Facebook, Twitter, and Slack.