Thrust: A Prophecy-Based Refinement Type System for Rust
This program is tentative and subject to change.
We introduce \textsc{Thrust}, a new verification tool for ensuring functional correctness in \textsc{Rust}, distinguished by its strengths in \emph{automated} verification, including the synthesis of inductive invariants for loops and recursive functions. \textsc{Thrust} is built on a novel dependent refinement type system for \textsc{Rust} and refinement type inference techniques based on Constrained Horn Clause (CHC) solvers. Leveraging advantages of the type system, \textsc{Thrust} also supports semi-automated verification utilizing user type annotations to complement CHC solvers in cases where automatic constraint solving is unsuccessful, as well as \emph{modular} verification at the function and subexpression levels.
\textsc{Thrust} also achieves \emph{precise} verification, especially for programs involving pointer aliasing and borrowing, without sacrificing the benefits of automated verification, by incorporating the notion of \emph{prophecy} into the refinement type system: it not only enables strong updates by leveraging the aliasing XOR mutability'' guarantee provided by \textsc{Rust}'s type system, but also achieves propagation of update information to the original owner upon mutable borrow release through the use of a prophecy variable. Incorporating prophecy into a refinement type system is itself challenging and requires certain tricks, as discussed in this paper, making a theoretical contribution and paving the way for further research into prophecy-based refinement type systems. While our type system addresses the challenge, we keep it simple for extensibility, specifically by delegating the guarantee of
aliasing XOR mutability,'' and, more technically, the ``well-borrowedness'' of the program in the sense of the \emph{stacked borrows} aliasing model, to \textsc{Rust}'s type system, allowing us to focus on reasoning about functional correctness and propagating update information through prophecy variables. Compared to \textsc{RustHorn}, another automated verification tool based on prophecy, our approach leverages the strengths of refinement types to support modular verification, higher-order functions, and refinement of data stored in algebraic data structures.
We implemented \textsc{Thrust}, a refinement type inference tool as a plugin for the \textsc{Rust} compiler, and evaluated it using \textsc{RustHorn} benchmarks, as well as additional new benchmarks, including those that are beyond the capabilities of \textsc{RustHorn} and other semi-automated verification tools, obtaining promising results.
This program is tentative and subject to change.
Fri 20 JunDisplayed time zone: Seoul change
10:30 - 11:50 | |||
10:30 20mTalk | Usability Barriers for Liquid Types PLDI Research Papers Catarina Gamboa Carnegie Mellon University and University of Lisbon, Abigail Elena Reese Carnegie Mellon University, Alcides Fonseca LASIGE; University of Lisbon, Jonathan Aldrich Carnegie Mellon University DOI Pre-print | ||
10:50 20mTalk | Dynamic Region Ownership for Concurrency Safety PLDI Research Papers Fridtjof Stoldt Uppsala University, Brandt Bucher Microsoft, Sylvan Clebsch Microsoft Azure Research, Matthew A. Johnson Microsoft Azure Research, Matthew J. Parkinson Microsoft Azure Research, Guido van Rossum Microsoft, Eric Snow Microsoft, Tobias Wrigstad Uppsala University DOI | ||
11:10 20mTalk | Practical Type Inference with Levels PLDI Research Papers DOI | ||
11:30 20mTalk | Thrust: A Prophecy-Based Refinement Type System for Rust PLDI Research Papers Hiromi Ogawa University of Tsukuba, Taro Sekiyama National Institute of Informatics, Hiroshi Unno Tohoku University DOI |