Nola: Later-Free Ghost State for Verifying Termination in Iris
summary
Nola presents a concrete method to remove Iris’s obstructive later modality by encoding shared state as syntactic SL formulas and giving them a separate semantics, enabling later-free higher-order ghost state that supports invariants and Rust-style borrows. Mechanized as an Iris library in Rocq, it allows ordinary induction in the meta-logic to prove termination and liveness properties and subsumes the existing later-weakened approach via stratification and parameterization. A working artifact is the RustHalt prototype for total correctness of Rust programs; artifacts and paper DOI are available.
AI-written summary · about
chapters (17)
- 0:00Introduction
- 0:22Termination challenges
- 1:27Name origin and overview
- 2:50Later modality in Iris
- 4:15Separation logic limits
- 5:41Removing later modality
- 7:28Syntactic separation logic
- 8:32Nola’s logic syntax
- 9:13Mutable references in Nola
- 9:54Infinite list verification
- 10:37Soundness and paradoxes
- 11:18Expressivity and extensibility
- 12:02Rust borrows in Nola
- 12:46RustBelt case study
- 13:48Leelo and fair scheduling
- 14:10Magic derivability
- 14:59Q&A
related talks
22mThe Nextgen Modality: A Modality for Non-Frame-Preserving Updates in Separation Logic
19mProof Automation for Linearizability in Separation Logic
15mModular Reasoning about Global Variables and Their Initialization
19mA Proof Recipe for Linearizability in Relaxed Memory Separation Logic
24mProving False in Object Oriented Verification Programs by Exploiting Non-Termination
11mMorello Cerise: proving secure encapsulation (work in progress)
17mModular Verification of Safe Memory Reclamation in Concurrent Separation Logic
24mTaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Pr