Load the shared RocqRefRunner JTS↔NTS equivalence vectors.

Pin Java refSign to the Proofs corpus that NTS also loads
(oracle/rocqref/jts_nts_equiv_vectors.txt).

Co-authored-by: jbloemscheer <jbloemscheer@gmail.com>

Author: cursoragent

modules/core/src/test/java/org/locationtech/jts/algorithm/RocqRefRunnerTest.java

@@ -34,6 +34,13 @@ public class RocqRefRunnerTest extends TestCase {
   private static final String PROOF_VECTORS_RESOURCE =
       "/org/locationtech/jts/algorithm/rocqref/orientation_proof_vectors.txt";
 
+  /**
+   * Shared JTS ↔ NTS RocqRefRunner corpus from
+   * {@code NetTopologySuite.Proofs/oracle/rocqref/jts_nts_equiv_vectors.txt}.
+   */
+  private static final String JTS_NTS_EQUIV_RESOURCE =
+      "/org/locationtech/jts/algorithm/rocqref/jts_nts_equiv_vectors.txt";
+
   public static void main(String[] args) {
     TestRunner.run(RocqRefRunnerTest.class);
   }
@@ -109,6 +116,24 @@ public void testExportedProofVectors() throws Exception {
     }
   }
 
+  /**
+   * The catalyst port-equivalence gate: Java {@link RocqRefRunner#refSign}
+   * must match the Coq {@code rocqref_refSign} signs shipped in the shared
+   * Proofs corpus (the same file NTS loads).
+   */
+  public void testJtsNtsEquivVectors() throws Exception {
+    InputStream in = getClass().getResourceAsStream(JTS_NTS_EQUIV_RESOURCE);
+    assertNotNull("shared JTS↔NTS RocqRefRunner vectors missing", in);
+    try {
+      List<RocqRefRunner.RefCase> cases = RocqRefRunner.loadProofCases(in);
+      assertTrue("shared equiv corpus is empty", cases.size() > 0);
+      RocqRefRunner.Result r = RocqRefRunner.run(cases);
+      assertTrue("JTS disagrees with RocqRefRunner JTS↔NTS vectors:\n" + r, r.isSound());
+    } finally {
+      in.close();
+    }
+  }
+
   private static long rndIn(Random rnd, long bound) {
     long span = 2 * bound + 1;
     return Math.floorMod(rnd.nextLong(), span) - bound;

modules/core/src/test/resources/org/locationtech/jts/algorithm/rocqref/jts_nts_equiv_vectors.txt

@@ -0,0 +1,35 @@
+# Shared RocqRefRunner JTS ↔ NTS equivalence vectors.
+# Provenance: theories/RocqRefRunner.v
+#   rocqref_refSign_eq_cross
+#   rocqref_idet_fits_int64
+#
+# Format (whitespace-separated; '#' comments and blank lines ignored):
+#   p0x p0y  p1x p1y  qx qy  expected
+# expected in {-1, 0, 1}: -1 = CW, 0 = collinear, +1 = CCW.
+# Every coordinate is an integer in [-2^25, 2^25] (RocqRefRunner.SAFE_BOUND).
+# The expected sign is Z.sgn of the integer 2x2 determinant — the algorithm
+# both language ports implement. Production Orientation.index is NOT the
+# reference; these rows pin the ports to each other and to the Qed formula.
+
+# --- unit turns (locked Examples in RocqRefRunner.v) ---
+0 0    1 0    0 1     1
+0 0    1 0    0 -1   -1
+0 0    2 2    1 1     0
+
+# --- basic / JTS RocqRefRunnerTest resource ---
+0 0    0 1    1 0    -1
+0 0    4 2    2 1     0
+-33554432 -33554432   33554432 33554432   0 0   0
+
+# --- near-collinear (one unit off a long diagonal) ---
+0 0    1000000 1000000   1000001 1000000   -1
+0 0    1000000 1000000   1000000 1000001    1
+
+# --- domain boundary (largest representable determinants) ---
+33554432 33554432    -33554432 -33554432    33554432 -33554432    1
+-33554432 33554432    33554432 -33554432    33554431 -33554432   -1
+
+# --- coincident / zero-length ---
+0 0    0 0    1 1     0
+5 5    5 5    5 5     0
+3 4    3 4    0 0     0