Recalling a Witness: Foundations and Applications of Monotonic State

International audienceWe provide a way to ease the verification of programs whose stateevolves monotonically. The main idea is that a property witnessed ina prior state can be soundly recalled in the current state, provided(1) state evolves according to a given preorder, and (2) the propertyis preserved by this preorder. In many scenarios, such monotonicreasoning yields concise modular proofs, saving the need for explicitprogram invariants. We distill our approach into the monotonic-statemonad, a general yet compact interface for Hoare-style reasoning aboutmonotonic state in a dependently typed language. We prove thesoundness of the monotonic-state monad and use it as a unifiedfoundation for reasoning about monotonic state in the F* verificationsystem. Based on this foundation, we build libraries for variousmutable data structures like monotonic references and apply theselibraries at scale to the verification of several distributed applications