Precision- and Error-Aware SQL Equivalence: Deciding Rewrites Under IEEE-754 Rounding and Runtime Errors

Abstract

Every published SQL equivalence checker — Cosette/HoTTSQL, EQUITAS, SPES, WeTune, and the current frontier QED, VeriEQL, and Polygon — decides whether two queries are equivalent by modeling numeric columns as exact mathematical integers or reals under total, error-free arithmetic. That model is convenient and, for its purpose, sound; but it is silent on two behaviors observable in every production engine. First, floating-point rounding: rewrites that hold over the reals — reassociation, distribution, cancellation — can change the result of an IEEE-754 DOUBLE computation, and an exact-real prover accepts them anyway. Second, runtime errors: division by zero, overflow, and CAST failure are outcomes distinct from a value or NULL, and a total-arithmetic model silently equates an edit that errors with one that returns NULL (the archetypal a/b → SAFE_DIVIDE(a,b) refactor). We present the first precision- and error-aware SQL equivalence checker. It decides scalar rewrites under (i) an IEEE-754 floating-point model via the SMT theory of floating point, and (ii) a three-outcome ERROR/NULL/value lattice. Its primary, sound use is disproof: producing a concrete witness on which a real-number-valid rewrite diverges under rounding or error semantics. We disprove reassociation, distribution, and cancellation with Float32 counterexamples validated by re-execution, and separate error-preserving from error-changing edits with witnesses. We then run the checker against a production optimizer: it re-derives, mechanically, the IntegralType guard Apache Spark's ReorderAssociativeOperator applies by hand, and flags the exact case Apache Calcite's RexSimplify got wrong and had to patch (CALCITE-7145). Finally, we automatically ingest Calcite's own checkSimplify test assertions (391 pairs) and audit the 26 that fall in our modeled fragment: the checker agrees with all 26 and contradicts none — external validation on independently-authored pairs — while measuring that the floating-point axis is essentially absent from that suite. Proving precision-equivalence is intractable even for commutativity, so the value is in disproof and bug-finding, exactly where the axis is open.