一句话：提出 μdiv-模拟关系，统一强、弱、发散敏感等 12 种模拟，并在 Rocq 中形式化验证。
模拟是程序精化的常用概念。既有弱模拟需对发散敏感，而证明助手（如验证编译）中常用的 normed simulation 相对发散敏感弱模拟不完备。本文提出 μdiv-simulation，它与经典发散敏感弱模拟等价，又像 normed simulation 的现代刻画一样易用。进一步定义参数化模拟，覆盖强模拟、弱模拟、μdiv-模拟等 12 种模拟，并统一建立多种 “up-to” 推理技术。结果在 Rocq 中形式化，并在 Choice Trees 与 CompCert 编译 pass 两个案例上实例化。虽以验证编译为动机，但抽象 LTS 设定也适用于模型检测等领域。
Simulations are widely-used notions of program refinement. This paper discusses and compares several of them, in particular notions of simulation that are both weak and sensitive to divergence. Complex simulation proofs performed in proof assistants, for instance in a verified compilation setting, often rely on variants of normed simulation, which is not complete with respect to divergence-sensitive weak simulation. We propose to bridge this gap with μdiv-simulation, a novel notion of simulation that is equivalent to classical divergence-sensitive weak simulation, and designed to be as comfortable to use as modern characterizations of normed simulation. We then define a parameterized notion of simulation that covers strong simulation, weak simulation, μdiv-simulation, and 9 more notions of simulation, and jointly establish various “up-to” reasoning techniques for these 12 notions. Our results are formalized in Rocq and instantiated on two case studies: Choice Trees and a CompCert pass. Verified compilation is a major motivation for our study, but because we work with an abstract LTS setting, our results are also relevant to other fields that make use of divergence-sensitive weak simulation, such as model checking.