Gas Analysis in Vyper Extension for the Ethereum Blockchain

In the last years, blockchain technologies like Bitcoin have demonstrated that it is possible to build decentralized, anonymous and secure systems to make digital transactions. In 2013, a cryptocurrency researcher and programmer called Vitalik Buterin saw the potential of blockchains and wondered whether it was possible to create something that extends the functionalities of Bitcoin. Eventually, he proposed Ethereum, which is a decentralized open source blockchain featuring smart contract functionality. This feature is one of the main differences between Bitcoin and Ethereum, and it highlights how Buterin was focused on facilitating the creation of peer-to-peer contracts and applications. One of the main problems of the Ethereum blockchain is to establish upper bounds to the operational cost of certain operations. In fact, users who want to benefit from a certain application must pay an amount of Ether to the miner for their effort and that amount is equal to the total amount of gas it took to complete the operation. A lot of researches have been conducted to obtain more precise bounds at a less computational effort, but, in case of while loops or recursion, such bounds cannot always be computed. For this reason, a non Turing-Complete language was created, called Vyper, so that, since it does not allow programs to diverge, it is possible to compute precise and non symbolic upper bounds. In this thesis, we consider extensions of the Vyper language and compiler, allowing the programmer to use while constructs in smart contracts. Afterward, we will illustrate the implementation of a compiler from Vyper source code to CITRS (Complexity Integer Term Rewrite System). Then, a tool named KoAT will be used to infer symbolic upper bounds on while loops from the CITRS code, which will allow us to calculate the maximum amount of gas spent by a program.