A simulator of Solidity-style smart contracts in the theorem prover Agda - Anton Setzer (Proceedings of the 2023 6th International Conference on Blockchain Technology and Applications, 2023)
This paper extends the previous paper [6] by implementing two blockchain simulators of Solidity-style smart contracts – a simple and a complex one, using the interactive theorem prover Agda. In the previous article [6], we built a simple and complex abstract model of Solidity-style smart contracts in Agda. These models had many features, such as calling different smart contracts, supporting the ability to call different smart contracts, and providing simple and complex instructions. Because of the use of coalgebras for representing smart contracts they supported loops and conditionals, using the support of those features for coalgebraic programs in Agda. The complex model supported gas costs and pure functions, similar to the Solidity language.In this paper, we implement and design interfaces which allow to interactively interact with users in the simple and complex models. This makes use of the fact that Agda is as well a dependently typed programming language. Therefore we can write interactive programs which are running in the same language in which we will in a future next step verify smart contracts, avoiding the translation of programs which could be a source of errors. The simple blockchain simulator we have created can call other contracts, transfer funds to specific contracts, and update contracts. The complex blockchain simulator has in addition features that can deal with more complex blockchain instructions, support gas costs, and evaluate and update pure functions.