Resource Specifications for Resource-Manipulating Programs

TL;DR

The paper addresses the semantic gap in specifying resource-manipulating programs by showing that state-based specifications requiring explicit frame conditions are verbose and brittle. It proposes first-class resources, ghost resource state, resource operations, and coupling invariants to express resource changes directly, implemented as an extension to the Prusti verifier via Viper. A Fungible Token Transfer case study on cross-chain IBC demonstrates that resource-based specifications enable concise, structurally simpler proofs while preserving key properties like a Two-Way Peg and Preservation of Supply. The evaluation across multiple applications indicates substantial reductions in specification size and syntactic complexity, with a modest verification-time overhead, underscoring the practical impact for verifying resource-based systems such as smart contracts and blockchain protocols.

Abstract

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.

Figures (23)

• Figure 1: Rust code defining a Bank interface. Monetary values are represented as unsigned 128-bit integers, account identifiers are represented by values of type AcctId (u32).
• Figure 2: Specifications for the deposit and withdraw functions. Each includes an explicit frame condition; specification lines used to encode the frame condition are highlighted in red.
• Figure 3: A specification for the transfer function, which makes calls to withdraw and then deposit
• Figure 4: A function that performs two withdrawals in sequence. When acct_id1 and acct_id2 are the same, this function performs two operations on the same account.
• Figure 5: The specifications for the withdraw2 function in Fig. \ref{['fig:motivation:withdraw2']}. The conditional in the precondition is necessary to handle the possible aliasing between acct_id1 and acct_id2. The postcondition includes an analogous conditional, as well as a frame condition stating that other account balances remain unchanged.