From Monolithic to Compositional: A Compositional Operational Semantics for Crystality
Provides formal reasoning tools for parallel smart contract execution, benefiting blockchain developers and researchers seeking rigorous verification.
This paper introduces a compositional operational semantics for Crystality, a smart contract language for parallel EVMs, enabling simple proofs of locality, global isolation, and strong commutativity, and proves semantic equivalence to the original monolithic semantics via bisimulation theorems.
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.