  Some of the most significant high-level properties of currencies are the sums
of certain account balances. Properties of such sums can ensure the integrity
of currencies and transactions. For example, the sum of balances should not be
changed by a transfer operation. Currencies manipulated by code present a
verification challenge to mathematically prove their integrity by reasoning
about computer programs that operate over them, e.g., in Solidity. The ability
to reason about sums is essential: even the simplest ERC-20 token standard of
the Ethereum community provides a way to access the total supply of balances.
  Unfortunately, reasoning about code written against this interface is
non-trivial: the number of addresses is unbounded, and establishing global
invariants like the preservation of the sum of the balances by operations like
transfer requires higher-order reasoning. In particular, automated reasoners do
not provide ways to specify summations of arbitrary length.
  In this paper, we present a generalization of first-order logic which can
express the unbounded sum of balances. We prove the decidablity of one of our
extensions and the undecidability of a slightly richer one. We introduce
first-order encodings to automate reasoning over software transitions with
summations. We demonstrate the applicability of our results by using SMT
solvers and first-order provers for validating the correctness of common
transitions in smart contracts.
