论文标题
具有谓词变压器语义的证明工程
Proof Engineering with Predicate Transformer Semantics
论文作者
论文摘要
我们提出了一个轻巧的开源AGDA框架，用于使用谓词变压器语义来手动验证有效程序。我们代表具有广义代数数据类型（GADT）AST的有效程序的抽象语法树（AST），其通用性甚至可以使复杂的操作成为原始的AST节点。然后，用户可以将定制的谓词变形金刚分配给此类操作，以帮助证明工作，例如，通过自动分解分支代码的证明义务。我们的框架编码并概括了作者使用的证明工程方法，以推理librabft的原型实现，这是一种拜占庭错误的耐受共识协议，其中参与者执行的代码可能具有更新状态和发送消息等效果。在这种情况下，成功使用我们的框架证明了其实际适用性。
We present a lightweight, open source Agda framework for manually verifying effectful programs using predicate transformer semantics. We represent the abstract syntax trees (AST) of effectful programs with a generalized algebraic datatype (GADT) AST, whose generality enables even complex operations to be primitive AST nodes. Users can then assign bespoke predicate transformers to such operations to aid the proof effort, for example by automatically decomposing proof obligations for branching code. Our framework codifies and generalizes a proof engineering methodology used by the authors to reason about a prototype implementation of LibraBFT, a Byzantine fault tolerant consensus protocol in which code executed by participants may have effects such as updating state and sending messages. Successful use of our framework in this context demonstrates its practical applicability.
