From c9e1352897290ff2a54262e23543a89933344b36 Mon Sep 17 00:00:00 2001 From: Jeroen Bloemscheer Date: Wed, 5 Aug 2026 03:30:55 +0200 Subject: [PATCH] =?UTF-8?q?docs:=20FFI=20rungs=20=E2=80=94=20restore=20lib?= =?UTF-8?q?ntsrocq=20path=20+=20#1093=20orient=20scout?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Re-extract rebuild helper, rung ladder, and Ozaki vs Shewchuk vs ORIENT_EXACT harness. Full libntsrocq builds after extract; exact FFI still YELLOW on extremes. --- docs/ffi-rungs-2026-08.md | 151 +++++++++++ docs/jts-open-prs-scout-2026-08.md | 8 +- docs/phase5-ffi-abi.md | 15 ++ oracle/Makefile | 11 +- oracle/gen_jts1093_orient_scout.py | 386 +++++++++++++++++++++++++++++ oracle/jts1093_orient_vectors.txt | 16 ++ oracle/scout_incircle_ffi.ml | 5 +- scripts/rebuild_oracle_ffi.sh | 60 +++++ 8 files changed, 648 insertions(+), 4 deletions(-) create mode 100644 docs/ffi-rungs-2026-08.md create mode 100644 oracle/gen_jts1093_orient_scout.py create mode 100644 oracle/jts1093_orient_vectors.txt create mode 100644 scripts/rebuild_oracle_ffi.sh diff --git a/docs/ffi-rungs-2026-08.md b/docs/ffi-rungs-2026-08.md new file mode 100644 index 00000000..e1c66a7e --- /dev/null +++ b/docs/ffi-rungs-2026-08.md @@ -0,0 +1,151 @@ +# FFI rungs — restore full `libntsrocq` + orientation lane (2026-08) + +**Date**: 2026-08-05. +**topic:** `precision` / `docs` · epics **#66** (orient), Phase 5 FFI. +**Trigger**: Mesh in-circle sessions used a scout-only library because workspace +`extracted.ml` was stale (missing `b64_orient2d_exact`). Next JTS picks +(#1093 Ozaki, #1197 DD characterization) need **filtered + exact** orient in +process — not new ABI symbols. + +**Product call from scout**: expand **ergonomics**, not surface area +([jts-open-prs-scout-2026-08.md](jts-open-prs-scout-2026-08.md)). + +--- + +## §0 — Rung ladder + +| Rung | Goal | Status (2026-08-05) | +|---|---|---| +| **0** | Document gap + rebuild path | **This doc** | +| **1** | Re-extract `Validate_binary64_extract.v` → freshen `oracle/extracted.ml` | **GREEN** (local WSL; extract is gitignored) | +| **2** | `make -C oracle ffi` → full `libntsrocq.so` + `ffi_probe` | **GREEN** after rung 1 | +| **3** | `make -C oracle ffi-parity` | **YELLOW** — 3 ORIENT_EXACT* cases segfault on extreme coords (see §3) | +| **4** | Orientation differential scout for [jts#1093](https://github.com/locationtech/jts/pull/1093) | **Harness landed** (`oracle/gen_jts1093_orient_scout.py`) | +| **5** | Retire / demote `scout_incircle_*` once full FFI is the default path | Pending CI green on parity | +| **6** | Optional: post numbers on jts#1093 / keep #1197 green | Later | + +--- + +## §1 — Root cause of the scout fork + +`oracle/nts_ffi.ml` registers `orient_sign_exact` → `b64_orient2d_exact`. +`theories-flocq/Validate_binary64_extract.v` **lists** that symbol in the +`Extraction` command, but a workspace `extracted.ml` produced without a +fresh Flocq extract omits it → `make -C oracle ffi` fails with +`Unbound value b64_orient2d_exact`. + +Mesh session 2 therefore shipped `scout_incircle_ffi.ml` (in-circle only). +That was correct as a temporary path; it is **not** the long-term Phase 5 +story. + +--- + +## §2 — Rebuild (rungs 1–2) + +Extract is **gitignored**. Rebuild on a Linux/WSL host with Rocq + Flocq and +compiled `.vo` for the extract dependency closure: + +```bash +# From repo root (Rocq 9.x + Flocq; theories-flocq/*.vo present): +coqc -Q theories NTS.Proofs -Q theories-flocq NTS.Proofs.Flocq \ + theories-flocq/Validate_binary64_extract.v + +make -C oracle # oracle_bin +make -C oracle ffi # libntsrocq.so + ffi_probe +make -C oracle ffi-parity +``` + +Helper script (best-effort): [`scripts/rebuild_oracle_ffi.sh`](../scripts/rebuild_oracle_ffi.sh). + +Smoke (exact escalation + filter + in-circle): + +```bash +printf '0 0\n1 0\n0 1\n' | oracle/ffi_probe ORIENT_EXACT # → 1 (POS) +printf '0 0\n1 0\n0 1\n' | oracle/ffi_probe ORIENT_FILTERED # → 1 #... +printf '0 0\n2 0\n1 1\n1 -0.5\n' | oracle/oracle_bin # mode on stdin first +# INCIRCLE_SIGN via oracle_bin (ffi_probe mode name is INCIRCLE_SIGN): +printf '0 0\n2 0\n1 1\n1 -0.5\n' | oracle/ffi_probe INCIRCLE_SIGN +``` + +--- + +## §3 — Parity result (rung 3) + +Local run after re-extract (2026-08-05, ~1215 cases): + +| Mode | Result | +|---|---| +| ORIENT_FILTERED / ORIENT | OK | +| INTERSECT_* / PASSES_* / SNAP / EDGE / INCIRCLE / ARC / TWOSUM / GROW / SIMPLIFY | OK | +| **ORIENT_EXACT** | **1 MISMATCH** (FFI side errored) | +| **ORIENT_EXACT_EXTRACTED** | **2 MISMATCH** (FFI side errored) | + +**Failure shape:** `ffi_probe ORIENT_EXACT` **segfaults** on at least one +adversarial input with mixed subnormal / near-overflow coordinates, e.g.: + +```text +0x0.0p+0 0x0.0p+0 +0x0.0000000000001p-1022 0x0.0000000000001p-1022 +0x1.1ccf385ebc8a0p+1023 0x1.1ccf385ebc8a0p+1023 +``` + +`oracle_bin` `ORIENT_EXACT` / extracted path still answers (`ZERO` / `NEG`). +So the bug is **in-process Callback / runtime path** (stack, GC, or Z +allocation under the shared-lib runtime), not the abstract algorithm. + +**Policy until fixed:** + +- Use **`oracle_bin` ORIENT_EXACT** as ground truth for #1093 / #1197 scouts. +- Use **FFI** for filtered/naive/in-circle/snap (parity green). +- Do **not** claim full-plane exact FFI for production escalation until the + segfault class is gone or bounded out of the contract. + +--- + +## §4 — Orientation lane (rung 4) + +Upstream: [jts#1093](https://github.com/locationtech/jts/pull/1093) replaces +JTS `orientationIndexFilter` Shewchuk-ish / `DP_SAFE_EPSILON=1e-15` path with +**Ozaki et al.** permanent-style bound: + +```text +detleft = (pax - pcx) * (pby - pcy) +detright = (pay - pcy) * (pbx - pcx) +det = detleft - detright +errbound = |detleft + detright| * 3.3306690621773724e-16 +certain iff |det| >= errbound +``` + +Corpus counterpart: + +| Asset | Role | +|---|---| +| `b64_orient_sign_filtered` | Shewchuk Stage A (corpus / FFI) | +| `b64_orient2d_exact` / `ORIENT_EXACT` | Full-plane sign GT | +| `oracle/gen_jts1093_orient_scout.py` | Ozaki mirror vs Shewchuk filter vs exact | + +Gate intent: **Ozaki CERTAIN never disagrees with exact**; report how often +Ozaki is CERTAIN when Shewchuk is UNCERTAIN (tighter filter claim). + +--- + +## §5 — What not to do + +- Do **not** add Ozaki as a Rocq FFI entry until/unless the corpus proves an + Ozaki filter (product decision + claimId). Differential scouts mirror in Python. +- Do **not** dual-track scout + full lib in CI forever — pick full lib after + exact-FFI is fixed or explicitly excluded from parity. +- Do **not** invent claimId for history/scout scripts (ADR-0004 cold). + +--- + +## §6 — Next actions + +1. Track ORIENT_EXACT FFI segfault (rung 3 close-out) — isolated repro above. +2. Run `python3 oracle/gen_jts1093_orient_scout.py` in CI-ish local loop; comment + on jts#1093 only with numbers. +3. Wire `make -C oracle ffi` into developer docs / optional CI once parity is + green or exact is skipped under a named env flag. + +**AI assistance**: Grok (grok-4.5), human-directed. +**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 9e7a04db..f633d40a 100644 --- a/docs/jts-open-prs-scout-2026-08.md +++ b/docs/jts-open-prs-scout-2026-08.md @@ -65,7 +65,13 @@ Ordered by **risk÷cost** for the proofs corpus (not JTS merge politics). + [`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. +2. **Orientation lane (P0)** — **STARTED 2026-08-05 (FFI rungs):** + Full `libntsrocq` rebuild path after re-extract (`docs/ffi-rungs-2026-08.md`, + `scripts/rebuild_oracle_ffi.sh`). + Differential scout: `oracle/gen_jts1093_orient_scout.py` (Ozaki mirror vs + Shewchuk Stage A vs `ORIENT_EXACT`). + Note: `ORIENT_EXACT` **FFI** still has a segfault class on extreme coords + (parity YELLOW); use `oracle_bin` for exact GT. 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. 5. **Coverage #1084 (P1)** — Spec sketch only until #425 cleaner is stable. diff --git a/docs/phase5-ffi-abi.md b/docs/phase5-ffi-abi.md index 5bd9d6f0..98ce582b 100644 --- a/docs/phase5-ffi-abi.md +++ b/docs/phase5-ffi-abi.md @@ -13,6 +13,21 @@ Companion sources: --- +## 0. Rebuild / freshness (2026-08) + +`oracle/extracted.ml` is **gitignored**. A stale extract (missing +`b64_orient2d_exact`) breaks `make -C oracle ffi` while still allowing the +mesh scout library (`scout_incircle_*`). Refresh with: + +```bash +./scripts/rebuild_oracle_ffi.sh --parity +``` + +Rung status, parity YELLOW on exact-orient extremes, and the orientation +lane scout: [`docs/ffi-rungs-2026-08.md`](ffi-rungs-2026-08.md). + +--- + ## 1. Where Phase 5 actually stood The roadmap row read "pending Phase 1+ / 0%", which had gone stale in one diff --git a/oracle/Makefile b/oracle/Makefile index 3b2f3110..8fb4b57f 100644 --- a/oracle/Makefile +++ b/oracle/Makefile @@ -20,6 +20,10 @@ # make -C oracle ffi # builds libntsrocq.so + the ffi_probe driver # make -C oracle ffi-parity # gates FFI == oracle_bin, bit for bit # +# If `make ffi` fails with Unbound value b64_orient2d_exact, re-extract: +# ./scripts/rebuild_oracle_ffi.sh [--parity] +# (see docs/ffi-rungs-2026-08.md) +# # ============================================================================= OCAMLOPT := ocamlfind ocamlopt @@ -41,7 +45,7 @@ FFI_LDLIBS := -L$(OCAML_WHERE) -lasmrun_pic -lm -ldl -lpthread 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 +.PHONY: all clean ffi ffi-parity jts1093-orient-scout 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) @@ -227,6 +231,11 @@ $(FFI_PROBE): ffi_probe.c nts_ffi.h $(FFI_LIB) ffi-parity: $(TARGET) $(FFI_PROBE) cd .. && python3 oracle/gen_ffi_parity_tests.py +# Orientation lane (jts#1093): Ozaki vs Shewchuk Stage A vs ORIENT_EXACT. +# Does not require libntsrocq; optional FFI_PROBE for filtered parity spot-check. +jts1093-orient-scout: $(TARGET) + cd .. && python3 oracle/gen_jts1093_orient_scout.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. diff --git a/oracle/gen_jts1093_orient_scout.py b/oracle/gen_jts1093_orient_scout.py new file mode 100644 index 00000000..e9e91664 --- /dev/null +++ b/oracle/gen_jts1093_orient_scout.py @@ -0,0 +1,386 @@ +#!/usr/bin/env python3 +""" +JTS #1093 orientation lane — Ozaki filter scout vs corpus exact orient. + +topic: precision (epic #66) +Upstream: locationtech/jts#1093 (Ozaki et al. orientationIndexFilter) +Corpus GT: oracle_bin ORIENT_EXACT (zarith / full-plane sign) +Optional: ffi_probe ORIENT_FILTERED (Shewchuk Stage A via libntsrocq) + +What this gates (no new Rocq claimId — ADR-0004 cold): + I1 Ozaki CERTAIN never disagrees with ORIENT_EXACT sign (nonzero). + I2 Shewchuk-corpus Stage A CERTAIN never disagrees with exact. + I3 Report tighter-filter stats: Ozaki CERTAIN when Shewchuk UNCERTAIN. + +Ozaki (PR #1093): + detleft = (ax-cx)*(by-cy) + detright = (ay-cy)*(bx-cx) + det = detleft - detright + errbound = |detleft + detright| * 3.3306690621773724e-16 + certain iff |det| >= errbound + +Corpus Shewchuk Stage A (Orientation_b64 / JTS pre-Ozaki shape with +published constant): errbound = (3+16ε)ε * detsum, ε=2^-53, with the +standard detsum construction (see stage_a_shewchuk). + +Usage: + python oracle/gen_jts1093_orient_scout.py + python oracle/gen_jts1093_orient_scout.py --wsl-oracle /path/to/oracle_bin + python oracle/gen_jts1093_orient_scout.py --ffi-probe /path/to/ffi_probe +""" +from __future__ import annotations + +import argparse +import math +import os +import subprocess +import sys +from dataclasses import dataclass +from typing import List, Optional, Sequence, Tuple + +# Ozaki constant from jts#1093 (double literal in CGAlgorithmsDD). +OZAKI_K = 3.3306690621773724e-16 + +# Shewchuk ε and ccwerrboundA coefficient (Orientation_b64 / predicates.c). +SHEWCHUK_EPS = math.ldexp(1.0, -53) +CCWERRBOUND_A = (3.0 + 16.0 * SHEWCHUK_EPS) * SHEWCHUK_EPS + +Point = Tuple[float, float] + + +@dataclass +class Vec: + name: str + a: Point # p0 + b: Point # p1 + q: Point # query + expected: Optional[str] # POS | NEG | ZERO | None + note: str = "" + + +def det_parts(a: Point, b: Point, q: Point) -> Tuple[float, float, float]: + """Return (detleft, detright, det) with origin at q (Shewchuk/Ozaki form).""" + ax, ay = a[0] - q[0], a[1] - q[1] + bx, by = b[0] - q[0], b[1] - q[1] + detleft = ax * by + detright = ay * bx + return detleft, detright, detleft - detright + + +def stage_a_ozaki(a: Point, b: Point, q: Point) -> Tuple[str, float, bool]: + """Mirror of jts#1093 orientationIndexFilter.""" + detleft, detright, det = det_parts(a, b, q) + errbound = abs(detleft + detright) * OZAKI_K + certain = abs(det) >= errbound + if det > 0: + sign = "POS" + elif det < 0: + sign = "NEG" + else: + sign = "ZERO" + return sign, det, certain + + +def stage_a_shewchuk(a: Point, b: Point, q: Point) -> Tuple[str, float, bool]: + """Shewchuk Stage A permanent-style filter (corpus / predicates.c shape). + + detsum construction matches the classic public-domain orientation filter: + if detleft and detright have opposite signs (or either is zero), the sign + of det is already exact in floating point for this form; else scale. + """ + detleft, detright, det = det_parts(a, b, q) + if detleft > 0.0: + if detright <= 0.0: + certain = True + detsum = 0.0 + else: + detsum = detleft + detright + certain = False + elif detleft < 0.0: + if detright >= 0.0: + certain = True + detsum = 0.0 + else: + detsum = -detleft - detright + certain = False + else: + certain = True + detsum = 0.0 + + if not certain: + errbound = CCWERRBOUND_A * detsum + certain = abs(det) >= errbound + + if det > 0: + sign = "POS" + elif det < 0: + sign = "NEG" + else: + sign = "ZERO" + return sign, det, certain + + +def corpus_vectors() -> List[Vec]: + v: List[Vec] = [] + # Classic CCW unit right triangle → POS + v.append(Vec("pin_ccw_unit", (0.0, 0.0), (1.0, 0.0), (0.0, 1.0), "POS", "area +1/2")) + v.append(Vec("pin_cw_unit", (0.0, 0.0), (0.0, 1.0), (1.0, 0.0), "NEG", "area -1/2")) + v.append(Vec("pin_collinear_x", (0.0, 0.0), (2.0, 0.0), (1.0, 0.0), "ZERO", "on segment")) + v.append(Vec("pin_collinear_diag", (0.0, 0.0), (2.0, 2.0), (1.0, 1.0), "ZERO", "diagonal")) + # Near-collinear at moderate scale + v.append( + Vec( + "near_collinear_1e-8", + (0.0, 0.0), + (1.0, 0.0), + (0.5, 1e-8), + "POS", + "slightly above segment", + ) + ) + v.append( + Vec( + "near_collinear_1e-12", + (0.0, 0.0), + (1.0, 0.0), + (0.5, 1e-12), + None, + "may be filter-uncertain", + ) + ) + # Large magnitude (filter stress; exact still defined) + s = 1e8 + v.append( + Vec( + "large_ccw", + (0.0, 0.0), + (s, 0.0), + (0.0, s), + "POS", + "homothetic CCW", + ) + ) + # JTS-style nearly collinear at ~1e6 (common DD fallback band) + v.append( + Vec( + "jts_style_near_col", + (2089426.5233462777, 1180182.3877339689), + (2085646.6891757075, 1195618.7333999649), + (2099870.0, 1141480.0), + None, + "near-collinear geographic-scale sample", + ) + ) + # Integer-regime pins (corpus sound_small_int) + v.append(Vec("int_tri", (0.0, 0.0), (4.0, 0.0), (0.0, 3.0), "POS", "3-4-5 area")) + v.append(Vec("int_vertex", (0.0, 0.0), (4.0, 0.0), (0.0, 0.0), "ZERO", "q = a")) + return v + + +def resolve_oracle_cmd(args: argparse.Namespace) -> List[str]: + 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 resolve_ffi_probe(args: argparse.Namespace) -> Optional[List[str]]: + if args.ffi_probe: + return [args.ffi_probe] + if args.wsl_ffi_probe: + return ["wsl.exe", "-e", args.wsl_ffi_probe] + env = os.environ.get("FFI_PROBE") + if env and os.path.isfile(env): + return [env] + local = os.path.join(os.path.dirname(__file__), "ffi_probe") + if os.path.isfile(local): + return [local] + return None + + +def run_orient_exact(oracle_cmd: Sequence[str], a: Point, b: Point, q: Point) -> str: + payload = ( + "ORIENT_EXACT\n" + f"{a[0]} {a[1]}\n" + f"{b[0]} {b[1]}\n" + f"{q[0]} {q[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()}" + ) + line = proc.stdout.strip().splitlines()[-1].strip() + # POS / NEG / ZERO / NAN + tok = line.split()[0].upper() + if tok in ("POS", "NEG", "ZERO", "NAN"): + return tok + raise RuntimeError(f"bad ORIENT_EXACT output: {line!r}") + + +def run_ffi_filtered( + probe_cmd: Sequence[str], a: Point, b: Point, q: Point +) -> Tuple[int, float]: + """ffi_probe ORIENT_FILTERED → (sign_code, orient2d bits as float via hex).""" + payload = f"{a[0]} {a[1]} {b[0]} {b[1]} {q[0]} {q[1]}\n" + proc = subprocess.run( + list(probe_cmd) + ["ORIENT_FILTERED"], + input=payload, + 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()}" + ) + # "1 #3ff0000000000000" or "3 #..." + parts = proc.stdout.strip().split() + code = int(parts[0]) + bits_hex = parts[1].lstrip("#") + import struct + + val = struct.unpack(">d", bytes.fromhex(bits_hex.zfill(16)))[0] + return code, val + + +def code_to_sign(code: int) -> str: + return {1: "POS", -1: "NEG", 0: "ZERO", 2: "NAN", 3: "UNCERTAIN"}.get( + code, f"CODE{code}" + ) + + +def main() -> int: + ap = argparse.ArgumentParser(description=__doc__) + ap.add_argument("--oracle", help="Path to oracle_bin") + ap.add_argument("--wsl-oracle", help="Linux path via wsl.exe -e") + ap.add_argument("--ffi-probe", help="Optional path to ffi_probe") + ap.add_argument("--wsl-ffi-probe", help="Optional Linux ffi_probe via wsl") + ap.add_argument( + "--out", + default=os.path.join(os.path.dirname(__file__), "jts1093_orient_vectors.txt"), + ) + args = ap.parse_args() + + oracle_cmd = resolve_oracle_cmd(args) + ffi_cmd = resolve_ffi_probe(args) + + # Sanity: ORIENT_EXACT on unit CCW + try: + pin = run_orient_exact(oracle_cmd, (0.0, 0.0), (1.0, 0.0), (0.0, 1.0)) + except Exception as e: + print(f"FATAL: oracle unavailable ({oracle_cmd}): {e}", file=sys.stderr) + return 2 + if pin != "POS": + print(f"FATAL: ORIENT_EXACT pin failed: {pin} (expected POS)", file=sys.stderr) + return 2 + print(f"Oracle ORIENT_EXACT pin OK: {pin} via {oracle_cmd}") + if ffi_cmd: + try: + c, _ = run_ffi_filtered(ffi_cmd, (0.0, 0.0), (1.0, 0.0), (0.0, 1.0)) + print(f"FFI ORIENT_FILTERED pin: code={c} ({code_to_sign(c)}) via {ffi_cmd}") + except Exception as e: + print(f"WARN: FFI probe failed (continuing without FFI): {e}") + ffi_cmd = None + else: + print("FFI probe: (none — oracle-only)") + + vecs = corpus_vectors() + lines = [ + "# JTS #1093 Ozaki orientation filter scout", + "# topic: precision epic: #66", + f"# OZAKI_K = {OZAKI_K!r}", + f"# CCWERRBOUND_A (Shewchuk) = {CCWERRBOUND_A!r}", + "# Columns: name EXACT OZAKI_SIGN/CERT SHEW_SIGN/CERT FFI_FILT note", + "#", + ] + + n_ozaki_conflict = 0 + n_shew_conflict = 0 + n_ozaki_unc = 0 + n_shew_unc = 0 + n_ozaki_tighter = 0 # Ozaki CERTAIN, Shewchuk UNCERTAIN + n_shew_tighter = 0 + n_expected_fail = 0 + failures: List[str] = [] + + for vec in vecs: + exact = run_orient_exact(oracle_cmd, vec.a, vec.b, vec.q) + o_sign, o_det, o_cert = stage_a_ozaki(vec.a, vec.b, vec.q) + s_sign, s_det, s_cert = stage_a_shewchuk(vec.a, vec.b, vec.q) + + if not o_cert: + n_ozaki_unc += 1 + if not s_cert: + n_shew_unc += 1 + if o_cert and not s_cert: + n_ozaki_tighter += 1 + if s_cert and not o_cert: + n_shew_tighter += 1 + + if o_cert and exact in ("POS", "NEG") and o_sign != exact: + n_ozaki_conflict += 1 + failures.append(f"{vec.name}: Ozaki CERTAIN {o_sign} vs exact {exact}") + if s_cert and exact in ("POS", "NEG") and s_sign != exact: + n_shew_conflict += 1 + failures.append(f"{vec.name}: Shewchuk CERTAIN {s_sign} vs exact {exact}") + + if vec.expected is not None and exact != vec.expected: + if not (vec.expected == "ZERO" and exact == "ZERO"): + n_expected_fail += 1 + failures.append(f"{vec.name}: EXPECTED {vec.expected} exact {exact}") + + ffi_s = "-" + if ffi_cmd: + try: + code, _ = run_ffi_filtered(ffi_cmd, vec.a, vec.b, vec.q) + ffi_s = code_to_sign(code) + except Exception as e: + ffi_s = f"ERR:{e}" + + lines.append( + f"{vec.name}\tEXACT={exact}\t" + f"OZAKI={o_sign}/{'CERT' if o_cert else 'UNC'}\t" + f"SHEW={s_sign}/{'CERT' if s_cert else 'UNC'}\t" + f"FFI_FILT={ffi_s}\t# {vec.note}" + ) + + with open(args.out, "w", encoding="utf-8") as f: + f.write("\n".join(lines) + "\n") + + print(f"Vectors: {len(vecs)} → {args.out}") + print(f"EXPECTED pin failures: {n_expected_fail}") + print(f"Ozaki CERTAIN vs exact conflicts: {n_ozaki_conflict}") + print(f"Shewchuk CERTAIN vs exact conflicts: {n_shew_conflict}") + print(f"Ozaki UNCERTAIN: {n_ozaki_unc} Shewchuk UNCERTAIN: {n_shew_unc}") + print(f"Ozaki tighter (CERT while Shew UNCERTAIN): {n_ozaki_tighter}") + print(f"Shewchuk tighter (CERT while Ozaki UNCERTAIN): {n_shew_tighter}") + 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/jts1093_orient_vectors.txt b/oracle/jts1093_orient_vectors.txt new file mode 100644 index 00000000..6b194431 --- /dev/null +++ b/oracle/jts1093_orient_vectors.txt @@ -0,0 +1,16 @@ +# JTS #1093 Ozaki orientation filter scout +# topic: precision epic: #66 +# OZAKI_K = 3.3306690621773724e-16 +# CCWERRBOUND_A (Shewchuk) = 3.3306690738754716e-16 +# Columns: name EXACT OZAKI_SIGN/CERT SHEW_SIGN/CERT FFI_FILT note +# +pin_ccw_unit EXACT=POS OZAKI=POS/CERT SHEW=POS/CERT FFI_FILT=POS # area +1/2 +pin_cw_unit EXACT=NEG OZAKI=NEG/CERT SHEW=NEG/CERT FFI_FILT=NEG # area -1/2 +pin_collinear_x EXACT=ZERO OZAKI=ZERO/CERT SHEW=ZERO/CERT FFI_FILT=ZERO # on segment +pin_collinear_diag EXACT=ZERO OZAKI=ZERO/UNC SHEW=ZERO/UNC FFI_FILT=ZERO # diagonal +near_collinear_1e-8 EXACT=POS OZAKI=POS/CERT SHEW=POS/CERT FFI_FILT=POS # slightly above segment +near_collinear_1e-12 EXACT=POS OZAKI=POS/CERT SHEW=POS/CERT FFI_FILT=POS # may be filter-uncertain +large_ccw EXACT=POS OZAKI=POS/CERT SHEW=POS/CERT FFI_FILT=POS # homothetic CCW +jts_style_near_col EXACT=NEG OZAKI=NEG/CERT SHEW=NEG/CERT FFI_FILT=NEG # near-collinear geographic-scale sample +int_tri EXACT=POS OZAKI=POS/CERT SHEW=POS/CERT FFI_FILT=POS # 3-4-5 area +int_vertex EXACT=ZERO OZAKI=ZERO/CERT SHEW=ZERO/CERT FFI_FILT=ZERO # q = a diff --git a/oracle/scout_incircle_ffi.ml b/oracle/scout_incircle_ffi.ml index 12762dcf..ce4cd827 100644 --- a/oracle/scout_incircle_ffi.ml +++ b/oracle/scout_incircle_ffi.ml @@ -5,8 +5,9 @@ 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. + Prefer full `libntsrocq` after `./scripts/rebuild_oracle_ffi.sh` + (docs/ffi-rungs-2026-08.md). This scout remains a thin fallback when + extract is stale (missing e.g. `b64_orient2d_exact`). Bit-identity with oracle_bin is the same construction as Phase 5: one extracted symbol, two call paths (subprocess protocol vs C ABI). diff --git a/scripts/rebuild_oracle_ffi.sh b/scripts/rebuild_oracle_ffi.sh new file mode 100644 index 00000000..1ebe829a --- /dev/null +++ b/scripts/rebuild_oracle_ffi.sh @@ -0,0 +1,60 @@ +#!/usr/bin/env bash +# Rebuild oracle/extracted.ml + oracle_bin + libntsrocq (Phase 5 FFI). +# +# Requires: Rocq 9.x, Flocq, ocamlfind/ocamlopt, a compiled theories-flocq/ +# dependency closure for Validate_binary64_extract.v (and its Requires). +# +# Usage (repo root): +# ./scripts/rebuild_oracle_ffi.sh +# ./scripts/rebuild_oracle_ffi.sh --parity # also run ffi-parity gate +# +# extracted.ml is gitignored; this script is the supported refresh path after +# the b64_orient2d_exact gap (see docs/ffi-rungs-2026-08.md). + +set -euo pipefail + +ROOT="$(cd "$(dirname "$0")/.." && pwd)" +cd "$ROOT" + +PARITY=0 +for arg in "$@"; do + case "$arg" in + --parity) PARITY=1 ;; + -h|--help) + sed -n '2,14p' "$0" + exit 0 + ;; + esac +done + +if ! command -v coqc >/dev/null 2>&1; then + echo "error: coqc not on PATH" >&2 + exit 2 +fi + +echo "==> Extraction: theories-flocq/Validate_binary64_extract.v" +coqc -Q theories NTS.Proofs -Q theories-flocq NTS.Proofs.Flocq \ + theories-flocq/Validate_binary64_extract.v + +if ! grep -q 'b64_orient2d_exact' oracle/extracted.ml; then + echo "error: extracted.ml missing b64_orient2d_exact after extract" >&2 + exit 1 +fi +echo " OK: b64_orient2d_exact present in oracle/extracted.ml" + +echo "==> make -C oracle (oracle_bin)" +make -C oracle + +echo "==> make -C oracle ffi (libntsrocq + ffi_probe)" +make -C oracle ffi + +echo "==> smoke: ORIENT_EXACT via ffi_probe" +printf '0 0\n1 0\n0 1\n' | oracle/ffi_probe ORIENT_EXACT +echo + +if [[ "$PARITY" -eq 1 ]]; then + echo "==> make -C oracle ffi-parity" + make -C oracle ffi-parity +fi + +echo "Done. See docs/ffi-rungs-2026-08.md"