We present a unification of refinement and Hoare-style reasoning in a foundational mechanized higher-order distributed separation logic. This unification enables us to prove formally in the Coq proof assistant that concrete implementations of challenging distributed systems refine more abstract models and to combine refinement-style reasoning with Hoare-style program verification. We use our logic to prove correctness of concrete implementations of two-phase commit and single-decree Paxos by showing that they refine their abstract TLA+ specifications. We further use our notion of refinement to transfer fairness assumptions on program executions to model traces and then transfer liveness properties of fair model traces back to program executions, which enables us to prove liveness properties such as strong eventual consistency of a concrete implementation of a Conflict-Free Replicated Data Type and fair termination of a concurrent program.

翻译：我们在一个基础性机械化的更高秩序的分布式分离逻辑中统一了完善和Hoare式推理。这种统一使我们能够在Coq验证助理中正式证明,具有挑战性的分布式系统的具体实施将改进更抽象的模式,并将完善式推理与Hoare式程序核查相结合。我们用我们的逻辑来证明两阶段承诺和单层和平的具体实施是正确的,表明它们完善了抽象的TLA+规格。我们进一步利用我们的推理概念,将关于方案执行的公平假设转换为模拟痕迹,然后将公平模型的活性特性追溯到方案执行,从而使我们能够证明具体实施一个冲突重复的数据类型和公平终止一个同时的方案最终具有很强的一致性。