一句话：在 Iris 中验证局部通用求解器的部分正确性，证明其虽用可变状态记忆与窥探，外部行为仍纯且计算最优最小不动点。
本文关注局部通用求解器（local generic solver）的部分正确性验证。该求解器按需求值、增量计算并记忆化最小不动点，用于求解单调方程组；其内部依赖可变状态做 memoization 和 spying（动态依赖发现），但对外表现为纯函数。作者在 Iris 并发分离逻辑中给出规格与证明：求解器计算最优最小不动点。辅助地，论文展示了 Iris 预言变量（prophecy variables）的使用，建立受限的无穷合取规则，并给出 Longley 模函数这一 spying 典型案例的规格与证明。
We verify the partial correctness of a "local generic solver", that is, an on-demand, incremental, memoizing least fixed point computation algorithm. The verification is carried out in Iris, a modern breed of concurrent separation logic. The specification is simple: the solver computes the optimal least fixed point of a system of monotone equations. Although the solver relies on mutable internal state for memoization and for "spying", a form of dynamic dependency discovery, it is apparently pure: no side effects are mentioned in its specification. As auxiliary contributions, we provide several illustrations of the use of prophecy variables, a novel feature of Iris; we establish a restricted form of the infinitary conjunction rule; and we provide a specification and proof of Longley's modulus function, an archetypical example of spying.
@article{paperbot570,
title = {Spy game: verifying a local generic solver in Iris},
author = {Paulo Emílio de Vilhena and François Pottier and Jacques-Henri Jourdan},
journal = {Proceedings of the ACM on Programming Languages},
volume = {4},
number = {POPL},
year = {2019},
doi = {10.1145/3371101}
}