论文标题
通过经过验证的重写引擎加速验证的兼职器开发
Accelerating Verified-Compiler Development with a Verified Rewriting Engine
论文作者
论文摘要
编译器是正式验证的主要目标，因为编译器错误无效更高级别的正确性保证，但是如果必须使用证明补丁，则编译器的更改可能会变得更加劳动力实施。一种吸引人的方法是将编译器作为代数改写规则集，通用引擎可以有效地应用。现在，每个重写规则都可以单独证明，而无需重新审视编译器其他部分的过去证明。我们以COQ证明助手的框架的形式提出了这个想法的第一个实现。我们的新COQ命令采用正常的证明定理，并将它们自动结合到具有证据的快速编译器中。我们应用了框架来改进菲亚特加密工具链来生成加密算术，生成了提取的命令行编译器，该编译器的速度约为1000 $ \ times $，而实际上具有更简单的编译器特定于特定的证明。
Compilers are a prime target for formal verification, since compiler bugs invalidate higher-level correctness guarantees, but compiler changes may become more labor-intensive to implement, if they must come with proof patches. One appealing approach is to present compilers as sets of algebraic rewrite rules, which a generic engine can apply efficiently. Now each rewrite rule can be proved separately, with no need to revisit past proofs for other parts of the compiler. We present the first realization of this idea, in the form of a framework for the Coq proof assistant. Our new Coq command takes normal proved theorems and combines them automatically into fast compilers with proofs. We applied our framework to improve the Fiat Cryptography toolchain for generating cryptographic arithmetic, producing an extracted command-line compiler that is about 1000$\times$ faster while actually featuring simpler compiler-specific proofs.
