Skip to content

docs: JTS #1094 in-circle FFI scout + corpus code review #445

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
grootstebozewolf merged 1 commit into from
Aug 5, 2026
Merged

docs: JTS #1094 in-circle FFI scout + corpus code review #445

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
250 changes: 250 additions & 0 deletions docs/jts-1094-incircle-lane-2026-08.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,250 @@
# Mesh in-circle lane — JTS #1094 FFI scout + corpus code review

**Date**: 2026-08-05.
**topic:** `mesh` · epic **#68**
**Upstream**: [locationtech/jts#1094](https://github.com/locationtech/jts/pull/1094)
*Make isInCircleRobust robust* (tinko92, 2024-10-29) — full Shewchuk adaptive
port of `incircle` / `incircleadapt` into `TrianglePredicate`.
**Sibling tip**: [locationtech/jts#1212](https://github.com/locationtech/jts/pull/1212)
(Stage A + existing `isInCircleDDNormalized` + `Vertex.isCCW` → `Orientation.index`).
**Lane policy**: **one product lane** — prefer **#1212 as current tip**; #1094 is
design history + stronger exact-arithmetic reference. Same corpus gate.

**Scope**: FFI-backed differential scout of Stage A vs Rocq `b64_inCircle`
(`nts_rocq_in_circle`); high-quality code review of the PR against the mesh
corpus. No new Rocq theorems.

**Verdict**: **GREEN (scout)** + **review: approve-with-nits, do not dual-track**.
All EXPECTED pins match FFI; Stage A CERTAIN never disagrees with FFI on
nonzero signs; FFI ≡ `oracle_bin` bit-for-bit on the table. Implementation is
a serious Shewchuk port, but **#1212 remains the merge tip** for maintainability
and broader mesh regression coverage.

---

## §1 — What #1094 changes

`TrianglePredicate.isInCircleRobust` (was non-robust `isInCircleNormalized`):

1. **Stage A** — Shewchuk in-circle determinant in double, coords translated so
`P` is the origin (same matrix as corpus `inCircle_R` / `b64_inCircle`).
2. Error bound
`iccerrboundA = (10 + 96·ε)·ε`, `ε = Math.ulp(0.5)` (= \(2^{-53}\) on binary64),
scaled by the matrix permanent.
3. If `|det| >= errbound`, return `det > 0` (**non-strict** comparison).
4. Else call **`incircleadapt`** — full expansion-arithmetic adaptive stages
B/C/D ported from Shewchuk `predicates.c` (~900 lines of private helpers:
`Two_Sum` / `Two_Product` / `scale_expansion_zeroelim` / …).

**Also**: retargets `DelaunayTest.testCircle` expected MULTILINESTRING under the
assumption that Shewchuk’s robust predicate is ground truth (one test change).

**Does not**: touch `Vertex.isCCW` (still non-robust cross product in master;
#1212 does fix that).

Claims (PR body): addresses JTS #310; more thoroughly achieves the motivation of
PR #311.

---

## §2 — FFI ground truth (corpus)

| Asset | Role |
|---|---|
| `b64_inCircle` / `INCIRCLE_SIGN` | Extracted binary64 evaluator |
| `nts_rocq_in_circle` | Phase 5 C ABI (`oracle/nts_ffi.h`) — **same symbol** |
| `oracle/scout_incircle_probe` | Scout-only FFI driver (in-circle surface only) |
| `ArcOrient.inCircle_R` | Exact-reals Shewchuk determinant (Qed algebra) |
| `DelaunayDegeneratePins` (68-c) | Vertex ZERO + cocircular square ZERO + knife ± |
| `DelaunayLocallyDelaunay` (68-b) | Flip witness POS \(3/2\) |
| `DelaunayEdgeEmptyCircle` (68-a) | Outside-disk NEG witness |
| `InCircle_b64_exact.v` | Full-plane sign soundness of `b64_inCircle` |

Sign convention (aligned with JTS “inside iff true” under CCW triangle):

> `POS` ⇔ `(A,B,C)` CCW and `P` strictly inside the circumcircle.
> Boolean `isInCircleRobust` ⇔ `det > 0` (strict).

---

## §3 — Deliverables

| Path | Purpose |
|---|---|
| `oracle/scout_incircle_ffi.ml` | Minimal Callback registration for `b64_inCircle` |
| `oracle/scout_incircle_stubs.c` | `nts_rocq_init` + `nts_rocq_in_circle` |
| `oracle/scout_incircle_probe.c` | `ffi_probe`-style INCIRCLE_SIGN driver |
| `oracle/gen_jts1094_incircle_scout.py` | Generator + Stage A#1094 mirror + FFI/oracle parity |
| `oracle/jts1094_incircle_vectors.txt` | 27-vector table (regenerated by the script) |
| `oracle/Makefile` targets | `scout-incircle-ffi`, `jts1094-scout` |

```text
make -C oracle scout-incircle-ffi
# from repo root (Linux or WSL):
python3 oracle/gen_jts1094_incircle_scout.py \
--oracle oracle/oracle_bin \
--ffi-probe oracle/scout_incircle_probe
```

Windows host with WSL oracle binary:

```text
python oracle/gen_jts1094_incircle_scout.py \
--wsl-oracle /home/user/nettopologysuite.proofs/oracle/oracle_bin \
--wsl-ffi-probe /mnt/c/.../oracle/scout_incircle_probe
```

Why a scout library instead of full `libntsrocq`: workspace `extracted.ml` is
stale vs full `nts_ffi.ml` (missing e.g. `b64_orient2d_exact`). The scout
registers **only** the in-circle entry — still the production extracted
symbol, still the production C calling convention for that entry.

---

## §4 — Gate results (2026-08-05)

| Metric | Value |
|---|---|
| Vectors | **27** |
| FFI pin (flip witness) | **POS 1.5** ✓ |
| FFI ≡ `oracle_bin` bit parity | **0 failures** |
| EXPECTED pin failures | **0** |
| Stage A#1094 CERTAIN vs FFI sign conflicts | **0** |
| Stage A#1094 UNCERTAIN | **4** (correct declines; adaptive path required) |
| Bound-policy diverge vs #1212 (`>=` vs `>`) | **6** (all vertex-on-triangle with `permanent = 0`) |

### Pin class (EXPECTED set)

| Class | FFI | Stage A#1094 | Stage A#1212 |
|---|---|---|---|
| Vertex-on-circle (pin_1190 / jts1190) | ZERO | **CERTAIN** ZERO | UNCERTAIN |
| Cocircular square diagonals (1039) | ZERO | UNCERTAIN | UNCERTAIN |
| Knife in / out | POS / NEG | CERTAIN match | CERTAIN match |
| Flip witness 68-b | POS | CERTAIN match | CERTAIN match |
| Outside ABC 68-a | NEG | CERTAIN match | CERTAIN match |
| Scaled flip | POS | CERTAIN match | CERTAIN match |

**Reading vertex CERTAIN under #1094:** when the query is a triangle vertex,
translation yields `permanent = 0` and `det = 0`, so `|det| >= errbound` holds
as `0 >= 0`. The PR returns `det > 0` → **false** (not strictly inside) without
calling adaptive code. #1212’s **strict** `>` leaves this UNCERTAIN and falls
through to DD — same boolean, extra work. **No soundness conflict with FFI.**

**GEOS955 subset:** Stage A det = 0 · UNCERTAIN; FFI **POS**. Adaptive (or DD
in #1212) **must** run; Stage A alone would treat zero as outside.

### Open regression sites (oracle-signed, no Qed EXPECTED)

| Vector | FFI | Stage A#1094 | Note |
|---|---|---|---|
| `jts1094_circle_quad_*` | NEG | CERTAIN | Densified near-circle quads |
| `jts1094_circle_cardinal` | ZERO | UNCERTAIN | Near-cocircular cardinals |
| `jts_geos1040_quad` | NEG | CERTAIN | Near-cocircular GEOS#1040 |
| **`jts_geos955_subset`** | **POS** | **ZERO · UNCERTAIN** | Adaptive path load-bearing |
| unit-circle ε nudges | POS | CERTAIN | 1e-12 … 1e-6 |

---

## §5 — High-quality code review (corpus-backed)

Review stance: **proofs-corpus differential review**, not a JTS maintainer merge
vote. Findings ranked by severity for mesh legality / soundness.

### Strengths

1. **Correct Stage A algebra** — permanent-scaled `iccerrboundA` matches the
Shewchuk / corpus Stage A discipline used by #1212 and by
`oracle/gen_jts1212_incircle_vectors.py`. CERTAIN nonzero signs never
conflicted with FFI on this table.
2. **Escalation is real** — unlike pre-PR `isInCircleNormalized`, uncertain
cases go to adaptive expansions. GEOS955 proves Stage A is insufficient
alone; this PR structure addresses that class.
3. **Literal port of public-domain `predicates.c`** — intentional closeness
aids debugging against the C reference (author’s stated goal). Private
methods do not pollute the public JTS API.
4. **Boolean contract** remains “strictly inside” (`det > 0`), consistent with
corpus `0 < inCircle_R` flip guards and `DelaunayDegeneratePins` (vertices /
cocircular ties are **not** strict violations).

### Findings

| ID | Sev | Finding | Corpus / evidence |
|---|---|---|---|
| **F1** | **Medium** | **Bound comparison is non-strict (`>=`)** while #1212 and common Shewchuk Stage A snippets use **strict** magnitude clear. | 6/27 vectors: vertex cases CERTAIN under #1094, UNCERTAIN under #1212. Boolean still agrees (ZERO → false). Prefer documenting intentional `>=` or aligning with Shewchuk’s published Stage A form; on `|det| == errbound` with nonzero det, non-strict returns without adaptive — rare but is the **only** CERTAIN path that Shewchuk’s analysis does not justify as “strictly larger than the error bound”. |
| **F2** | **Medium** | **`Two_Product` uses `Math.fma`** | Requires a Java runtime where `Math.fma` is a true fused multiply-add (or correctly rounded substitute). On platforms that emulate FMA poorly, expansion error-free transforms break silently. Corpus does not run the Java port; flag for CI matrix (x86-64 + aarch64, latest LTS JDKs). Shewchuk C uses splitter-based Two_Product without hardware FMA. |
| **F3** | **Medium** | **No `Vertex.isCCW` fix** | Mesh legality is the product of **in-circle × orientation**. #1212 pairs in-circle Stage A with robust `Orientation.index`. #1094 leaves non-robust CCW in `Vertex` — known failure mode for near-collinear sites (JTS #20 cluster). Corpus lane treats both predicates as mesh-critical. |
| **F4** | **Low–Med** | **`testCircle` expected-edge retarget** | Near-cocircular DTs are **non-unique**; changing expected MULTILINESTRING under “Shewchuk is GT” is reasonable for a golden test but **does not prove** local Delaunay legality of every edge. Corpus recommendation: assert empty-circle on **internal edges** (as `tests/Discussion839Mre` does with FFI), not only edge-set equality. |
| **F5** | **Low** | **~900 lines of private expansion code, zero reviews** | Author notes “borderline unreviewable”. Array-returning error-free transforms (Java lacks macros/refs) allocate on the uncertain path. Acceptable if Stage A catches almost all calls; still a **maintenance and audit** cost vs #1212’s reuse of existing DD. |
| **F6** | **Low** | **Stale / unused DD helpers remain** | Class still carries `isInCircleDD*` / check helpers; robust path no longer uses DD. Not wrong, but #1212’s “filter then DD” reuses battle-tested JTS arithmetic instead of a second exact stack. |
| **F7** | **Info** | **Permanent recomputed only at Stage A** | Adaptive receives `permanent` from Stage A (Shewchuk pattern). Correct if Stage A permanent is the right scale; do not recompute with different rounding without care. |
| **F8** | **Info** | **No NaN / non-finite policy** | Corpus `b64_inCircle` is total on NaNs in the IEEE sense; production JTS typically assumes finite coordinates. Document “finite inputs only” if not already a triangulation invariant. |

### Non-findings (checked, not issues)

- **Sign convention** matches Shewchuk / `inCircle_R` / FFI (CCW + inside → positive).
- **ε source**: `Math.ulp(0.5)` equals `0x1.0p-53` on binary64 — matches #1212 `DOUBLE_EPS`.
- **Cocircular square (1039)** correctly UNCERTAIN at Stage A; adaptive must return 0 / non-positive strict-inside — consistent with Qed `cocircular_square_tie_1039`.
- **No CERTAIN wrong-sign** vs FFI on this adversarial + pin set.

### Comparison table vs #1212 (product)

| Axis | #1094 | #1212 (tip) |
|---|---|---|
| Stage A | Yes (`>=`) | Yes (strict `>`) |
| Escalation | Full adaptive expansions | Existing `isInCircleDDNormalized` |
| Orient fix | No | Yes (`Orientation.index`) |
| Diff size | +913 / −5 (2 files) | +149 / −30 (5 files) |
| Tests | Retargets `testCircle` | ConformingDelaunay + Delaunay + Voronoi |
| CI / activity | 2024-10, no review comments | 2026-07, CI green, updated 2026-08 |
| Corpus gate cost | Same Stage A table | Same (already GREEN session 1) |
| Formal completeness | Closer to Shewchuk thesis path | Relies on DD soundness (unproven vs Rocq) |

**Corpus product call:** keep **#1212 as tip**. #1094 remains the reference for
“what full adaptive looks like in JTS Java” and a design archive for Stage D
expansion work in the proofs repo. Do **not** maintain two NTS ports.

---

## §6 — Review summary (for optional JTS comment)

Numbers-only bullets suitable for a PR comment (if maintainers want corpus
signal):

1. Stage A mirror vs Rocq FFI `nts_rocq_in_circle` (`b64_inCircle`): **27**
vectors; **0** CERTAIN sign conflicts; **0** EXPECTED pin failures.
2. FFI ≡ `oracle_bin` **bit-identical** on the table (marshalling check).
3. Load-bearing uncertain case: GEOS955 subset — Stage A **ZERO/UNCERTAIN**,
FFI **POS** → adaptive path required (double Stage A alone is wrong).
4. Vertex pins: with `permanent = 0`, `|det| >= 0` makes Stage A CERTAIN ZERO
(returns false without adapt); #1212 uses strict `>` and declines — same
boolean.
5. Caveats for merge evaluation: `Math.fma` portability; no `Vertex.isCCW`
fix; prefer edge-wise empty-circle assertions over sole MULTILINESTRING
golden diffs on near-cocircular inputs.

*(Affiliation: NetTopologySuite.Proofs — formal mesh/predicate companion, not a
JTS committer review.)*

---

## §7 — Next sessions (optional)

| Step | Work | Size |
|---|---|---|
| 1b | Wire `jts1094-scout` into optional CI once full `libntsrocq` rebuild is easy | small |
| 1c | Optional comment on jts#1094 with §6 numbers | 15 min |
| 1d | Prefer engagement on **#1212** (tip) for any public comment | — |
| 2 | Orientation lane (#1093 Ozaki) — separate session | — |

---

## §8 — Non-claims

- No proof that Java `incircleadapt` equals `b64_inCircle` bit-for-bit (or
equals Shewchuk C bit-for-bit).
- No full re-run of JTS unit tests under Maven in this session.
- No claim that #1094 should merge **instead of** #1212.
- No NTS port in this session.

**AI assistance**: Grok (grok-4-5 / grok-4.5).
**License**: project documentation (BSD-3-Clause).
19 changes: 12 additions & 7 deletions docs/jts-open-prs-scout-2026-08.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -49,12 +49,17 @@ Ordered by **risk÷cost** for the proofs corpus (not JTS merge politics).

### Recommended immediate work sequence (this repo)

1. **Mesh in-circle lane (P0)** — **LANDED 2026-08-05 (session 1 GREEN):**
`oracle/gen_jts1212_incircle_vectors.py` + `oracle/jts1212_incircle_vectors.txt`
+ outcome [`docs/jts-1212-incircle-lane-2026-08.md`](jts-1212-incircle-lane-2026-08.md).
29 vectors; all EXPECTED pins match `INCIRCLE_SIGN`; Stage A CERTAIN never
disagrees with oracle; GEOS955 subset forces Stage A UNCERTAIN while oracle
POS (DD path necessary). Optional follow-ups: CI smoke, comment on #1212.
1. **Mesh in-circle lane (P0)** — **LANDED 2026-08-05:**
- **Session 1 GREEN (#1212 tip):**
`oracle/gen_jts1212_incircle_vectors.py` + `oracle/jts1212_incircle_vectors.txt`
+ [`docs/jts-1212-incircle-lane-2026-08.md`](jts-1212-incircle-lane-2026-08.md).
29 vectors; Stage A CERTAIN never disagrees with oracle; GEOS955 → UNCERTAIN / oracle POS.
- **Session 2 GREEN (#1094 FFI scout + corpus review):**
`oracle/gen_jts1094_incircle_scout.py` + `oracle/jts1094_incircle_vectors.txt`
+ 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.
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.
Expand Down Expand Up @@ -159,7 +164,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 |
| **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) |
| **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 |
Expand Down
6 changes: 6 additions & 0 deletions oracle/.gitignore
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,12 @@ libntsrocq.dylib
libntsrocq.dll
ffi_probe

# Mesh scout in-circle-only FFI (JTS #1094 / #1212 lane)
libscout_incircle.so
libscout_incircle.dylib
libscout_incircle.dll
scout_incircle_probe

# Python bytecode cache
__pycache__/
*.pyc
35 changes: 33 additions & 2 deletions oracle/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,11 @@ FFI_PROBE := ffi_probe
FFI_CFLAGS := -O2 -fPIC -I$(OCAML_WHERE) -I.
FFI_LDLIBS := -L$(OCAML_WHERE) -lasmrun_pic -lm -ldl -lpthread

.PHONY: all clean ffi ffi-parity arc-arc-tests arc-segment-tests arc-arc-distance-tests arc-segment-distance-tests ring-simple-tests cp-ring-simple-tests cp-boundary-simplify-tests cp-boundary-simplify-test arc-offset-tests point-in-curve-ring-tests ring-orientation-tests holes-disjoint-tests curve-relate-matrix-tests buffer-region-tests arc-centroid-tests arc-area-centroid-tests arc-distance-tests arc-area-tests arc-buffer-simple-tests arc-simplify-decision-tests arc-offset-filtered-tests curve-adversarial-hunt elliptic-hunt bezier-hunt winding-number-tests
# Mesh scout lane: in-circle-only FFI (does not need full nts_ffi.ml extraction).
SCOUT_IC_LIB := libscout_incircle.$(FFI_SOEXT)
SCOUT_IC_PROBE := scout_incircle_probe

.PHONY: all clean ffi ffi-parity scout-incircle-ffi jts1094-scout arc-arc-tests arc-segment-tests arc-arc-distance-tests arc-segment-distance-tests ring-simple-tests cp-ring-simple-tests cp-boundary-simplify-tests cp-boundary-simplify-test arc-offset-tests point-in-curve-ring-tests ring-orientation-tests holes-disjoint-tests curve-relate-matrix-tests buffer-region-tests arc-centroid-tests arc-area-centroid-tests arc-distance-tests arc-area-tests arc-buffer-simple-tests arc-simplify-decision-tests arc-offset-filtered-tests curve-adversarial-hunt elliptic-hunt bezier-hunt winding-number-tests

all: $(TARGET)

Expand Down Expand Up @@ -223,5 +227,32 @@ $(FFI_PROBE): ffi_probe.c nts_ffi.h $(FFI_LIB)
ffi-parity: $(TARGET) $(FFI_PROBE)
cd .. && python3 oracle/gen_ffi_parity_tests.py

# ---- Mesh scout: in-circle-only FFI (JTS #1094 / #1212 lane) ---------------
# Builds when full `make ffi` cannot (stale extracted.ml missing e.g.
# b64_orient2d_exact). Same b64_inCircle symbol as production nts_rocq_in_circle.
scout_incircle_ffi.cmx: scout_incircle_ffi.ml extracted.cmi extracted.cmx
$(OCAMLOPT) -c scout_incircle_ffi.ml

scout_incircle_ml.o: extracted.cmx scout_incircle_ffi.cmx
$(OCAMLOPT) -output-obj extracted.cmx scout_incircle_ffi.cmx -o scout_incircle_ml.o

scout_incircle_stubs.o: scout_incircle_stubs.c nts_ffi.h
$(CC) $(FFI_CFLAGS) -c scout_incircle_stubs.c -o scout_incircle_stubs.o

$(SCOUT_IC_LIB): scout_incircle_ml.o scout_incircle_stubs.o
$(CC) -shared -o $@ scout_incircle_ml.o scout_incircle_stubs.o $(FFI_LDLIBS)

$(SCOUT_IC_PROBE): scout_incircle_probe.c nts_ffi.h $(SCOUT_IC_LIB)
$(CC) -O2 -I. scout_incircle_probe.c -o $@ -L. -lscout_incircle -Wl,-rpath,'$$ORIGIN'

scout-incircle-ffi: $(SCOUT_IC_LIB) $(SCOUT_IC_PROBE)

# Differential gate for JTS#1094 vs nts_rocq_in_circle (scout FFI).
jts1094-scout: scout-incircle-ffi $(TARGET)
cd .. && python3 oracle/gen_jts1094_incircle_scout.py \
--oracle oracle/oracle_bin \
--ffi-probe oracle/scout_incircle_probe

clean:
rm -f *.cmi *.cmo *.cmx *.o $(TARGET) $(FFI_LIB) $(FFI_PROBE)
rm -f *.cmi *.cmo *.cmx *.o $(TARGET) $(FFI_LIB) $(FFI_PROBE) \
$(SCOUT_IC_LIB) $(SCOUT_IC_PROBE) scout_incircle_ml.o scout_incircle_stubs.o
Loading
Loading