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}
}