pith. machine review for the scientific record. sign in

arxiv: 2604.22210 · v1 · submitted 2026-04-24 · 💻 cs.PL

Recognition: unknown

From Monolithic to Compositional: A Compositional Operational Semantics for Crystality

Ziyun Xu , Hao Wang , Meng Sun
Authors on Pith no claims yet

Pith reviewed 2026-05-08 08:56 UTC · model grok-4.3

classification 💻 cs.PL
keywords compositional operational semanticsCrystalitysmart contractsparallel executionbisimulationblockchainEVMscoped state
0
0 comments X

The pith

Crystality admits a compositional operational semantics that decomposes parallel execution into local engines and a global coordinator while remaining equivalent to the monolithic model.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

This paper develops a compositional operational semantics for Crystality, a smart contract language built for parallel EVM execution that includes scoped state and asynchronous relays. The new semantics factors the system state into separate engine components that run locally plus one global component that handles coordination. This structure makes it direct to prove that local steps stay confined to their engines, that global state remains isolated, and that independent local steps commute. The authors then show the compositional version produces exactly the same behaviors as the original monolithic semantics by constructing a transaction-level bisimulation that uses encoding and decoding maps between configurations, plus separate code-level bisimulations for local and global steps. Readers care because the decomposition supplies modular reasoning tools for parallel smart contracts without requiring any change to observable outcomes.

Core claim

The paper establishes that the compositional operational semantics for Crystality, obtained by decomposing configurations into independent engine components and a global component, is semantically equivalent to the monolithic semantics. Equivalence follows from a transaction-level bisimulation theorem built on encoding and decoding functions between configurations, together with two code-level bisimulation theorems that cover local execution and global execution separately. The same decomposition yields elementary proofs of locality, global isolation, and strong commutativity of independent local steps.

What carries the argument

Decomposition of execution configurations into independent local engine components plus a single global component, connected by encoding and decoding functions that enable bisimulation proofs.

Load-bearing premise

The scoped state and asynchronous relay features of Crystality can be faithfully captured by a decomposition into independent engine components plus a global component, without omitting or adding behaviors relative to the monolithic semantics.

What would settle it

A Crystality program together with an execution trace that produces a different final state or observable transaction outcome under the compositional semantics than under the original monolithic semantics.

Figures

Figures reproduced from arXiv: 2604.22210 by Hao Wang, Meng Sun, Ziyun Xu.

Figure 1
Figure 1. Figure 1: A simplified banking contract deducts tokens from the sender’s balance and relays two operations: a deposit to the recipient and an update to the global variable total. Assume there are two execution engines. Let a,d be addresses managed by engine 1, and b,c be addresses managed by engine 2. Suppose the current block contains exactly two user-initiated transactions: transfer(b,3) sent by a and transfer(d,2… view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The paper claims to develop a compositional operational semantics for the Crystality smart contract language by decomposing the monolithic semantics into independent engine components and a global component. It proves structural properties including locality, global isolation, and strong commutativity of independent local steps. Additionally, it establishes semantic equivalence to the original semantics through a transaction-level bisimulation theorem using encoding and decoding functions, along with code-level bisimulation theorems for local and global execution.

Significance. If the results hold, this work is significant for providing a more structured and modular semantics for parallel execution in blockchain smart contracts, which can simplify reasoning about scalability features like scoped state and asynchronous relays. The use of standard bisimulation techniques for proving equivalence is a strength, as it allows for rigorous verification of the decomposition. This could aid in the development of formal tools for parallel EVMs.

minor comments (2)
  1. The abstract is clear but could briefly mention the key structural properties proved to give readers a better overview.
  2. Consider adding a small example configuration to illustrate the encoding and decoding functions between monolithic and compositional semantics.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive and accurate summary of our paper on the compositional operational semantics for Crystality. The assessment correctly identifies the decomposition into engine and global components, the proofs of locality, isolation, and commutativity, as well as the bisimulation-based equivalence results. We appreciate the recommendation for minor revision and will incorporate any editorial suggestions in the revised manuscript.

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper introduces a compositional operational semantics for Crystality by decomposing the system into engine components and a global component, then proves semantic equivalence to the prior monolithic semantics via a transaction-level bisimulation (with encoding/decoding functions) and two code-level bisimulations. This is a standard formal-methods construction using conventional bisimulation techniques; the equivalence proof is independent of the definitions and does not reduce any claim to a fitted parameter, self-referential definition, or load-bearing self-citation. The derivation chain is self-contained against external benchmarks in operational semantics.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The central claim rests on standard mathematical concepts from operational semantics and concurrency theory with no free parameters or new postulated entities.

axioms (2)
  • standard math Operational semantics are defined using transition rules on configurations.
    This is the established foundation for defining program behavior in programming language theory.
  • standard math Bisimulation relations prove behavioral equivalence between different semantic definitions.
    Bisimulation is a standard technique for showing that two transition systems exhibit the same observable behavior.

pith-pipeline@v0.9.0 · 5436 in / 1314 out tokens · 59681 ms · 2026-05-08T08:56:14.461193+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

41 extracted references · 3 canonical work pages

  1. [1]

    8 innovations that make solana the first web-scale blockchain (2019), https://solana.com/news/8-innovations-that-make-solana-the-first- web-scale-blockchain

    2019

  2. [2]

    Solidity documentation (2021),https://docs.soliditylang.org/en/latest/

    2021

  3. [3]

    The aptos blockchain: safe, scalable, and upgradeable web3 infrastructure (2022), https://aptosfoundation.org/whitepaper/aptos-whitepaper_en.pdf

    2022

  4. [4]

    The sui smart contracts platform (2023),https://docs.sui.io/paper/sui.pdf

    2023

  5. [5]

    Verification: Theory and Practice: Essays Dedicated to Zohar Manna on the Occasion of His 64th Birthday pp

    Ábrahám, E., de Boer, F.S., de Roever, W.P., Steffen, M.: A compositional opera- tional semantics for java mt. Verification: Theory and Practice: Essays Dedicated to Zohar Manna on the Occasion of His 64th Birthday pp. 290–303 (2003)

    2003

  6. [6]

    arXiv preprint arXiv:1708.03778 (2017)

    Al-Bassam, M., Sonnino, A., Bano, S., Hrycyszyn, D., Danezis, G.: Chainspace: A sharded smart contracts platform. arXiv preprint arXiv:1708.03778 (2017)

    work page arXiv 2017

  7. [7]

    In: 2019 27th Euromicro International Conference on Parallel, Distributed and Network-Based Processing (PDP)

    Anjana, P.S., Kumari, S., Peri, S., Rathor, S., Somani, A.: An efficient framework for optimistic concurrent execution of smart contracts. In: 2019 27th Euromicro International Conference on Parallel, Distributed and Network-Based Processing (PDP). pp. 83–92. IEEE (2019)

    2019

  8. [8]

    In: Proceedings of the 2016 ACM workshop on programming languages and analysis for security

    Bhargavan, K., Delignat-Lavaud, A., Fournet, C., Gollamudi, A., Gonthier, G., Kobeissi, N., Kulatova, N., Rastogi, A., Sibut-Pinote, T., Swamy, N., et al.: Formal verification of smart contracts: Short paper. In: Proceedings of the 2016 ACM workshop on programming languages and analysis for security. pp. 91–96 (2016)

    2016

  9. [9]

    In: Proceedings of the ACM SIGOPS 28th Symposium on Operating Systems Principles

    Chen, Y., Guo, Z., Li, R., Chen, S., Zhou, L., Zhou, Y., Zhang, X.: Forerunner: Constraint-based speculative transaction execution for ethereum. In: Proceedings of the ACM SIGOPS 28th Symposium on Operating Systems Principles. pp. 570– 587 (2021)

    2021

  10. [10]

    New Generation Computing10, 315–328 (1992)

    Cheng, M.H., Horspool, R.N., Levy, M.R., Van Emden, M.: Compositional oper- ational semantics for prolog programs. New Generation Computing10, 315–328 (1992)

    1992

  11. [11]

    VALID pp

    Crosara, M., Centurino, G., Arceri, V.: Towards an operational semantics for so- lidity. VALID pp. 1–6 (2019)

    2019

  12. [12]

    In: Proceedings of the ACM Symposium on Principles of Distributed Computing

    Dickerson, T., Gazzillo, P., Herlihy, M., Koskinen, E.: Adding concurrency to smart contracts. In: Proceedings of the ACM Symposium on Principles of Distributed Computing. pp. 303–312 (2017)

    2017

  13. [13]

    In: Proceedings of the 44th International Conference on Software Engineering

    Garamvölgyi, P., Liu, Y.,Zhou, D., Long, F.,Wu, M.:Utilizing parallelism in smart contracts on decentralized blockchains by taming application-inherent conflicts. In: Proceedings of the 44th International Conference on Software Engineering. pp. 2315–2326 (2022)

    2022

  14. [14]

    In: Proceedings of the 28th ACM SIGPLAN Annual Sym- posium on Principles and Practice of Parallel Programming

    Gelashvili, R., Spiegelman, A., Xiang, Z., Danezis, G., Li, Z., Malkhi, D., Xia, Y., Zhou, R.: Block-stm: Scaling blockchain execution by turning ordering curse to a performance blessing. In: Proceedings of the 28th ACM SIGPLAN Annual Sym- posium on Principles and Practice of Parallel Programming. pp. 232–244 (2023)

    2023

  15. [15]

    Grishchenko, I., Maffei, M., Schneidewind, C.: A semantic framework for the secu- rity analysis of ethereum smart contracts. In: Principles of Security and Trust: 7th International Conference, POST 2018, Held As Part of the European Joint Con- ferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings 7. ...

    2018

  16. [16]

    In: Verified Software

    Hajdu, Á., Jovanovic, D.: solc-verify: A modular verifier for solidity smart con- tracts. In: Verified Software. Theories, Tools, and Experiments. LNCS, vol. 12031, pp. 161–179. Springer (2019) 18 Z. Xu et al

    2019

  17. [17]

    In: Proceedings of ESOP 2020

    Hajdu, Á., Jovanovic, D.: Smt-friendly formalization of the solidity memory model. In: Proceedings of ESOP 2020. LNCS, vol. 12075, pp. 224–250. Springer (2020)

    2020

  18. [18]

    Prentice Hall (1998)

    Hoare, C.A.R., He, J.: Unifying theories of programming. Prentice Hall (1998)

    1998

  19. [19]

    Rap- port Technique178, 113 (1997)

    Huet, G., Kahn, G., Paulin-Mohring, C.: The coq proof assistant a tutorial. Rap- port Technique178, 113 (1997)

    1997

  20. [20]

    Jiao, J., Kan, S., Lin, S., Sanán, D., Liu, Y., Sun, J.: Executable operational se- manticsofsolidity.CoRRabs/1804.01295(2018),http://arxiv.org/abs/1804. 01295

    work page arXiv 2018

  21. [21]

    In: Proceedings of SP 2020

    Jiao, J., Kan, S., Lin, S., Sanán, D., Liu, Y., Sun, J.: Semantic understanding of smart contracts: Executable operational semantics of solidity. In: Proceedings of SP 2020. pp. 1695–1712. IEEE (2020)

    2020

  22. [22]

    In: Proceedings of the 2016 ACM SIGSAC conference on computer and communications security

    Luu, L., Chu, D.H., Olickel, H., Saxena, P., Hobor, A.: Making smart contracts smarter. In: Proceedings of the 2016 ACM SIGSAC conference on computer and communications security. pp. 254–269 (2016)

    2016

  23. [23]

    In: Proceedings of SEFM 2021

    Marmsoler, D., Brucker, A.D.: A denotational semantics of solidity in isabelle/hol. In: Proceedings of SEFM 2021. LNCS, vol. 13085, pp. 403–422. Springer (2021)

    2021

  24. [24]

    The Journal of Logic and Algebraic Programming60, 195–228 (2004)

    Mosses, P.D.: Modular structural operational semantics. The Journal of Logic and Algebraic Programming60, 195–228 (2004)

    2004

  25. [25]

    Plotkin, G.D.: A structural approach to operational semantics (1981)

    1981

  26. [26]

    In: 2023 IEEE 43rd International Conference on Distributed Computing Systems (ICDCS)

    Qi, X., Jiao, J., Li, Y.: Smart contract parallel execution with fine-grained state accesses. In: 2023 IEEE 43rd International Conference on Distributed Computing Systems (ICDCS). pp. 841–852. IEEE (2023)

    2023

  27. [27]

    Sanka, A.I., Cheung, R.C.C.: A systematic review of blockchain scalability: Issues, solutions, analysis and future research. J. Netw. Comput. Appl.195, 103232 (2021)

    2021

  28. [28]

    In: Proceedings of the 30th ACM SIGPLAN Annual Symposium on Principles and Practice of Parallel Programming

    Wang,H.,Pan,M.,Wang,J.:Crystality:Aprogrammingmodelforsmartcontracts on parallel evms. In: Proceedings of the 30th ACM SIGPLAN Annual Symposium on Principles and Practice of Parallel Programming. p. 412–425. PPoPP ’25, As- sociation for Computing Machinery (2025)

    2025

  29. [29]

    MIT Press (1993)

    Winskel, G.: The formal semantics of programming languages - an introduction. MIT Press (1993)

    1993

  30. [30]

    In: International Symposium on Theoretical Aspects of Software Engineering

    Xu, Z., Wang, H., Sun, M.: Operational semantics for crystality: A smart contract language for parallel evms. In: International Symposium on Theoretical Aspects of Software Engineering. pp. 303–321. Springer (2025)

    2025

  31. [31]

    CoRRabs/1803.09885(2018),http://arxiv.org/abs/ 1803.09885

    Yang, Z., Lei, H.: Lolisa: Formal syntax and semantics for a subset of the solidity programming language. CoRRabs/1803.09885(2018),http://arxiv.org/abs/ 1803.09885

    work page arXiv 2018

  32. [32]

    In: Verified Software

    Zakrzewski, J.: Towards verification of ethereum smart contracts: A formalization of core of solidity. In: Verified Software. Theories, Tools, and Experiments. LNCS, vol. 11294, pp. 229–247. Springer (2018) A Syntax of Crystality In the following, we give the whole syntax of Crystality, represented by a variant of Extended Backus-Naur Form (known as EBNF)...

    2018

  33. [33]

    Lemma 8 (Agreement of local stacks during global execution).Let C o = (σo 1, Ωo 1, P rogo 1,

    = · · ·=gprefix(P rog o n)is preserved throughout execution. Lemma 8 (Agreement of local stacks during global execution).Let C o = (σo 1, Ωo 1, P rogo 1, . . . , σo n, Ωo n, P rogo n, Go) be a well-formed configuration of the original semantics, where σo i = (Ψ o i , M o i ) (1≤i≤n). If gprefix(P rogo i )̸=· for somei(and hence for alli, by well-formednes...

  34. [34]

    If this common global prefix is non-empty, then the system is currently execut- ing global transactions

    =· · ·=gprefix(P rog o n). If this common global prefix is non-empty, then the system is currently execut- ing global transactions. In the original semantics, global functions are executed jointly by all engines using the same code, and their execution is synchronized by the consensus mechanism. Therefore, the temporary stacks maintained by all engines ev...

  35. [35]

    thei-th component ofΓisγ i; and

  36. [36]

    Definition 11 (Local correspondence).Leti∈ {1,

    the global program is empty, i.e.,P rogG =·. Definition 11 (Local correspondence).Leti∈ {1, . . . , n}. We write Rl(i, γi, Co) if there exists a configurationCsuch that 1.W rap l(i, γi, C); 2.R(C o, C); and

  37. [37]

    Remark 4.Intuitively, the relationR l isolates the behavior of a single enginei during the local phase

    for every enginej,gprefix(P rog o j) =·. Remark 4.Intuitively, the relationR l isolates the behavior of a single enginei during the local phase. The conditionW rapl(i, γi, C)embeds the componentγ i into a well-formed system configuration in which no global transactions remain to be executed. The relationR(Co, C)then establishes the code-level correspon- d...

  38. [38]

    the global component ofCis¯γG, i.e.,γ G = ¯γG

  39. [39]

    the global program is non-empty, i.e.,P rogG ̸=·; and

  40. [40]

    for every local componentγi inΓ, its program is empty, i.e.,P rogi =·. 40 Z. Xu et al. Definition 15 (Global correspondence).We write Rg(γG, Co) if there exists a configurationCsuch that 1.W rap g(γG, C); 2.R(C o, C); and

  41. [41]

    Remark 8.The relationW rap g isolates the global phase of execution

    for every enginei,gprefix(P rog o i )̸=·. Remark 8.The relationW rap g isolates the global phase of execution. It embeds the global componentγ G into a well-formed system configuration in which the global program is still pending, while all local components are inactive. Remark 9.Intuitively, the relationR g matches a global component in the com- position...