V-CP and V-CS: tests with hunter for counterexamples + impl hardening

.github/workflows/auto-rebase-upstream.yml

@@ -0,0 +1,274 @@
+name: Auto-rebase saga branches
+
+# Two-stage scheduled rebase chain.
+#
+# Stage 1 ("rebase-master"): rebase this fork's master onto
+#   locationtech/jts:master, force-push on success, open/update a
+#   "Auto-rebase conflict on master" issue on failure.
+#
+# Stage 2 ("rebase-saga", matrix, needs: stage 1): for every saga
+#   branch in the matrix, rebase onto the (now upstream-current) fork
+#   master, force-push on success, open/update a per-branch conflict
+#   issue on failure. Branches run in parallel; one branch's conflict
+#   doesn't block the others (fail-fast: false).
+#
+# RULE-OUT spike branches (F-CP-spike-optionB, F-CP-spike-optionC) are
+# intentionally NOT in the matrix — they're frozen records of failed
+# experiments and force-pushing would erase the audit trail. Add them
+# below if you decide they should follow master.
+#
+# All knobs are in the env block; the matrix list below is the second
+# place to edit when the saga grows.
+
+on:
+  schedule:
+    - cron: '0 6 * * *'   # 06:00 UTC daily
+  workflow_dispatch:       # manual trigger from the Actions tab
+
+permissions:
+  contents: write
+  issues: write
+
+env:
+  UPSTREAM_REPO: locationtech/jts
+  UPSTREAM_BRANCH: master
+  CONFLICT_LABEL: upstream-rebase-conflict
+
+jobs:
+  # ---------------------------------------------------------------
+  # Stage 1: fork master  <-  locationtech/jts:master
+  # ---------------------------------------------------------------
+  rebase-master:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout master with full history
+        uses: actions/checkout@v4
+        with:
+          ref: master
+          fetch-depth: 0
+          token: ${{ secrets.GITHUB_TOKEN }}
+
+      - name: Configure git identity
+        run: |
+          git config user.name  "github-actions[bot]"
+          git config user.email "41898282+github-actions[bot]@users.noreply.github.com"
+
+      - name: Add upstream remote and fetch
+        run: |
+          git remote remove upstream 2>/dev/null || true
+          git remote add upstream "https://github.com/${UPSTREAM_REPO}.git"
+          git fetch upstream "${UPSTREAM_BRANCH}"
+
+      - name: Attempt rebase
+        id: rebase
+        run: |
+          set +e
+          git rebase "upstream/${UPSTREAM_BRANCH}"
+          RC=$?
+          if [ $RC -ne 0 ]; then
+            CONFLICTS=$(git diff --name-only --diff-filter=U)
+            git rebase --abort
+            {
+              echo "status=conflict"
+              echo "conflicts<<EOF"
+              echo "$CONFLICTS"
+              echo "EOF"
+            } >> "$GITHUB_OUTPUT"
+            exit 0
+          fi
+          echo "status=clean" >> "$GITHUB_OUTPUT"
+
+      - name: Force-push if ahead of origin
+        if: steps.rebase.outputs.status == 'clean'
+        run: |
+          if ! git diff --quiet origin/master..HEAD; then
+            git push --force-with-lease origin HEAD:master
+          fi
+
+      - name: Ensure conflict label exists
+        if: steps.rebase.outputs.status == 'conflict'
+        env:
+          GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+        run: |
+          gh label create "${CONFLICT_LABEL}" \
+            --description "Auto-rebase against ${UPSTREAM_REPO} hit a conflict" \
+            --color "B60205" \
+          || true
+
+      - name: Open or update master conflict issue
+        if: steps.rebase.outputs.status == 'conflict'
+        env:
+          GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+          CONFLICTS: ${{ steps.rebase.outputs.conflicts }}
+        run: |
+          UPSTREAM_SHA=$(git rev-parse "upstream/${UPSTREAM_BRANCH}")
+          TITLE_PREFIX="Auto-rebase conflict on master"
+          BODY_FILE=$(mktemp)
+          cat > "$BODY_FILE" <<EOF
+          The scheduled rebase of \`master\` onto \`upstream/${UPSTREAM_BRANCH}\` (${UPSTREAM_REPO}) hit a conflict and was aborted. \`master\` is unchanged.
+
+          **Upstream HEAD:** \`${UPSTREAM_SHA}\`
+          **Workflow run:** ${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}
+
+          **Conflicting paths:**
+          \`\`\`
+          ${CONFLICTS}
+          \`\`\`
+
+          Resolve locally:
+          \`\`\`
+          git fetch upstream
+          git checkout master
+          git rebase upstream/${UPSTREAM_BRANCH}
+          # resolve files, then:
+          git add -A && git rebase --continue
+          git push --force-with-lease origin master
+          \`\`\`
+
+          This issue auto-updates on each subsequent failed run. Close it once the rebase has been resolved manually.
+          EOF
+          EXISTING=$(gh issue list \
+            --label "${CONFLICT_LABEL}" \
+            --state open \
+            --search "${TITLE_PREFIX}" \
+            --json number,title \
+            --jq ".[] | select(.title | startswith(\"${TITLE_PREFIX}\")) | .number" \
+            | head -1)
+          if [ -n "$EXISTING" ]; then
+            gh issue comment "$EXISTING" --body-file "$BODY_FILE"
+          else
+            gh issue create \
+              --title "${TITLE_PREFIX} ($(date -u +%Y-%m-%d))" \
+              --label "${CONFLICT_LABEL}" \
+              --body-file "$BODY_FILE"
+          fi
+
+  # ---------------------------------------------------------------
+  # Stage 2: every saga branch  <-  fork master
+  # Runs after stage 1 so each saga branch sees the freshly updated
+  # master. fail-fast: false so one branch's conflict doesn't block
+  # the others.
+  # ---------------------------------------------------------------
+  rebase-saga:
+    needs: rebase-master
+    runs-on: ubuntu-latest
+    strategy:
+      fail-fast: false
+      matrix:
+        branch:
+          - feature/sfa-curve-AT-NS-spike
+          - feature/sfa-curve-F-CP-spike
+          - feature/sfa-curve-F-CP-spike-optionA
+          - feature/sfa-curve-F-MC-F-MS-spike
+          - feature/sfa-curve-PRC-SN-spike
+          - feature/sfa-curve-R-EQ-spike
+          - feature/sfa-curve-buffer-spike
+          - feature/sfa-curve-clothoid-playground
+          - feature/sfa-curve-compoundcurve-members
+          - feature/sfa-curve-extension-points
+          - feature/sfa-curve-multisurface-function
+          - feature/sfa-curve-testbuilder-ui
+          - feature/sfa-curve-tin-tool
+          - feature/sfa-curve-toLinear-densification
+          - feature/sfa-curve-triangle-tool
+    steps:
+      - name: Checkout ${{ matrix.branch }}
+        uses: actions/checkout@v4
+        with:
+          ref: ${{ matrix.branch }}
+          fetch-depth: 0
+          token: ${{ secrets.GITHUB_TOKEN }}
+
+      - name: Configure git identity
+        run: |
+          git config user.name  "github-actions[bot]"
+          git config user.email "41898282+github-actions[bot]@users.noreply.github.com"
+
+      - name: Fetch latest master
+        run: git fetch origin master
+
+      - name: Attempt rebase onto origin/master
+        id: rebase
+        run: |
+          set +e
+          git rebase origin/master
+          RC=$?
+          if [ $RC -ne 0 ]; then
+            CONFLICTS=$(git diff --name-only --diff-filter=U)
+            git rebase --abort
+            {
+              echo "status=conflict"
+              echo "conflicts<<EOF"
+              echo "$CONFLICTS"
+              echo "EOF"
+            } >> "$GITHUB_OUTPUT"
+            exit 0
+          fi
+          echo "status=clean" >> "$GITHUB_OUTPUT"
+
+      - name: Force-push if ahead of origin
+        if: steps.rebase.outputs.status == 'clean'
+        run: |
+          BRANCH="${{ matrix.branch }}"
+          if ! git diff --quiet "origin/${BRANCH}..HEAD"; then
+            git push --force-with-lease origin "HEAD:${BRANCH}"
+          fi
+
+      - name: Ensure conflict label exists
+        if: steps.rebase.outputs.status == 'conflict'
+        env:
+          GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+        run: |
+          gh label create "${CONFLICT_LABEL}" \
+            --description "Auto-rebase against ${UPSTREAM_REPO} hit a conflict" \
+            --color "B60205" \
+          || true
+
+      - name: Open or update conflict issue for ${{ matrix.branch }}
+        if: steps.rebase.outputs.status == 'conflict'
+        env:
+          GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+          CONFLICTS: ${{ steps.rebase.outputs.conflicts }}
+          BRANCH: ${{ matrix.branch }}
+        run: |
+          MASTER_SHA=$(git rev-parse origin/master)
+          TITLE_PREFIX="Auto-rebase conflict on ${BRANCH}"
+          BODY_FILE=$(mktemp)
+          cat > "$BODY_FILE" <<EOF
+          The scheduled rebase of \`${BRANCH}\` onto fresh \`origin/master\` hit a conflict and was aborted. \`${BRANCH}\` is unchanged.
+
+          **Master HEAD:** \`${MASTER_SHA}\`
+          **Workflow run:** ${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}
+
+          **Conflicting paths:**
+          \`\`\`
+          ${CONFLICTS}
+          \`\`\`
+
+          Resolve locally:
+          \`\`\`
+          git fetch origin
+          git checkout ${BRANCH}
+          git rebase origin/master
+          # resolve files, then:
+          git add -A && git rebase --continue
+          git push --force-with-lease origin ${BRANCH}
+          \`\`\`
+
+          This issue auto-updates on each subsequent failed run. Close it once the rebase has been resolved manually.
+          EOF
+          EXISTING=$(gh issue list \
+            --label "${CONFLICT_LABEL}" \
+            --state open \
+            --search "${TITLE_PREFIX}" \
+            --json number,title \
+            --jq ".[] | select(.title | startswith(\"${TITLE_PREFIX}\")) | .number" \
+            | head -1)
+          if [ -n "$EXISTING" ]; then
+            gh issue comment "$EXISTING" --body-file "$BODY_FILE"
+          else
+            gh issue create \
+              --title "${TITLE_PREFIX} ($(date -u +%Y-%m-%d))" \
+              --label "${CONFLICT_LABEL}" \
+              --body-file "$BODY_FILE"
+          fi

EPIC_PROGRESS_OVERVIEW.md

@@ -0,0 +1,84 @@
+# Curve Awareness Epic — Progress Overview
+
+**Epic source:** the full text in the user query (to be lifted as `EPIC_SFA_CURVE_AWARENESS.md` or GitHub Epic body).  
+**Date of this overview:** 2026-06-03 (post latest artifact processing + RGR/hardening).  
+**Live meter:** `CurveAwarenessSpecTest` (46–50 red `test_*` methods; run with `-Dtest=CurveAwarenessSpecTest`; delete methods on ship per §5/11).  
+**Current branch (last work):** `feature/sfa-curve-V-CP-rgr` (V-CP arc-aware CurvePolygon.isValid; self-intersect, orientation, holes).  
+**Key infra:** `CurveRefRunner` + `CurveAdversarialTest` (RocqRefRunner pattern from #1197), vectors in `src/test/resources/.../rocqref/`, proofs artifacts (NetTopologySuite.Proofs runs), Flocq/Rocq oracles.
+
+## High-level Status (Phases per epic §9)
+
+- **Phase 1 (Foundations):** F-CP / F-MC / F-MS **landed** (structural CurvePolygon with LineString/CompoundCurve/CircularString rings per Option A + SPEC_F_CP.md; MultiCurve/MultiSurface subtype-preserving; copy/toLinear/WKT/reader/writer/getExteriorCurve etc.; early FCP tests removed from CurvePolygonStructuralSpec, DOVE + EQ doc tests remain). F-RD **green impl on RGR branch** (CurvedShapeWriter added with structural ring walking + CircularString arc sampling for visual curves in Shapes; verification test passes; red TAG marker + no GeometryPainter/ShapeWriter hook integration yet per "don't integrate yet").
+- **Phase 2 (Properties):** 
+  - M-LEN-CS **landed + hardened**.
+  - M-LEN-CC **landed** (sums via structural members + CircularString analytical).
+  - B-CP / B-MS **landed + hardened**.
+  - B-CC **landed** (explicit guard override on CompoundCurve asserting standard lineal open/closed boundary rules).
+  - V-CP **landed** (CurvePolygon.isValid arc-aware: ring isSimple, sector orientation, hole containment approx).
+  - M-AREA-CP / M-DIM / V-CP / V-CS **red** (area with segment correction, dim guards, validity for curves not yet).
+- **Phases 3–7:** Almost entirely **red** (no production changes for distance/centroid/buffer/overlay/noding/polygonizer/snap/tri/TestBuilder etc.). N-AA has **foundation hardening** (see below). Some core-touching TAGs (N-*, PLG, PRC-SN, DSF) still untouched per §6.
+- **Early cross-cutting fixes (pre-RGR, from user reports + review):** COMPOUNDCURVE member-structured WKT emission (non-flat "( ( " form), outer-ring-only Z/M dimension in CurvedWKT*, structural curves excluded from equalsExact (with test_FCP_EQ... documenting view-based + isEquivalentClass; epic §7 risk).
+
+**RGR discipline followed:** New branch per TAG (or cluster), red-first (seam docs in meter methods), green (minimal impl + verification in *StructuralSpec or adversarial, meter fail untouched), refactor (readability/soundness). Meter methods + fail("TAG:") lines never edited green.
+
+## Hardening Status (RocqRefRunner + Proofs Artifacts)
+
+"Hardening" = dedicated adversarial tests using:
+- CurveRefRunner (modeled on RocqRefRunner: Case classes, load*Cases that cross-validate claimed vs Java oracle on load, Result with isSound(), run(Iterable) that exercises the *impl*).
+- Vectors baked from (or citing) NetTopologySuite.Proofs GHA artifacts (run with oracle_bin ARC_* / ORIENT modes + b64 extracted oracles; stand-ins + py port of exact fn when direct 404/auth needed; headers always cite exact run/artifact URL).
+- Asserts in CurveAdversarialTest (load + isSound() + hunter mains for "search effective (current fails)").
+- Ties to recent RGR (length/boundary) or future (N-AA arc primitives).
+
+**Marked as HARDENED (with links in code/comments):**
+
+- **M-LEN-CS** (and supporting length infra): 
+  - Full: `testLoadArcLengthVectors` (load + validate + `CurveRefRunner.run(cases); assert r.isSound()`), `testHunterFindsArcLengthDeviationsOnAdversarialInputs` (post-M-LEN-CS hunter finds 0), `testKnownNearFlatCaseFromVectorsDeviatesUnderLinearImpl` (vector case verification).
+  - Vectors: `curve_arc_length_vectors.txt` (headers cite multiple proofs runs + #64 ArcLength.v + b64_circular_arc_length; additional cases appended for 26856051962 via py port of `exactCircularArcLength`).
+  - Oracle in CurveRefRunner + private exact fn (r*theta after circumcenter + sweep disambig; matches proofs).
+  - Also exercised `CircularString.getLength()` (analytical, not chord) + `CurveCounterexampleHunter`.
+
+- **B-CP / B-MS** (boundary):
+  - `testCurveBoundaryHardeningUsingRocqRefRunner` (builds CP + mixed MS via CurvedWKTReader; calls getBoundary(); uses local `refSign` (naive orient) + orientation vectors on the curve control points of the returned boundary members; asserts !=0 and presence).
+  - Vectors: `orientation_proof_vectors.txt` (headers updated for 26800356316 + fresh oracle_bin from 26856051962; supports predicate/boundary hardening).
+  - Ties directly to the RGR boundary seams (getBoundary overrides, MultiCurve return, orient preservation on control pts per proofs).
+
+- **N-AA foundation (arc–arc / chord–circle primitives for future noding/overlay/validity):**
+  - New from processing the provided artifact URL: `testLoadArcChordCrossVectorsFromOracleBinArtifact` (load + mix of TRUE/FALSE + `CurveRefRunner.runChordCross(cases); assert r.isSound()`).
+  - New support in CurveRefRunner: `ArcChordCrossCase`, `chordCrossesArcCircle` (ref using `TrianglePredicate.isInCircleRobust` sign-product, matching proofs hand-rolled), `loadArcChordCrossCases`, `ChordCrossResult`, `runChordCross`.
+  - Vectors: `curve_arc_chord_cross_vectors.txt` (freshly generated by driving the downloaded `oracle_bin` (from run 26856051962 / artifact 7373024936) with ARC_CHORD_CROSSES_CIRCLE mode + cases; headers cite exact URL + Proofs#64 + ArcIntersectIVT.v; load validates claimed oracle vs Java ref).
+  - This bin (oracle-bin-linux) was the direct output of the given artifact; supports ARC_CHORD_CROSSES_CIRCLE + ARC_PASSES_THROUGH_PIXEL + ORIENT (ARC_LENGTH added in proofs post-this-run).
+
+**General / supporting:**
+- Orientation vectors load test (`testLoadAndValidateOrientationVectorsUsingRocqRefRunnerPattern`) updated with both runs + oracle_bin note.
+- All vectors updated with the 26856051962 citation during latest "hardening using RocqRefRunner" pass.
+- Pattern ready for more (D-*, V-*, BUF-*, R-*, OV etc.): add Case/Result/run + vectors + assert in adversarial, wire into TAG RGR when green lands.
+
+**No hardening yet for:** everything else (BUF_*, D-*, C-*, V-*, S-*, AT-*, LRF-*, DSF, TRI-*, PLG, COV, PRC-SN, TB-*, R-*, OV, N-AL/N-SS (N-AA only via chord), M-AREA etc.). M-LEN-CC can reuse existing arc-length vectors for future hardening. More proofs artifacts will feed the rest (see proofs-first-batch/01-arc-primitives.md which refs JTS#1195 + M-LEN-*/V-CP/N-* + this exact hardening pattern).
+
+## Cross-refs to Epic Sections
+- Matches §4 (spike landed items), §5 (meter + delete-on-ship + TAG PR convention), §6 (core touch list; only N-*/PLG/PRC-SN/DSF/F-RD would), §7 (risks noted in red tests + structural spec for FCP-DOVE + R-EQ).
+- RGR examples in the red-test javadocs for M-LEN-CS / B-CP / B-MS exactly follow "red test first: identify interface/arch seams, green simplest, refactor readability/soundness".
+- Artifact processing (this query URL + priors) directly fulfills repeated "Use RocqRefRunner to create adverserial tests Artifact download URL..." + "hardening using RocqRefRunner" requests.
+- Proofs issues batch + triage + Flocq build (prior turns) feed the oracles.
+
+## Next (suggested, per epic order + pending in history)
+- Continue RGR on low-risk remaining Phase 2 (M-AREA-CP, V-CS, M-DIM guard). V-CP done (with B-CC etc).
+- Wire more vectors/hunter into new TAGs (e.g. once N-AA utility lands, use chord-cross vectors + hunter for arc-arc cases).
+- F-RD (TestBuilder + CurvedShapeWriter full).
+- When core seams (Phase 5 N-SS etc.) ready, open the WKB sibling epic per §3.
+- Full meter empty = epic DoD #1.
+
+## Files touched for this overview + recent hardening
+- `modules/curved/src/test/java/org/locationtech/jts/spec/curveawareness/CurveAwarenessSpecTest.java` (progress header table + M-LEN-CC notes)
+- `modules/curved/src/main/java/org/locationtech/jts/geom/curved/CompoundCurve.java` (M-LEN-CC getLength + B-CC getBoundary guard + V-CP isSimple support + prior structural)
+- `modules/curved/src/main/java/org/locationtech/jts/io/curved/CurvedWKTWriter.java` (member-tagged CC emission)
+- `modules/curved/src/test/java/org/locationtech/jts/geom/curved/CompoundCurveMembersTest.java` (B-CC + M-LEN-CC verification tests)
+- `modules/curved/src/main/java/org/locationtech/jts/geom/curved/CircularString.java` (V-CP arc helpers + B-CC isSimple)
+- `modules/curved/src/main/java/org/locationtech/jts/geom/curved/CurvePolygon.java` (V-CP isValid + sector checks)
+- `modules/curved/src/test/java/org/locationtech/jts/spec/curveawareness/CurvePolygonStructuralSpec.java` (V-CP verifications)
+- `modules/curved/src/test/java/org/locationtech/jts/geom/curved/adversarial/CurveRefRunner.java` + `CurveAdversarialTest.java` (chord cross + latest artifact citations)
+- `.../rocqref/*.txt` (headers + cases for 26856051962)
+
+Run `mvn -pl modules/curved test -Dtest=CurveAdversarialTest` (or full with excludes) to exercise all hardening. The spec meter is intentionally excluded from default CI (§11).
+
+This overview can be merged into the root EPIC_*.md when created.