Lolisa: Formal syntax and semantics for a subset of the solidity programming language in Mathematical Tool Coq

TL;DR

This paper introduces Lolisa, a formal syntax and semantics for a Solidity subset in Coq, enhancing type safety and enabling direct translation from Solidity with potential for extension to other languages.

Contribution

It develops the first mechanized formal syntax and semantics for Solidity, incorporating a stronger type system and facilitating language extension.

Findings

Lolisa includes most Solidity syntax components.

Lolisa allows direct line-by-line translation from Solidity.

It provides a foundation for extending to other programming languages.

Abstract

This article presents the formal syntax and semantics for a large subset of the Solidity programming language developed for the Etheruem blockchain platform based on our resent work about developing a general, extensible, and reusable formal memory (GERM) framework and an extension of Curry-Howard isomorphism, denoted as execution-verification isomorphism (EVI). This subset is denoted as Lolisa, which, to our knowledge, is the first mechanized and validated formal syntax and semantics developed for Solidity. The formal syntax of Lolisa adopts a stronger static type system than Solidity for enhanced type safety. In addition, Lolisa not only includes nearly all the syntax components of Solidity, such as mapping, modifier, contract, and address types, but it also contains general-purpose programming language features, such as multiple return values, pointer arithmetic, struct, and field access. Therefore, the inherent compatibility of Lolisa allows Solidity programs to be directly translated into Lolisa with a line-by-line correspondence without rebuilding or abstracting, and, in addition, the inherent generality of Lolisa allows it to be extended to express other programming languages as well. To this end, we also present a preliminary scheme for extending Lolisa to other languages systematically.