Translation Certification for Smart Contracts
Authors:
Jacco O. G. Krijnen,
Manuel M. T. Chakravarty,
Gabriele Keller,
Wouter Swierstra
Abstract:
Compiler correctness is an old problem, but with the emergence of smart contracts on blockchains that problem presents itself in a new light. Smart contracts are self-contained pieces of software that control assets, which are often of high financial value, in an adversarial environment and, once committed to the blockchain, they cannot be changed anymore. Smart contracts are typically developed i…
▽ More
Compiler correctness is an old problem, but with the emergence of smart contracts on blockchains that problem presents itself in a new light. Smart contracts are self-contained pieces of software that control assets, which are often of high financial value, in an adversarial environment and, once committed to the blockchain, they cannot be changed anymore. Smart contracts are typically developed in a high-level contract language and compiled to low-level virtual machine code before being committed to the blockchain. For a smart contract user to trust a given piece of low-level code on the blockchain, they must convince themselves that (a) they are in possession of the matching source code and (b) that the compiler faithfully translated the source code's semantics.
Classic approaches to compiler correctness tackle the second point. We argue that translation certification also addresses the first. We describe the proof architecture of a novel translation certification framework, implemented in Coq, for a functional smart contract language. We demonstrate that we can model the compilation pipeline as a sequence of translation relations that facilitate a modular proof approach and are robust in the face of an evolving compiler implementation.
△ Less
Submitted 22 February, 2022; v1 submitted 13 January, 2022;
originally announced January 2022.
Babel Fees via Limited Liabilities
Authors:
Manuel M. T. Chakravarty,
Nikos Karayannidis,
Aggelos Kiayias,
Michael Peyton Jones,
Polina Vinogradova
Abstract:
Custom currencies (ERC-20) on Ethereum are wildly popular, but they are second class to the primary currency Ether. Custom currencies are more complex and more expensive to handle than the primary currency as their accounting is not natively performed by the underlying ledger, but instead in user-defined contract code. Furthermore, and quite importantly, transaction fees can only be paid in Ether.…
▽ More
Custom currencies (ERC-20) on Ethereum are wildly popular, but they are second class to the primary currency Ether. Custom currencies are more complex and more expensive to handle than the primary currency as their accounting is not natively performed by the underlying ledger, but instead in user-defined contract code. Furthermore, and quite importantly, transaction fees can only be paid in Ether.
In this paper, we focus on being able to pay transaction fees in custom currencies. We achieve this by way of a mechanism permitting short term liabilities to pay transaction fees in conjunction with offers of custom currencies to compensate for those liabilities. This enables block producers to accept custom currencies in exchange for settling liabilities of transactions that they process.
We present formal ledger rules to handle liabilities together with the concept of babel fees to pay transaction fees in custom currencies. We also discuss how clients can determine what fees they have to pay, and we present a solution to the knapsack problem variant that block producers have to solve in the presence of babel fees to optimise their profits.
△ Less
Submitted 8 April, 2022; v1 submitted 2 June, 2021;
originally announced June 2021.
