Transform contracts written in Peyton Jones’ contract descriptive language to Solidity Assembly Language

Abstract

Financial contracts play a vital role in the modern economy. As there are variety of contracts being traded in the financial markets, the natural language used to define those contracts imposed an ambiguity in the financial contracts. To eliminate that, Peyton Jones and co-authors proposed a standard representation towards the financial contracts by introducing a combinator library embedded in Haskell programming language. However, the fundamental problem of the need of a trusted central counterparty, suffered by every financial contract remained unchanged with this representation. The existence of the middle man in the financial contracts introduced certain risks and overhead to the contracts. In order to overcome this situation, V.U. Wickramarachchi proposed an approach to facilitate the autonomous contract execution by exploiting the features and use cases of Ethereum blockchain and its scripting language Solidity. This was achieved through the special purpose compiler which facilitates transformation from Peyton Jones’ Contract Descriptive language to Solidity. However, the cost related to the execution of contracts in Ethereum network curtail the benefits received through the transformation of those contracts. In this dissertation, a novel approach to facilitate the reduction of cost by optimizing the smart contract is proposed using different optimization techniques. This approach involves the transformation of the Peyton Jones’ Contract Descriptive language to Assembly language which enables the manipulation of data locations in the Ethereum Virtual Machine. To substantiate that, the proposed method was able to scale down the execution cost factor in a significant manner, the solution is evaluated with the approach which transform Peyton Jones’ CDL to solidity with a comparison between the execution cost of both the approaches. A formal verification is provided by verifying the semantic equivalence between the Peyton Jones’ Contract Descriptive language and the proposed solution to make sure the correctness of the proposed approach is preserved while it is being optimized.