From c271363c2a440c553a5b955d53e836b2bb19922c Mon Sep 17 00:00:00 2001 From: Jeroen Bloemscheer Date: Wed, 5 Aug 2026 03:23:06 +0200 Subject: [PATCH] docs: JTS #311 in-circle design history (mesh lane session 3) Archive the 2018 isInCircleAdapt sketch against the #1212/#1094 lineage: Stage A gate with ulp(1.0) epsilon note, vector table, and optional PR comment draft. --- docs/jts-311-incircle-lane-2026-08.md | 204 +++++++++ docs/jts-open-prs-scout-2026-08.md | 9 +- oracle/gen_jts311_incircle_history.py | 512 ++++++++++++++++++++++ oracle/jts311_incircle_history.txt | 51 +++ tests/Discussion839Mre/jts-311-comment.md | 25 ++ 5 files changed, 799 insertions(+), 2 deletions(-) create mode 100644 docs/jts-311-incircle-lane-2026-08.md create mode 100644 oracle/gen_jts311_incircle_history.py create mode 100644 oracle/jts311_incircle_history.txt create mode 100644 tests/Discussion839Mre/jts-311-comment.md diff --git a/docs/jts-311-incircle-lane-2026-08.md b/docs/jts-311-incircle-lane-2026-08.md new file mode 100644 index 00000000..f8a8c3ea --- /dev/null +++ b/docs/jts-311-incircle-lane-2026-08.md @@ -0,0 +1,204 @@ +# Mesh in-circle lane — JTS #311 design history (session 3) + +**Date**: 2026-08-05. +**topic:** `mesh` · epic **#68** +**Upstream**: [locationtech/jts#311](https://github.com/locationtech/jts/pull/311) + *isInCircleAdapt sketch Java port* (Komzpa / Darafei Praliaskouski) — + opened **2018-09-04**, tests refreshed **2026-05-25**. +**Product tip**: [locationtech/jts#1212](https://github.com/locationtech/jts/pull/1212) + (Stage A + `isInCircleDDNormalized` + `Vertex.isCCW` → `Orientation.index`). +**Full adaptive reference**: [locationtech/jts#1094](https://github.com/locationtech/jts/pull/1094). + +**Scope**: Design-history archive of the earliest open Shewchuk-style Stage A +sketch for `TrianglePredicate.isInCircleRobust`. Pure-Python Stage A gate vs +Rocq `INCIRCLE_SIGN` (`b64_inCircle`). No new Rocq theorems; no NTS port. + +**Verdict**: **GREEN (history)** — Stage A algebra is the right shape; +CERTAIN signs never disagree with the oracle on this table. The PR is +**superseded in product** by #1212 (and #1094 for full expansions). Keep as +lineage + one concrete constant lesson (`Math.ulp(1.0)` vs Shewchuk ε). + +--- + +## §1 — What #311 actually is (and is not) + +### Is + +1. **Stage A filter** on the Shewchuk in-circle determinant with coords + translated so `P` is the origin (same matrix as corpus `inCircle_R` / + `b64_inCircle`). +2. Error bound + `iccerrboundA = (10 + 96·ε)·ε` with **`ε = Math.ulp(1.0)`** (= \(2^{-52}\) + on binary64) — see §3. +3. Strict magnitude clear: + `det > errbound` → inside; `-det > errbound` → outside; else escalate. +4. Escalation to existing **`isInCircleDDFast`** (not full expansion arithmetic). +5. Wires `isInCircleRobust` → `isInCircleAdapt`. +6. Retargets `DelaunayTest.testCircle` expected MULTILINESTRING; adds + `TrianglePredicateTest` clear + large-coordinate cases (2026-05). + +### Is not + +- Despite the name **`isInCircleAdapt`**, this is **not** a port of Shewchuk’s + `incircleadapt` (expansion Stages B/C/D). That fuller port is **#1094**. +- Not a `Vertex.isCCW` / orientation fix (that arrives in **#1212**). +- Not the production merge tip for the mesh lane. + +**PR body (2018):** “Do the non-robust calculation and calculation of error +margin. If calculation is possibly not robust, fall back on slower math.” +References JTS #298; cites CMU `predicates.c`. + +**Maintainer reaction (dr-jts, 2018-09-04):** positive on the approach; +requested unit tests and `isInCircleDDFast` (faster equivalent of the then +fallback). Author invited a Java-familiar takeover for style/tests. Stalled +until the 2026-05 test commit — still open. + +--- + +## §2 — Lineage (product + corpus) + +``` +#311 (2018) Stage A sketch + DDFast + │ + ├─► #1094 (2024) Stage A + full incircleadapt expansions + │ (stronger exact path; no orient fix) + │ + └─► #1212 (2026) Stage A + isInCircleDDNormalized + Vertex.isCCW + ★ product tip for JTS / NTS port watch +``` + +| Axis | #311 | #1094 | #1212 (tip) | +|---|---|---|---| +| Stage A | Yes | Yes | Yes | +| ε source | `ulp(1.0)` = \(2^{-52}\) | `ulp(0.5)` = \(2^{-53}\) | `DOUBLE_EPS` = \(2^{-53}\) | +| Bound test | strict `>` | non-strict `>=` | strict `>` | +| Escalation | `isInCircleDDFast` | full adaptive expansions | `isInCircleDDNormalized` | +| Orient fix | No | No | Yes | +| Diff size | +92 / −4 (3 files) | ~+900 lines | +149 / −30 | +| Opened | 2018-09 | 2024-10 | 2026-07 | +| Corpus sessions | **3 (this)** | 2 | 1 | + +**Corpus formal counterpart of “go beyond Stage A”:** Stage D expansion / +filtered-exact orientation and in-circle work under `theories-flocq/` +(`B64_*`, `Orient_b64_exact*`, `InCircle_b64_exact.v`) — not a Java port of +#311, but the machine-checked reason the adaptive *idea* matters. + +--- + +## §3 — The ε lesson (design history that still pays rent) + +Shewchuk’s published Stage A constant uses machine epsilon +\(\varepsilon = 2^{-53}\) on binary64 (see `predicates.c` / +corpus `DOUBLE_EPS`). + +| Source | Expression | Value | +|---|---|---| +| Shewchuk / #1212 / #1094 / corpus | \(2^{-53}\) or `ulp(0.5)` | `1.1102230246251565e-16` | +| **#311** | `Math.ulp(1.0)` | **`2.220446049250313e-16`** (= \(2^{-52}\)) | + +Consequence for + +\[ +\texttt{iccerrboundA} = (10 + 96\,\varepsilon)\,\varepsilon +\] + +- Ratio \(\varepsilon_{311}/\varepsilon_{\mathrm{Shew}} = 2\). +- Bound coefficient ratio \(\approx 4\) (quadratic in ε dominates the small + \(96\varepsilon^2\) term; leading \(10\varepsilon\) alone already doubles). +- **Larger errbound → more conservative Stage A** (more UNCERTAIN → more DD + work). Direction is safe if escalation is correct; it is **not** the published + Shewchuk constant and is slightly wasteful vs #1212/#1094. + +Later PRs quietly fixed this to \(2^{-53}\). Archive that so nobody “restores” +`ulp(1.0)` as more faithful to the C reference. + +--- + +## §4 — Deliverables + +| Path | Role | +|---|---| +| `oracle/gen_jts311_incircle_history.py` | Stage A#311 + Shewchuk-ε comparator + oracle gate | +| `oracle/jts311_incircle_history.txt` | Vector table (regenerated by the script) | +| this doc | Design history + product call | + +```text +python oracle/gen_jts311_incircle_history.py +# or: +python oracle/gen_jts311_incircle_history.py --wsl-oracle /home/user/.../oracle_bin +``` + +Vectors: corpus pins (68-a/b, 1039, 1190) + #311 unit-test quads (clear ± +large-coord) + sample #1212 near-cocircular / GEOS955 / GEOS1040 sites. + +--- + +## §5 — Gate results (2026-08-05) + +| Metric | Value | +|---|---| +| Vectors | **22** | +| Oracle flip pin | **POS 1.5** ✓ | +| EXPECTED pin failures | **0** | +| Stage A#311 CERTAIN vs oracle sign conflicts | **0** | +| Stage A#311 UNCERTAIN | **7** (zeros, GEOS955, large-coord) | +| Stage A Shewchuk-ε UNCERTAIN | **7** (same set on this table) | +| ε-policy CERT diverge (311 vs \(2^{-53}\)) | **0** on this table | +| `ICCERRBOUND_A_311 / ICCERRBOUND_A_SHEW` | **≈ 2** (ε ratio 2; leading term \(10\varepsilon\)) | + +**Load-bearing uncertain case (shared with sessions 1–2):** + +```text +A = (18.68285714285716, 100.105) +B = (13.41, 104.82100000000001) +C = (13.41, 107.179) +P = (18.682857142857145, 111.89500000000001) +``` + +Stage A (either ε) declines / zero-classifies; oracle **POS**. Escalation +(DD or adapt) is load-bearing — the 2018 design insight of #311. + +### Finding — 2026 unit-test large-coord quad + +PR `testAdaptiveInCircleFallbackUsesDDComputation` uses ~\(10^{14}\) +coordinates and `assertTrue` on both `isInCircleDDFast` and +`isInCircleRobust`. Under IEEE binary64: + +| Probe | Result | +|---|---| +| Stage A det | **0.0** (UNCERTAIN — correct decline) | +| Rocq `b64_inCircle` / `INCIRCLE_SIGN` | **ZERO** | +| Translated deltas | multiples of \(2^{-5}\) after collapse of the decimal tails | + +So the **decimal literals do not encode a strict-inside configuration once +rounded to binary64**. Independent extracted kernel says not strictly inside. +If Java DDFast still returns `true` on these exact doubles, that is a +**fallback-path discrepancy** worth a maintainer look — not a Stage A failure. +This session does **not** re-run the JUnit assertion; it only records the +corpus side as **ZERO / open characterization** (not an EXPECTED POS pin). + +--- + +## §6 — Product / corpus call + +1. **Do not** dual-track an NTS port of #311. +2. **Tip remains #1212** (session 1 GREEN); **#1094** is full-adaptive + reference (session 2 GREEN). +3. **#311** is **design history**: first open JTS sketch of filter-then-escalate + for in-circle; ancestor of both later PRs; ε footnote for implementers. +4. Optional public comment: short “thanks / lineage / ε note / tip is #1212” + only if maintainers want corpus signal — lower priority than commenting + #1212 / #1094 with numbers. + +--- + +## §7 — Non-claims + +- No proof that Java `isInCircleDDFast` equals `b64_inCircle` bit-for-bit. +- No re-run of the full JTS Maven suite in this session. +- No claim that #311 should merge **instead of** #1212 or #1094. +- No new Rocq theorems; Stage D remains the formal expansion counterpart + elsewhere in the corpus. + +**AI assistance**: Grok (grok-4.5), human-directed. +**License**: project documentation (BSD-3-Clause corpus). diff --git a/docs/jts-open-prs-scout-2026-08.md b/docs/jts-open-prs-scout-2026-08.md index bec8b624..9e7a04db 100644 --- a/docs/jts-open-prs-scout-2026-08.md +++ b/docs/jts-open-prs-scout-2026-08.md @@ -59,7 +59,12 @@ Ordered by **risk÷cost** for the proofs corpus (not JTS merge politics). + scout FFI (`scout_incircle_probe` / `nts_rocq_in_circle`) + [`docs/jts-1094-incircle-lane-2026-08.md`](jts-1094-incircle-lane-2026-08.md). 27 vectors; FFI≡oracle_bin bits; CERTAIN vs FFI clean; review: tip stays **#1212**, - nits on `>=` bound / `Math.fma` / missing `Vertex.isCCW` fix. + nits on `>=` bound / `Math.fma` / missing `Vertex.isCCW` fix. + - **Session 3 GREEN (#311 design history):** + `oracle/gen_jts311_incircle_history.py` + `oracle/jts311_incircle_history.txt` + + [`docs/jts-311-incircle-lane-2026-08.md`](jts-311-incircle-lane-2026-08.md). + Stage A sketch + DDFast lineage; **ε = `ulp(1.0)` = \(2^{-52}\)** (looser than + Shewchuk \(2^{-53}\)); name is not full `incircleadapt` (#1094). Product tip stays **#1212**. 2. **Orientation lane (P0)** — Differential plan for #1093 (Ozaki) vs `b64_orient_sign_filtered` / exact escalation; keep #1197 green. 3. **PIP gallery on #1145 (P0/P1)** — Reuse `docs/nts-oracle-gallery.md` WKT as Java tests / differential. 4. **ScaledNoder #90 (P1)** — Scope whether scale=0/1 bug maps to a named snap claim. @@ -164,7 +169,7 @@ Columns: **Pri** = P0/P1/P2 · **Rel/Cost/Risk** · **Epic**. | Cluster | Members | Action | |---|---|---| -| **In-circle robustness** | #311 → #1094 → **#1212** | Treat **#1212 as tip**; archive others as predecessors once merged. FFI scout + review: [`jts-1094-incircle-lane-2026-08.md`](jts-1094-incircle-lane-2026-08.md) | +| **In-circle robustness** | #311 → #1094 → **#1212** | Treat **#1212 as tip**; archive others as predecessors once merged. History: [`jts-311-incircle-lane-2026-08.md`](jts-311-incircle-lane-2026-08.md). FFI scout + review: [`jts-1094-incircle-lane-2026-08.md`](jts-1094-incircle-lane-2026-08.md). Tip differential: [`jts-1212-incircle-lane-2026-08.md`](jts-1212-incircle-lane-2026-08.md) | | **Orientation filters** | #1093 (Ozaki production), #1197 (DD limits tests), #1189 (isCCW test INVALID) | Gate #1093 against corpus exact; keep #1197; mine #1189 for vectors only | | **DistanceOp / LineSegment** | #926, #930 | One review pass if either moves; low proof cost | | **CI matrix** | #638, #646 | Ignore unless JTS maintainers revive | diff --git a/oracle/gen_jts311_incircle_history.py b/oracle/gen_jts311_incircle_history.py new file mode 100644 index 00000000..a8a6b9a8 --- /dev/null +++ b/oracle/gen_jts311_incircle_history.py @@ -0,0 +1,512 @@ +#!/usr/bin/env python3 +""" +JTS #311 mesh in-circle lane — design-history Stage A gate (session 3). + +topic: mesh (epic #68) +Upstream: locationtech/jts#311 (isInCircleAdapt sketch Java port, Komzpa) + superseded in product by #1094 (full adaptive) / #1212 (tip: Stage A + DD). + +What this script is: + - Pure-Python mirror of PR #311 Stage A only (not DDFast, not full adapt). + - Reuses the #1212/#1094 vector bank + #311's own unit-test quads. + - Compares CERTAIN signs against Rocq INCIRCLE_SIGN when oracle_bin is available. + - Highlights the #311 ε choice: Math.ulp(1.0) == 2^-52 vs Shewchuk/corpus 2^-53. + +What this script is not: + - A claim that Java isInCircleDDFast equals b64_inCircle bit-for-bit. + - A reason to dual-track an NTS port of #311. + +Usage: + python oracle/gen_jts311_incircle_history.py + python oracle/gen_jts311_incircle_history.py --oracle /path/to/oracle_bin + python oracle/gen_jts311_incircle_history.py --wsl-oracle /home/user/.../oracle_bin + +Writes: + oracle/jts311_incircle_history.txt +""" +from __future__ import annotations + +import argparse +import math +import os +import struct +import subprocess +import sys +from dataclasses import dataclass +from typing import List, Optional, Sequence, Tuple + +# --------------------------------------------------------------------------- +# Constants +# --------------------------------------------------------------------------- +# Shewchuk / corpus / #1212 / #1094: eps = 2^-53 +SHEWCHUK_EPS = math.ldexp(1.0, -53) +ICCERRBOUND_A_SHEWCHUK = (10.0 + 96.0 * SHEWCHUK_EPS) * SHEWCHUK_EPS + +# PR #311: double epsilon = Math.ulp(1.0) → 2^-52 on binary64 +# (one binade larger than Shewchuk's published machine epsilon for Stage A). +PR311_EPS = math.ulp(1.0) # == 2^-52 +assert PR311_EPS == math.ldexp(1.0, -52) +ICCERRBOUND_A_311 = (10.0 + 96.0 * PR311_EPS) * PR311_EPS + +Point = Tuple[float, float] + + +@dataclass +class Vec: + name: str + a: Point + b: Point + c: Point + p: Point + expected: Optional[str] # POS | NEG | ZERO | None + note: str = "" + + +def stage_a( + a: Point, + b: Point, + c: Point, + p: Point, + iccerrbound_a: float, +) -> Tuple[str, float, bool, float]: + """Shewchuk in-circle Stage A (translated so P is origin). + + CERTAIN when |det| > errbound (strict), matching both #311 and #1212. + Returns (sign, det, certain, errbound). + """ + adx, ady = a[0] - p[0], a[1] - p[1] + bdx, bdy = b[0] - p[0], b[1] - p[1] + cdx, cdy = c[0] - p[0], c[1] - p[1] + + bdxcdy = bdx * cdy + cdxbdy = cdx * bdy + alift = adx * adx + ady * ady + + cdxady = cdx * ady + adxcdy = adx * cdy + blift = bdx * bdx + bdy * bdy + + adxbdy = adx * bdy + bdxady = bdx * ady + clift = cdx * cdx + cdy * cdy + + det = ( + alift * (bdxcdy - cdxbdy) + + blift * (cdxady - adxcdy) + + clift * (adxbdy - bdxady) + ) + permanent = ( + (abs(bdxcdy) + abs(cdxbdy)) * alift + + (abs(cdxady) + abs(adxcdy)) * blift + + (abs(adxbdy) + abs(bdxady)) * clift + ) + errbound = iccerrbound_a * permanent + # #311: if (det > errbound) true; if (-det > errbound) false; else DD + certain = det > errbound or -det > errbound + if det > 0: + sign = "POS" + elif det < 0: + sign = "NEG" + else: + sign = "ZERO" + return sign, det, certain, errbound + + +def stage_a_311(a: Point, b: Point, c: Point, p: Point) -> Tuple[str, float, bool, float]: + return stage_a(a, b, c, p, ICCERRBOUND_A_311) + + +def stage_a_shewchuk( + a: Point, b: Point, c: Point, p: Point +) -> Tuple[str, float, bool, float]: + return stage_a(a, b, c, p, ICCERRBOUND_A_SHEWCHUK) + + +def fmt_pt(q: Point) -> str: + return f"{q[0]:.17g} {q[1]:.17g}" + + +# --------------------------------------------------------------------------- +# Vectors: corpus pins + #1212 bank + #311 unit tests +# --------------------------------------------------------------------------- + + +def corpus_vectors() -> List[Vec]: + v: List[Vec] = [] + A, B, C = (0.0, 0.0), (4.0, 0.0), (0.0, 4.0) + for name, P in (("A", A), ("B", B), ("C", C)): + v.append( + Vec( + f"pin_1190_vertex_{name}", + A, + B, + C, + P, + "ZERO", + "DelaunayDegeneratePins / inCircle_R_at_vertex", + ) + ) + A, B, C, D = (0.0, 0.0), (2.0, 0.0), (2.0, 2.0), (0.0, 2.0) + v.append(Vec("pin_1039_diag_ABC_D", A, B, C, D, "ZERO", "cocircular_square_tie_1039")) + v.append(Vec("pin_1039_diag_ABD_C", A, B, D, C, "ZERO", "cocircular_square_tie_1039 mirror")) + v.append(Vec("pin_1039_knife_in", A, B, C, (0.0, 1.5), "POS", "knife +3")) + v.append(Vec("pin_1039_knife_out", A, B, C, (0.0, 2.5), "NEG", "knife -5")) + v.append( + Vec( + "pin_68b_flip_witness", + (0.0, 0.0), + (2.0, 0.0), + (1.0, 1.0), + (1.0, -0.5), + "POS", + "loc_in_circle_test_D; inCircle_R = 3/2", + ) + ) + v.append( + Vec( + "pin_68a_D_outside_ABC", + (0.0, 0.0), + (2.0, 0.0), + (1.0, 1.0), + (1.0, -2.0), + "NEG", + "DelaunayEdgeEmptyCircle outside disk", + ) + ) + return v + + +def jts311_unit_test_vectors() -> List[Vec]: + """Quads from TrianglePredicateTest added in the 2026-05 refresh of #311.""" + a, b, c = (0.0, 0.0), (10.0, 0.0), (0.0, 10.0) + v = [ + Vec( + "jts311_clear_inside", + a, + b, + c, + (1.0, 1.0), + "POS", + "TrianglePredicateTest.testAdaptiveInCircleClearCases inside", + ), + Vec( + "jts311_clear_outside", + a, + b, + c, + (20.0, 20.0), + "NEG", + "TrianglePredicateTest.testAdaptiveInCircleClearCases outside", + ), + Vec( + "jts311_large_coord_fallback", + (100000000000000.19, 100000000000000.53), + (100000000000000.19, 100000000000000.47), + (100000000000000.22, 100000000000000.38), + (100000000000000.40, 100000000000000.75), + # PR asserts isInCircleDDFast / robust true, but binary64 Stage A and + # b64_inCircle both classify ZERO after literal collapse at 1e14 — + # keep open (characterization), not EXPECTED POS. + None, + "TrianglePredicateTest large-magnitude fallback; PR expects true, " + "corpus oracle ZERO after b64 rounding (see jts-311 lane doc §5)", + ), + ] + return v + + +def jts1212_sample_vectors() -> List[Vec]: + """Subset of the #1212 adversarial bank (same float literals).""" + v: List[Vec] = [] + circle = [ + (42.0, 30.0), + (41.96, 29.61), + (41.85, 29.23), + (41.66, 28.89), + (41.41, 28.59), + (41.11, 28.34), + (40.77, 28.15), + (40.39, 28.04), + (40.0, 28.0), + (39.61, 28.04), + (39.23, 28.15), + (38.89, 28.34), + (38.59, 28.59), + (38.34, 28.89), + (38.15, 29.23), + (38.04, 29.61), + (38.0, 30.0), + (38.04, 30.39), + (38.15, 30.77), + (38.34, 31.11), + (38.59, 31.41), + (38.89, 31.66), + (39.23, 31.85), + (39.61, 31.96), + (40.0, 32.0), + (40.39, 31.96), + (40.77, 31.85), + (41.11, 31.66), + (41.41, 31.41), + (41.66, 31.11), + (41.85, 30.77), + (41.96, 30.39), + ] + for i in range(0, len(circle) - 3, 4): + aa, bb, cc, pp = circle[i], circle[i + 1], circle[i + 2], circle[i + 3] + v.append( + Vec( + f"jts1212_circle_quad_{i}", + aa, + bb, + cc, + pp, + None, + "DelaunayTest.testCircle near-cocircular sample (also #311 retarget)", + ) + ) + geos955_sub = [ + (18.68285714285716, 100.105), + (13.41, 104.82100000000001), + (13.41, 107.179), + (18.682857142857145, 111.89500000000001), + ] + v.append( + Vec( + "jts1212_geos955_subset", + geos955_sub[0], + geos955_sub[1], + geos955_sub[2], + geos955_sub[3], + None, + "GEOS955 / JTS#1171 — Stage A must decline; DD or adapt required", + ) + ) + geos1040 = [ + (6.6584, 53.583000000000006), + (6.6576, 53.583600000000004), + (6.657, 53.5848), + (6.6572000000000005, 53.5842), + ] + v.append( + Vec( + "jts1212_geos1040_quad", + geos1040[0], + geos1040[1], + geos1040[2], + geos1040[3], + None, + "GEOS#1040 / JTS#1171 near-cocircular", + ) + ) + return v + + +def all_vectors() -> List[Vec]: + return corpus_vectors() + jts311_unit_test_vectors() + jts1212_sample_vectors() + + +# --------------------------------------------------------------------------- +# Oracle driver (same wire format as other scouts) +# --------------------------------------------------------------------------- + + +def resolve_oracle_cmd(args: argparse.Namespace) -> List[str]: + """Same resolution policy as gen_jts1212_incircle_vectors.py.""" + if args.oracle: + return [args.oracle] + if args.wsl_oracle: + return ["wsl.exe", "-e", args.wsl_oracle] + env = os.environ.get("ORACLE_BIN") + if env and os.path.isfile(env): + return [env] + local = os.path.join(os.path.dirname(__file__), "oracle_bin") + if os.path.isfile(local): + return [local] + wsl = os.environ.get( + "WSL_ORACLE_BIN", "/home/user/nettopologysuite.proofs/oracle/oracle_bin" + ) + return ["wsl.exe", "-e", wsl] + + +def run_oracle( + oracle_cmd: Sequence[str], a: Point, b: Point, c: Point, p: Point +) -> Tuple[str, float]: + """Call INCIRCLE_SIGN via stdin (same wire format as #1212 generator).""" + payload = ( + "INCIRCLE_SIGN\n" + f"{a[0]} {a[1]}\n" + f"{b[0]} {b[1]}\n" + f"{c[0]} {c[1]}\n" + f"{p[0]} {p[1]}\n" + ) + proc = subprocess.run( + list(oracle_cmd), + input=payload, + capture_output=True, + text=True, + timeout=30, + check=False, + ) + if proc.returncode != 0: + raise RuntimeError( + f"oracle exit {proc.returncode}: {proc.stderr.strip()} {proc.stdout.strip()}" + ) + parts = proc.stdout.strip().split() + if len(parts) < 2: + raise RuntimeError(f"bad oracle output: {proc.stdout!r}") + sign = parts[0] + tok = parts[1] + val = ( + float.fromhex(tok) + if tok.lower().startswith(("0x", "-0x", "+0x")) + else float(tok) + ) + return sign, val + + +def main() -> int: + ap = argparse.ArgumentParser(description=__doc__) + ap.add_argument("--oracle", default=None, help="Path to oracle_bin") + ap.add_argument("--wsl-oracle", default=None, help="WSL path to oracle_bin") + ap.add_argument( + "--out", + default=os.path.join(os.path.dirname(__file__), "jts311_incircle_history.txt"), + help="Output table path", + ) + args = ap.parse_args() + + vectors = all_vectors() + oracle_cmd = resolve_oracle_cmd(args) + + # Sanity pin (same as other mesh scouts) + try: + pin_s, pin_val = run_oracle( + oracle_cmd, (0.0, 0.0), (2.0, 0.0), (1.0, 1.0), (1.0, -0.5) + ) + except Exception as e: + print(f"FATAL: oracle unavailable ({oracle_cmd}): {e}", file=sys.stderr) + return 2 + if pin_s != "POS" or abs(pin_val - 1.5) > 1e-12: + print( + f"FATAL: oracle pin failed: {pin_s} {pin_val} (expected POS 1.5)", + file=sys.stderr, + ) + return 2 + print(f"Oracle pin OK: {pin_s} {pin_val} via {oracle_cmd}") + + lines: List[str] = [] + lines.append("# JTS #311 isInCircleAdapt — Stage A design-history gate") + lines.append("# topic: mesh epic: #68") + lines.append(f"# PR311_EPS = ulp(1.0) = {PR311_EPS!r} (2^-52)") + lines.append(f"# SHEWCHUK_EPS = {SHEWCHUK_EPS!r} (2^-53)") + lines.append( + f"# ICCERRBOUND_A_311 / ICCERRBOUND_A_SHEW ≈ " + f"{ICCERRBOUND_A_311 / ICCERRBOUND_A_SHEWCHUK:.6g}" + ) + lines.append( + "# Columns: NAME | ORACLE | A311_SIGN | A311_CERT | A53_CERT | DET | ERR311 | NOTE" + ) + lines.append("#") + + n_expected_fail = 0 + n_certain_conflict = 0 + n_a311_uncertain = 0 + n_a53_uncertain = 0 + n_eps_diverge = 0 + n_pass = 0 + failures: List[str] = [] + divergences: List[str] = [] + + for vec in vectors: + a311_sign, det, a311_cert, err311 = stage_a_311(vec.a, vec.b, vec.c, vec.p) + _, _, a53_cert, _ = stage_a_shewchuk(vec.a, vec.b, vec.c, vec.p) + + if not a311_cert: + n_a311_uncertain += 1 + if not a53_cert: + n_a53_uncertain += 1 + if a311_cert != a53_cert: + n_eps_diverge += 1 + divergences.append( + f" {vec.name}: A311={'CERT' if a311_cert else 'UNC'} " + f"A53={'CERT' if a53_cert else 'UNC'} det={det:.6g} err311={err311:.6g}" + ) + + try: + oracle_s, oracle_val = run_oracle( + oracle_cmd, vec.a, vec.b, vec.c, vec.p + ) + except RuntimeError as e: + failures.append(f"{vec.name}: oracle error {e}") + oracle_s, oracle_val = "ERR", float("nan") + + if vec.expected is not None and oracle_s in ("POS", "NEG", "ZERO"): + if oracle_s != vec.expected: + if vec.expected == "ZERO" and abs(oracle_val) < 1e-9: + pass # soft-zero + else: + n_expected_fail += 1 + failures.append( + f"{vec.name}: EXPECTED {vec.expected} oracle " + f"{oracle_s} ({oracle_val})" + ) + + if a311_cert and oracle_s in ("POS", "NEG", "ZERO"): + if {a311_sign, oracle_s} <= {"POS", "NEG"} and a311_sign != oracle_s: + n_certain_conflict += 1 + failures.append( + f"{vec.name}: A311 CERTAIN {a311_sign} vs oracle {oracle_s}" + ) + else: + n_pass += 1 + elif not a311_cert: + n_pass += 1 # UNCERTAIN is OK for Stage A + + lines.append( + f"{vec.name}\t" + f"ORACLE={oracle_s}\t" + f"A311={a311_sign}/{'CERT' if a311_cert else 'UNC'}\t" + f"A53={'CERT' if a53_cert else 'UNC'}\t" + f"det={det:.17g}\t" + f"err311={err311:.17g}\t" + f"# {vec.note}" + ) + lines.append( + f" A=({fmt_pt(vec.a)}) B=({fmt_pt(vec.b)}) " + f"C=({fmt_pt(vec.c)}) P=({fmt_pt(vec.p)})" + ) + + out_path = args.out + with open(out_path, "w", encoding="utf-8") as f: + f.write("\n".join(lines) + "\n") + + print(f"Vectors: {len(vectors)}") + print(f"oracle: {oracle_cmd}") + print(f"PR311_EPS / SHEWCHUK_EPS = {PR311_EPS / SHEWCHUK_EPS:.0f}x") + print( + f"ICCERRBOUND_A_311 / ICCERRBOUND_A_SHEW ≈ " + f"{ICCERRBOUND_A_311 / ICCERRBOUND_A_SHEWCHUK:.6g}" + ) + print(f"EXPECTED pin failures: {n_expected_fail}") + print(f"Stage A#311 CERTAIN vs oracle conflicts: {n_certain_conflict}") + print(f"Stage A#311 UNCERTAIN: {n_a311_uncertain}") + print(f"Stage A Shewchuk-ε UNCERTAIN: {n_a53_uncertain}") + print(f"ε-policy CERT diverge (311 vs 2^-53): {n_eps_diverge}") + print(f"CERTAIN/uncertain handled: {n_pass}") + print(f"Wrote: {out_path}") + if divergences: + print("ε divergences:") + for d in divergences: + print(d) + if failures: + print("FAILURES:") + for x in failures: + print(" ", x) + return 1 + print("GATE: GREEN") + return 0 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/oracle/jts311_incircle_history.txt b/oracle/jts311_incircle_history.txt new file mode 100644 index 00000000..afa0686c --- /dev/null +++ b/oracle/jts311_incircle_history.txt @@ -0,0 +1,51 @@ +# JTS #311 isInCircleAdapt — Stage A design-history gate +# topic: mesh epic: #68 +# PR311_EPS = ulp(1.0) = 2.220446049250313e-16 (2^-52) +# SHEWCHUK_EPS = 1.1102230246251565e-16 (2^-53) +# ICCERRBOUND_A_311 / ICCERRBOUND_A_SHEW ≈ 2 +# Columns: NAME | ORACLE | A311_SIGN | A311_CERT | A53_CERT | DET | ERR311 | NOTE +# +pin_1190_vertex_A ORACLE=ZERO A311=ZERO/UNC A53=UNC det=0 err311=0 # DelaunayDegeneratePins / inCircle_R_at_vertex + A=(0 0) B=(4 0) C=(0 4) P=(0 0) +pin_1190_vertex_B ORACLE=ZERO A311=ZERO/UNC A53=UNC det=0 err311=0 # DelaunayDegeneratePins / inCircle_R_at_vertex + A=(0 0) B=(4 0) C=(0 4) P=(4 0) +pin_1190_vertex_C ORACLE=ZERO A311=ZERO/UNC A53=UNC det=0 err311=0 # DelaunayDegeneratePins / inCircle_R_at_vertex + A=(0 0) B=(4 0) C=(0 4) P=(0 4) +pin_1039_diag_ABC_D ORACLE=ZERO A311=ZERO/UNC A53=UNC det=0 err311=1.4210854715202034e-13 # cocircular_square_tie_1039 + A=(0 0) B=(2 0) C=(2 2) P=(0 2) +pin_1039_diag_ABD_C ORACLE=ZERO A311=ZERO/UNC A53=UNC det=0 err311=1.4210854715202034e-13 # cocircular_square_tie_1039 mirror + A=(0 0) B=(2 0) C=(0 2) P=(2 2) +pin_1039_knife_in ORACLE=POS A311=POS/CERT A53=CERT det=3 err311=8.9928064994637869e-14 # knife +3 + A=(0 0) B=(2 0) C=(2 2) P=(0 1.5) +pin_1039_knife_out ORACLE=NEG A311=NEG/CERT A53=CERT det=-5 err311=2.4424906541753494e-13 # knife -5 + A=(0 0) B=(2 0) C=(2 2) P=(0 2.5) +pin_68b_flip_witness ORACLE=POS A311=POS/CERT A53=CERT det=1.5 err311=1.3322676295501907e-14 # loc_in_circle_test_D; inCircle_R = 3/2 + A=(0 0) B=(2 0) C=(1 1) P=(1 -0.5) +pin_68a_D_outside_ABC ORACLE=NEG A311=NEG/CERT A53=CERT det=-6 err311=1.4654943925052097e-13 # DelaunayEdgeEmptyCircle outside disk + A=(0 0) B=(2 0) C=(1 1) P=(1 -2) +jts311_clear_inside ORACLE=POS A311=POS/CERT A53=CERT det=1800 err311=4.0056846728475737e-12 # TrianglePredicateTest.testAdaptiveInCircleClearCases inside + A=(0 0) B=(10 0) C=(0 10) P=(1 1) +jts311_clear_outside ORACLE=NEG A311=NEG/CERT A53=CERT det=-40000 err311=2.2204460492503176e-09 # TrianglePredicateTest.testAdaptiveInCircleClearCases outside + A=(0 0) B=(10 0) C=(0 10) P=(20 20) +jts311_large_coord_fallback ORACLE=ZERO A311=ZERO/UNC A53=UNC det=0 err311=1.0601464367834845e-16 # TrianglePredicateTest large-magnitude fallback; PR expects true, corpus oracle ZERO after b64 rounding (see jts-311 lane doc §5) + A=(100000000000000.19 100000000000000.53) B=(100000000000000.19 100000000000000.47) C=(100000000000000.22 100000000000000.38) P=(100000000000000.41 100000000000000.75) +jts1212_circle_quad_0 ORACLE=NEG A311=NEG/CERT A53=CERT det=-0.0022993800000004373 err311=1.3503101303769282e-15 # DelaunayTest.testCircle near-cocircular sample (also #311 retarget) + A=(42 30) B=(41.960000000000001 29.609999999999999) C=(41.850000000000001 29.23) P=(41.659999999999997 28.890000000000001) +jts1212_circle_quad_4 ORACLE=NEG A311=NEG/CERT A53=CERT det=-0.0019248000000005351 err311=1.2539510763076614e-15 # DelaunayTest.testCircle near-cocircular sample (also #311 retarget) + A=(41.409999999999997 28.59) B=(41.109999999999999 28.34) C=(40.770000000000003 28.149999999999999) P=(40.390000000000001 28.039999999999999) +jts1212_circle_quad_8 ORACLE=NEG A311=NEG/CERT A53=CERT det=-0.0022993800000005692 err311=1.3503101303768955e-15 # DelaunayTest.testCircle near-cocircular sample (also #311 retarget) + A=(40 28) B=(39.609999999999999 28.039999999999999) C=(39.229999999999997 28.149999999999999) P=(38.890000000000001 28.34) +jts1212_circle_quad_12 ORACLE=NEG A311=NEG/CERT A53=CERT det=-0.001924800000001144 err311=1.2539510763076665e-15 # DelaunayTest.testCircle near-cocircular sample (also #311 retarget) + A=(38.590000000000003 28.59) B=(38.340000000000003 28.890000000000001) C=(38.149999999999999 29.23) P=(38.039999999999999 29.609999999999999) +jts1212_circle_quad_16 ORACLE=NEG A311=NEG/CERT A53=CERT det=-0.0022993800000004373 err311=1.3503101303769282e-15 # DelaunayTest.testCircle near-cocircular sample (also #311 retarget) + A=(38 30) B=(38.039999999999999 30.390000000000001) C=(38.149999999999999 30.77) P=(38.340000000000003 31.109999999999999) +jts1212_circle_quad_20 ORACLE=NEG A311=NEG/CERT A53=CERT det=-0.0019248000000005351 err311=1.2539510763076614e-15 # DelaunayTest.testCircle near-cocircular sample (also #311 retarget) + A=(38.590000000000003 31.41) B=(38.890000000000001 31.66) C=(39.229999999999997 31.850000000000001) P=(39.609999999999999 31.960000000000001) +jts1212_circle_quad_24 ORACLE=NEG A311=NEG/CERT A53=CERT det=-0.0022993800000005692 err311=1.3503101303768955e-15 # DelaunayTest.testCircle near-cocircular sample (also #311 retarget) + A=(40 32) B=(40.390000000000001 31.960000000000001) C=(40.770000000000003 31.850000000000001) P=(41.109999999999999 31.66) +jts1212_circle_quad_28 ORACLE=NEG A311=NEG/CERT A53=CERT det=-0.001924800000001144 err311=1.2539510763076665e-15 # DelaunayTest.testCircle near-cocircular sample (also #311 retarget) + A=(41.409999999999997 31.41) B=(41.659999999999997 31.109999999999999) C=(41.850000000000001 30.77) P=(41.960000000000001 30.390000000000001) +jts1212_geos955_subset ORACLE=POS A311=ZERO/UNC A53=UNC det=0 err311=3.6841392970041058e-11 # GEOS955 / JTS#1171 — Stage A must decline; DD or adapt required + A=(18.682857142857159 100.105) B=(13.41 104.82100000000001) C=(13.41 107.179) P=(18.682857142857145 111.89500000000001) +jts1212_geos1040_quad ORACLE=NEG A311=NEG/CERT A53=CERT det=-1.4936607923816726e-25 err311=4.4764192352667416e-27 # GEOS#1040 / JTS#1171 near-cocircular + A=(6.6584000000000003 53.583000000000006) B=(6.6576000000000004 53.583600000000004) C=(6.657 53.584800000000001) P=(6.6572000000000005 53.584200000000003) diff --git a/tests/Discussion839Mre/jts-311-comment.md b/tests/Discussion839Mre/jts-311-comment.md new file mode 100644 index 00000000..8410e813 --- /dev/null +++ b/tests/Discussion839Mre/jts-311-comment.md @@ -0,0 +1,25 @@ +Thanks for keeping this open — design-history note from the NetTopologySuite.Proofs mesh / Delaunay lane (we treated **#311 → #1094 → #1212** as one product lineage; tip for merge discussion is **#1212**). + +### What this PR established (2018) +Stage A Shewchuk in-circle filter (coords translated so `P` is origin) with permanent-scaled `iccerrboundA`, then escalate when uncertain. That filter-then-escalate shape is exactly what #1212 and #1094 still use. Maintainer notes from 2018 (`isInCircleDDFast`, unit tests) aged well. + +### Numbers (Stage A only vs extracted `b64_inCircle`) +Write-up: [jts-311-incircle-lane](https://github.com/grootstebozewolf/NetTopologySuite.Proofs/blob/main/docs/jts-311-incircle-lane-2026-08.md) (`oracle/jts311_incircle_history.txt`, 22 vectors). + +| Check | Result | +|---|---| +| Oracle flip pin | **POS 1.5** | +| Stage A#311 **CERTAIN** vs oracle sign conflicts | **0** | +| Stage A#311 **UNCERTAIN** | **7** (correct declines) | + +GEOS955 / JTS#1171 subset still shows why escalation exists: Stage A **ZERO/UNCERTAIN**, oracle **POS**. + +### Two archive notes (not merge blockers for a history PR) +1. **Name vs body:** `isInCircleAdapt` here is Stage A + **DDFast**, not Shewchuk’s full `incircleadapt` expansion stages (that fuller port is #1094). +2. **ε:** this PR uses `Math.ulp(1.0)` (= \(2^{-52}\)); Shewchuk / #1212 / #1094 use \(2^{-53}\). Bound is ~2× looser (more DD). Direction is safe; later PRs align with the published constant. +3. **2026 large-coord unit test:** after binary64 rounding of the \(10^{14}\) literals, Stage A det and the Rocq in-circle kernel both say **ZERO** (not strictly inside). If `isInCircleDDFast` still returns `true` on those doubles, that is a useful DD-path check against an independent kernel — happy to dig further if useful. + +### Bottom line +Valuable as the **first open sketch** of robust in-circle Stage A in JTS. For production merge we point at **#1212** (Stage A + DDNormalized + `Vertex.isCCW` → `Orientation.index`); corpus gates for the tip are already green. + +*(Affiliation: [NetTopologySuite.Proofs](https://github.com/grootstebozewolf/NetTopologySuite.Proofs) — formal mesh/predicate companion, not a JTS committer review.)*