Rich Specifications for Ethereum Smart Contract Verification[J] PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL 2021(5) Braem, Christian Eilers, Marco Mueller, Peter Sierra, Robin Summers, Alexander J.