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