{"id":"3a86244c-e8b3-4ff0-8d0d-babf859c8285","arxiv_id":"1908.09478","paper_version":1,"verdict":"ACCEPT","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"Coq proofs establish arbitrary-bit-width invertibility equivalences for 18 bit-vector formula families, including 11 that prior SMT-based methods could not verify.","lead":"This paper reports machine-checked Coq proofs of 18 bit-vector invertibility conditions used by the SMT solver CVC4, covering arbitrary bit-widths instead of only widths up to 65. The proofs extend a Coq bit-vector library and strictly improve on a previous SMT-based verification that left 50 conditions unproved.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The Coq proofs are machine-checked, but they certify theorems about the library's own bit-vector definitions; the paper never shows the definition of bv_ashr_a or a formal link to SMT-LIB 2 semantics, so a semantic mismatch in the newly added operators would break the central claim.","rationale":"The reader's weakest assumption is exactly the semantic fidelity of the Coq library to SMT-LIB 2. I agree that this is the most load-bearing point: the proofs are machine-checked relative to the library definitions, so any divergence in those definitions would sever the connection to CVC4. I sharpen the concern by noting that the arithmetic right shift, the most subtle newly added operator, is never defined in the paper, and the handling of shift amounts at or beyond the width is the classic place for bugs. However, this is a verification gap rather than a demonstrated error. The paper honestly describes its work as initial, provides a public artifact, and the mathematical statements are plausible and supported by the proof sketches shown. The reader's ACCEPT with moderate confidence already accounts for the lack of independent compilation. Therefore my read does not change the verdict, while the proposed concrete test would settle whether the semantic-fidelity concern actually lands.","tokens_in":8769,"tokens_out":19867,"duration_ms":192895,"concrete_test":"Check the pxtp2019 artifact: extract the Coq definitions of bv_ashr_a, bv_shr_a, bv_shl_a, bv_ule, and bv_ult; evaluate them for widths 1 through 8 over all or randomly sampled inputs by running Coq's extraction to OCaml, and compare the results against an independent SMT-LIB reference such as CVC4 or Z3, covering all shift amounts including those at least the width. Also run 'Print Assumptions' on the 18 equivalence theorems to confirm that no admitted axioms are used. Any mismatch or axiom would invalidate the central claim.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim is that 18 invertibility equivalences are proved for the SMT-LIB 2 theory of fixed-width bit-vectors. Coq checks the proofs, but it cannot check the paper's assertion that the library's little-endian list definitions—especially the newly added bv_ashr_a and the redefined << and >> operators—match SMT-LIB 2. Figure 1 shows the definition of bv_ule and Figure 3 shows the new left shift, but the definition of bv_ashr_a is never given; the paper only mentions 'two definitions' for >>a and a proof of their equivalence. Section 5 states that proofs proceed against these definitions, so the theorems are only as meaningful as the definitions are faithful. If bv_ashr_a computes the shift amount modulo the width, or fills with zeros instead of the sign bit when the shift amount is at least the width, then Equation (4) and the row for s >>a x would be theorems about a different operation. The same risk applies to the redefined shifts in the n >= width case. Because no independent formalization of SMT-LIB semantics is provided, the chain from Coq theorem to CVC4 correctness has a gap at exactly this point.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":9030,"tokens_out":5884,"duration_ms":63066,"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":[{"comment":"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.","section":"Sections 4 and 5"},{"comment":"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.","section":"Section 4, first paragraph; Section 5"}],"minor_comments":[{"comment":"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.","section":"Table 1"},{"comment":"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.","section":"Section 5"},{"comment":"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.","section":"Reproducibility"},{"comment":"Reference [10] lists 'Aina Niemetz, Mathias Preiner, Andrew Reynolds Yoni Zohar' with a missing comma before 'Yoni Zohar'; please correct the author list.","section":"References"}],"recommendation":"major_revision","confidential_remarks":"The reader's verdict was accept, and I agree that the machine-checked proofs are strong evidence. My main hesitation is the missing definition of bv_ashr_a and the absence of an explicit semantic bridge to SMT-LIB 2; both are fixable with additional text or a short appendix. The lack of a pinned commit also prevented me from independently building the artifact during review. If the authors supply the omitted definitions and clarify the semantic link, the paper would be acceptable."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Worth a look if you care about SMT solver correctness. The paper reports machine-checked Coq proofs of 18 bit-vector invertibility equivalences for arbitrary bit-widths, a strict improvement over the earlier SMT-translation approach [10], and the first formal treatment of these conditions. The core claim is believable: the proofs compile with coqc-8.9.0, the artifact is on GitHub, and the work builds on the SMTCoq library rather than starting from scratch.\n\nThe main new content is the 11 additional equivalences proved in Coq beyond [10], plus the library extensions that made them possible: unsigned weak comparisons, arithmetic right shift, and cleaner shift definitions. The equivalence theorem linking the original and redefined left shift (Figure 3) is a good sign of care, and the proofs are direct derivations with no fitted parameters or invented entities.\n\nSoft spots, in proportion: this is an extended abstract, so proof details are thin. The stress-test note is right that the definition of bv_ashr_a never appears in the text, and there is no formal bridge from the Coq list-of-Booleans semantics to SMT-LIB 2. If those definitions diverge from SMT-LIB semantics — say, shift amounts modulo width, or fill behavior when the shift amount is at least the width — the theorems would be about different operations. That is a genuine gap in the paper as written, though not a red flag: the library was explicitly built to represent SMT-LIB 2 bit-vectors, and the equivalence proof for the two shift definitions suggests the authors were mindful of semantics. They should show bv_ashr_a and state the intended correspondence to SMT-LIB. Also, the artifact lacks a commit hash, so the exact code is not pinned down.\n\nWho gets value: people working on quantifier instantiation in SMT, bit-vector theory, and Coq formalizations of SMT semantics. The result is incremental but real. It deserves serious peer review; with the missing definitions added and a bit more detail on the SMT-LIB connection, this would be a solid workshop-to-CADE type contribution. I would send it to referees rather than desk-reject.","headline":"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.","tokens_in":9582,"tokens_out":1750,"would_cite":false,"duration_ms":20156,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03B35","68Q60"],"pacs":[],"model":"deepseek-v4-flash","headline":"Coq verification proves 18 bit-vector invertibility equivalences for arbitrary bit-widths, including 11 results beyond a previous automated attempt.","keywords":["fixed-width bit-vectors","invertibility conditions","invertibility equivalences","quantified bit-vector formulas","SMT-LIB 2","Coq","interactive theorem proving","quantifier instantiation"],"falsifier":"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.","tokens_in":8612,"feed_emoji":"✅","tokens_out":16517,"duration_ms":149585,"temperature":0.7,"pith_summary":"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.","feed_headline":"Coq proofs verify 18 bit-vector conditions for all widths","feed_subtitle":"These side conditions drive quantified bit-vector solving; now they hold for arbitrary widths, not just up to 65.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"defines the SMT-LIB 2 bit-vector theory whose semantics the Coq library is intended to match.","marker":"[1]"},{"why":"supplies the automated proof search used to discharge many subgoals in the Coq proofs.","marker":"[4]"},{"why":"provides the original Coq bit-vector library, which this paper extends with new operators and lemmas.","marker":"[6]"},{"why":"introduces the invertibility conditions and equivalences that are the object of verification.","marker":"[9]"},{"why":"is the earlier translation-based verification whose unproved cases set the target list this paper improves on.","marker":"[10]"}],"fun_headline_variants":["Coq proves 18 bit-vector conditions for any bit-width","Bit-vector invertibility: Coq proofs cover all widths","Coq extends bit-vector invertibility proofs beyond width 65","First Coq proofs for four bit-vector equality conditions","18 bit-vector conditions proved in Coq for all bit-widths"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Coq proves 18 bit-vector conditions for any bit-width","Bit-vector invertibility: Coq proofs cover all widths","Coq extends bit-vector invertibility proofs beyond width 65","First Coq proofs for four bit-vector equality conditions","18 bit-vector conditions proved in Coq for all bit-widths"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000984,"raw_usage":{"total_tokens":4144,"prompt_tokens":880,"completion_tokens":3264,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":496,"completion_tokens_details":{"reasoning_tokens":3175}},"tokens_in":496,"tokens_out":3264,"duration_ms":25044,"temperature":1.0,"reasoning_tokens":3175,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T11:09:53.134747+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"defines the SMT-LIB 2 bit-vector theory whose semantics the Coq library is intended to match."},{"cited_title":"To appear in the proceedings of CADE-27","cited_arxiv_id":null,"evidence_quote":"is the earlier translation-based verification whose unproved cases set the target list this paper improves on."}],"review_version":1}