Thrust: A Prophecy-Based Refinement Type System for Rust
summary
A new Rust verifier called Thrust implements a dependent refinement type system plus an inference pipeline that emits Constrained Horn Clauses to a CHC solver, synthesizes inductive invariants for loops and recursion, and uses prophecy variable annotations to propagate mutable-borrow updates back to owners and enable sound strong updates. It ships as a Rustc plugin, runs fully automated or semi-automated with per-function annotations, verifies RustHorn benchmarks plus 32 additional cases, and matches RustHorn’s runtime on most examples.
AI-written summary · about
chapters (15)
- 0:00Thrust introduction and goals
- 1:07Single mutability rule in Rust
- 2:53Comparison with verification tools
- 3:37Thrust design goals
- 4:18Dependent types in Thrust
- 6:04Mutation with refinement types
- 7:28Challenge of strong updates
- 8:10Two typing contexts in Thrust
- 9:36Mutable references challenges
- 11:01Introducing prophecies
- 12:25How prophecies work
- 13:47Soundness proof and well-boundedness
- 14:30Automation with inference
- 15:13Evaluation on benchmarks
- 16:40Q&A
related talks
10mAutomatically Enforcing Rust Trait Properties
13mA Type System for Extracting Functional Specifications from Memory-Safe Imperative Programs
15mTowards Verifying Crash Consistency
28mGradual Verification: Assuring Software Incrementally
19mPredictable Verification using Intrinsic Definitions
06mLayered Configuration and Safe Hot Reload in Rust
15mIncremental Certified Programming
17mA HAT Trick: Automatically Verifying Representation Invariants using Symbolic Finite(…)