Operational Semantics for Crystality: A Smart Contract Language for Parallel EVMs

TL;DR

Crystality addresses blockchain scalability by introducing a parallel smart contract language designed for parallel EVMs, featuring Programmable Contract Scopes and Asynchronous Functional Relay. The authors present the first structural operational semantics for Crystality and implement the core model in Coq to enable mechanized verification. A token transfer case study demonstrates correctness properties, including balance updates and relay-based recipient updates, and a refinement relation between transfers. This formal foundation supports secure, scalable, and verifiable parallel smart contracts with potential impact on throughput and security in blockchain systems.

Abstract

The increasing demand for scalable blockchain has driven research into parallel execution models for smart contracts. Crystality is a novel smart contract programming language designed for parallel Ethereum Virtual Machines (EVMs), enabling fine-grained concurrency through Programmable Contract Scopes and Asynchronous Functional Relay. This paper presents the first formal structural operational semantics for Crystality, providing a rigorous framework to reason about its execution. We mechanize the syntax and semantics of Crystality in the theorem-proving assistant Coq, enabling formal verification of correctness properties. As a case study, we verify a simplified token transfer function, demonstrating the applicability of our semantics in ensuring smart contract correctness. Our work lays the foundation for formally verified parallel smart contracts, contributing to the security and scalability of blockchain systems.