We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.LO

Change to browse by:

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Logic in Computer Science

Title: Smart Contract Interactions in Coq

Abstract: We present a model/executable specification of smart contract execution in Coq. Our formalization allows for inter-contract communication and generalizes existing work by allowing modelling of both depth-first execution blockchains (like Ethereum) and breadth-first execution blockchains (like Tezos). We represent smart contracts programs in Coq's functional language Gallina, enabling easier reasoning about functional correctness of concrete contracts than other approaches. In particular we develop a Congress contract in this style. This contract -- a simplified version of the infamous DAO -- is interesting because of its very dynamic communication pattern with other contracts. We give a high-level partial specification of the Congress's behavior, related to reentrancy, and prove that the Congress satisfies it for all possible smart contract execution orders.
Subjects: Logic in Computer Science (cs.LO); Programming Languages (cs.PL)
Cite as: arXiv:1911.04732 [cs.LO]
  (or arXiv:1911.04732v1 [cs.LO] for this version)

Submission history

From: Bas Spitters [view email]
[v1] Tue, 12 Nov 2019 08:23:19 GMT (33kb)

Link back to: arXiv, form interface, contact.