智能合约转账中的余额求和推理

货币的一些最重要高层属性是某些账户余额之和。此类和的性质可确保货币与交易的完整性。例如，转账操作不应改变余额之和。由代码操纵的货币带来了一个验证挑战，即需要通过推理操作它们的计算机程序（如Solidity中）来数学证明它们的完整性。对和进行推理至关重要：即便是以太坊社区最简单的ERC-20代币标准也提供了访问余额总供给的方式。遗憾的是，对针对此接口编写的代码进行推理并非易事：地址数量无界，而建立如转账等操作保持余额之和这样的全局不变量需要高阶推理。特别地，自动化推理器未提供指定任意长度求和的方法。本文提出了一阶逻辑的一种推广，可表达无界的余额求和。我们证明了其中一个扩展的可判定性，以及稍丰富一点的扩展的不可判定性。我们引入一阶编码以自动化对带求和的软件状态转移的推理。我们通过使用SMT求解器和一阶证明器来验证智能合约中常见转账的正确性，展示了我们结果的适用性。