exact-predicates

Geometric predicates that cannot be wrong - with the committed proof that the float versions are

Floating point silently corrupts geometric and graph algorithms at exact ties and near-degeneracies, and the failure is invisible until it isn't. I know because it happened to me: my D* Lite planner froze stale state into paths because two mathematically equal priority keys landed one ulp apart (the bug and its fix, solved with an exact integer cost metric). This repository generalizes that lesson into its own artifact: a small set of provably-exact predicates, and - the part most correctness repos skip - a committed corpus of adversarial inputs on which CI asserts the naive double version gives the wrong answer and the exact version gives the right one, case by case. The danger is proven, not asserted; the fix is proven against an independent unbounded oracle.

Scope, stated as a hard boundary

Exact for int64 coordinates within enforced bounds, evaluated in __int128. That is the regime grid robotics actually lives in, and the same move as the planner fix: make the domain exact rather than the arithmetic adaptive. For exact predicates over arbitrary doubles, use Shewchuk's adaptive predicates or CGAL - a reimplementation here would risk something that looks right and is subtly wrong in the error-bound bookkeeping, which is the exact anti-pattern this repository exists to refute. This is a focused demonstration of a bug class and a guarantee, not a production geometry library.

Predicate	Bound	Static proof sketch
orientation(a,b,c)	|coord| ≤ 2^60	diffs ≤ 2^61, products ≤ 2^122, sum ≤ 2^123 < 2^126
incircle(a,b,c,d)	|coord| ≤ 2^28	diffs ≤ 2^29, minors ≤ 2^59, terms ≤ 2^118, sum ≤ 2^120 < 2^126
segmentRelation(...)	|coord| ≤ 2^60	built entirely from orientation

The bounds are enforced by code, not prose

Every predicate validates its inputs against the bound and throws BoundError before any arithmetic happens - the guard is a plain magnitude comparison against a compile-time constant, so it can never rely on observing the (undefined-behavior) overflow it prevents. A documented bound that isn't checked would let an out-of-range input overflow __int128 and return a confidently wrong answer while the README still said "exact" - true on the page, unenforced in the artifact. The single most important test in this repository feeds coordinates one past each bound, in every argument position, and asserts the throw fires; it guards the word "exact" itself.

What CI proves on every push

1. Corpus regeneration - the committed adversarial corpus is byte-identical to what the committed generator produces (make corpus-check); claims and code cannot drift apart.
2. Bound guards - at-the-bound answers correctly, one-past-the-bound throws, every argument position, both signs.
3. Float wrong, exact right, case by case - on every committed adversarial case the double predicate returns the wrong sign or class and the exact predicate returns the proven one. No thresholds: all cases, both assertions.
4. Unbounded oracle differential - a Python big-integer oracle (no coordinate bound) re-verifies every committed case, and additionally computes answers outside the C++ bound where the guard refuses - demonstrating the bound is a domain restriction of the implementation, not of the problem.
5. Hull invariants - Andrew's monotone chain built on the exact predicate always yields a hull that is convex, contains every input, and uses only input vertices; the same algorithm on the float predicate violates at least one invariant on every committed degenerate configuration.

The failure, drawn from committed data

Every figure renders from committed files (reports/figure_data/, emitted by tools/dump_figure_data.cpp and drift-checked by CI exactly like the corpus; tools/render_figures.py only draws).

The threshold curve is the honest map of the danger: double arithmetic is flawless on this family up to coordinate scale ~2^24 and fails routinely after it. A corpus built at small scales would have "proven" the danger with cases that don't exist - documenting where the bug class actually lives is part of not building a strawman.

The adversarial constructions

• Orientation: Fibonacci triples (0,0), (F_k,F_{k+1}), (F_{k+1},F_{k+2})
  • by Catalan's identity the true determinant is exactly ±1 while the coordinates reach ~2^59, so the double evaluation multiplies ~2^119 quantities and cannot see it - plus seeded extended-gcd pairs with bx*cy - by*cx = 1 at the same scale.
• In-circle: near-collinear lattice quadruples near the 2^28 bound with exact residues off a common line (extended-gcd construction). Four such points are near-cocircular: the true determinant collapses to the rounding-error scale of the ~2^112 intermediate terms, which is where double decides signs by noise. (Well-spread points cannot embarrass a double: a ±1 perturbation moves the determinant ~2^83, far above the ~2^55 error - the corpus documents where the danger actually lives, not a strawman.)
• Segments: parallel segments offset by a true determinant of ±1: exactly disjoint, but the double orientation rounds the offset to zero and reports contact.
• Hull: near-collinear clouds at ~2^55 with ±1 wobble, where the float hull visibly breaks convexity or containment.

Plain-language guide

For a non-specialist reader there is a five-page guide, docs/explainer/explainer.pdf, which explains the which-side question, the Fibonacci construction that makes the failure undeniable, why the corpus asserts both directions, and where the bug class does not live. Its source is committed alongside it and builds with latexmk -pdf explainer.tex.

Results

Verbatim tool output, committed under reports/:

adversarial corpus verdicts (float wrong AND exact right on every case):
  orientation 400, incircle 154, segments 43, hull configs 60
all tests passed

oracle: 1554 in-bound cases re-verified, 4 out-of-bound cases computed where the C++ guard refuses, 0 disagreements
PASS: C++ exact predicates match the unbounded oracle everywhere

657 committed adversarial cases; the double predicate is wrong on every one, the exact predicate is right on every one, and both facts are re-asserted by CI on every push. The 60 hull configurations each make the float-predicate monotone chain violate convexity or containment while the exact hull - also property-tested on random clouds - never does.

And the honest cost of exactness (reports/bench_x86-64_wsl2.txt, measured on x86-64 under WSL2; nanoseconds vary with hardware, the verdicts above do not):

orientation: exact 49.9 ns, float 27.5 ns  (exact is 1.8x slower)
incircle:    exact 71.4 ns, float 34.4 ns  (exact is 2.1x slower)

Roughly 2x, not orders of magnitude: __int128 is cheap. The float versions buy their speed by being wrong on the committed corpus.

Reproduce

git clone https://github.com/munawarkazmi/exact-predicates.git
cd exact-predicates
make corpus-check   # committed corpus == generated corpus
make test           # guards + float-wrong/exact-right on every case
make oracle         # unbounded big-integer differential (python3, stdlib)
make bench          # what exactness costs on your machine

Deterministic throughout: seeded generators, integer arithmetic, and the naive double versions compiled with -ffp-contract=off so their (wrong) verdicts are the same on every conforming platform.

License

MIT, Munawar Kazmi.