Interactive Bitvector Reasoning using Verified Bit-Blasting

Henrik Böving

doi:10.1145/3763167

Interactive Bitvector Reasoning using Verified Bit-Blasting

2025-10-01

0

PRE

AI

DOI：10.1145/3763167

原文求助

摘要

En 中文

位 blasting SMT 解算器能够实现关于位向量的高效自动推理，这对于编译器后端、加密算法、硬件设计以及其他软硬件任务的验证至关重要。尽管对高效位向量推理基础设施有明确需求，且尖端位 blasting SMT 解算器（如 Bitwuzla）取得了显著进展，但在交互式定理证明器（ITPs）中进行有效的位向量推理仍是一项挑战，阻碍了其在机械化证明中的应用。不完整的位向量库、不可用或仅部分集成的决策过程、复杂且难以位 blasting 的操作，以及与宿主语言有限的集成，都限制了位向量推理在证明场景中的广泛应用。我们介绍了 bv_decide：首个针对依赖类型 ITP 中交互式位向量推理设计的端到端验证的位 blasting 解算器。我们的验证位 blasting 解算器具有可扩展性，包含完整的端到端证明（仅信任 Lean 编译器和内核），并可作为证明策略提供，允许直接在编程语言（本例中为 Lean）内部进行交互式推理。我们使用 Lean 的函数式但原地（FBIP）范式高效编码核心数据结构（如 AIGs），证明 SMT 解算器的快速执行无需以严格的正式化为代价。我们通过基于我们的位向量类型构建 Lean 的 C 风格标准数据类型 UInt/SInt，添加从枚举和结构体到位向量的降级以实现对复合类型的透明位 blasting 支持，并提供一个交互式策略（可解决目标或提供反例），从而实现对用户编写代码的可靠交互式验证。此外，我们介绍了 Lean 的标准位向量库的设计，该库支持 SMT-LIB 2.7 标准（包括溢出建模）的所有操作（附带推理原理），执行速度快，并提供全面的 API 和自动化，用于位宽无关推理。我们通过全面的基准测试集（包括完整的 SMT-LIB 数据集）全面评估了我们的位 blasting 解算器，其中 bv_decide 比当前验证位 blasting 领域的尖端工具 CoqQFBV 解决了更多定理。我们还验证了从 LLVM 中提取的 7000 多条 SMT 语句，据我们所知，这提供了迄今为止规模最大的 LLVM 重写机械化验证。通过将位 blasting 位向量推理打造成现代 ITPs 中一个精良、受良好支持且交互式的功能，我们实现了针对位向量级别验证的有效、可靠的“白盒”推理。

Keyword:

bitvector

decision procedure

bit-blasting

Lean

Interactive Bitvector Reasoning using Verified Bit-Blasting

摘要

期刊

机构

引用论文