From Monolithic to Compositional: A Compositional Operational Semantics for Crystality

TL;DR

This paper presents a compositional operational semantics for Crystality, a parallel smart contract language, enabling formal reasoning about parallel execution in blockchain systems.

Contribution

It introduces a new compositional semantics that decomposes the system into components, facilitating proofs of key properties and equivalence to the original semantics.

Findings

Proves locality, global isolation, and commutativity of local steps.

Establishes semantic equivalence via bisimulation theorems.

Enables rigorous reasoning about parallel smart contract execution.

Abstract

Parallel execution has become a key approach to improving blockchain scalability, but the lack of formal semantics for smart contract languages in such settings makes rigorous reasoning difficult. Crystality is a smart contract language designed for parallel EVMs, supporting scoped state and asynchronous relay across execution engines. This paper introduces a compositional operational semantics for Crystality. Unlike the original monolithic semantics, the new semantics decomposes the system into engine components and a global component, making the structure of parallel execution explicit. The compositional formulation enables simple proofs of key structural properties, including locality, global isolation, and strong commutativity of independent local steps. Furthermore, we prove that the compositional semantics is semantically equivalent to the original one via a transaction-level bisimulation theorem based on encoding and decoding functions between configurations, and two code-level bisimulation theorems for local and global execution.