Automatic Linear Resource Bound Analysis for Rust via Prophecy Potentials
summary
Claims an automatic, type-based AARA for Rust that infers symbolic linear cost bounds and proves soundness via a new Resource-Aware Borrow Calculus (RABC). Implements RaRust prototype as a front end to the Rust compiler and encodes prophecy potentials to transfer and reclaim potential across mutable borrows compositionally. Evaluated on examples with shared and mutable borrows, reborrows, heap data, loops and recursion; infers linear bounds automatically and ships reproducible artifacts and benchmarks.
AI-written summary · about
chapters (7)
- 0:00Resource bounds in Rust
- 1:46Prior work on resource analysis
- 4:37Mutable references challenge
- 7:30Prophecy potentials for references
- 8:57Evaluation and supported features
- 10:24Summary and limitations
- 11:06Q&A
related talks
31mTowards a linear functional translation for borrowing
19mPure Borrow: Linear Haskell Meets Rust-Style Borrowing
19mRavencheck: Effectively-Propositional Reasoning for Rust
15mAeneas: Rust Verification by Functional Translation
35mFunctional Reactive Rust
50mRust's Borrow Checker Proven Correct!
35mBuilding Actor Systems in Rust
21mExtending the horizons of R with Rust