用验证证明生成优化代码，自动实现跨语言高效编译。
Compiling by Proving: Language-Agnostic Automatic Optimization from Formal Semantics
- 用符号执行构建完整路径可达性证明，转化为优化规则
- 指令级优化提升速度，全程序编译性能提升数个数量级
- 不依赖特定语言，可扩展至多种编程语言
验证证明完整记录了程序行为，但验证后通常被丢弃。本文提出「编译即证明」新范式，将证明转换为优化执行规则。通过符号执行构建全路径可达性证明，并将其图结构编译为单一优化规则，在保持正确性的同时合并大量语义重写。该方法作为K框架的语言无关扩展实现。评估表明：在不同编译粒度下均表现优异——指令级优化持续提速，全程序编译实现数量级性能提升。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。