Resource Specifications for Resource-Manipulating Programs

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.