Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2407.15676 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866916331881758720 |
|---|---|
| author | Aceto, Luca Gorla, Daniele Lybech, Stian Hamdaqa, Mohammad |
| author_facet | Aceto, Luca Gorla, Daniele Lybech, Stian Hamdaqa, Mohammad |
| contents | We continue the development of TinySol, a minimal object-oriented language based on Solidity, the standard smart-contract language used for the Ethereum platform. We first extend TinySol with exceptions and a gas mechanism, and equip it with a small-step operational semantics. Introducing the gas mechanism is fundamental for modelling real-life smart contracts in TinySol, since this is the way in which termination of Ethereum smart contracts is usually ensured. We then devise a type system for smart contracts guaranteeing that such programs never run out of gas at runtime. This is a desirable property for smart contracts, since a transaction that runs out of gas is aborted, but the price paid to run the code is not returned to the invoker. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2407_15676 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Preventing Out-of-Gas Exceptions by Typing Aceto, Luca Gorla, Daniele Lybech, Stian Hamdaqa, Mohammad Programming Languages We continue the development of TinySol, a minimal object-oriented language based on Solidity, the standard smart-contract language used for the Ethereum platform. We first extend TinySol with exceptions and a gas mechanism, and equip it with a small-step operational semantics. Introducing the gas mechanism is fundamental for modelling real-life smart contracts in TinySol, since this is the way in which termination of Ethereum smart contracts is usually ensured. We then devise a type system for smart contracts guaranteeing that such programs never run out of gas at runtime. This is a desirable property for smart contracts, since a transaction that runs out of gas is aborted, but the price paid to run the code is not returned to the invoker. |
| title | Preventing Out-of-Gas Exceptions by Typing |
| topic | Programming Languages |
| url | https://arxiv.org/abs/2407.15676 |