Interactive Bit Vector Reasoning using Verified Bitblasting
summary
A verified bit-blasting pipeline called bv_decide tactic compiles Lean bitvector goals to AIGs, converts to CNF, calls an external SAT solver that emits conflict proofs, and replay-checks unsatisfiability inside Lean. The implementation uses Lean’s FBIP arrays and hashmaps for fast AIG construction, supports SMT-LIB 2.7 operations, and verifies over 7000+ LLVM assertions and the full SMT-LIB suite, outperforming CoqQFBV by a few thousand problems while approaching Bitwuzla on many benchmarks as a verified bitblaster.
AI-written summary · about
chapters (12)
- 0:00Interactive bit vector reasoning
- 1:27Verified bit vector reasoning
- 2:11BBDIET tactic in Lean
- 3:33Bit vector standard library
- 4:58Efficient inverter graphs
- 6:42BBDIET performance evaluation
- 8:48Lean type system integration
- 10:14Summary and future directions
- 10:35Q&A: Variable length bit vectors
- 11:17Q&A: General purpose use
- 12:19Q&A: Proof certification
- 13:01Closing remarks
related talks
30mBit-Precise Reasoning via Int-Blasting
19mPanel: Compilation Frameworks
20mBit Blasting Probabilistic Programs
29mA Real-Blasting Extension of Cvc5 for Reasoning about Floating-Point Arithmetic
01h 01mMulti-Modal Verification of Distributed Systems in Lean
19mVelvet: A Multi-Modal Verifier for Effectful Programs
19mEnhanced Enumeration Techniques for Syntax-Guided Synthesis of Bit-Vector Manipu...
19mLean on Dafny: Exploring Interactive Verification of Dafny Programs in Lean