一句话：提出 Nola 框架实现无 later 模态的高阶幽灵状态，支撑 Iris 中对 Rust 程序终止性等完全正确性的验证。
分离逻辑近年发展迅速，已被用于证明 Rust 所有权类型系统的可靠性并对 Rust 程序做函数式验证。然而，在具有不变式、借用等高级特性（尤其是 Rust 所有权类型）的场景下验证终止性，无法通过简单套用仅处理安全性（safety）的已有工作实现。这些工作为高层推理 Rust 中共享可变状态而采用高阶幽灵状态（即依赖分离逻辑断言的高阶逻辑状态），但其方式依赖 later 模态，而 later 恰是验证终止性的根本障碍。为此，作者提出通用框架 Nola，实现无 later 的高阶幽灵状态：其核心思想是对高阶幽灵状态进行参数化，从而一般化并涵盖既有方法。即使在不变式与借用等高级特性存在下，Nola 也支持自然的终止性验证，并允许在元逻辑中使用任意归纳。Nola 已在 Rocq 中作为 Iris 的库完全机械化，作者还开发了 RustHalt 原型，作为首个用于 Rust 程序完全正确性验证的语义化、机械化基础。
Separation logic (SL) has recently evolved at an exciting pace, opening the way to more complex goals, notably soundness proof of Rust's ownership type system and functional verification of Rust programs. In this paper, we address verification of termination in the presence of advanced features, especially Rust's ownership types. Perhaps surprisingly, this goal cannot be achieved by a simple application of existing studies that dealt only with safety properties. For high-level reasoning about advanced shared mutable state as used in Rust, they used higher-order ghost state (i.e., logical state that depends on SL assertions), but in a way that depends on the later modality, a fundamental obstacle to verifying termination. To solve this situation, we propose a novel general framework, Nola, which achieves later-free higher-order ghost state. Even in the presence of advanced features such as invariants and borrows, Nola enables natural termination verification, allowing arbitrary induction in the meta-logic. Its key idea is to parameterize higher-order ghost state, generalizing and subsuming the existing approach. Nola is fully mechanized in Rocq as a library of Iris. Moreover, to demonstrate the power of Nola, we develop a prototype of RustHalt, the first semantic and mechanized foundation for total correctness verification of Rust programs.
@article{paperbot3079,
title = {Nola: Later-Free Ghost State for Verifying Termination in Iris},
author = {Yusuke Matsushita and Takeshi Tsukada},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {PLDI},
year = {2025},
doi = {10.1145/3729250}
}