build-oracle.yml

name: Build and publish oracle_bin

# Build the standalone `oracle_bin` (the RocqRefRunner used by
# NetTopologySuite.Curve's differential-test harness) and publish it as a
# GHA artifact on every push to main.  On release events the same binary
# is attached to the release as a downloadable asset, giving .Curve's CI
# a stable URL to consume.
#
# Toolchain pin: reuses the project's Dockerfile `toolchain` stage
# (rocq 9.2.0 + ocaml 4.14.2-flambda + coq-flocq.4.2.2 + ocamlfind),
# pulled from GHCR under its Dockerfile-hash tag (published by ci.yml on
# main pushes) with a buildx + GHA-layer-cache fallback on a miss, so
# the slow `opam install coq-flocq.4.2.2` step is not repeated.
#
# SPEED (June 2026): PULL REQUESTS reuse the incremental corpus cache
# that ci.yml maintains (.vo artefacts + sha256 manifest;
# scripts/ci_invalidate_stale_vo.py makes make's mtime logic sound
# against it by content).  This job is a STRICTLY READ-ONLY cache
# consumer: it never saves the cache and never writes the manifest,
# because it does not run the axiom audit or refresh the .palog/
# chunks -- a cache saved here could pair a fresh manifest with stale
# Print Assumptions chunks and silently weaken ci.yml's guardrail 4.
# Main pushes and release events skip the restore entirely: the
# PUBLISHED oracle_bin always comes from a full from-clean build.
# `Validate_binary64_extract.v` (a leaf: nothing imports it) is touched
# after the invalidation pass so the extraction always re-runs and
# oracle/extracted.ml is always regenerated fresh.

on:
  push:
    branches: [main]
    paths:
      - 'oracle/**'
      - 'theories-flocq/**'
      - '_CoqProject.full'
      - 'Dockerfile'
      - '.github/workflows/build-oracle.yml'
  # Gate `oracle/driver.ml` (the RocqRefRunner sources) on PRs into main.
  # Without this trigger the oracle is only compiled AFTER merge to main:
  # ci.yml never runs `make -C oracle/`, so a syntax/type error in a new
  # driver mode (e.g. CLOTHOID_INTERSECT) would otherwise reach main
  # unvalidated.  Same `paths:` filter as the push trigger keeps the slow
  # container build off PRs that don't touch the oracle/flocq corpus.
  pull_request:
    branches: [main]
    paths:
      - 'oracle/**'
      - 'theories-flocq/**'
      - '_CoqProject.full'
      - 'Dockerfile'
      - '.github/workflows/build-oracle.yml'
  workflow_dispatch:
  release:
    types: [published]

# Opt into Node.js 24 for JavaScript actions (actions/checkout,
# actions/upload-artifact, docker/* actions etc.).  GitHub Actions
# deprecated the Node.js 20 runtime on 2025-09-19 and forces Node.js 24
# as the default on 2026-06-02; setting this flag now silences the
# transitional deprecation warning and verifies the workflow runs
# cleanly on the new runtime before the cutover.  See
# https://github.blog/changelog/2025-09-19-deprecation-of-node-20-on-github-actions-runners/
env:
  FORCE_JAVASCRIPT_ACTIONS_TO_NODE24: "true"

jobs:
  build-oracle:
    name: Build oracle_bin in pinned rocq 9.2.0 + flocq 4.2.2 container
    # Skip standalone-package releases (robust-predicates-v* / spatial-algebra-v*):
    # those are published by the package-*.yml workflows and have nothing to do
    # with oracle_bin.  Without this guard, every package release triggers this
    # job and its release-attach step fails ("Resource not accessible by
    # integration" -- this job only has contents: read), reding the release.
    if: >-
      github.event_name != 'release' ||
      (!startsWith(github.event.release.tag_name, 'robust-predicates-v') &&
       !startsWith(github.event.release.tag_name, 'spatial-algebra-v'))
    runs-on: ubuntu-latest
    permissions:
      contents: read
      packages: read
    env:
      TOOLCHAIN_IMAGE: ghcr.io/${{ github.repository_owner }}/nts-proofs-toolchain
    steps:
      - uses: actions/checkout@v6

      - name: Compute toolchain tag (content-addressed by Dockerfile)
        id: toolchain
        run: echo "tag=df-$(sha256sum Dockerfile | cut -c1-16)" >> "$GITHUB_OUTPUT"

      - name: Log in to GHCR
        continue-on-error: true
        uses: docker/login-action@v3
        with:
          registry: ghcr.io
          username: ${{ github.actor }}
          password: ${{ secrets.GITHUB_TOKEN }}

      - name: Pull toolchain image from GHCR
        # Publishing is ci.yml's job (it runs on EVERY main push); this
        # workflow only consumes the tag, with a local build fallback.
        id: pull
        run: |
          if docker pull "$TOOLCHAIN_IMAGE:${{ steps.toolchain.outputs.tag }}"; then
            docker tag "$TOOLCHAIN_IMAGE:${{ steps.toolchain.outputs.tag }}" nts-proofs-oracle:ci
            echo "hit=true" >> "$GITHUB_OUTPUT"
          else
            echo "hit=false" >> "$GITHUB_OUTPUT"
          fi

      - name: Set up Docker Buildx
        if: steps.pull.outputs.hit != 'true'
        uses: docker/setup-buildx-action@v3

      - name: Build toolchain image (GHCR miss)
        # Only when the Dockerfile changed (or the tag was never
        # published).  The GHA layer cache is shared with ci.yml's
        # `rocq-flocq` job, so the slow `opam install coq-flocq.4.2.2`
        # step (~5 min cold) is not repeated.
        if: steps.pull.outputs.hit != 'true'
        uses: docker/build-push-action@v6
        with:
          context: .
          target: toolchain
          load: true
          tags: nts-proofs-oracle:ci
          cache-from: type=gha
          cache-to: type=gha,mode=max

      - name: Restore compiled-corpus cache (PRs only)
        # READ-ONLY reuse of the cache ci.yml maintains.  Main pushes
        # and releases skip this: the published oracle_bin is always
        # built from clean (artifact provenance).  See the header
        # comment for why this job must never SAVE the cache.
        if: github.event_name == 'pull_request'
        uses: actions/cache/restore@v4
        with:
          path: |
            theories/*.vo*
            theories/*.glob
            theories/.*.aux
            theories-flocq/*.vo*
            theories-flocq/*.glob
            theories-flocq/.*.aux
            .palog
            .vo-manifest
          key: vo-cache-${{ hashFiles('Dockerfile') }}-${{ github.run_id }}
          restore-keys: |
            vo-cache-${{ hashFiles('Dockerfile') }}-

      - name: Invalidate stale artefacts (content-addressed)
        # Same script as ci.yml: ages unchanged .v files / touches
        # changed ones by sha256 so make rebuilds exactly the changed
        # files plus dependents.  No-op on a cold cache.
        run: python3 scripts/ci_invalidate_stale_vo.py

      - name: Force extraction freshness
        # Validate_binary64_extract.v is a leaf (nothing imports it);
        # touching it AFTER the invalidation pass guarantees the
        # extraction target always re-runs, so oracle/extracted.ml and
        # .mli are regenerated from the (cached or rebuilt) dependency
        # chain on every run.  extracted.ml is gitignored -- it never
        # exists before the build.
        run: touch theories-flocq/Validate_binary64_extract.v

      - name: Build corpus, extract, link oracle_bin
        # Inside the pinned container, on the MOUNTED live checkout
        # (cached .vo files are visible to make; oracle_bin lands
        # directly in the runner workspace -- no docker cp dance):
        #   1. Clean host-leaked makefile artefacts (NOT .vo -- those
        #      are the incremental cache).
        #   2. rocq makefile -f _CoqProject.full -o Makefile.gen.
        #   3. make -- rebuilds changed files + dependents + the touched
        #      extraction leaf, which writes oracle/extracted.ml + .mli.
        #   4. make -C oracle/ -- links extracted.cmx + driver.cmx
        #      against -package str (ocamlfind is baked into the
        #      toolchain image).
        # chmod lets the image's `rocq` user (uid 1000) write into
        # runner-owned dirs; the chown hands the artefacts back.
        run: |
          chmod -R a+rwX .
          docker run --rm -v "$PWD:/workspace" -w /workspace \
            nts-proofs-oracle:ci \
            bash -lc '
              set -euxo pipefail
              rm -f Makefile.gen Makefile.gen.conf .Makefile.d .Makefile.gen.d \
                    .nra.cache
              rocq makefile -f _CoqProject.full -o Makefile.gen
              make -f Makefile.gen -j"$(nproc)"
              test -f oracle/extracted.ml
              test -f oracle/extracted.mli
              make -C oracle/
              test -x oracle/oracle_bin
              make -C oracle/ ffi
              test -f oracle/libntsrocq.so
              test -x oracle/ffi_probe
            '
          sudo chown -R "$(id -u):$(id -g)" .

      - name: Sanity check artifact
        run: |
          test -x oracle/oracle_bin
          file oracle/oracle_bin
          ls -la oracle/oracle_bin
          test -f oracle/libntsrocq.so
          file oracle/libntsrocq.so
          ls -la oracle/libntsrocq.so

      - name: FFI parity gate (libntsrocq == oracle_bin, bit for bit)
        # Phase 5: the in-process C ABI and the stdin/stdout oracle protocol
        # call the SAME extracted code, so any divergence is a marshalling bug
        # (argument order, enum encoding, truncated result list).  Doubles are
        # compared as raw IEEE 754 bit patterns.  Nonzero exit on any '!!'.
        run: |
          docker run --rm -v "$PWD:/workspace" -w /workspace \
            nts-proofs-oracle:ci \
            bash -lc '
              set -euxo pipefail
              python3 oracle/gen_ffi_parity_tests.py
            '

      - name: Run oracle gated-invariant tests
        # Runs each oracle test generator that gates proven invariants.
        # oracle/oracle_bin was just built and is at the expected path.
        # Nonzero exit on any '!!' invariant violation fails the build.
        run: |
          ORACLE_BIN=oracle/oracle_bin python3 oracle/gen_winding_number_tests.py \
            > oracle/winding_number_tests.txt
          ORACLE_BIN=oracle/oracle_bin python3 oracle/gen_disc_overlay_tests.py \
            > oracle/disc_overlay_tests.txt
          ORACLE_BIN=oracle/oracle_bin python3 oracle/gen_lec_circle_tests.py \
            > oracle/lec_circle_tests.txt
          ORACLE_BIN=oracle/oracle_bin python3 oracle/gen_obstacle_distance_tests.py \
            > oracle/obstacle_distance_tests.txt
          ORACLE_BIN=oracle/oracle_bin python3 oracle/gen_arc_distance_tests.py \
            > oracle/arc_distance_tests.txt
          ORACLE_BIN=oracle/oracle_bin python3 oracle/gen_i_circular_tests.py \
            > oracle/i_circular_tests.txt
          ORACLE_BIN=oracle/oracle_bin python3 oracle/gen_ieee_oracle_bridge_tests.py \
            > oracle/ieee_oracle_bridge_run.txt

      - name: Upload oracle_bin artifact (90-day retention)
        uses: actions/upload-artifact@v4
        with:
          name: oracle-bin-linux
          path: oracle/oracle_bin
          retention-days: 90

      - name: Upload libntsrocq artifact (90-day retention)
        # Phase 5: the in-process native library + its ABI header, so the
        # NetTopologySuite.Curve consumer can bind it without rebuilding the
        # corpus.  Linux x64 only for now (the runner's architecture).
        uses: actions/upload-artifact@v4
        with:
          name: libntsrocq-linux-x64
          path: |
            oracle/libntsrocq.so
            oracle/nts_ffi.h
          retention-days: 90

      - name: Attach oracle_bin to release (release events only)
        if: github.event_name == 'release'
        uses: softprops/action-gh-release@v2
        with:
          files: |
            oracle/oracle_bin
            oracle/libntsrocq.so
            oracle/nts_ffi.h