Compiling by Proving: Language-Agnostic Automatic Optimization from Formal Semantics
This addresses the inefficiency of discarding verification proofs in program optimization, offering a language-agnostic method for automatic optimization from formal semantics, though it appears incremental in building on existing verification frameworks.
The paper tackled the problem of discarding verification proofs after checking correctness by introducing compiling by proving, a paradigm that transforms these proofs into optimized execution rules, resulting in performance improvements including consistent speedups at opcode-level and orders of magnitude gains in whole-program compilation.
Verification proofs encode complete program behavior, yet we discard them after checking correctness. We present compiling by proving, a paradigm that transforms these proofs into optimized execution rules. By constructing All-Path Reachability Proofs through symbolic execution and compiling their graph structure, we consolidate many semantic rewrites into single rules while preserving correctness by construction. We implement this as a language-agnostic extension to the K framework. Evaluation demonstrates performance improvements across different compilation scopes: opcode-level optimizations show consistent speedups, while whole-program compilation achieves orders of magnitude greater performance gains.