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.

翻译：并行执行已成为提升区块链可扩展性的关键途径，但在此类场景下智能合约语言缺乏形式语义，导致严格推理难以进行。Crystality是为并行EVM设计的智能合约语言，支持作用域状态和跨执行引擎的异步中继。本文提出了Crystality的组合式操作语义。与原有的整体式语义不同，新语义将系统分解为引擎组件和全局组件，使并行执行的结构更加明确。组合式表述能够简洁地证明关键结构性质，包括局部性、全局隔离性以及独立局部步骤的强交换性。此外，我们通过基于配置间编码与解码函数的事务级孪拟定理，以及两个分别针对局部执行与全局执行的代码级孪拟定理，证明了组合式语义与原始语义在语义上等价。