Transformation of Contract Descriptions in a Domain Specific Language to Solidity Assembly

There are a variety of contracts being traded in the financial markets. To eliminate the ambiguities imposed by the financial contracts written in natural languages, Peyton Jones and co-researchers proposed a contract definition language for standard representation of the financial contracts and a combinator library embedded in Haskell programming language to define financial contracts. Further, a special purpose compiler which is an extension to this work has been already proposed by exploiting major advancements such as autonomous contract execution and elimination of central counterparty in contemporary smart contracts, to transform contracts written in Peyton Jones' Contract Descriptive Language to Solidity which is the scripting language used in Ethereum smart contract platform. However, we have noticed that the cost related to the execution of contracts in Ethereum platform curtails the benefits received through the transformation of those contracts. Hence, we propose a novel approach to reduce the cost using different optimization techniques and it involves the direct transformation of the Peyton Jones' Contract Descriptive language to Solidity (inline) Assembly language which enables the manipulation of data locations in the Ethereum Virtual Machine. A formal verification is provided by verifying the semantic equivalence between the Peyton Jones' Contract Descriptive language and the proposed solution to ensure the correctness of the proposed approach is preserved while it is being optimized.