Using Ghost Ownership to Verify Union-Find and Persistent Arrays in Rust
summary
Creusot gains support for linear ghost resources and implements a ptr_own with permission map that lets mutable borrows be expressed and borrow‑checked in ghost code. The implementation provides allocate/read/write primitives (allocate returns a permission, as_ref/as_mut consume it), enforces ghost‑block entry/exit rules, and reuses Iris‑style resource algebras. The team verifies a pointer‑based union‑find and persistent arrays, proves correctness with no runtime overhead (ghost types compile to unit), and implements functions Verus cannot.
AI-written summary · about
chapters (6)
- 0:00Ghost ownership intro
- 3:57Pointer aliasing issues
- 7:25Ghost pointers with ownership
- 10:23Union-Find with ghost state
- 14:19Persistent array proofs
- 15:05Q&A on Rust
related talks
18mVerus: Verifying Rust Programs using Linear Ghost Types
23mA Verified Thread-Safe Array in Rust
28mYou Don't Own Me
50mRust's Borrow Checker Proven Correct!
45mRust: safe and concurrent. But how does it do it?
15mNon-binary Rust: Between Safe and Unsafe
54mMemory Safety with Rust
28mDetecting Borrow and Provenance Bugs Across Unsafe Rust [...]