No Cover Image

Conference Paper/Proceeding/Abstract 246 views 18 downloads

A simulator of Solidity-style smart contracts in the theorem prover Agda

Fahad Alhabardi Orcid Logo, Anton Setzer Orcid Logo

Proceedings of the 2023 6th International Conference on Blockchain Technology and Applications, Pages: 1 - 11

Swansea University Author: Anton Setzer Orcid Logo

  • 64152.pdf

    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...

Full description

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!
first_indexed 2023-08-29T08:14:07Z
last_indexed 2023-08-29T08:14:07Z
id cronfa64152
recordtype SURis
fullrecord <?xml version="1.0" encoding="utf-8"?><rfc1807 xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:xsd="http://www.w3.org/2001/XMLSchema"><bib-version>v2</bib-version><id>64152</id><entry>2023-08-29</entry><title>A simulator of Solidity-style smart contracts in the theorem prover Agda</title><swanseaauthors><author><sid>5f7695285397f46d121207120247c2ae</sid><ORCID>0000-0001-5322-6060</ORCID><firstname>Anton</firstname><surname>Setzer</surname><name>Anton Setzer</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2023-08-29</date><deptcode>MACS</deptcode><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.</abstract><type>Conference Paper/Proceeding/Abstract</type><journal>Proceedings of the 2023 6th International Conference on Blockchain Technology and Applications</journal><volume/><journalNumber/><paginationStart>1</paginationStart><paginationEnd>11</paginationEnd><publisher>ACM</publisher><placeOfPublication>New York, NY, USA</placeOfPublication><isbnPrint/><isbnElectronic/><issnPrint/><issnElectronic/><keywords>Agda, Ethereum, Solidity, blockchain, interface, simulator, smart contracts, theorem prover</keywords><publishedDay>15</publishedDay><publishedMonth>12</publishedMonth><publishedYear>2023</publishedYear><publishedDate>2023-12-15</publishedDate><doi>10.1145/3651655.3651656</doi><url>http://dx.doi.org/10.1145/3651655.3651656</url><notes/><college>COLLEGE NANME</college><department>Mathematics and Computer Science School</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>MACS</DepartmentCode><institution>Swansea University</institution><apcterm/><funders/><projectreference/><lastEdited>2024-06-11T15:20:27.6301362</lastEdited><Created>2023-08-29T09:09:26.8815003</Created><path><level id="1">Faculty of Science and Engineering</level><level id="2">School of Mathematics and Computer Science - Computer Science</level></path><authors><author><firstname>Fahad</firstname><surname>Alhabardi</surname><orcid>0000-0003-0992-2709</orcid><order>1</order></author><author><firstname>Anton</firstname><surname>Setzer</surname><orcid>0000-0001-5322-6060</orcid><order>2</order></author></authors><documents><document><filename>64152__28389__59f0ff018e414015bc5dcf53383c47ce.pdf</filename><originalFilename>64152.pdf</originalFilename><uploaded>2023-08-29T09:11:58.4821115</uploaded><type>Output</type><contentLength>953750</contentLength><contentType>application/pdf</contentType><version>Accepted Manuscript</version><cronfaStatus>true</cronfaStatus><embargoDate>2023-12-15T00:00:00.0000000</embargoDate><documentNotes>© 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.</documentNotes><copyrightCorrect>true</copyrightCorrect><language>eng</language></document></documents><OutputDurs/></rfc1807>
spelling v2 64152 2023-08-29 A simulator of Solidity-style smart contracts in the theorem prover Agda 5f7695285397f46d121207120247c2ae 0000-0001-5322-6060 Anton Setzer Anton Setzer true false 2023-08-29 MACS 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. Conference Paper/Proceeding/Abstract Proceedings of the 2023 6th International Conference on Blockchain Technology and Applications 1 11 ACM New York, NY, USA Agda, Ethereum, Solidity, blockchain, interface, simulator, smart contracts, theorem prover 15 12 2023 2023-12-15 10.1145/3651655.3651656 http://dx.doi.org/10.1145/3651655.3651656 COLLEGE NANME Mathematics and Computer Science School COLLEGE CODE MACS Swansea University 2024-06-11T15:20:27.6301362 2023-08-29T09:09:26.8815003 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Fahad Alhabardi 0000-0003-0992-2709 1 Anton Setzer 0000-0001-5322-6060 2 64152__28389__59f0ff018e414015bc5dcf53383c47ce.pdf 64152.pdf 2023-08-29T09:11:58.4821115 Output 953750 application/pdf Accepted Manuscript true 2023-12-15T00:00:00.0000000 © 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. true eng
title A simulator of Solidity-style smart contracts in the theorem prover Agda
spellingShingle A simulator of Solidity-style smart contracts in the theorem prover Agda
Anton Setzer
title_short A simulator of Solidity-style smart contracts in the theorem prover Agda
title_full A simulator of Solidity-style smart contracts in the theorem prover Agda
title_fullStr A simulator of Solidity-style smart contracts in the theorem prover Agda
title_full_unstemmed A simulator of Solidity-style smart contracts in the theorem prover Agda
title_sort A simulator of Solidity-style smart contracts in the theorem prover Agda
author_id_str_mv 5f7695285397f46d121207120247c2ae
author_id_fullname_str_mv 5f7695285397f46d121207120247c2ae_***_Anton Setzer
author Anton Setzer
author2 Fahad Alhabardi
Anton Setzer
format Conference Paper/Proceeding/Abstract
container_title Proceedings of the 2023 6th International Conference on Blockchain Technology and Applications
container_start_page 1
publishDate 2023
institution Swansea University
doi_str_mv 10.1145/3651655.3651656
publisher ACM
college_str Faculty of Science and Engineering
hierarchytype
hierarchy_top_id facultyofscienceandengineering
hierarchy_top_title Faculty of Science and Engineering
hierarchy_parent_id facultyofscienceandengineering
hierarchy_parent_title Faculty of Science and Engineering
department_str School of Mathematics and Computer Science - Computer Science{{{_:::_}}}Faculty of Science and Engineering{{{_:::_}}}School of Mathematics and Computer Science - Computer Science
url http://dx.doi.org/10.1145/3651655.3651656
document_store_str 1
active_str 0
description 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.
published_date 2023-12-15T15:20:26Z
_version_ 1801574811223195648
score 11.017797

Similar Items