  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.
