AI 中文总结
该研究针对编译器启发式算法的性能与编译时间缺陷，提出在Rocq中验证编译器 passes 的性能与编译时间属性，通过内联展开的概念验证实现语义保留及相关界的验证，为编译器优化的形式化保证提供方案。
AI 中文摘要
现代优化编译器依赖启发式搜索算法求解NP难优化问题，这可能导致生成代码性能不佳，且编译时间过长或不可预测，用户将此类情况视为缺陷，但已验证的编译器很少超出语义保留范畴进行推理。我们提出对编译器 passes 的性能与编译时间属性进行验证，作为概念验证，我们使用估算指令缓存性能的代价模型来形式化内联展开，在 Rocq 中实现该过程，证明内联变换的语义保留性，并验证该算法的单调改进性、收敛时间界，以及中间和最终解的性能界。
英文摘要
Modern optimizing compilers rely on heuristic search algorithms for NP-hard optimization problems, which can result in poor generated-code performance and long or unpredictable compile times. These are considered bugs by users, but verified compilers rarely reason beyond semantic preservation. We propose verifying performance and compile time properties of compiler passes. As a proof-of-concept, we formulate inline expansion using a cost model estimating instruction-cache performance. We mechanize this in Rocq, prove semantic preservation of the inlining transformation, and verify the algorithm's monotone improvement, convergence-time bound, and performance bounds for intermediate and final solutions.
CommentsTo appear in Formal Methods in Computer-Aided Design 2026 (FMCAD '26) Student Forum. 3 pages
