A minimal core calculus for Solidity contracts

Letterio Galletta; Massimo Bartoletti; Maurizio Murgia

REVIEW 2 major objections 4 minor 19 references

A minimal core calculus for Solidity contracts

T0 review · 2 major / 4 minor · reviewed 2026-08-14 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read One call-and-transfer primitive reproduces Solidity's re-entrancy

desk verdict A clean minimal calculus whose reentrancy examples work, but the flagship escrow example is broken under the paper's own semantics, and no formal link to Solidity is established. read the letter →

arxiv 1908.02709 v1 pith:AQ4THOZI submitted 2019-08-06 cs.PL

Massimo Bartoletti , Letterio Galletta , Maurizio Murgia This is my paper · ORCID

classification cs.PL

keywords EthereumsmartcontractsSolidityTinySolcorecalculusoperationalsemanticsre-entrancyblockchaintransactions

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

TinySol is a deliberately small core calculus for Solidity-style smart contracts: an imperative language with key-value stores, plus a single construct that performs an external procedure call and a currency transfer in one step. The paper gives this calculus a big-step operational semantics, then layers transaction and blockchain semantics on top, so that a sequence of transactions folds into a resulting global state. The authors demonstrate the calculus on a harmless re-entrancy attempt, a vicious DAO-style re-entrancy drain, and several realistic contracts including wallets, escrow, a lottery, and a Ponzi scheme. The claim is that this minimal calculus is expressive enough to support formal reasoning about typical Solidity quirks, most notably re-entrancy, in a way that full-language formalizations make harder.

What carries the argument

The load-bearing object is the call-and-transfer primitive, the only contract-oriented construct in TinySol. Its semantics first checks that the caller has enough balance and that the target contract has the named procedure, then transfers the currency, binds `sender` and `value`, and evaluates the callee body in the callee's address with the caller as a visible context. Because the callee can in turn call back into the caller, re-entrancy arises naturally from the primitive itself. The transaction layer then wraps this with two rules: a successful transaction is one whose procedure body terminates with a defined state, and any undefined or divergent execution reverts the entire state.

What would settle it

Execute on the EVM a transaction whose body is just `throw`, with a positive gas price, and record the post-transaction balances of the sender and the miner. Ethereum's resulting state decreases the sender's balance by the gas cost and increases the miner's, while TinySol's transaction rule predicts the original state unchanged. That observable difference settles that the calculus's failure semantics is not a faithful full-state model of Ethereum unless gas is explicitly excluded from the notion of state.

Watch

Extended reading notes

Core claim

The paper's central claim is that a minimal imperative calculus extended with a single external call-and-transfer primitive is enough to model the distinctive behavior of Solidity contracts. In TinySol, a procedure call moves the currency, binds the special names `sender` and `value`, and executes the callee's body in the callee's own context, which makes re-entrancy a derived behavior rather than a special feature. The semantics treats every statement whose evaluation is undefined, including exceptions, failed call preconditions, and nontermination, as having no result, and the transaction rule reverts the whole state in those cases. This gives a two-rule account of transaction success and failure: either the callee terminates normally and the state advances, or the transaction leaves the state untouched. The paper supports the claim by proving re-entrancy scenarios by hand and by encoding a range of example contracts, all within the single-primitive calculus.

Load-bearing premise

The load-bearing assumption is that any statement whose evaluation is undefined, whether from a failed call condition, an exception, or nontermination, makes the whole transaction revert to its initial state, and that this is how Solidity and Ethereum actually behave; the paper states this equivalence rather than proving it by a compilation, simulation, or bisimulation.

Editorial extensions

If this is right

Re-entrancy attacks can be stated and proved within TinySol without any extra machinery, as shown by both the failed attack and the successful drain.
Transactions that fail, throw, or diverge become no-ops on the global state, giving a simple all-or-nothing model of Ethereum's revert behavior at the contract-state level.
Representing a blockchain as a sequence of transactions lets the authors reason about transaction reordering and forks by folding the transaction semantics over the sequence.
Because the calculus is tiny, it is a plausible target for proof techniques such as axiomatic or denotational semantics, and for static analyses of smart contracts.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

The biggest payoff would be a compiler or abstraction from Solidity to TinySol: if one existed, verification tools could reason about the calculus instead of the full language or EVM bytecode.
Treating bottom as transaction-wide rollback suggests that a denotational semantics or Hoare-style logic for TinySol could capture safety properties like 'value never leaves the contract except through authorized procedures'.
A testable extension would add an abstract gas model and check whether gas-dependent outcomes, such as out-of-gas rollback after partial execution, remain indistinguishable from explicit throws under TinySol's current semantics.
The key-value store abstraction likely makes TinySol a natural setting for data-flow and taint analyses that track whether attacker-controlled values can reach a call-and-transfer site.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

Colleague,

TinySol is a clean, carefully worked-out core calculus: an imperative language with key-value stores, plus a single call-and-transfer primitive, with a big-step semantics and a transaction-sequence blockchain semantics. The reentrancy derivations in Section 3 are correct as far as I checked, and they show the calculus can express both harmless and vicious reentrancy succinctly. The blockchain-as-sequence model is a genuine difference from Featherweight Solidity, which treats blockchains as functions from contract IDs to states, and it is the right foundation if you want to talk about transaction reordering and forks.

That is the good news. The bad news is that the paper's showcase escrow example in Section 5.2 does not work under the paper's own semantics. In TinySol, the statement `?escrow:?buyer $ (...)` inside Oracle.closeDispute is a call evaluated in the context X = Oracle, so the balance precondition is `n ≤ σ_Oracle balance` and the transfer comes out of Oracle's balance, not out of TinyEscrow's. If Oracle's balance is zero (which is the normal case, since the deposit went to TinyEscrow), the call is undefined and [Tx2] reverts the whole transaction, so the buyer and seller never get paid. The contract has no payout function for the oracle to invoke, so this is not a typo; it points at a real limitation of the single call-and-transfer primitive. The example needs a different design, for instance a function on TinyEscrow that the oracle can authorize.

There are two more soft spots. First, the paper never establishes a formal correspondence between TinySol and Solidity or EVM – no compilation, no bisimulation, no abstraction. The authors say the call primitive is 'inspired by' Solidity external calls, and Section 6 lists omissions, but the failure model (failed calls and nontermination as bottom, rolled back by [Tx2]) is asserted rather than derived. Second, the paper says the sequence-based blockchain lets you reason about forks, but no fork example appears; the claim is undemonstrated.

Proportionately, the core calculus itself is sound and the reentrancy examples are valuable. The problems are in the examples and the framing. A careful revision that fixes the escrow contract and explicitly labels the abstraction as a design assumption would make this a solid paper. I would send it to a serious referee rather than desk reject, because the calculus is clean and the sequence-semantics idea is worth examining, but I would not cite it in its current form.

Referee Report

2 major / 4 minor

Summary. The paper introduces TinySol, a minimal imperative core calculus for Solidity-like smart contracts, featuring a single construct for external calls and currency transfers. It gives a big-step operational semantics for statements, a transaction-level semantics with rollback on undefined outcomes, and a blockchain semantics as a sequence of transactions. The paper illustrates the calculus with reentrancy derivations in Section 3 and with larger examples in Section 5, including a wallet, an escrow contract, a lottery, and a Ponzi scheme. The central claim is that TinySol is expressive enough to reason about typical Solidity quirks such as reentrancy.

Significance. If the expressiveness claim were fully established, TinySol would be a useful foundation for reasoning about smart contract behavior: the big-step semantics is clean, the reentrancy derivations in Section 3 are detailed enough to verify by hand and are internally coherent, and the transaction semantics is simple. The paper ships no mechanized proofs or code, but the derivations are explicit and checkable. However, the incorrect escrow example in Section 5.2 and the absence of a formal correspondence between TinySol and Solidity or EVM currently limit the significance of the claimed contribution.

major comments (2)

[§5.2, Fig. 4] In Oracle.closeDispute (Fig. 4, lines 32–35), the statements `?escrow:?buyer $ (...)` and `?escrow:?seller $ ...` are evaluated with X = Oracle, because the Oracle contract is the one executing closeDispute. According to the call rule in Fig. 2, the precondition n ≤ σX balance therefore refers to Oracle's balance, and the transfer deducts from Oracle's balance, not from TinyEscrow's balance. If Oracle's balance is 0, these calls are undefined and rule [Tx2] reverts the whole transaction, so the buyer and seller are never paid. This contradicts the intended escrow behavior and the paper's own note that the escrow's balance is zero after pay/refund; the example must be repaired, for instance by adding a payout procedure to TinyEscrow that the Oracle can invoke, or by extending the calculus with an explicit source address for transfers. As written, this example does not demonstrate that TinySol can express escrow services.
[§1, §4, §6] The abstract and introduction claim that TinySol is a calculus 'for Solidity contracts' and that the paper gives 'semantics to the Ethereum blockchain', but no formal correspondence between TinySol and Solidity or EVM is provided, such as a compilation, a simulation, or an abstraction. Section 6 acknowledges that gas, dynamic contract creation, fallback functions, and delegate calls are omitted, and Section 4's rules [Tx1] and [Tx2] treat nontermination or failed preconditions as full transaction rollback. This rollback behavior is a design assumption, not a derived result about Solidity. The examples are internally consistent with TinySol, but the 'for Solidity' claim would require a formal link or at least a precise statement of the intended correspondence; otherwise the paper should be framed as a calculus inspired by Solidity rather than a semantics for it.

minor comments (4)

[§3, Example 4] The derivation starts with `/llbracket S /rrbracket^X_{σ,ρ}` for a statement whose first step evaluates a call to C, and then switches to evaluating the body in C; stating at the outset that the initial call is evaluated in the context of C would avoid ambiguity about which contract's balance is checked.
[§5.4, Fig. 6] The assignment `?n := (sender,value)` uses the current value of n as a key; the text should explain explicitly that keys are values and that this updates the array entry indexed by the current number of investors, since the notation `?n` on the left-hand side is nonstandard.
[§2, Fig. 2] The presentation would be clearer if the strictness of all semantic operators, including the behavior of `!E` and `?E` on undefined subexpressions, were stated directly in the rule preamble rather than in the surrounding prose.
[§5.2, paragraph after Fig. 4] The sentence about the first four instructions of closeDispute having 'null' effect conflates the balance of Oracle with the balance of TinyEscrow; even after the escrow is empty, the transfers described would be evaluated against Oracle's balance under the current call rule.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: TinySol is defined from scratch in Section 2, and the claimed expressiveness examples are derived directly from the big-step semantics, with no fitted parameters and no load-bearing self-citations.

full rationale

The paper's derivation chain is self-contained. TinySol's syntax (Figure 1) and big-step semantics (Figure 2) are introduced from first principles, and the transaction semantics [Tx1]/[Tx2] is defined directly on top of that calculus. The claim that TinySol is expressive enough to reason about Solidity quirks such as re-entrancy is supported by explicit derivations in Examples 4 and 5, which unfold the call rule step by step. There are no fitted parameters, no quantities predicted from a fitted subset, and no result that reduces by construction to an input. The only self-citation in the references ([3], a survey of Ethereum attacks) is used as background motivation for the re-entrancy examples, not as a load-bearing formal premise. The paper also openly acknowledges its limitations in Section 6 (no gas mechanism, fixed contract set, no dynamic creation, no fallback/delegate/internal calls), which is an honest scoping statement rather than an attempt to smuggle in assumptions as derivations. Even if the Section 5.2 escrow example is internally inconsistent with the call rule — as the skeptic contends — that would be a correctness flaw, not circularity: it does not make the paper's claims equivalent to their inputs. Therefore the appropriate circularity score is 0.

Assumptions & free parameters 0 free parameters · 4 assumptions · 0 invented entities

TinySol is a definitional calculus, so the central claim rests on modeling choices rather than fitted parameters. No free parameters or invented physical entities are introduced. The key axioms are standard semantic assumptions about well-typedness, a fixed contract universe, strict error propagation, and the account model; these are stated or acknowledged in Sections 2, 4, and 6.

assumptions (4)

domain assumption Expressions and statements are well-typed, e.g., guards in conditionals and loops have type bool.
Stated as postulate (ii) in Section 2; needed for the semantics to be defined on well-formed programs and to avoid runtime type errors.
domain assumption The mapping Gamma from addresses to contracts is fixed; no dynamic contract creation.
Assumed in Section 2 and acknowledged in Section 6 as a divergence from Ethereum, where contracts can be created at runtime.
domain assumption All semantic operators are strict, so bottom propagates, and a statement with no derivation tree has undefined semantics.
Defined in Section 2; this partiality is what allows rule [Tx2] to roll back failed or nonterminating transactions.
domain assumption Account addresses have exactly one key (balance) and only the procedure fskip.
Postulated in Section 2 to unify accounts and contracts; needed for pure currency transfers to accounts.

how reviews work

0 comments

Cite this review

Pith. "Pith review of A minimal core calculus for Solidity contracts." pith.science (2026). https://pith.science/paper/AQ4THOZI

@misc{pith2026190802709,
  author       = {Pith},
  title        = {Pith review of: A minimal core calculus for Solidity contracts},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/AQ4THOZI}},
  note         = {Machine review of arXiv:1908.02709}
}

read the original abstract

The Ethereum platform supports the decentralized execution of smart contracts, i.e. computer programs that transfer digital assets between users. The most common language used to develop these contracts is Solidity, a Javascript-like language which compiles into EVM bytecode, the language actually executed by Ethereum nodes. While much research has addressed the formalisation of the semantics of EVM bytecode, relatively little attention has been devoted to that of Solidity. In this paper we propose a minimal calculus for Solidity contracts, which extends an imperative core with a single primitive to transfer currency and invoke contract procedures. We build upon this formalisation to give semantics to the Ethereum blockchain. We show our calculus expressive enough to reason about some typical quirks of Solidity, like e.g. re-entrancy.

Figures

Figures reproduced from arXiv: 1908.02709 by the authors.

**Figure 1.** Syntax of TinySol. procedures in Γ(C) have distinct names; (iii) the key balance cannot stay at the left of an assignment; (iv) the constant names sender and value cannot stay in the formal parameters of a procedure. We use the following syntactic sugar. For a call X : f(v)$n, when there is no money transfer (i.e., n = 0) we just write it as X : f(v); when the target is an account address A (so, the call is to the p… view at source ↗

**Figure 2.** Semantics of statements and expressions. [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗

**Figure 3.** An extended wallet contract. 5.2 An escrow contract In [PITH_FULL_IMAGE:figures/full_fig_p009_3.png] view at source ↗

Figures from the paper (3 more)

**Figure 4.** Figure 4: An escrow contract using an oracle. ensure that a participant cannot authorize a transfer to herself. Either buyer and seller can call dispute, which in turns calls the procedure openDispute of the contract at address oracle. A possible contract with this procedure is …

**Figure 5.** Figure 5: A two-players lottery. 2 units of currency as collateral, which are used as compensation in case of dishonest behaviour. The procedure join allows the players to join the lottery; the parameter h is the hash of a secret, used to implement a timed commitment protocol, s…

**Figure 6.** Figure 6: A Ponzi scheme. The procedure init sets the contract owner, and initializes to 0 the key n, which counts the total number of investors, and p, which counts the number of investors who have been paid. The procedure join allows users to invest money, and distributes the …

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

19 extracted references · 16 canonical work pages

[1]

https://solidity.readthedocs.io/en/v0.5.4/ (2019)

Solidity documentation. https://solidity.readthedocs.io/en/v0.5.4/ (2019)

work page 2019
[2]

Andrychowicz, M., Dziembowski, S., Malinowski, D., Mazu rek, L.: Secure multi- party computations on Bitcoin. Commun. ACM 59(4), 76–84 (20 16)

work page
[3]

In: POST

Atzei, N., Bartoletti, M., Cimoli, T.: A survey of attacks on Ethereum smart con- tracts (SoK). In: POST. LNCS, vol. 10204, pp. 164–186. Sprin ger (2017)

work page 2017
[4]

In: Financial Cryptography Workshops

Biryukov, A., Khovratovich, D., Tikhomirov, S.: Findel: Secure derivative contracts for Ethereum. In: Financial Cryptography Workshops. LNCS, vol. 10323, pp. 453–

work page
[5]

https://github.com/ethereum/wiki/wiki/White-Paper (2013)

Buterin, V.: Ethereum: a next generation smart contract a nd decentralized applica- tion platform. https://github.com/ethereum/wiki/wiki/White-Paper (2013)

work page 2013
[6]

Crafa, S., Pirro, M.D., Zucca, E.: Is Solidity solid enoug h? In: Financial Cryptog- raphy Workshops (2019)

work page 2019
[7]

Business & Information Systems Engineering 59(6), 457–467 (2017)

Egelund-M¨ uller, B., Elsman, M., Henglein, F., Ross, O.: Automated execution of ﬁnancial contracts on blockchains. Business & Information Systems Engineering 59(6), 457–467 (2017)

work page 2017
[8]

In: IEEE Compute r Security Foun- dations Symposium (CSF)

Hildenbrandt, E., Saxena, M., Rodrigues, N., Zhu, X., Dai an, P., Guth, D., Moore, B.M., Park, D., Zhang, Y., Stefanescu, A., Rosu, G.: KEVM: A c omplete formal semantics of the Ethereum Virtual Machine. In: IEEE Compute r Security Foun- dations Symposium (CSF). pp. 204–217. IEEE Computer Societ y (2018)

work page 2018

Show all 19 references

[9]

ACM Trans

Igarashi, A., Pierce, B.C., Wadler, P.: Featherweight Ja va: a minimal core calculus for Java and GJ. ACM Trans. Program. Lang. Syst. 23(3), 396–4 50 (2001)

2001
[10]

CoRR abs/1804.01295 (2018)

Jiao, J., Kan, S., Lin, S., San´ an, D., Liu, Y., Sun, J.: Ex ecutable operational semantics of Solidity. CoRR abs/1804.01295 (2018)

2018 arXiv
[11]

Soft- ware: Practice and Experience (2019)

L´ opez-Pintado, O., Garc ´ ıa-Ba˜ nuelos, L., Dumas, M.,Weber, I., Ponomarev, A.: Caterpillar: A business process execution engine on the Eth ereum blockchain. Soft- ware: Practice and Experience (2019)

2019
[12]

In: ACM CCS

Luu, L., Chu, D.H., Olickel, H., Saxena, P., Hobor, A.: Ma king smart contracts smarter. In: ACM CCS. pp. 254–269 (2016)

2016
[13]

In: Financial Cryptography a nd Data Security (2019)

Mavridou, A., Laszka, A., Stachtiari, E., Dubey, A.: Ver iSolid: Correct-by-design smart contracts for Ethereum. In: Financial Cryptography a nd Data Security (2019)

2019
[14]

Journal of Logic and Algebraic Programming 79(6), 397–434 (2010)

Ro¸ su, G., S ¸erb˘ anut ¸˘ a, T.F.: An overview of the K semantic framework. Journal of Logic and Algebraic Programming 79(6), 397–434 (2010)

2010
[15]

In: Financial Cryptography Workshops

Sergey, I., Hobor, A.: A concurrent perspective on smart contracts. In: Financial Cryptography Workshops. pp. 478–493 (2017)

2017
[16]

CoRR abs/1801.00687 (2018)

Sergey, I., Kumar, A., Hobor, A.: Scilla: a smart contrac t intermediate-level lan- guage. CoRR abs/1801.00687 (2018)

2018 arXiv
[17]

Tran, A.B., Lu, Q., Weber, I.: Lorikeet: A model-driven e ngineering tool for blockchain-based business process execution and asset man agement. In: BPM. pp. 56–60 (2018)

2018
[18]

CoRR abs/1803.09885 (2018)

Yang, Z., Lei, H.: Lolisa: Formal syntax and semantics fo r a subset of the Solidity programming language. CoRR abs/1803.09885 (2018)

2018 arXiv
[19]

In: VSTTE

Zakrzewski, J.: Towards veriﬁcation of Ethereum smart c ontracts: A formalization of core of Solidity. In: VSTTE. LNCS, vol. 11294, pp. 229–247 . Springer (2018)

2018

Pith tools

Reviewed August 14, 2026 · model on record in the stance chip above.

[1] [1]

https://solidity.readthedocs.io/en/v0.5.4/ (2019)

Solidity documentation. https://solidity.readthedocs.io/en/v0.5.4/ (2019)

work page 2019

[2] [2]

Andrychowicz, M., Dziembowski, S., Malinowski, D., Mazu rek, L.: Secure multi- party computations on Bitcoin. Commun. ACM 59(4), 76–84 (20 16)

work page

[3] [3]

In: POST

Atzei, N., Bartoletti, M., Cimoli, T.: A survey of attacks on Ethereum smart con- tracts (SoK). In: POST. LNCS, vol. 10204, pp. 164–186. Sprin ger (2017)

work page 2017

[4] [4]

In: Financial Cryptography Workshops

Biryukov, A., Khovratovich, D., Tikhomirov, S.: Findel: Secure derivative contracts for Ethereum. In: Financial Cryptography Workshops. LNCS, vol. 10323, pp. 453–

work page

[5] [5]

https://github.com/ethereum/wiki/wiki/White-Paper (2013)

Buterin, V.: Ethereum: a next generation smart contract a nd decentralized applica- tion platform. https://github.com/ethereum/wiki/wiki/White-Paper (2013)

work page 2013

[6] [6]

Crafa, S., Pirro, M.D., Zucca, E.: Is Solidity solid enoug h? In: Financial Cryptog- raphy Workshops (2019)

work page 2019

[7] [7]

Business & Information Systems Engineering 59(6), 457–467 (2017)

Egelund-M¨ uller, B., Elsman, M., Henglein, F., Ross, O.: Automated execution of ﬁnancial contracts on blockchains. Business & Information Systems Engineering 59(6), 457–467 (2017)

work page 2017

[8] [8]

In: IEEE Compute r Security Foun- dations Symposium (CSF)

Hildenbrandt, E., Saxena, M., Rodrigues, N., Zhu, X., Dai an, P., Guth, D., Moore, B.M., Park, D., Zhang, Y., Stefanescu, A., Rosu, G.: KEVM: A c omplete formal semantics of the Ethereum Virtual Machine. In: IEEE Compute r Security Foun- dations Symposium (CSF). pp. 204–217. IEEE Computer Societ y (2018)

work page 2018