diff --git a/docs/jts-1094-incircle-lane-2026-08.md b/docs/jts-1094-incircle-lane-2026-08.md new file mode 100644 index 00000000..66ddd641 --- /dev/null +++ b/docs/jts-1094-incircle-lane-2026-08.md @@ -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). diff --git a/docs/jts-open-prs-scout-2026-08.md b/docs/jts-open-prs-scout-2026-08.md index e900dc80..bec8b624 100644 --- a/docs/jts-open-prs-scout-2026-08.md +++ b/docs/jts-open-prs-scout-2026-08.md @@ -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. @@ -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 | diff --git a/oracle/.gitignore b/oracle/.gitignore index 3a869f6c..bcdd1fe6 100644 --- a/oracle/.gitignore +++ b/oracle/.gitignore @@ -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 diff --git a/oracle/Makefile b/oracle/Makefile index da7b631f..3b2f3110 100644 --- a/oracle/Makefile +++ b/oracle/Makefile @@ -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) @@ -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 diff --git a/oracle/gen_jts1094_incircle_scout.py b/oracle/gen_jts1094_incircle_scout.py new file mode 100644 index 00000000..e802eb51 --- /dev/null +++ b/oracle/gen_jts1094_incircle_scout.py @@ -0,0 +1,647 @@ +#!/usr/bin/env python3 +""" +JTS #1094 mesh in-circle scout — FFI differential vs Rocq b64_inCircle. + +topic: mesh (epic #68) +Upstream: locationtech/jts#1094 (Make isInCircleRobust robust) — tinko92 +Sibling tip: locationtech/jts#1212 (Stage A + DD); treat as **one lane**. + +For each 4-tuple (A,B,C,P): + - **FFI ground truth**: nts_rocq_in_circle via scout_incircle_probe + (same extracted b64_inCircle as production libntsrocq / oracle_bin). + - **oracle_bin parity** (optional): bit-pattern agreement with FFI. + - **Stage A mirror of #1094**: CERTAIN sign or UNCERTAIN + (iccerrboundA, permanent-scaled; bound test uses |det| >= errbound + exactly as the PR, which differs from #1212's strict |det| > errbound). + - Optional EXPECTED from Qed pins / algebraic identities. + +Usage (from repo root, after `make -C oracle scout-incircle-ffi`): + python oracle/gen_jts1094_incircle_scout.py + python oracle/gen_jts1094_incircle_scout.py --oracle /path/to/oracle_bin \\ + --ffi-probe /path/to/scout_incircle_probe + python oracle/gen_jts1094_incircle_scout.py --wsl-oracle ... --wsl-ffi-probe ... + +Writes: + oracle/jts1094_incircle_vectors.txt + stdout: gate summary + review-relevant counters +""" +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 + +# Shewchuk iccerrboundA = (10 + 96 * eps) * eps, eps = 2^-53 +# Java Math.ulp(0.5) == 2^-53 on IEEE754 binary64 (same as #1212 DOUBLE_EPS). +DOUBLE_EPS = math.ldexp(1.0, -53) +ICCERRBOUND_A = (10.0 + 96.0 * DOUBLE_EPS) * DOUBLE_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_1094(a: Point, b: Point, c: Point, p: Point) -> Tuple[str, float, bool]: + """Mirror of JTS#1094 TrianglePredicate.isInCircleRobust Stage A. + + Returns (sign POS/NEG/ZERO, det, certain). + Certain uses **|det| >= errbound** (PR#1094), not strict > (#1212). + """ + 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 + ) + err_bound = ICCERRBOUND_A * permanent + # PR#1094: Math.abs(det) >= errbound (non-strict) + certain = abs(det) >= err_bound + if det > 0: + sign = "POS" + elif det < 0: + sign = "NEG" + else: + sign = "ZERO" + return sign, det, certain + + +def stage_a_1212(a: Point, b: Point, c: Point, p: Point) -> Tuple[str, float, bool]: + """Mirror of JTS#1212 for differential count only (strict |det| > bound).""" + sign, det, _ = stage_a_1094(a, b, c, p) + 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 + permanent = ( + (abs(bdxcdy) + abs(cdxbdy)) * alift + + (abs(cdxady) + abs(adxcdy)) * blift + + (abs(adxbdy) + abs(bdxady)) * clift + ) + err_bound = ICCERRBOUND_A * permanent + certain = det > err_bound or -det > err_bound + return sign, det, certain + + +def fmt_pt(q: Point) -> str: + return f"{q[0]:.17g} {q[1]:.17g}" + + +def sign_of(v: float) -> str: + if math.isnan(v): + return "NAN" + if v > 0: + return "POS" + if v < 0: + return "NEG" + return "ZERO" + + +def bits_of(v: float) -> int: + return struct.unpack(">Q", struct.pack(">d", v))[0] + + +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.single_triangle_pin_1190 / 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 diagonal", + ) + ) + v.append( + Vec( + "pin_1039_knife_in", + A, + B, + C, + (0.0, 1.5), + "POS", + "cocircular_tie_is_knife_edge +3", + ) + ) + v.append( + Vec( + "pin_1039_knife_out", + A, + B, + C, + (0.0, 2.5), + "NEG", + "cocircular_tie_is_knife_edge -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: D outside empty circumdisk of ABC", + ) + ) + return v + + +def jts_lane_vectors() -> List[Vec]: + """Shared regression sites with the #1212 harness + #1094 testCircle focus.""" + v: List[Vec] = [] + t0 = (-221.72957795130824, -26.56505117707799) + t1 = (-149.72957795130824, -26.56505117707799) + t2 = (0.0, -90.0) + for name, P in (("t0", t0), ("t1", t1), ("t2", t2)): + v.append( + Vec( + f"jts1190_vertex_{name}", + t0, + t1, + t2, + P, + "ZERO", + "single-triangle constraint sites; vertex on circumcircle", + ) + ) + # DelaunayTest.testCircle densified ring (same WKT as #1094/#1212) + 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): + a, b, c, p = circle[i], circle[i + 1], circle[i + 2], circle[i + 3] + v.append( + Vec( + f"jts1094_circle_quad_{i}", + a, + b, + c, + p, + None, + "DelaunayTest.testCircle near-cocircular sample quad (#1094 retarget)", + ) + ) + v.append( + Vec( + "jts1094_circle_cardinal", + (42.0, 30.0), + (40.0, 28.0), + (38.0, 30.0), + (40.0, 32.0), + None, + "four cardinal-ish points on densified circle", + ) + ) + geos1040 = [ + (6.6584, 53.583000000000006), + (6.6576, 53.583600000000004), + (6.657, 53.5848), + (6.6572000000000005, 53.5842), + ] + v.append( + Vec( + "jts_geos1040_quad", + geos1040[0], + geos1040[1], + geos1040[2], + geos1040[3], + None, + "VoronoiTest nearly cocircular GEOS#1040 / JTS#1171", + ) + ) + geos955_sub = [ + (18.68285714285716, 100.105), + (13.41, 104.82100000000001), + (13.41, 107.179), + (18.682857142857145, 111.89500000000001), + ] + v.append( + Vec( + "jts_geos955_subset", + geos955_sub[0], + geos955_sub[1], + geos955_sub[2], + geos955_sub[3], + None, + "VoronoiTest JTS#1171 ex2 — Stage A must decline (adaptive path)", + ) + ) + # #1094-specific: equality boundary for |det| == errbound (if any appear) + # Unit circle with tiny inward nudge (CERTAIN for larger eps). + for k, eps in enumerate((1e-12, 1e-9, 1e-6)): + v.append( + Vec( + f"adv_unit_circle_eps_{k}", + (1.0, 0.0), + (0.0, 1.0), + (-1.0, 0.0), + (0.0, -1.0 + eps), + None, + f"south pole of unit circle nudged by {eps}", + ) + ) + s = 1e8 + v.append( + Vec( + "adv_large_scale_flip", + (0.0, 0.0), + (2.0 * s, 0.0), + (1.0 * s, 1.0 * s), + (1.0 * s, -0.5 * s), + "POS", + "scaled flip witness (homothety preserves sign)", + ) + ) + return v + + +def all_vectors() -> List[Vec]: + return corpus_vectors() + jts_lane_vectors() + + +def run_oracle_bin( + oracle_cmd: Sequence[str], a: Point, b: Point, c: Point, p: Point +) -> Tuple[str, float]: + 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] + val = ( + float.fromhex(parts[1]) + if parts[1].lower().startswith(("0x", "-0x", "+0x")) + else float(parts[1]) + ) + return sign, val + + +def run_ffi_probe( + probe_cmd: Sequence[str], a: Point, b: Point, c: Point, p: Point +) -> float: + """Call scout_incircle_probe / ffi_probe INCIRCLE_SIGN → raw determinant.""" + # Prefer hex floats for exact cross-boundary decode + nums = " ".join( + [ + float(a[0]).hex(), + float(a[1]).hex(), + float(b[0]).hex(), + float(b[1]).hex(), + float(c[0]).hex(), + float(c[1]).hex(), + float(p[0]).hex(), + float(p[1]).hex(), + ] + ) + proc = subprocess.run( + list(probe_cmd) + ["INCIRCLE_SIGN"], + input=nums + "\n", + capture_output=True, + text=True, + timeout=30, + check=False, + ) + if proc.returncode != 0: + raise RuntimeError( + f"ffi probe exit {proc.returncode}: {proc.stderr.strip()} {proc.stdout.strip()}" + ) + out = proc.stdout.strip() + # "IC #<16 hex digits>" + if not out.startswith("IC"): + raise RuntimeError(f"bad ffi probe output: {out!r}") + hexpart = out[2:].strip() + if not hexpart.startswith("#"): + raise RuntimeError(f"bad ffi probe bits: {out!r}") + bits = int(hexpart[1:], 16) + return struct.unpack(">d", struct.pack(">Q", bits))[0] + + +def resolve_cmd( + path: Optional[str], wsl_path: Optional[str], env_key: str, default_wsl: str +) -> List[str]: + if path: + return [path] + if wsl_path: + return ["wsl.exe", "-e", wsl_path] + env = os.environ.get(env_key) + if env and os.path.isfile(env): + return [env] + # WSL default (Windows host running WSL binary) + if os.name == "nt" or sys.platform.startswith("win"): + return ["wsl.exe", "-e", default_wsl] + if os.path.isfile(default_wsl): + return [default_wsl] + # relative from repo root + rel = default_wsl.split("/")[-1] + for cand in (f"oracle/{rel}", rel): + if os.path.isfile(cand): + return [os.path.abspath(cand)] + return ["wsl.exe", "-e", default_wsl] + + +def main() -> int: + ap = argparse.ArgumentParser(description=__doc__) + ap.add_argument("--oracle", help="Path to native oracle_bin") + ap.add_argument("--wsl-oracle", help="Linux path via wsl.exe -e") + ap.add_argument("--ffi-probe", help="Path to scout_incircle_probe or ffi_probe") + ap.add_argument("--wsl-ffi-probe", help="Linux path via wsl.exe -e") + ap.add_argument( + "--out", + default="oracle/jts1094_incircle_vectors.txt", + help="Vector table output path", + ) + ap.add_argument( + "--skip-oracle-parity", + action="store_true", + help="Only use FFI (skip oracle_bin bit-parity check)", + ) + args = ap.parse_args() + + # Prefer workspace mount under WSL when running from Windows + default_oracle = "/mnt/c/com/github/grootstebozewolf/NetTopologySuite.Proofs/oracle/oracle_bin" + if not os.path.isfile("oracle/oracle_bin"): + # fall back to older WSL clone if mount binary missing + alt = "/home/user/nettopologysuite.proofs/oracle/oracle_bin" + default_oracle = alt + default_probe = ( + "/mnt/c/com/github/grootstebozewolf/NetTopologySuite.Proofs/oracle/scout_incircle_probe" + ) + + oracle_cmd = resolve_cmd( + args.oracle, args.wsl_oracle, "ORACLE_BIN", default_oracle + ) + probe_cmd = resolve_cmd( + args.ffi_probe, args.wsl_ffi_probe, "SCOUT_IC_PROBE", default_probe + ) + + # Sanity: FFI pin (flip witness → POS 1.5) + try: + ffi_val = run_ffi_probe(probe_cmd, (0, 0), (2, 0), (1, 1), (1, -0.5)) + except Exception as e: + print(f"FATAL: FFI probe unavailable ({probe_cmd}): {e}", file=sys.stderr) + return 2 + if sign_of(ffi_val) != "POS" or abs(ffi_val - 1.5) > 1e-12: + print( + f"FATAL: FFI pin failed: {sign_of(ffi_val)} {ffi_val} (expected POS 1.5)", + file=sys.stderr, + ) + return 2 + print(f"FFI pin OK: POS {ffi_val} via {probe_cmd}") + + if not args.skip_oracle_parity: + try: + o_sign, o_val = run_oracle_bin( + oracle_cmd, (0, 0), (2, 0), (1, 1), (1, -0.5) + ) + except Exception as e: + print( + f"FATAL: oracle_bin unavailable ({oracle_cmd}): {e}", + file=sys.stderr, + ) + return 2 + if o_sign != "POS" or abs(o_val - 1.5) > 1e-12: + print( + f"FATAL: oracle pin failed: {o_sign} {o_val}", + file=sys.stderr, + ) + return 2 + if bits_of(o_val) != bits_of(ffi_val): + print( + f"FATAL: FFI/oracle bit mismatch on pin: " + f"ffi={ffi_val.hex()} oracle={o_val.hex()}", + file=sys.stderr, + ) + return 2 + print(f"oracle_bin pin OK + bit-parity with FFI via {oracle_cmd}") + + vecs = all_vectors() + lines: List[str] = [ + "# JTS #1094 mesh in-circle differential vectors (FFI scout)", + "# topic: mesh epic: #68", + "# Format: name A B C P FFI STAGE_A1094 CERTAIN STAGE_A1212_CERT " + "EXPECTED note", + "# FFI = nts_rocq_in_circle / b64_inCircle via scout_incircle_probe.", + "# STAGE_A1094 uses |det| >= errbound (PR#1094); STAGE_A1212_CERT is " + "strict > (PR#1212).", + "# EXPECTED is POS|NEG|ZERO when a corpus pin applies; else -", + "#", + ] + + n_pass = 0 + n_uncertain = 0 + n_open = 0 + n_bound_diverge = 0 # #1094 CERTAIN while #1212 UNCERTAIN (or reverse) + failures: List[str] = [] + parity_fail = 0 + + for vec in vecs: + ffi_v = run_ffi_probe(probe_cmd, vec.a, vec.b, vec.c, vec.p) + ffi_sign = sign_of(ffi_v) + + if not args.skip_oracle_parity: + o_sign, o_val = run_oracle_bin(oracle_cmd, vec.a, vec.b, vec.c, vec.p) + if bits_of(o_val) != bits_of(ffi_v): + # NaN collapse: treat both NaN as OK + if not (math.isnan(o_val) and math.isnan(ffi_v)): + parity_fail += 1 + failures.append( + f"{vec.name}: FFI/oracle bits diverge " + f"ffi={ffi_v.hex()} oracle={o_val.hex()}" + ) + + a_sign, det, certain1094 = stage_a_1094(vec.a, vec.b, vec.c, vec.p) + _, _, certain1212 = stage_a_1212(vec.a, vec.b, vec.c, vec.p) + if certain1094 != certain1212: + n_bound_diverge += 1 + + if certain1094: + tag = "CERTAIN" + if {a_sign, ffi_sign} <= {"POS", "NEG"} and a_sign != ffi_sign: + failures.append( + f"{vec.name}: StageA1094 CERTAIN {a_sign} != FFI {ffi_sign} " + f"(det={det})" + ) + else: + n_pass += 1 + else: + tag = "UNCERTAIN" + n_uncertain += 1 + n_pass += 1 + + if vec.expected is not None: + if ffi_sign != vec.expected: + if vec.expected == "ZERO" and abs(ffi_v) < 1e-9: + pass + else: + failures.append( + f"{vec.name}: expected {vec.expected} got {ffi_sign} " + f"val={ffi_v}" + ) + else: + n_open += 1 + + lines.append( + f"{vec.name}\t{fmt_pt(vec.a)}\t{fmt_pt(vec.b)}\t{fmt_pt(vec.c)}\t" + f"{fmt_pt(vec.p)}\t{ffi_sign}\t{a_sign}\t{tag}\t" + f"{'CERTAIN' if certain1212 else 'UNCERTAIN'}\t" + f"{vec.expected or '-'}\t{vec.note}" + ) + + out_path = args.out + os.makedirs(os.path.dirname(out_path) or ".", exist_ok=True) + with open(out_path, "w", encoding="utf-8") as f: + f.write("\n".join(lines) + "\n") + + print() + print(f"Vectors: {len(vecs)} written → {out_path}") + print( + f"Gate rows: pass≈{n_pass} fail={len(failures)} " + f"StageA UNCERTAIN={n_uncertain} open(no EXPECTED)={n_open}" + ) + print( + f"Bound policy diverge (#1094 ≥ vs #1212 >): {n_bound_diverge} vectors" + ) + print(f"FFI/oracle bit-parity failures: {parity_fail}") + if failures: + print("FAILURES:") + for msg in failures: + print(f" {msg}") + return 1 + print( + "GATE: all expected pins match FFI; no StageA1094 CERTAIN≠FFI conflicts; " + "FFI≡oracle_bin bits." + ) + return 0 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/oracle/jts1094_incircle_vectors.txt b/oracle/jts1094_incircle_vectors.txt new file mode 100644 index 00000000..8ba45d9b --- /dev/null +++ b/oracle/jts1094_incircle_vectors.txt @@ -0,0 +1,34 @@ +# JTS #1094 mesh in-circle differential vectors (FFI scout) +# topic: mesh epic: #68 +# Format: name A B C P FFI STAGE_A1094 CERTAIN STAGE_A1212_CERT EXPECTED note +# FFI = nts_rocq_in_circle / b64_inCircle via scout_incircle_probe. +# STAGE_A1094 uses |det| >= errbound (PR#1094); STAGE_A1212_CERT is strict > (PR#1212). +# EXPECTED is POS|NEG|ZERO when a corpus pin applies; else - +# +pin_1190_vertex_A 0 0 4 0 0 4 0 0 ZERO ZERO CERTAIN UNCERTAIN ZERO DelaunayDegeneratePins.single_triangle_pin_1190 / inCircle_R_at_vertex +pin_1190_vertex_B 0 0 4 0 0 4 4 0 ZERO ZERO CERTAIN UNCERTAIN ZERO DelaunayDegeneratePins.single_triangle_pin_1190 / inCircle_R_at_vertex +pin_1190_vertex_C 0 0 4 0 0 4 0 4 ZERO ZERO CERTAIN UNCERTAIN ZERO DelaunayDegeneratePins.single_triangle_pin_1190 / inCircle_R_at_vertex +pin_1039_diag_ABC_D 0 0 2 0 2 2 0 2 ZERO ZERO UNCERTAIN UNCERTAIN ZERO cocircular_square_tie_1039 +pin_1039_diag_ABD_C 0 0 2 0 0 2 2 2 ZERO ZERO UNCERTAIN UNCERTAIN ZERO cocircular_square_tie_1039 mirror diagonal +pin_1039_knife_in 0 0 2 0 2 2 0 1.5 POS POS CERTAIN CERTAIN POS cocircular_tie_is_knife_edge +3 +pin_1039_knife_out 0 0 2 0 2 2 0 2.5 NEG NEG CERTAIN CERTAIN NEG cocircular_tie_is_knife_edge -5 +pin_68b_flip_witness 0 0 2 0 1 1 1 -0.5 POS POS CERTAIN CERTAIN POS loc_in_circle_test_D; inCircle_R = 3/2 +pin_68a_D_outside_ABC 0 0 2 0 1 1 1 -2 NEG NEG CERTAIN CERTAIN NEG DelaunayEdgeEmptyCircle: D outside empty circumdisk of ABC +jts1190_vertex_t0 -221.72957795130824 -26.56505117707799 -149.72957795130824 -26.56505117707799 0 -90 -221.72957795130824 -26.56505117707799 ZERO ZERO CERTAIN UNCERTAIN ZERO single-triangle constraint sites; vertex on circumcircle +jts1190_vertex_t1 -221.72957795130824 -26.56505117707799 -149.72957795130824 -26.56505117707799 0 -90 -149.72957795130824 -26.56505117707799 ZERO ZERO CERTAIN UNCERTAIN ZERO single-triangle constraint sites; vertex on circumcircle +jts1190_vertex_t2 -221.72957795130824 -26.56505117707799 -149.72957795130824 -26.56505117707799 0 -90 0 -90 ZERO ZERO CERTAIN UNCERTAIN ZERO single-triangle constraint sites; vertex on circumcircle +jts1094_circle_quad_0 42 30 41.960000000000001 29.609999999999999 41.850000000000001 29.23 41.659999999999997 28.890000000000001 NEG NEG CERTAIN CERTAIN - DelaunayTest.testCircle near-cocircular sample quad (#1094 retarget) +jts1094_circle_quad_4 41.409999999999997 28.59 41.109999999999999 28.34 40.770000000000003 28.149999999999999 40.390000000000001 28.039999999999999 NEG NEG CERTAIN CERTAIN - DelaunayTest.testCircle near-cocircular sample quad (#1094 retarget) +jts1094_circle_quad_8 40 28 39.609999999999999 28.039999999999999 39.229999999999997 28.149999999999999 38.890000000000001 28.34 NEG NEG CERTAIN CERTAIN - DelaunayTest.testCircle near-cocircular sample quad (#1094 retarget) +jts1094_circle_quad_12 38.590000000000003 28.59 38.340000000000003 28.890000000000001 38.149999999999999 29.23 38.039999999999999 29.609999999999999 NEG NEG CERTAIN CERTAIN - DelaunayTest.testCircle near-cocircular sample quad (#1094 retarget) +jts1094_circle_quad_16 38 30 38.039999999999999 30.390000000000001 38.149999999999999 30.77 38.340000000000003 31.109999999999999 NEG NEG CERTAIN CERTAIN - DelaunayTest.testCircle near-cocircular sample quad (#1094 retarget) +jts1094_circle_quad_20 38.590000000000003 31.41 38.890000000000001 31.66 39.229999999999997 31.850000000000001 39.609999999999999 31.960000000000001 NEG NEG CERTAIN CERTAIN - DelaunayTest.testCircle near-cocircular sample quad (#1094 retarget) +jts1094_circle_quad_24 40 32 40.390000000000001 31.960000000000001 40.770000000000003 31.850000000000001 41.109999999999999 31.66 NEG NEG CERTAIN CERTAIN - DelaunayTest.testCircle near-cocircular sample quad (#1094 retarget) +jts1094_circle_quad_28 41.409999999999997 31.41 41.659999999999997 31.109999999999999 41.850000000000001 30.77 41.960000000000001 30.390000000000001 NEG NEG CERTAIN CERTAIN - DelaunayTest.testCircle near-cocircular sample quad (#1094 retarget) +jts1094_circle_cardinal 42 30 40 28 38 30 40 32 ZERO ZERO UNCERTAIN UNCERTAIN - four cardinal-ish points on densified circle +jts_geos1040_quad 6.6584000000000003 53.583000000000006 6.6576000000000004 53.583600000000004 6.657 53.584800000000001 6.6572000000000005 53.584200000000003 NEG NEG CERTAIN CERTAIN - VoronoiTest nearly cocircular GEOS#1040 / JTS#1171 +jts_geos955_subset 18.682857142857159 100.105 13.41 104.82100000000001 13.41 107.179 18.682857142857145 111.89500000000001 POS ZERO UNCERTAIN UNCERTAIN - VoronoiTest JTS#1171 ex2 — Stage A must decline (adaptive path) +adv_unit_circle_eps_0 1 0 0 1 -1 0 0 -0.99999999999900002 POS POS CERTAIN CERTAIN - south pole of unit circle nudged by 1e-12 +adv_unit_circle_eps_1 1 0 0 1 -1 0 0 -0.99999999900000003 POS POS CERTAIN CERTAIN - south pole of unit circle nudged by 1e-09 +adv_unit_circle_eps_2 1 0 0 1 -1 0 0 -0.99999899999999997 POS POS CERTAIN CERTAIN - south pole of unit circle nudged by 1e-06 +adv_large_scale_flip 0 0 200000000 0 100000000 100000000 100000000 -50000000 POS POS CERTAIN CERTAIN POS scaled flip witness (homothety preserves sign) diff --git a/oracle/scout_incircle_ffi.ml b/oracle/scout_incircle_ffi.ml new file mode 100644 index 00000000..12762dcf --- /dev/null +++ b/oracle/scout_incircle_ffi.ml @@ -0,0 +1,25 @@ +(* ============================================================================ + oracle/scout_incircle_ffi.ml + ---------------------------------------------------------------------------- + Minimal Phase-5-style FFI surface for the mesh in-circle scout lane. + + Registers only `b64_inCircle` (the same extracted symbol that + `oracle_bin` INCIRCLE_SIGN and production `nts_rocq_in_circle` use). + Full `nts_ffi.ml` currently needs a fresher extraction (e.g. + `b64_orient2d_exact`); this scout library does not. + + Bit-identity with oracle_bin is the same construction as Phase 5: + one extracted symbol, two call paths (subprocess protocol vs C ABI). + + AI disclosure: authored with AI assistance (see CONTRIBUTING.md). + ========================================================================== *) + +open Extracted + +let pt (a : float array) (i : int) : bPoint = { bx = a.(i); by_ = a.(i + 1) } + +(* [| ax; ay; bx; by; cx; cy; px; py |] *) +let in_circle (a : float array) : float = + b64_inCircle (pt a 0) (pt a 2) (pt a 4) (pt a 6) + +let () = Callback.register "nts_ffi_in_circle" in_circle diff --git a/oracle/scout_incircle_probe.c b/oracle/scout_incircle_probe.c new file mode 100644 index 00000000..79e79eba --- /dev/null +++ b/oracle/scout_incircle_probe.c @@ -0,0 +1,64 @@ +/* ============================================================================ + oracle/scout_incircle_probe.c + ---------------------------------------------------------------------------- + Thin driver over the scout in-circle library (nts_rocq_in_circle). + Same output style as ffi_probe for INCIRCLE_SIGN: "IC #<16 hex digits>". + + Usage: scout_incircle_probe INCIRCLE_SIGN < 8 doubles + + AI disclosure: authored with AI assistance (see CONTRIBUTING.md). + ========================================================================== */ + +#include +#include +#include + +#include "nts_ffi.h" + +static double vals[16]; +static int n_vals = 0; + +static void read_vals(void) +{ + char tok[128]; + while (n_vals < 16 && scanf("%127s", tok) == 1) { + vals[n_vals++] = strtod(tok, NULL); + } +} + +static void put_d(double d) +{ + unsigned long long bits; + memcpy(&bits, &d, sizeof(bits)); + printf(" #%016llx", (unsigned long long)bits); +} + +int main(int argc, char **argv) +{ + if (argc < 2) { + fprintf(stderr, "usage: scout_incircle_probe INCIRCLE_SIGN < 8 doubles\n"); + return 2; + } + if (strcmp(argv[1], "INCIRCLE_SIGN") != 0) { + fprintf(stderr, "scout_incircle_probe: only INCIRCLE_SIGN supported\n"); + return 2; + } + if (nts_rocq_init() != 0) { + fprintf(stderr, "scout_incircle_probe: nts_rocq_init failed\n"); + return 2; + } + if (nts_rocq_abi_version() != NTS_ROCQ_ABI_VERSION) { + fprintf(stderr, "scout_incircle_probe: ABI mismatch\n"); + return 2; + } + read_vals(); + if (n_vals < 8) { + fprintf(stderr, "scout_incircle_probe: need 8 doubles, got %d\n", n_vals); + return 2; + } + printf("IC"); + put_d(nts_rocq_in_circle(vals[0], vals[1], vals[2], vals[3], + vals[4], vals[5], vals[6], vals[7])); + printf("\n"); + return 0; +} diff --git a/oracle/scout_incircle_stubs.c b/oracle/scout_incircle_stubs.c new file mode 100644 index 00000000..2c5010e3 --- /dev/null +++ b/oracle/scout_incircle_stubs.c @@ -0,0 +1,76 @@ +/* ============================================================================ + oracle/scout_incircle_stubs.c + ---------------------------------------------------------------------------- + Minimal C ABI for the mesh in-circle scout: only + nts_rocq_init / nts_rocq_abi_version / nts_rocq_in_circle + matching the production signatures in nts_ffi.h for those three entries. + + AI disclosure: authored with AI assistance (see CONTRIBUTING.md). + ========================================================================== */ + +#include + +#include +#include +#include +#include + +#include "nts_ffi.h" + +static int nts_rocq_started = 0; + +int32_t nts_rocq_init(void) +{ + static char arg0[] = "libscout_incircle"; + static char *argv[] = { arg0, NULL }; + + if (nts_rocq_started) { + return 0; + } + caml_startup(argv); + nts_rocq_started = 1; + return 0; +} + +int32_t nts_rocq_abi_version(void) +{ + return NTS_ROCQ_ABI_VERSION; +} + +#define NTS_FFI_NO_CALLBACK_DBL ((double)0.0 / (double)0.0) + +static value nts_args(const double *v, int n) +{ + CAMLparam0(); + CAMLlocal1(a); + int i; + + a = caml_alloc(n * Double_wosize, Double_array_tag); + for (i = 0; i < n; i++) { + Store_double_field(a, i, v[i]); + } + CAMLreturn(a); +} + +static double nts_call_double(const char *name, const double *v, int n) +{ + CAMLparam0(); + CAMLlocal2(args, res); + const value *closure; + + nts_rocq_init(); + closure = caml_named_value(name); + if (closure == NULL) { + CAMLreturnT(double, NTS_FFI_NO_CALLBACK_DBL); + } + args = nts_args(v, n); + res = caml_callback(*closure, args); + CAMLreturnT(double, Double_val(res)); +} + +double nts_rocq_in_circle(double ax, double ay, double bx, double by, + double cx, double cy, double px, double py) +{ + const double v[8] = { ax, ay, bx, by, cx, cy, px, py }; + return nts_call_double("nts_ffi_in_circle", v, 8); +}