Pith. sign in

REVIEW 2 major objections 4 minor 13 references

Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract)

T0 review · 2 major / 4 minor · reviewed 2026-08-14 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read Coq verification proves 18 bit-vector invertibility equivalences for arbitrary bit-widths, including 11 results beyond a previous automated attempt.

desk verdict A genuinely useful, modest formal-verification result: 18 bit-vector invertibility equivalences proved in Coq for arbitrary bit-widths, with a few presentation gaps that a revision can fix. read the letter →

arxiv 1908.09478 v1 pith:LLY552VG submitted 2019-08-26 cs.LO

Burak Ekici (University of Innsbruck) , Arjun Viswanathan (University of Iowa) , Yoni Zohar (Stanford University) , Clark Barrett (Stanford University) , Cesare Tinelli (University of Iowa) This is my paper · ORCID
classification cs.LO MSC 03B3568Q60
keywords fixed-widthbit-vectorsinvertibilityconditionsequivalencesquantifiedbit-vectorformulasSMT-LIB2Coqinteractivetheoremprovingquantifierinstantiation
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

Quantified formulas over bit-vectors are hard for SMT solvers partly because quantifier instantiation relies on invertibility conditions: side conditions that say exactly when a literal containing a distinguished variable can be solved for that variable. Previously these conditions were checked only for concrete bit-widths up to 65, and an automated translation to integer arithmetic still left many unproved. This paper reports a first step in verifying them in Coq for every bit-width at once. The authors prove 18 invertibility equivalences: all equality cases expressible in their restricted signature, including four that had resisted the earlier approach, plus seven of the eight non-equality cases that the earlier approach had left open. The result leaves only one partially proved equivalence in the restricted signature and shows that interactive theorem proving can complement solver-based verification for width-parametric bit-vector reasoning.

What carries the argument

The load-bearing object is the invertibility equivalence $IC[s,t] \Leftrightarrow \exists x.\, \ell[x,s,t]$, which packages the side condition that licenses quantifier instantiation. The proof machinery is a two-layer Coq bit-vector library: bit-vectors are little-endian lists of Booleans, with a raw layer for simple case analysis and a dependent layer carrying the width in the type, connected by a functor that lifts raw proofs to dependent ones. This paper extends that library with arithmetic right shift, unsigned weak comparisons, and shift operations redefined in terms of list prefix functions, which reduces many goals to standard list lemmas.

What would settle it

Pick one of the 18 stated equivalences, instantiate it at a small concrete width such as 8, and enumerate all assignments to the three variables; if the side condition and the existence of a witness differ, the proof of that equivalence cannot be correct. Because the theorems quantify over all widths, a single such mismatch at any width is a decisive refutation.

Watch

Extended reading notes

Core claim

For every positive bit-width $n$, the paper proves in Coq the invertibility equivalence $IC[s,t] \Leftrightarrow \exists x.\, \ell[x,s,t]$ for 18 literals built from the restricted signature $\Sigma_0$: unary and bitwise negation, conjunction, disjunction, left and right shifts, arithmetic right shift, addition, and the comparison predicates $=$, $\neq$, $<_u$, $>_u$, $\leq_u$, $\geq_u$. All eleven equality equivalences expressible in this signature are proved, four of them for the first time; among the non-equality predicate cases previously left open, seven of eight are proved. The proofs are carried out on raw bit-vectors and lifted to dependently typed bit-vectors, and the library is extended with arithmetic right shift, unsigned weak comparisons, and redefined shift operations. The single remaining unproved restricted equivalence is the reverse direction for the literal $x \gg s >_u t$, whose forward direction has already been proved both in Coq and by the earlier approach.

Load-bearing premise

Everything rests on the Coq library's bit-vector operations, especially the added arithmetic shift, the unsigned weak comparisons, and the redefined shifts, faithfully matching the SMT-LIB 2 semantics that solver-side invertibility conditions are meant to describe.

Editorial extensions

If this is right

  • The 18 verified equivalences hold at every bit-width, so quantifier-instantiation techniques built on them are justified even when the formula width is not fixed in advance.
  • Four previously unproved equality conditions and seven previously unproved inequality conditions now have machine-checked proofs, going beyond width-bounded SMT checks.
  • The two-layer proof style, raw lemmas lifted to dependent types, gives a reusable template for proving other width-parametric bit-vector properties in Coq.
  • Only one restricted equivalence remains only partially proved, so the question of whether every $\Sigma_0$ invertibility condition has a correct side condition is nearly settled.
  • The extended Coq library, with its new shift and unsigned-comparison lemmas, is directly reusable for further verification tasks inside the same bit-vector theory.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • A natural next stress test is the one partially proved equivalence: if the reverse direction fails at some concrete width, then no invertibility condition expressible in the restricted signature exists for that literal, which would explain why earlier solvers could not prove it.
  • The same Coq developments could be packaged as a certification back end: an SMT solver emits the invertibility condition it uses, and Coq produces a machine-checkable certificate that the condition matches existence of a witness at every width.
  • The shift-redefinition lemmas, centered on prefix monotonicity and firstn length, are likely useful beyond invertibility, for example in verifying width-parametric shift and rotate circuit identities.
  • Because the proofs are parametric in the width, they can be seen as a meta-theorem: the solver's internal rule is established once and for all, rather than re-checked for each concrete bit-width.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

2 major / 4 minor

Summary. This extended abstract reports on an ongoing effort to verify bit-vector invertibility conditions in Coq. The authors extend an existing bit-vector library (from SMTCoq) with the arithmetic right shift operator, unsigned weak inequalities, and redefined shift operators, and then prove 18 invertibility equivalences for the signature Sigma_0, where the variables range over arbitrary bit-widths. The paper compares the new results with the previous SMT-based verification of Niemetz et al. [10], claims 11 additional equivalences beyond that work, and makes the Coq development available on GitHub. The proofs are machine-checked with Coq 8.9.0, and proof excerpts are shown in Figures 1-4 and Table 1.

Significance. If the semantic gap identified below is closed, this is a valuable contribution to the meta-verification of SMT solver techniques. The work demonstrates that an interactive proof assistant can verify bit-width-parametric invertibility equivalences for a theory where SMT solvers can only handle concrete widths, and it strictly improves the coverage of [10]. The two-layer raw/dependent representation of bit-vectors and the use of a functor to lift proofs are sensible engineering choices that the paper explains clearly. The use of machine-checked proofs and the public availability of the development are explicit strengths, as is the honest reporting of the one incomplete equivalence for x >> s >u t.

major comments (2)
  1. [Sections 4 and 5] The manuscript never shows the Coq definition of bv_ashr_a or the second equivalent definition of arithmetic right shift; it only states that 'We also have two definitions for >>a, and a proof of their equivalence.' Since Equation (4) and the Table 1 rows for >>a are among the main new results, and since arithmetic right shift has subtle behavior when the shift amount is at least the width (all remaining bits must become copies of the sign bit), the formal content of these theorems is not pinned down in the paper. Please include the definition of bv_ashr_a and the redefined right shift, state explicitly how shift amounts greater than or equal to the width are handled, and indicate that these definitions are exactly the ones used in the reported proofs.
  2. [Section 4, first paragraph; Section 5] The paper asserts that the library 'models the theory ... adopted by the SMT-LIB 2 standard,' but it provides no formal statement relating the little-endian Boolean-list definitions, after the redefinition of the shift operators and the addition of bv_ashr_a, to the SMT-LIB 2 semantics. The central claim that the proved invertibility equivalences are valid for fixed-width bit-vectors as used by CVC4 is only as strong as the faithfulness of these definitions. Add a concise statement of the intended semantics for the new and redefined operators, and ideally prove or state sanity lemmas such as sign-filling for bv_ashr_a and the equivalence of the two shift definitions.
minor comments (4)
  1. [Table 1] The legend of Table 1 is hard to read: the symbols for 'verified in Coq but not in [10]' and 'verified in [10] but not in Coq' are visually very similar in the PDF, and the symbol for 'not fully proved' does not convey the paper's statement that one direction of x >> s >u t was proved in both approaches. Please use distinct, clearly labeled markers and add a footnote explaining the partial-proof status.
  2. [Section 5] The sentence 'One does not need to install CoqHammer in order to build the bit-vector library, since all the proof reconstruction tactics of CoqHammer are included in it' is slightly ambiguous: it is unclear whether 'included in it' means included with the released library or still requiring a separate installation. Please clarify the dependency status.
  3. [Reproducibility] The paper points to a GitHub branch but gives no commit hash or build instructions beyond 'it compiles with coqc-8.9.0'. A pinned commit or archive would make the artifact easier for readers to reproduce and verify.
  4. [References] Reference [10] lists 'Aina Niemetz, Mathias Preiner, Andrew Reynolds Yoni Zohar' with a missing comma before 'Yoni Zohar'; please correct the author list.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the Coq proofs are machine-checked and the self-citations are contextual; the semantic-link gap is a correctness risk, not a circular step.

full rationale

The paper's derivation chain is direct and machine-checked. Invertibility conditions from [9] are treated as statements to be proven, not as trusted premises: the Coq development proves each equivalence IC[s,t] <-> exists x. l[x,s,t] against the library's bit-vector definitions, with the Coq kernel checking every step. [10] is used only as a baseline for which equivalences were already verified, and [6] is used for the original library, but the new operators (bv_ule, bv_ashr_a, redefined shifts) are defined in this paper, and the paper states an internal equivalence theorem (bv_shl_eq) between old and new shift definitions. No parameter is fitted to data and then renamed a prediction, and no author-imported uniqueness theorem forces the choice of conditions. The genuine weakness is external adequacy, not circularity: the definition of bv_ashr_a is never shown, and no formal link between the library's little-endian list representation and the SMT-LIB 2 semantics is given, so the theorems certify properties of the library's own operators. A semantic mismatch in the newly added operators would break the transfer to CVC4, but that is a correctness risk and does not make the proof circular.

Assumptions & free parameters 0 free parameters · 2 assumptions · 0 invented entities

The central claim rests on the correctness of the formalization rather than on free parameters. The two assumptions listed are standard for proof-engineering papers: faithful encoding semantics and axiom-free compilation.

assumptions (2)
  • domain assumption The Coq bit-vector library's definitions faithfully model the SMT-LIB 2 theory of fixed-width bit-vectors
    All proofs are conducted against these definitions; if the encoding is wrong, the theorems do not apply to the intended semantics. Invoked in Sections 4 and 5.
  • domain assumption The shipped Coq development compiles with no axioms or admitted lemmas
    The paper states the code compiles with coqc-8.9.0 but does not discuss axiom usage; the verification claim would be weakened if the proofs relied on axioms (for example, from hammer reconstruction tactics).

how reviews work

0 comments
Cite this review

Pith. "Pith review of Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract)." pith.science (2026). https://pith.science/paper/LLY552VG

@misc{pith2026190809478,
  author       = {Pith},
  title        = {Pith review of: Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract)},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/LLY552VG}},
  note         = {Machine review of arXiv:1908.09478}
}
read the original abstract

This work is a part of an ongoing effort to prove the correctness of invertibility conditions for the theory of fixed-width bit-vectors, which are used to solve quantified bit-vector formulas in the Satisfiability Modulo Theories (SMT) solver CVC4. While many of these were proved in a completely automatic fashion for any bit-width, some were only proved for bit-widths up to 65, even though they are being used to solve formulas over arbitrary bit-widths. In this paper we describe our initial efforts in proving a subset of these invertibility conditions in the Coq proof assistant. We describe the Coq library that we use, as well as the extensions that we introduced to it.

Figures

Figures reproduced from arXiv: 1908.09478 by the authors.

Figure 1
Figure 1. Definitions of ≤u in Coq. the addition of ≤u (the definition of ≥u is similar). The relevant Coq definitions are provided in [PITH_FULL_IMAGE:figures/full_fig_p005_1.png] view at source ↗
Figure 2
Figure 2. A proof of one direction of the invertibility equivalence for [PITH_FULL_IMAGE:figures/full_fig_p006_2.png] view at source ↗
Figure 3
Figure 3. Various definitions of <<. and the shl_n_bits functions. shl_one_bit shifts the bit-vector to the left by one bit and is repeatedly called by shl_n_bits to complete the shift. The new definition shl_n_bits_a uses mk_list_false which constructs the necessary list of 0s and appends (++ in Coq) it to the beginning of the list (because of the little-endian encoding); the bits to be shifted from the original bit-vector a… view at source ↗
Figures from the paper (1 more)
Figure 4
Figure 4. Figure 4: Examples of lemmas used in proofs of invertibility equivalences. [PITH_FULL_IMAGE:figures/full_fig_p008_4.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

13 extracted references · 8 canonical work pages

  1. [10]

    To appear in the proceedings of CADE-27

    Aina Niemetz, Mathias Preiner, Andrew Reynolds Yoni Zohar, Clark Barrett & Cesare Tinelli (2019): To- wards Bit-Width-Independent Proofs in SMT Solvers. To appear in the proceedings of CADE-27

    work page 2019

  2. [1]

    Clark Barrett, Aaron Stump & Cesare Tinelli (2010): The SMT-LIB Standard: Version 2.0 . In A. Gupta & D. Kroening, editors: Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (Edinburgh, UK)

    work page 2010

  3. [2]

    Available at https://github.com/pedagand/ssrbit

    Arthur Blot, Pierre-Evariste Dagand, & Julia Lawall: Bit Sequences and Bit Sets Library . Available at https://github.com/pedagand/ssrbit

    work page

  4. [3]

    Available at https://github.com/mit-plv/bbv

    Tej 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 & Daniel Ziegler: Bedrock Bit Vectors Library. Available at https://github.com/mit-plv/bbv

    work page

  5. [4]

    Lukasz Czajka & Cezary Kaliszyk (2018): Hammer for Coq: Automation for Dependent Type Theory . J. Autom. Reasoning 61(1-4), pp. 423–453, doi:10.1007/s10817-018-9458-4

    doi:10.1007/s10817-018-9458-4 2018

  6. [5]

    Available at https://coq.inria.fr/library/Coq.Bool

    Jean Duprat: Library Coq.Bool.Bvector . Available at https://coq.inria.fr/library/Coq.Bool. Bvector.html

    work page

  7. [6]

    In: Proceedings of 29th International Con- ference on Computer Aided Verification (CA V 2017), Lecture Notes in Computer Science 10427, Springer, pp

    Burak Ekici, Alain Mebsout, Cesare Tinelli, Chantal Keller, Guy Katz, Andrew Reynolds & Clark Barrett (2017): SMTCoq: A Plug-In for Integrating SMT Solvers into Coq. In: Proceedings of 29th International Con- ference on Computer Aided Verification (CA V 2017), Lecture Notes in Computer Science 10427, Springer, pp. 126–133, doi:10.1007/s10703-012-0163-3

    doi:10.1007/s10703-012-0163-3 2017

  8. [7]

    Enderton (2001): Chapter TWO - First-Order Logic

    Herbert B. Enderton (2001): Chapter TWO - First-Order Logic . In Herbert B. Enderton, editor: A Math- ematical Introduction to Logic (Second Edition) , second edition edition, Academic Press, Boston, pp. 67 – 181, doi:10.1016/B978-0-08-049646-7.50008-4

    work page doi:10.1016/b978-0-08-049646-7.50008-4 2001

Show all 13 references
  1. [8]

    Fisher (1993): Representation and Symbolic Manipulation of Linearly Inductive Boolean Functions

    Aarti Gupta & Allan L. Fisher (1993): Representation and Symbolic Manipulation of Linearly Inductive Boolean Functions. In: Proceedings of the 1993 IEEE/ACM International Conference on Computer-aided Design, ICCAD ’93, IEEE Computer Society Press, Los Alamitos, CA, USA, pp. 19...

    1993

  2. [9]

    In: Proceedings of 30th International Conference on Computer Aided Verification (CA V 2018), pp

    Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett & Cesare Tinelli (2018):Solving Quantified Bit-Vectors Using Invertibility Conditions. In: Proceedings of 30th International Conference on Computer Aided Verification (CA V 2018), pp. 236–255, doi:10.1007/978-3-319-96142-2 16

    2018 doi

  3. [11]

    Lecture Notes in Computer Science 2283, Springer Science & Business Media, doi:10.1007/3- 540-45949-9 6

    Tobias Nipkow, Lawrence C Paulson & Markus Wenzel (2002): Isabelle/HOL: a proof assistant for higher- order logic. Lecture Notes in Computer Science 2283, Springer Science & Business Media, doi:10.1007/3- 540-45949-9 6

    2002 doi

  4. [12]

    In: Proceedings of the 1st International Conference on Interactive Theorem Proving (ITP 2010), pp

    Matthieu Sozeau (2010): Equations: A Dependent Pattern-Matching Compiler . In: Proceedings of the 1st International Conference on Interactive Theorem Proving (ITP 2010), pp. 419–434, doi:10.1007/978-3-642- 14052-5 29

    2010 doi

  5. [13]

    Available at https://coq.inria.fr/distrib/current/refman/

    The Coq development team (2019): The Coq Proof Assistant Reference Manual Version 8.9 . Available at https://coq.inria.fr/distrib/current/refman/

    2019

Pith tools

Reviewed August 14, 2026 · model on record in the stance chip above.