Smart contract interactions in coq

Publikation: Bidrag til bog/antologi/rapport/proceedingKonferencebidrag i proceedingsForskningpeer review

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.

TitelFormal Methods- FM 2019 International Workshops - Revised Selected Papers
RedaktørerEmil Sekerinski, Nelma Moreira, José N. Oliveira, Daniel Ratiu, Riccardo Guidotti, Marie Farrell, Matt Luckcuck, Diego Marmsoler, José Campos, Troy Astarte, Laure Gonnord, Antonio Cerone, Luis Couto, Brijesh Dongol, Martin Kutrib, Pedro Monteiro, David Delmas
Antal sider12
Udgivelsesårjan. 2020
ISBN (trykt)9783030549930
ISBN (Elektronisk)978-3-030-54994-7
StatusUdgivet - jan. 2020
Begivenhed3rd World Congress on Formal Methods, FM 2019 - Porto, Portugal
Varighed: 7 okt. 201911 okt. 2019


Konference3rd World Congress on Formal Methods, FM 2019
SerietitelLecture Notes in Computer Science

Se relationer på Aarhus Universitet Citationsformater

ID: 195652827