  Solidity smart contracts are programs that manage up to 2^160 users on a
blockchain. Verifying a smart contract relative to all users is intractable due
to state explosion. Existing solutions either restrict the number of users to
under-approximate behaviour, or rely on manual proofs. In this paper, we
present local bundles that reduce contracts with arbitrarily many users to
sequential programs with a few representative users. Each representative user
abstracts concrete users that are locally symmetric to each other relative to
the contract and the property. Our abstraction is semi-automated. The
representatives depend on communication patterns, and are computed via static
analysis. A summary for the behaviour of each representative is provided
manually, but a default summary is often sufficient. Once obtained, a local
bundle is amenable to sequential static analysis. We show that local bundles
are relatively complete for parameterized safety verification, under moderate
assumptions. We implement local bundle abstraction in SmartACE, and show
order-of-magnitude speedups compared to a state-of-the-art verifier.
