Characterize limits of DD orientation predicate soundness over arbitrary doubles (#1106)#1197
Open
grootstebozewolf wants to merge 5 commits into
Open
Conversation
Adds a bespoke Java reference runner (RocqRefRunner) and JUnit suite that exercise the orientation predicate (Orientation.index / CGAlgorithmsDD) against an exact reference, addressing the point-line orientation robustness requirement tracked in locationtech#1106. R^2 coverage (the property the issue actually asks for): compares Orientation.index against an exact BigDecimal determinant sign over arbitrary double coordinates -- uniform random (moderate and large magnitude), adversarial near-collinear (ULP-level perpendicular offsets), and the double-precision-hard cases from OrientationIndexFailureTest. JTS's double-double predicate agrees with the exact reference across the full ~1.6M-case sample. This is strong empirical evidence, not a proof: DD is ~106-bit, not adaptive-exact, so soundness over all of R^2 is not claimed. Bounded-integer floor: exhaustive (|c| <= 4) plus large randomized, near-collinear and domain-boundary samples over integer coords |c| <= 2^25, where the determinant is exact in 64-bit arithmetic. A loader consumes externally exported reference vectors (e.g. from a Rocq development) and cross-checks every supplied sign against the in-code reference. https://claude.ai/code/session_019x4KgiMf2qvbYV7c81D6Z3 Co-authored-by: Claude <noreply@anthropic.com> Signed-off-by: grootstebozewolf <jeroen@jeroentechsolutions.uk>
Adds DDCounterexampleHunter, which searches for inputs where an orientation predicate disagrees with the exact BigDecimal reference, and a regression test (OrientationDDRobustnessTest) that runs it. The hunter evaluates three predicates against the same exact oracle using adversarial generators (near-collinear across magnitudes up to ~2^52, minimal-determinant product collisions, uniform random): strategy / magnitude DD RobustDeterminant NonRobustCGAlgorithms near-collinear 1e7 0 36014 107214 near-collinear 1e12 0 35261 107522 near-collinear 4.5e15 0 34398 106623 product-collision 0 6295 395614 The current DD predicate (Orientation.index) yields zero counterexamples across millions of adversarial cases, while the naive and legacy predicates it replaced fail tens to hundreds of thousands of times. The test asserts both that the search is effective (legacy predicates do fail) and that DD does not. This is strong empirical evidence, not a proof: DD is ~106-bit, not adaptive-exact, but for double inputs the smallest non-zero orientation determinant is ~2^-104 relative to the product scale, giving DD about two bits of margin. https://claude.ai/code/session_019x4KgiMf2qvbYV7c81D6Z3 Co-authored-by: Claude <noreply@anthropic.com> Signed-off-by: grootstebozewolf <jeroen@jeroentechsolutions.uk>
The previous commit overstated the result. Its searches were bounded to
|coord| <= ~1e15, and concluded DD orientation had no discoverable
counterexamples. That conclusion was wrong: it implicitly assumed the DD
products neither overflow nor underflow.
Searching the full IEEE-754 double range finds counterexamples immediately:
(0,0),(1e200,1e200),(2e200,2.0000001e200) -> DD=0, exact=+1
Mechanism and sharp thresholds:
- Overflow: for |coord| >= 2^512 (~1.34e154) a DD product exceeds
Double.MAX_VALUE -> Infinity, the determinant is Infinity-Infinity=NaN,
and orientationIndex returns 0 (collinear) for non-collinear points.
- Underflow: for |coord| <~ 2^-512 the products flush to zero and the
determinant is reported as 0.
DD is sound only within roughly [2^-511, 2^511]; the ~2-bit margin argument
holds only inside that band.
Adds DDCounterexampleHunter.extremeMagnitude generator, KNOWN_COUNTEREXAMPLES,
and OVERFLOW/UNDERFLOW magnitude constants. OrientationDDRobustnessTest now
characterizes the limitation (testDDFailsOnOverflow, testDDFailsOnUnderflow,
testKnownCounterexamples) and scopes the soundness assertions to the safe band.
https://claude.ai/code/session_019x4KgiMf2qvbYV7c81D6Z3
Co-authored-by: Claude <noreply@anthropic.com>
Signed-off-by: grootstebozewolf <jeroen@jeroentechsolutions.uk>
…efect
Property-tests the Shewchuk expansion primitives in ShewchuksDeterminant
(test-source) against an exact BigDecimal reference, mirroring refSignExact:
- Two_Sum / Fast_Two_Sum / Two_Product are exact (head+tail == a+b / a*b);
- ShewchuksDeterminant.orientationIndex is exact end-to-end within the safe
magnitude band (transitively exercising the expansion stack);
- Two_Product overflows for products beyond Double.MAX_VALUE (range limit;
adaptive precision does not grant overflow immunity).
Documents a real defect found while probing fast_expansion_sum_zeroelim: lines
713/717 use post-increment (e[eindex++]) where Shewchuk's reference uses
pre-increment (e[++eindex]), so it re-reads the first component instead of
advancing -- double-counting the first and dropping the largest for inputs of
length >= 2 (e.g. [1,16,256,4096]+[2,32,512,8192] -> 822, should be 13107).
This is test-source code (production orientation uses CGAlgorithmsDD), and the
defect is masked in orientationIndex by the Stage-A float filter, so no sign
errors occur over 2M near-collinear cases. Not auto-fixed: a correct Java port
must also guard the one-past-end read Shewchuk's C relies on.
https://claude.ai/code/session_019x4KgiMf2qvbYV7c81D6Z3
Co-authored-by: Claude <noreply@anthropic.com>
Signed-off-by: grootstebozewolf <jeroen@jeroentechsolutions.uk>
Adds a brief prose note in DDCounterexampleHunter: the self-contained BigDecimal reference (RocqRefRunner.refSignExact) remains the sole ground truth for the tests, and its verdicts -- including the overflow/underflow counterexamples -- were independently spot-checked against an external GMP-backed exact-integer orientation oracle and agreed in all cases. The oracle is corroboration only, not a test dependency; no binary or harness is vendored. https://claude.ai/code/session_019x4KgiMf2qvbYV7c81D6Z3 Co-authored-by: Claude <noreply@anthropic.com> Signed-off-by: grootstebozewolf <jeroen@jeroentechsolutions.uk>
grootstebozewolf
pushed a commit
to grootstebozewolf/NetTopologySuite.Proofs
that referenced
this pull request
Jun 2, 2026
… / PR #1197 The JTS robustness PR (locationtech/jts#1197) adds RocqRefRunner + orientation_proof_vectors.txt -- a drop-in slot for 'future exports from the Rocq orientation-soundness development'. This fills it. oracle/gen_orientation_vectors.sh runs the oracle ORIENT_EXACT mode (the runnable form of the Qed-proven b64_orient2d_exact_sound -- exact over ALL finite binary64, no DD [2^-511, 2^511] band limit) and emits certified (x0 y0 x1 y1 x2 y2 EXPECTED) vectors. Coordinates are exact: decimal integers for |c| <= 2^53, hex floats for pure powers of two outside that band -- both round-trip exactly in OCaml and Java. oracle/orientation_proof_vectors.txt covers the regimes #1197's hunter characterizes, including the DD failure modes where the Rocq-backed exact sign is the ground truth: - basic CCW/CW/collinear; - adversarial near-collinear at 2^27 (exact=POS, naive double=ZERO; re-validated); - OVERFLOW band edge ~2^512 (DD -> inf -> NaN -> signum 0 = wrong ZERO); - UNDERFLOW band edge ~2^-540 (DD products flush to 0 = wrong ZERO); - ~600-binade dynamic range. This is the Rocq-side counterpart to RocqRefRunner.loadProofCases: the exact route is precisely the 'wider-range exact path' #1106 says a fully robust predicate needs. Format maps to loadProofCases (adjust there or here if the parser differs).
This was referenced Jun 4, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
This PR adds comprehensive test infrastructure and empirical characterization of the robustness limits of JTS's orientation predicate (
Orientation.index), directly addressing the core request in #1106.It does not change any public API or production behavior.
Key Findings
CGAlgorithmsDD.orientationIndex→DD) is sound for coordinates roughly in the band[2^-511, 2^511].DD.selfMultiplybecome+∞, the determinant evaluates toNaN, andsignum()returns 0 (collinear) for genuinely non-collinear input.The work also validates the historical 64-bit integer soundness claim for integer coordinates |c| ≤ 2^25 (the domain for which a short machine-checkable argument exists).
What This PR Delivers
DDCounterexampleHunter— a powerful adversarial search framework with multiple generators (nearCollinear,productCollision,extremeMagnitude, etc.) and three side-by-side predicates (current DD, legacyRobustDeterminant, naive double).OrientationDDRobustnessTest— JUnit suite that proves the hunter is effective, asserts soundness inside the safe band (millions of cases), and explicitly demonstrates the overflow/underflow failures.KNOWN_COUNTEREXAMPLES+extremeMagnitudegenerator — reproducible demonstrations of the exact failure modes.ShewchukExpansionExactnessTest— property-based verification of the Shewchuk expansion primitives (exactness vs BigDecimal + structural invariants offast_expansion_sum_zeroelim). Also documents a masked porting detail in the zero-elimination routine.RocqRefRunner+RocqRefRunnerTest— self-contained exact oracles:refSignExact(...)usingBigDecimal(exact for any finite dyadic double — the R² reference)BigIntegercross-checkloadProofCases(...)that validates imported Rocq vectors against the Java reference (a corrupt export cannot silently weaken the tests)orientation_proof_vectors.txt— drop-in slot for future exports from the Rocq orientation-soundness development (currently populated with manually-derived certified cases).All new tests are fast enough for CI while the
mainmethods in the hunter support very large-scale evidence gathering.Practical Impact
For all normal GIS, CAD, graphics, and most scientific workloads the coordinate magnitudes are many orders of magnitude below the failure threshold. This work documents a real theoretical limitation with excellent evidence rather than discovering a bug that affects everyday users.
Relationship to Formal Methods
The
RocqRefRunneris designed as a bridge to the separate Rocq (Coq) orientation-soundness proof development. The Java side can consume and independently validate proof vectors, allowing the formal guarantee (for the integer domain) to be exercised as ordinary JUnit tests.Testing
modules/core.mvn test -pl modules/core -Dtest=OrientationDDRobustnessTest,ShewchukExpansionExactnessTest,RocqRefRunnerTestmainmethod provides extended evidence (millions of adversarial cases).Contribution Checklist
-s)enhancement,jts-core,testsAddresses #1106 (orientation soundness over arbitrary doubles).
Feedback welcome on preferred mitigation strategies (pre-scaling, adaptive BigDecimal fallback on detected overflow, etc.) if/when a production fix is desired in the future.