ci.yml

name: build proofs

# For CI / Quality Gatekeeper (formerly CI Cara): see docs/HELP.md + docs/READING-GUIDE.md (Quality Gatekeeper card)
# for the full path. The registries and scripts/check_* are the core.

on:
  push:
    branches: [main]
  pull_request:
    branches: [main]
  workflow_dispatch:

# Opt into Node.js 24 for JavaScript actions (actions/checkout,
# 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:
  guards:
    # Build-INDEPENDENT corpus guardrails, split into their own job so
    # registry / doc / allowlist drift fails in ~seconds and IN PARALLEL
    # with the proof builds, instead of gating behind the multi-minute
    # macOS `theories/` compile (where these used to run as trailing
    # steps).  Every script here is pure grep/perl/python and scans the
    # SOURCE tree (both theories/ and theories-flocq/), so it needs no
    # `.vo` and no `rocq`.  Reproduce locally with `make ci-guards`.
    name: Corpus guardrails (build-independent)
    runs-on: ubuntu-latest
    # Pure grep/perl/python; seconds in practice. A low ceiling turns a hung
    # script into a fast, clear failure instead of a 6h default-timeout stall.
    timeout-minutes: 10
    steps:
      - uses: actions/checkout@v6

      - name: Run all corpus guardrails (make ci-guards)
        # Covers, in one fast pass (see the per-script headers for detail):
        #   check_admitted               two-tier Admitted registry
        #   check_readme_axioms          README <-> axiom-allowlist sync
        #   check_deferred_registry_sync doc <-> Admitted-registry drift
        #   validate-claims              verified-claims.md references resolve
        #   check_oracle_handrolled      hand-rolled float-kernel ratchet
        #   hunt.py --selfcheck          RELATE_MATRIX token allowlist (no oracle)
        # The macOS `rocq` job below no longer repeats these — this job is
        # the single source of the guardrail verdict on every PR and push.
        run: make ci-guards

  rocq:
    name: Build with Rocq ${{ matrix.rocq-version }}
    # Gate the (slow, paid-runner) build on the fast guardrails: a
    # registry/doc/allowlist failure skips this job entirely instead of
    # burning a full macOS compile, and keeps the guardrail verdict a
    # hard prerequisite of this build even though it now lives in its own
    # job (so branch protection on this build still implies guards pass).
    needs: guards
    runs-on: macos-latest
    # A full theories/ build is well under this; the ceiling caps a runaway.
    timeout-minutes: 60
    strategy:
      fail-fast: false
      matrix:
        rocq-version: ['9.2.0']
    steps:
      - uses: actions/checkout@v6

      - name: Install Rocq via Homebrew
        # Bottled install ~30s; caching the Cellar misses Homebrew's
        # config files under /opt/homebrew/etc/, which breaks ocamlfind.
        # Easier to install fresh each run.
        run: brew install rocq

      - name: Show Rocq version
        id: rocqv
        # Capture the ACTUAL installed version: `brew install rocq` is
        # unpinned, so the .vo cache key must track what Homebrew shipped
        # (not the cosmetic matrix string) or a compiler bump would try to
        # load version-incompatible cached .vo.
        run: |
          rocq -v
          echo "ver=$(rocq --version | head -1 | tr -cd '[:alnum:].-')" >> "$GITHUB_OUTPUT"

      - name: Restore theories/ .vo cache (PRs only)
        # PR == "theories-quick": restore the previous run's .vo + manifest so
        # only changed files + dependents recompile.  Pushes to main skip this
        # and build "theories-full" from clean, re-seeding the cache — the
        # integrity anchor (every merge revalidates the whole lane).
        if: github.event_name == 'pull_request'
        uses: actions/cache/restore@v4
        with:
          path: |
            theories/*.vo*
            theories/*.glob
            theories/.*.aux
            .vo-manifest-theories
          key: theories-vo-${{ steps.rocqv.outputs.ver }}-${{ github.run_id }}
          restore-keys: |
            theories-vo-${{ steps.rocqv.outputs.ver }}-

      - name: Generate Makefile (parity with container + docs)
        # Use the same modern driver + .gen naming as the container job,
        # Dockerfile, README, and the committed convenience Makefile.
        # Never write to plain "Makefile" — that is the safe committed
        # convenience layer (make help, make host, etc.).
        run: rocq makefile -f _CoqProject -o Makefile.gen

      - name: Invalidate stale artefacts (content-addressed, theories/ lane)
        # Same content-addressed pass as the flocq job, pointed at the
        # Stdlib-only project + its own manifest: ages unchanged .v so make
        # skips them, touches changed/new ones so make rebuilds them + their
        # dependents.  No-op on a cold cache (main, or first PR run).
        run: |
          CI_VO_PROJECT=_CoqProject CI_VO_MANIFEST=.vo-manifest-theories \
            python3 scripts/ci_invalidate_stale_vo.py

      - name: Build proofs
        # Parallel + output-sync for readable logs (matches container job).
        # This job now does exactly one thing — compile the Stdlib-only
        # `theories/` lane end to end.  The build-independent guardrails
        # run separately in the `guards` job above (fast, parallel), and
        # the Admitted scan there covers this lane's sources too.
        run: make -f Makefile.gen -j"$(sysctl -n hw.ncpu)" --output-sync=target || make -f Makefile.gen -j"$(sysctl -n hw.ncpu)"

      - name: Refresh theories/ manifest
        # Only reached when the build passed: records the content hash of every
        # host-lane .v so the next PR run's invalidation is sound.
        run: |
          CI_VO_PROJECT=_CoqProject CI_VO_MANIFEST=.vo-manifest-theories \
            python3 scripts/ci_write_vo_manifest.py

      - name: Save theories/ .vo cache
        uses: actions/cache/save@v4
        with:
          path: |
            theories/*.vo*
            theories/*.glob
            theories/.*.aux
            .vo-manifest-theories
          key: theories-vo-${{ steps.rocqv.outputs.ver }}-${{ github.run_id }}

  rocq-flocq:
    # Container-based build of the Flocq-dependent corpus
    # (`theories-flocq/`).  The host-runner `rocq` job above only builds
    # `theories/` -- it grep-scans `theories-flocq/` for the corpus
    # invariant but does not compile those files.  This job closes that
    # gap using the project's pinned toolchain (Rocq 9.2.0 + opam
    # `coq-flocq.4.2.2`, see Dockerfile) to build `_CoqProject.full`.
    #
    # SPEED ARCHITECTURE (June 2026):
    #
    #   - The toolchain image (Dockerfile `--target toolchain`, no
    #     sources baked in) is published to GHCR under a tag derived
    #     from the Dockerfile's hash; runs pull it (~seconds) instead of
    #     reassembling layers from the buildx cache.  A miss (new
    #     Dockerfile) falls back to building it, and main pushes publish
    #     the new tag.
    #   - PULL REQUESTS build INCREMENTALLY: .vo artefacts, per-file
    #     Print Assumptions chunks (.palog/), and a content manifest are
    #     cached; scripts/ci_invalidate_stale_vo.py ages unchanged .v
    #     files and touches changed/new ones (sha256-based -- immune to
    #     rebase-backdated commit times), so make rebuilds exactly the
    #     changed files plus their dependents.
    #   - MAIN PUSHES always build from clean (the restore step is
    #     skipped): every merge re-validates the whole corpus end to end
    #     and re-seeds the cache.
    #
    # GUARDRAIL-4 SOUNDNESS UNDER INCREMENTALITY: the audit no longer
    # reads the raw build log (an incremental log only covers rebuilt
    # files).  Instead, the output-synced log -- each target's `ROCQ
    # compile <file>` line plus its `Print Assumptions` blocks emitted
    # atomically -- is split into per-file chunks cached alongside the
    # .vo they were compiled with (same provenance).  The audit runs on
    # the assembled chunks of EVERY project file, and a missing chunk
    # FAILS the build (scripts/ci_assemble_palog.sh), so coverage can
    # never silently shrink.  History: the May 2026 axiom-leak
    # investigation showed plain parallel logs interleave; output-sync
    # removes that at the root (the old -j1 rebuild is gone).
    name: Build theories-flocq in pinned container
    # Same fast-fail gate as the `rocq` job: don't spin up the container
    # build (toolchain pull + incremental corpus compile + axiom audit)
    # when a build-independent guardrail already failed.
    needs: guards
    runs-on: ubuntu-latest
    # Cold path (toolchain build + full corpus + audit) fits comfortably;
    # the ceiling turns a hang into a clear failure well before GitHub's 6h.
    timeout-minutes: 90
    permissions:
      contents: read
      packages: write
    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
        id: pull
        run: |
          if docker pull "$TOOLCHAIN_IMAGE:${{ steps.toolchain.outputs.tag }}"; then
            docker tag "$TOOLCHAIN_IMAGE:${{ steps.toolchain.outputs.tag }}" nts-proofs-flocq: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 buildx GHA layer cache still shortcuts the
        # slow `opam install coq-flocq.4.2.2` step (~5 min cold).
        if: steps.pull.outputs.hit != 'true'
        uses: docker/build-push-action@v6
        with:
          context: .
          target: toolchain
          load: true
          tags: nts-proofs-flocq:ci
          cache-from: type=gha
          cache-to: type=gha,mode=max

      - name: Publish toolchain image (main only)
        # Content-addressed tag: republishing only happens when the
        # Dockerfile actually changed.  PRs that change the Dockerfile
        # build locally; the tag is published on merge.
        if: steps.pull.outputs.hit != 'true' && github.event_name == 'push' && github.ref == 'refs/heads/main'
        run: |
          docker tag nts-proofs-flocq:ci "$TOOLCHAIN_IMAGE:${{ steps.toolchain.outputs.tag }}"
          docker push "$TOOLCHAIN_IMAGE:${{ steps.toolchain.outputs.tag }}"

      - name: Restore compiled-corpus cache (PRs only)
        # Main pushes skip this on purpose: every merge rebuilds the
        # corpus from clean and re-seeds the cache (integrity anchor).
        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)
        # Ages unchanged .v files / touches changed ones so make's
        # mtime logic agrees with actual content; wipes everything if
        # the _CoqProject.full flag lines changed; prunes artefacts and
        # chunks of files that left the project.  No-op on a cold cache.
        run: python3 scripts/ci_invalidate_stale_vo.py

      - name: Compile corpus (mounted workspace, output-synced)
        # The live checkout is mounted over the image's /workspace, so
        # cached .vo files are visible to make and new artefacts land on
        # the runner for the cache-save step.  chmod lets the image's
        # `rocq` user (uid 1000) write into runner-owned dirs; the chown
        # afterwards hands the artefacts back to the runner user.
        run: |
          chmod -R a+rwX .
          docker run --rm -v "$PWD:/workspace" -w /workspace \
            nts-proofs-flocq:ci \
            bash -lc '
              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)" --output-sync=target
            ' > /tmp/build_sync.log 2>&1 || {
              echo "::error::Corpus build failed; see /tmp/build_sync.log"
              grep -nE 'Error:|File "\./theories|Cannot find witness|Unable to unify|No primitive equality' \
                /tmp/build_sync.log | head -80 || true
              echo "----- tail -----"
              tail -80 /tmp/build_sync.log
              exit 1
            }
          sudo chown -R "$(id -u):$(id -g)" .

      - name: Smoke hunt probes (docs/h1-vacuity)
        # Qed-claiming hunt probes live next to the H1 pair and are
        # evidence, not _CoqProject.full product modules.  Compile them
        # here so a probe that claims Qed is a checked fact (Print
        # Assumptions lands in this step's log).
        run: |
          set -o pipefail
          chmod -R a+rwX .
          docker run --rm -v "$PWD:/workspace" -w /workspace \
            nts-proofs-flocq:ci \
            bash -lc 'bash scripts/hunt_probe_smoke.sh' \
            | tee /tmp/hunt_probe_smoke.log
          sudo chown -R "$(id -u):$(id -g)" .

      - name: Update per-file Print Assumptions chunks
        run: bash scripts/ci_update_palog.sh /tmp/build_sync.log

      - name: Per-theorem axiom audit on full-corpus chunk assembly (guardrails 1 + 4)
        # scripts/ci_assemble_palog.sh fails hard if ANY project file
        # lacks a chunk -- audit coverage cannot silently shrink.  The
        # audit enforces docs/axiom-allowlist.txt against every
        # per-theorem PA block, with file-level exemptions from
        # docs/audit-exceptions.txt.
        run: |
          bash scripts/ci_assemble_palog.sh > /tmp/audit_input.log
          # Hunt probes are off _CoqProject.full; their smoke PA must
          # still hit the allowlist / audit-exceptions gate.
          cat /tmp/hunt_probe_smoke.log >> /tmp/audit_input.log
          bash scripts/audit_axioms.sh /tmp/audit_input.log

      - name: Refresh corpus manifest
        # Only reached when build + audit passed: the manifest never
        # blesses artefacts that failed the gauntlet.
        run: python3 scripts/ci_write_vo_manifest.py

      - name: Save compiled-corpus cache
        uses: actions/cache/save@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 }}