回忆证人：单调状态的基础和应用
Recalling a Witness: Foundations and Applications of Monotonic State
摘要：
我们提供了一种方法来缓解其状态单调演变的程序的验证。其主要思想是，在先前状态中被证明的属性可以在当前状态中被正确地回忆，前提是（1）状态根据给定的前序演化，并且（2）该属性被该前序保存。在许多情况下，这种单调推理产生简洁的模块化证明，节省了显式程序不变式的需要。我们提炼我们的方法到单调状态单子，一个通用的，但紧凑的界面霍尔式的单调状态的推理依赖类型的语言。我们证明了单调状态单子的可靠性，并将其作为F* 验证系统中单调状态推理的统一基础。在此基础上，我们建立了各种可变的数据结构，如单调引用库，并将这些库的规模验证几个分布式应用程序。
英文摘要：
We provide a way to ease the verification of programs whose state evolves monotonically. The main idea is that a property witnessed in a prior state can be soundly recalled in the current state, provided (1) state evolves according to a given preorder, and (2) the property is preserved by this preorder. In many scenarios, such monotonic reasoning yields concise modular proofs, saving the need for explicit program invariants. We distill our approach into the monotonic-state monad, a general yet compact interface for Hoare-style reasoning about monotonic state in a dependently typed language. We prove the soundness of the monotonic-state monad and use it as a unified foundation for reasoning about monotonic state in the F* verification system. Based on this foundation, we build libraries for various mutable data structures like monotonic references and apply these libraries at scale to the verification of several distributed applications.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
