{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:57:01Z","timestamp":1776333421174,"version":"3.51.2"},"reference-count":68,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","funder":[{"DOI":"10.13039\/100018693","name":"Horizon Europe","doi-asserted-by":"crossref","award":["101070375"],"award-info":[{"award-number":["101070375"]}],"id":[{"id":"10.13039\/100018693","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,10,9]]},"abstract":"<jats:p>\n            Bit-blasting SMT solvers enable efficient automatic reasoning about bitvectors, which are fundamental for the verification of compiler backends, cryptographic algorithms, hardware designs and other soft- or hardware tasks. Despite the clear demand for efficient bitvector reasoning infrastructure and the impressive advancements in state-of-the-art bit-blasting SMT solvers such as Bitwuzla, effective bitvector reasoning within interactive theorem provers (ITPs) remains a challenge, hindering their use for mechanized proofs. Incomplete bitvector libraries, unavailable or only partially integrated decision procedures, complex and hard-to-bitblast operations, and limited integration with the host language prevent the wide adoption of bitvector reasoning in proving contexts. We introduce bv_decide:\n            <jats:italic toggle=\"yes\">the first end-to-end verified bitblaster designed for interactive bitvector reasoning in a dependently-typed ITP<\/jats:italic>\n            . Our verified bitblaster is scalable, comes with a complete end-to-end proof (trusting only the Lean compiler and kernel), and is available as a proof tactic that allows interactive reasoning right from within a programming language, in our case Lean. We use Lean\u2019s Functional But In-Place (FBIP) paradigm to efficiently encode our core data structures (e.g., AIGs), demonstrating that fast execution of an SMT solver need not come at the expense of rigorous formalization. We enable dependable interactive verification of user-written-code by basing Lean\u2019s C-Style standard dataypes UInt\/SInt on our bitvector type, adding a lowering from enums and structs to bitvectors to enable transparent bit-blasting support for composed types, and by offering an interactive tactic that either solves a goal or provides a counter-example. Moreover, we present the design of Lean\u2019s canonical bitvector library, which supports all operations (with reasoning principles) for the SMT-LIB 2.7 standard (including overflow modeling), is fast-to-execute, and offers a comprehensive API and automation for bit-width-independent reasoning. We thoroughly evaluate our bit-blaster on a comprehensive set of benchmarks, including the full SMT-LIB dataset, where bv_decide solves more theorems than the state-of-the-art in verified bit-blasting, CoqQFBV. We also verify over 7000 SMT statements extracted from LLVM, providing the largest mechanized verification of LLVM rewrites to date, to our knowledge. By making bit-blasting bitvector reasoning a polished, well-supported, and interactive feature of modern ITPs, we enable effective, dependable white-box reasoning for bitvector-level verification.\n          <\/jats:p>","DOI":"10.1145\/3763167","type":"journal-article","created":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T08:51:31Z","timestamp":1759999891000},"page":"3259-3285","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Interactive Bitvector Reasoning using Verified Bit-Blasting"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0007-8294-2710","authenticated-orcid":false,"given":"Henrik","family":"B\u00f6ving","sequence":"first","affiliation":[{"name":"Lean FRO, Munich, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-6410-3681","authenticated-orcid":false,"given":"Siddharth","family":"Bhat","sequence":"additional","affiliation":[{"name":"University of Cambridge, Cambridge, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8826-9607","authenticated-orcid":false,"given":"Luisa","family":"Cicolini","sequence":"additional","affiliation":[{"name":"University of Cambridge, Cambridge, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-9831-6968","authenticated-orcid":false,"given":"Alex","family":"Keizer","sequence":"additional","affiliation":[{"name":"University of Cambridge, Cambridge, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-1880-0602","authenticated-orcid":false,"given":"L\u00e9on","family":"Frenot","sequence":"additional","affiliation":[{"name":"ENS Lyon, Lyon, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1414-7073","authenticated-orcid":false,"given":"Abdalrhman","family":"Mohamed","sequence":"additional","affiliation":[{"name":"Stanford University, Stanford, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4719-2922","authenticated-orcid":false,"given":"L\u00e9o","family":"Stefanesco","sequence":"additional","affiliation":[{"name":"University of Cambridge, Cambridge, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3379-5631","authenticated-orcid":false,"given":"Harun","family":"Khan","sequence":"additional","affiliation":[{"name":"Stanford University, Stanford, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4047-6196","authenticated-orcid":false,"given":"Joshua","family":"Clune","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9522-3084","authenticated-orcid":false,"given":"Clark","family":"Barrett","sequence":"additional","affiliation":[{"name":"Stanford University, Stanford, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3874-6003","authenticated-orcid":false,"given":"Tobias","family":"Grosser","sequence":"additional","affiliation":[{"name":"University of Cambridge, Cambridge, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,10,9]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290384"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"e_1_2_1_4_1","volume-title":"Leonardo De Moura, and Pascal Fontaine","author":"Barrett Clark","year":"2015","unstructured":"Clark Barrett, Leonardo De Moura, and Pascal Fontaine. 2015. Proofs in satisfiability modulo theories. All about proofs, Proofs for all, 55, 1 (2015), 23\u201344."},{"key":"e_1_2_1_5_1","unstructured":"Clark Barrett Pascal Fontaine and Cesare Tinelli. 2024. The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org."},{"key":"e_1_2_1_6_1","volume-title":"Proceedings of the 8th international workshop on satisfiability modulo theories","author":"Barrett Clark","year":"2010","unstructured":"Clark Barrett, Aaron Stump, Cesare Tinelli, et al. 2010. The smt-lib standard: Version 2.0. In Proceedings of the 8th international workshop on satisfiability modulo theories (Edinburgh, UK). 13, 14."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/277044.277186"},{"key":"e_1_2_1_8_1","unstructured":"Joel Beeren Matthew Fernandez Xin Gao Gerwin Klein Rafal Kolanski Japheth Lim Corey Lewis Daniel Matichuk and Thomas Sewell. 2016. Finite Machine Word Library. Archive of Formal Proofs."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","unstructured":"Siddharth Bhat Alex Keizer Chris Hughes Andr\u00e9s Goens and Tobias Grosser. 2024. Verifying Peephole Rewriting in SSA Compiler IRs. arXiv preprint arXiv:2407.03685 https:\/\/doi.org\/10.48550\/arXiv.2407.03685 10.48550\/arXiv.2407.03685","DOI":"10.48550\/arXiv.2407.03685"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-65627-9_7"},{"key":"e_1_2_1_11_1","volume-title":"IsaSAT and Kissat Entering the SAT Competition","author":"Biere Armin","year":"2024","unstructured":"Armin Biere, Tobias Faller, Katalin Fazekas, Mathias Fleury, Nils Froleyks, and Florian Pollitt. 2024. CaDiCaL, Gimsatul, IsaSAT and Kissat Entering the SAT Competition 2024. In Proc. of SAT Competition 2024 \u2013 Solver, Benchmark and Proof Checker Descriptions, Marijn Heule, Markus Iser, Matti J\u00e4rvisalo, and Martin Suda (Eds.) (Department of Computer Science Report Series B, Vol. B-2024-1). University of Helsinki, 8\u201310."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24364-6_2"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14052-5_11"},{"key":"e_1_2_1_14_1","unstructured":"Arthur Blot Pierre-Evariste Dagand and Julia Lawall. [n. d.]. Bit Sequences and Bit Sets Library. https:\/\/github.com\/pedagand\/ssrbit"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-25379-9_15"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14203-1_9"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/ARITH.2013.30"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/ARITH.2011.40"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385965"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","unstructured":"Henrik B\u00f6ving Siddharth Bhat Luisa Cicolini Alex Keizer L\u00e9on Frenot Abdalrhman Mohamed L\u00e9o Stefanesco Harun Khan Joshua Clune Clark Barrett and Tobias Grosser. 2025. Interactive Bit Vector Reasoning using Verified Bitblasting. https:\/\/doi.org\/10.5281\/zenodo.15762083 10.5281\/zenodo.15762083","DOI":"10.5281\/zenodo.15762083"},{"key":"e_1_2_1_21_1","unstructured":"Robert Brummayer and Armin Biere. 2006. Local Two-Level And-Inverter Graph Minimization without Blowup. https:\/\/api.semanticscholar.org\/CorpusID:14512831"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00768-2_16"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3560810.3565290"},{"key":"e_1_2_1_24_1","unstructured":"Ted Chajed Haogang Chen Adam Chlipala Joonwon Choi Andres Erbsen Jason Gross Samuel Gruetter Frans Kaashoek Alex Konradi Gregory Malecha Duckki Oe Murali Vijayaraghavan Nickolai Zeldovich and Daniel Ziegler. [n. d.]. Bedrock Bitvectors Library. https:\/\/github.com\/mit-plv\/bbv"},{"key":"e_1_2_1_25_1","unstructured":"Microsoft Corporation. [n. d.]. Tactics | Online Z3 Guide. https:\/\/microsoft.github.io\/z3guide\/docs\/strategies\/tactics\/ Accessed: 2024-11-07"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63046-5_14"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.4204\/eptcs.114.8"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_1_29_1","volume-title":"d.]. Coq.Bool","author":"Duprat Jean","unstructured":"Jean Duprat. [n. d.]. Coq.Bool.BVector Library. https:\/\/coq.inria.fr\/library\/Coq.Bool. Bvector.html"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_7"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"e_1_2_1_32_1","volume-title":"Efficient Solving of the Satisfiability Modulo Bit-Vectors Problem and Some Extensions to SMT. Ph. D. Dissertation","author":"Franz\u00e9n Anders","unstructured":"Anders Franz\u00e9n. 2010. Efficient Solving of the Satisfiability Modulo Bit-Vectors Problem and Some Extensions to SMT. Ph. D. Dissertation. University of Trento, Italy. http:\/\/eprints-phd.biblio.unitn.it\/345\/"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73368-3_52"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.6092\/issn.1972-5787\/1979"},{"key":"e_1_2_1_35_1","volume-title":"Gnu mp","author":"Granlund Torbj\u00f6rn","year":"1996","unstructured":"Torbj\u00f6rn Granlund. 1996. Gnu mp. The GNU Multiple Precision Arithmetic Library, 2, 2 (1996)."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_45"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0031814"},{"key":"e_1_2_1_38_1","unstructured":"Joe Hurd. 2003. First-order proof tactics in higher-order logic theorem provers. Design and Application of Strategies\/Tactics in Higher Order Logics number NASA\/CP-2003-212448 in NASA Technical Reports 56\u201368."},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_53"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/CMPASS.1996.507872"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66263-3_29"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/CGO.2004.1281665"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24690-6_28"},{"key":"e_1_2_1_44_1","unstructured":"Lean FRO. 2025. Lean-MLIR GitHub. https:\/\/github.com\/opencompl\/lean-mlir"},{"key":"e_1_2_1_45_1","unstructured":"Lean FRO. 2025. Lean4 GitHub. https:\/\/github.com\/leanprover\/lean4"},{"key":"e_1_2_1_46_1","volume-title":"ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress.","author":"Leroy Xavier","year":"2016","unstructured":"Xavier Leroy, Sandrine Blazy, Daniel K\u00e4stner, Bernhard Schommer, Markus Pister, and Christian Ferdinand. 2016. CompCert-a formally verified optimizing compiler. In ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress."},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454030"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373824"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/1476589.1476628"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","unstructured":"Aina Niemetz and Mathias Preiner. 2023. Bitwuzla. In Computer Aided Verification Constantin Enea and Akash Lal (Eds.). Springer Nature Switzerland Cham. 3\u201317. isbn:978-3-031-37703-7 https:\/\/doi.org\/10.1007\/978-3-031-37703-7_1 10.1007\/978-3-031-37703-7_1","DOI":"10.1007\/978-3-031-37703-7_1"},{"key":"e_1_2_1_51_1","unstructured":"SMT-COMP Organizers. 2024. SMT-COMP 2024 Results. Online. https:\/\/smt-comp.github.io\/2024\/results.html Accessed: 2025-03-25"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","unstructured":"Yan Peng and Mark Greenstreet. 2015. Extending ACL2 with SMT solvers. arXiv preprint arXiv:1509.06082 https:\/\/doi.org\/10.4204\/EPTCS.192.6 10.4204\/EPTCS.192.6","DOI":"10.4204\/EPTCS.192.6"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.SAT.2023.21"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","unstructured":"Alastair Reid. 2016. Trustworthy specifications of ARM\u00ae v8-A and v8-M system level architecture. In 2016 Formal Methods in Computer-Aided Design (FMCAD). 161\u2013168. https:\/\/doi.org\/10.1109\/FMCAD.2016.7886675 10.1109\/FMCAD.2016.7886675","DOI":"10.1109\/FMCAD.2016.7886675"},{"key":"e_1_2_1_55_1","unstructured":"David M Russinoff. 2017. Polynomial terms and sparse horner normal form."},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408997"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_7"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/3605769.3623993"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-012-0163-3"},{"key":"e_1_2_1_60_1","unstructured":"Nikhil Swamy Guido Martinez and Aseem Rastogi. 2023. Proof-Oriented Programming in F*."},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","unstructured":"Sol Swords and Jared Davis. 2011. Bit-blasting ACL2 theorems. arXiv preprint arXiv:1110.4676 https:\/\/doi.org\/10.4204\/EPTCS.70.7 10.4204\/EPTCS.70.7","DOI":"10.4204\/EPTCS.70.7"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","unstructured":"Grigori S Tseitin. 1983. On the complexity of derivation in propositional calculus. Automation of reasoning: 2: Classical papers on computational logic 1967\u20131970 466\u2013483. https:\/\/doi.org\/10.1007\/978-3-642-81955-1_28 10.1007\/978-3-642-81955-1_28","DOI":"10.1007\/978-3-642-81955-1_28"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/3412932.3412935"},{"key":"e_1_2_1_64_1","unstructured":"Henry S Warren. 2013. Hacker\u2019s delight. Pearson Education."},{"key":"e_1_2_1_65_1","volume-title":"DeepSpec: Modular Certified Programming with Deep Specifications","author":"Weng Shu-Chun","unstructured":"Shu-Chun Weng. 2016. DeepSpec: Modular Certified Programming with Deep Specifications. Yale University."},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_7"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103709"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134043"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3763167","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T17:45:20Z","timestamp":1760031920000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3763167"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,9]]},"references-count":68,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2025,10,9]]}},"alternative-id":["10.1145\/3763167"],"URL":"https:\/\/doi.org\/10.1145\/3763167","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,9]]},"assertion":[{"value":"2025-03-25","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-12","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-10-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}