grootstebozewolf · grootstebozewolf · Aug 5, 2026 · Aug 5, 2026
diff --git a/docs/ffi-rungs-2026-08.md 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
@@ -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
@@ -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
@@ -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.