Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2604.22210 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866917432714592256 |
|---|---|
| author | Xu, Ziyun Wang, Hao Sun, Meng |
| author_facet | Xu, Ziyun Wang, Hao Sun, Meng |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2604_22210 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | From Monolithic to Compositional: A Compositional Operational Semantics for Crystality Xu, Ziyun Wang, Hao Sun, Meng Programming Languages 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. |
| title | From Monolithic to Compositional: A Compositional Operational Semantics for Crystality |
| topic | Programming Languages |
| url | https://arxiv.org/abs/2604.22210 |