Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Preventing Out-of-Gas Exceptions by Typing

Luca Aceto, Daniele Gorla, Stian Lybech, Mohammad Hamdaqa

TL;DR

This work extends a minimal Solidity-inspired language, TinySol, with a gas mechanism and exception handling to realistically model Ethereum-style smart-contract execution. It introduces a small-step operational semantics and a termination-focused type system that upper-bounds the number of execution steps for any transaction, thereby preventing out-of-gas failures. The core contributions include unit-gas semantics, a formal type-theoretic framework with bounded and unbounded integer types, and a subject-reduction theorem ensuring termination for well-typed configurations. The proposed approach enables static termination guarantees for smart-contract transactions, with clear limitations such as disallowing general recursion and while loops, and it outlines viable future directions toward more expressive termination proofs and practical case studies.

Abstract

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.

Preventing Out-of-Gas Exceptions by Typing

TL;DR

This work extends a minimal Solidity-inspired language, TinySol, with a gas mechanism and exception handling to realistically model Ethereum-style smart-contract execution. It introduces a small-step operational semantics and a termination-focused type system that upper-bounds the number of execution steps for any transaction, thereby preventing out-of-gas failures. The core contributions include unit-gas semantics, a formal type-theoretic framework with bounded and unbounded integer types, and a subject-reduction theorem ensuring termination for well-typed configurations. The proposed approach enables static termination guarantees for smart-contract transactions, with clear limitations such as disallowing general recursion and while loops, and it outlines viable future directions toward more expressive termination proofs and practical case studies.

Abstract

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.
Paper Structure (13 sections, 6 theorems, 5 equations, 11 figures)

This paper contains 13 sections, 6 theorems, 5 equations, 11 figures.

Table of Contents

  1. Introduction
  2. Related work
  3. TinySol with Gas and Exceptions
  4. A Small-step Semantics with Exceptions and Gas
  5. A Type System for Termination
  6. The Type System
  7. Properties of the type system
  8. Limitations of the type system
  9. Conclusion and Future Work
  10. Omitted Semantic Rules
  11. Subtyping rules
  12. Omitted type rules
  13. Proof of Theorem \ref{['thm:subject_reduction']} (subject reduction)

Key Result

theorem thmcountertheorem

Let $\Gamma \vdash \normalfont\text{\sffamily env}_{T}$ and $\Gamma, \Delta \vdash \left<Q, \normalfont\text{\sffamily env}_{SV}, g\right>$. If $\normalfont\text{\sffamily env}_{T} \vdash \left<Q, \normalfont\text{\sffamily env}_{SV}, g\right> \rightarrow \left<Q', \normalfont\text{\sffamily env}_{S

Figures (11)

  • Figure 1: The syntax of TinySol.
  • Figure 2: Small-step semantics transition rules for statements with gas.
  • Figure 3: Transition rules for blockchains.
  • Figure 4: Type rules for environment agreement.
  • Figure 5: Type rules for expressions
  • ...and 6 more figures

Theorems & Definitions (14)

  • definition thmcounterdefinition: Syntax of blockchains
  • definition thmcounterdefinition: Binding model
  • definition thmcounterdefinition: Syntax of stacks
  • definition thmcounterdefinition: Language of types
  • definition thmcounterdefinition: Extraction function
  • theorem thmcountertheorem: Subject reduction
  • corollary thmcountercorollary
  • lemma thmcounterlemma: Strengthening
  • proof
  • lemma thmcounterlemma: Update for variables
  • ...and 4 more