用于表达性精化类型的基础约束求解
Foundational Constraint Solving for Expressive Refinement Typing
浏览论文内容
中文总结 AI 辅助
研究基于SMT的程序验证器的问题，提出在LEAN中实现的基础约束Horn子句求解器FLEX。通过编码CHC为LEAN命题、实现验证CHC生成器及利用LEAN证明机制超越SMT限制，自动消除95.7%的CHC，证明其作为可信CHC后端的可行性。
中文摘要 AI 辅助
基于SMT的程序验证器存在两个问题：表达性方面，可预测验证限于SMT可判定性边界；信任方面，求解器是未经验证的大型工件，其健全性错误可能影响基于它构建的每个工具。我们提出了FLEX，这是一个在LEAN中实现的基础约束 Horn 子句（CHC）求解器。它将可信基础仅减少到内核，并允许通过三个贡献使用LEAN的整个证明生态系统来验证低级系统代码。首先，FLEX将CHC编码为普通的LEAN命题，其中Horn变量是存在量词约束的谓词，并展示如何将CHC求解器实现为计算CHC命题的内核可检查证明的策略（元程序）。其次，展示了如何在LEAN中实现两个经过验证的CHC生成器：一个用于命令式语言的Floyd-Hoare风格生成器和一个用于函数演算的基于精化类型的生成器，它们可以与求解策略组合以产生第一个基于CHC的端到端基础验证器。最后，通过使用FLUX精化类型检查器释放LEAN的整个证明机制生态系统来证明各种低级Rust库的任意功能正确性属性，展示了FLEX如何超越SMT的表达性限制，并通过显示它自动消除了FLUX基准套件中95.7%的CHC，证明了FLEX作为可信CHC后端的可行性。
英文摘要
SMT-based program verifiers are hamstrung by two problems: expressiveness, because predictable verification restricts to the boundaries of SMT decidability, and trust, because the solver is a large, unverified artifact whose soundness bugs may quietly compromise every tool built on it. We present FLEX, a foundational Constrained Horn Clause (CHC) solver implemented in LEAN, that reduces the trusted base to the kernel alone, and allows using LEAN's entire proof ecosystem to verify low-level systems code, via three contributions. First, FLEX encodes CHCs as plain LEAN propositions where the Horn variables are existentially bound predicates, and shows how to implement CHC solvers as tactics (meta-programs) that compute kernel checkable proofs of the CHC propositions. Second, we show how to implement two verified CHC generators in LEAN: a Floyd-Hoare style generator for an imperative language, and a refinement-type-based generator for a functional calculus, which can be composed with the solving tactics to yield the first end-to-end foundational CHC-based verifiers. Finally, we show how FLEX allows us to leapfrog the expressiveness limitations of SMT by unleashing LEAN's entire ecosystem of proof machinery to prove arbitrary functional correctness properties of various low-level Rust libraries using the FLUX refinement type checker, and demonstrate the viability of FLEX as a trustworthy CHC backend, by showing it automatically discharges 95.7% of the CHCs from FLUX's benchmark suite.
