Specifications for modular program verifiers are expressed as constraints on program states (e.g. preconditions) and relations on program states (e.g. postconditions). For programs whose domain is managing resources of any kind (e.g. cryptocurrencies), such state-based specifications must make explicit properties that a human would implicitly understand for free. For example, it's clear that depositing into your bank account will not change other balances, but classically this must be stated as a frame condition. As a result, classical specifications for resource-manipulating programs quickly become verbose and difficult to interpret, write and debug. In this paper, we present a novel methodology that extends a modular program verifier to support user-defined first-class resources, allowing resource-related operations and properties to be expressed directly and eliminating the need to reify implicit knowledge in the specifications. We implement our methodology as an extension of the program verifier Prusti, and use it to verify real-world smart contracts and a key part of a blockchain application. Our evaluation demonstrates that specifications written with our methodology are more concise and substantially simpler than specifications written purely in terms of program states.

翻译：模块化程序验证器的规格说明通常表示为对程序状态的约束（如前置条件）以及程序状态之间的关系（如后置条件）。对于以管理各类资源（例如加密货币）为领域的程序，这类基于状态的形式化规格必须明确表达人类本可直觉理解的隐含属性。例如，向银行账户存款显然不会改变其他账户余额，但在经典验证框架中，这种性质必须通过框架条件显式声明。因此，资源操作程序的经典规格说明往往变得冗长且难以理解、编写和调试。本文提出一种新颖的方法论，将模块化程序验证器扩展为支持用户定义的一等公民资源，使得资源相关操作和属性能够被直接表达，从而消除在规格说明中显式物化隐含知识的需求。我们以程序验证器Prusti的扩展形式实现该方法，并将其用于验证真实世界的智能合约及区块链应用的核心组件。实验评估表明，采用本方法编写的规格说明相较于纯程序状态描述的规格说明，在简洁性与易用性方面具有显著优势。