Conference Paper/Proceeding/Abstract 354 views 52 downloads
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, Pages: 1 - 11
Swansea University Author:
Anton Setzer
-
PDF | Accepted Manuscript
© The Authors | ACM} {2023}. This is the author's accepted manuscript version of the work. It is posted here for your personal use. Not for redistribution.
Download (931.4KB)
DOI (Published version): 10.1145/3651655.3651656
Abstract
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 i...
| Published in: | Proceedings of the 2023 6th International Conference on Blockchain Technology and Applications |
|---|---|
| Published: |
New York, NY, USA
ACM
2023
|
| Online Access: |
http://dx.doi.org/10.1145/3651655.3651656 |
| URI: | https://cronfa.swan.ac.uk/Record/cronfa64152 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Abstract: |
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. |
|---|---|
| Keywords: |
Agda, Ethereum, Solidity, blockchain, interface, simulator, smart contracts, theorem prover |
| College: |
Faculty of Science and Engineering |
| Start Page: |
1 |
| End Page: |
11 |