Refinement Proofs in Rust Using Ghost Locks

TL;DR

This paper introduces a new refinement technique for Rust programs that overcomes previous limitations, supporting diverse structures and properties, and demonstrates its practicality through substantial case studies.

Contribution

It presents a novel refinement method for Rust that handles various program and proof structures, enabling reasoning about safety and liveness properties.

Findings

Supports a wide range of program structures and data representations

Enables reasoning about both safety and liveness properties

Demonstrates practicality on substantial case studies

Abstract

Refinement transforms an abstract system model into a concrete, executable program, such that properties established for the abstract model carry over to the concrete implementation. Refinement has been used successfully in the development of substantial verified systems. Nevertheless, existing refinement techniques have limitations that impede their practical usefulness. Some techniques generate executable code automatically, which generally leads to implementations with sub-optimal performance. Others employ bottom-up program verification to reason about efficient implementations, but impose strict requirements on the structure of the code, the structure of the refinement proofs, as well as the employed verification logic and tools. In this paper, we present a novel refinement technique that removes these limitations. It supports a wide range of program structures, data representations, and proof structures. Our approach supports reasoning about both safety and liveness properties. We implement our approach in a state-of-the-art verifier for the Rust language, which itself offers a strong foundation for memory safety. We demonstrate the practicality of our approach on a number of substantial case studies.