verify.yml

# SPDX-License-Identifier: MPL-2.0
# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
#
# verify.yml — the foundation CI that CANNOT be taken out by another repository.
#
# WHY THIS EXISTS
# ---------------
# `rust-ci.yml`, `governance.yml`, `hypatia-scan.yml` and `secret-scanner.yml`
# are thin wrappers over reusable workflows in `hyperpolymath/standards`. That
# is the estate's intended shape, and it stays. But every one of those gates is
# only as available as the callee's Actions "Access" setting and this repo's
# allowlist permit at that instant. On 2026-10-25 all four died before their
# first job (`failure`, zero jobs, no log), and with them went the only
# build/test signal that did not depend on a foreign repository.
#
# So the guarantees that must never be absent live here, on actions this repo
# pins itself:
#
#   fmt        formatting is not a matter of taste in review
#   clippy     `-D warnings` — the repo's zero-warning policy, enforced
#   test       the suite, with the feature matrix that ships
#   doc        every public item is documented and the docs build
#   coverage-self-scan   the tool's own coverage ledger is honest
#
# The reusable-wrapper gates stay as the estate's richer checks (audit,
# coverage upload, Hypatia SARIF). This one is the floor.

name: Verify

on:
  pull_request:
    branches: ['**']
  push:
    branches: [main, master, develop]
  workflow_dispatch:

permissions:
  contents: read

concurrency:
  group: verify-${{ github.ref }}
  cancel-in-progress: true

env:
  CARGO_TERM_COLOR: always
  CARGO_INCREMENTAL: '0'
  RUST_BACKTRACE: '1'

jobs:
  entrypoints:
    name: Installation entrypoint controls
    runs-on: ubuntu-latest
    timeout-minutes: 5
    steps:
      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1  # v7.0.1
        with:
          persist-credentials: false
      - name: Verify pinned task runner and exercise isolated entrypoints
        shell: bash
        run: |
          set -euo pipefail
          tools_dir=$(mktemp -d)
          trap 'rm -rf "$tools_dir"' EXIT
          archive=just-1.36.0-x86_64-unknown-linux-musl.tar.gz
          curl --fail --silent --show-error --location --max-time 60 \
            "https://github.com/casey/just/releases/download/1.36.0/$archive" \
            --output "$tools_dir/$archive"
          (cd "$tools_dir" && printf '%s  %s\n' \
            bc7c9f377944f8de9cd0418b11d2955adebfa25a488c0b5e3dd2d2c0e9d732da "$archive" | sha256sum --check)
          tar --no-same-owner -xzf "$tools_dir/$archive" -C "$tools_dir" just
          JUST_BIN="$tools_dir/just" bash scripts/ci/test-entrypoints.sh

  fmt:
    name: cargo fmt --check
    runs-on: ubuntu-latest
    timeout-minutes: 10
    steps:
      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1  # v7.0.1
        with:
          persist-credentials: false
      - uses: dtolnay/rust-toolchain@683b588c487a69d01f6c6ddf40f036ff682cc2c8  # v1
        with:
          toolchain: stable
          components: rustfmt
      - name: Format
        run: bash scripts/ci/annotate.sh rustfmt -- cargo fmt --all -- --check

  clippy:
    name: cargo clippy -D warnings
    runs-on: ubuntu-latest
    timeout-minutes: 25
    steps:
      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1  # v7.0.1
        with:
          persist-credentials: false
      - uses: dtolnay/rust-toolchain@683b588c487a69d01f6c6ddf40f036ff682cc2c8  # v1
        with:
          toolchain: stable
          components: clippy
      - uses: Swatinem/rust-cache@d1527c8f67ef9af357290475d4af4b0fab8f12e0  # v2.9.3
      # `gui` is deliberately excluded: eframe/egui needs system libraries this
      # job does not install, and the GUI is opt-in. Everything else is checked.
      - name: Clippy
        run: bash scripts/ci/annotate.sh clippy -- cargo clippy --locked --all-targets --features http,sarif,signing -- -D warnings

  test:
    name: cargo test (${{ matrix.features }})
    runs-on: ubuntu-latest
    timeout-minutes: 30
    strategy:
      fail-fast: false
      matrix:
        include:
          - features: ''                    # default: offline, zero-network build
            cache-suffix: default
          - features: http                  # exact feature set used by bridge-gate consumers
            cache-suffix: http
          - features: http,sarif             # Patch Bridge + SARIF
            # A cache key may not contain a comma (Swatinem/rust-cache rejects
            # it at startup of the step), so the matrix carries its own label.
            cache-suffix: http-sarif
    steps:
      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1  # v7.0.1
        with:
          persist-credentials: false
      - uses: dtolnay/rust-toolchain@683b588c487a69d01f6c6ddf40f036ff682cc2c8  # v1
        with:
          toolchain: stable
      - uses: Swatinem/rust-cache@d1527c8f67ef9af357290475d4af4b0fab8f12e0  # v2.9.3
        with:
          key: features-${{ matrix.cache-suffix }}
      # `--locked` is a gate in itself: the lockfile must agree with Cargo.toml
      # in the commit under test, or the artefact CI verified is not the
      # artefact released.
      - name: Test
        run: |
          set -euo pipefail
          if [ -n "${{ matrix.features }}" ]; then
            bash scripts/ci/annotate.sh "tests[${{ matrix.features }}]" -- \
              cargo test --locked --features "${{ matrix.features }}"
          else
            bash scripts/ci/annotate.sh "tests[default]" -- cargo test --locked
          fi

  msrv:
    name: MSRV (rust-version in Cargo.toml)
    runs-on: ubuntu-latest
    timeout-minutes: 20
    steps:
      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1  # v7.0.1
        with:
          persist-credentials: false
      - name: Read rust-version
        id: msrv
        run: |
          set -euo pipefail
          msrv="$(sed -n 's/^rust-version *= *"\(.*\)"/\1/p' Cargo.toml | head -1)"
          [ -n "$msrv" ] || { echo "::error::Cargo.toml declares no rust-version"; exit 1; }
          echo "toolchain=$msrv" >> "$GITHUB_OUTPUT"
          echo "MSRV declared: $msrv"
      - uses: dtolnay/rust-toolchain@683b588c487a69d01f6c6ddf40f036ff682cc2c8  # v1
        with:
          toolchain: ${{ steps.msrv.outputs.toolchain }}
      - uses: Swatinem/rust-cache@d1527c8f67ef9af357290475d4af4b0fab8f12e0  # v2.9.3
        with:
          key: msrv
      - name: MSRV check
        run: bash scripts/ci/annotate.sh msrv -- cargo check --locked --all-targets

  docs:
    name: cargo doc (no broken intra-doc links)
    runs-on: ubuntu-latest
    timeout-minutes: 20
    env:
      RUSTDOCFLAGS: -D warnings
    steps:
      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1  # v7.0.1
        with:
          persist-credentials: false
      - uses: dtolnay/rust-toolchain@683b588c487a69d01f6c6ddf40f036ff682cc2c8  # v1
        with:
          toolchain: stable
      - uses: Swatinem/rust-cache@d1527c8f67ef9af357290475d4af4b0fab8f12e0  # v2.9.3
        with:
          key: docs
      - name: Docs
        run: bash scripts/ci/annotate.sh rustdoc -- cargo doc --locked --no-deps --features http,sarif,signing

  coverage-ledger:
    name: Coverage ledger is honest (--fail-on-incomplete)
    runs-on: ubuntu-latest
    timeout-minutes: 25
    steps:
      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1  # v7.0.1
        with:
          persist-credentials: false
      - uses: dtolnay/rust-toolchain@683b588c487a69d01f6c6ddf40f036ff682cc2c8  # v1
        with:
          toolchain: stable
      - uses: Swatinem/rust-cache@d1527c8f67ef9af357290475d4af4b0fab8f12e0  # v2.9.3
        with:
          key: coverage-ledger
      - name: Build
        run: cargo build --locked --release
      # A scan of a tree whose every file has an adapter must be `complete`.
      # This is the CI use of --fail-on-incomplete: a green here means the
      # declared inventory was actually analysed, not that no file was found.
      - name: Complete-coverage fixture must scan complete
        run: |
          set -euo pipefail
          mkdir -p /tmp/ph-ok/src
          printf '<?php\nfunction f($x) { return strlen($x); }\n' > /tmp/ph-ok/src/a.php
          printf 'fn main() { let s = "x"; println!("{}", s); }\n' > /tmp/ph-ok/src/main.rs
          ./target/release/panic-attack assail /tmp/ph-ok \
            --output /tmp/ph-ok.json --fail-on-incomplete --quiet
          python3 - <<'PY'
          import json
          report = json.load(open('/tmp/ph-ok.json'))
          coverage = report['coverage']
          assert coverage['status'] == 'complete', coverage['status']
          assert coverage['analyzed_files'] == coverage['candidate_files'] >= 2, coverage
          print(f"coverage={coverage['status']} files={coverage['analyzed_files']}")
          PY
      # An unparseable PHP file is a coverage GAP, not a silent pass, and the
      # process must say so with exit 2 after writing the report.
      - name: Malformed input must exit 2 with a written report
        run: |
          set -euo pipefail
          mkdir -p /tmp/ph-bad/src
          printf '<?php function broken( {\n' > /tmp/ph-bad/src/broken.php
          set +e
          ./target/release/panic-attack assail /tmp/ph-bad \
            --output /tmp/ph-bad.json --fail-on-incomplete --quiet
          code=$?
          set -e
          [ "$code" -eq 2 ] || { echo "::error::expected exit 2 for incomplete coverage, got $code"; exit 1; }
          [ -s /tmp/ph-bad.json ] || { echo "::error::report was not written before exit"; exit 1; }
          python3 - <<'PY'
          import json
          coverage = json.load(open('/tmp/ph-bad.json'))['coverage']
          assert coverage['status'] != 'complete', coverage['status']
          assert any(i.get('status') not in ('analyzed', 'excluded') for i in coverage['inputs']), coverage
          print(f"coverage={coverage['status']} (gap recorded)")
          PY

  # The generation-publish protocol (src/publish.rs) is model-checked with TLC,
  # PROOF-POLICY §4's worked exception for concurrency protocols. Results are
  # TESTED with the bounds in each .cfg, never PROVEN. Every config states its
  # expected outcome; the expected violations (the documented mirror limit and
  # three mutants) show the invariants can fail.
  #
  # Deviation (PROOF-POLICY §6), state: open. Leg: protocol model check. Tool:
  # tla2tools.jar v1.7.4 (TLC 2.19), SHA-256 below, checked by check.sh. Why not
  # Guix or the container: neither provides TLC yet. Java comes from the runner.
  tlaplus:
    name: TLA+ model check (GenerationPublish)
    runs-on: ubuntu-latest
    timeout-minutes: 20
    steps:
      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1  # v7.0.1
        with:
          persist-credentials: false
      - name: Fetch the pinned TLC and model-check every config
        shell: bash
        run: |
          set -euo pipefail
          java -version
          tools_dir=$(mktemp -d)
          trap 'rm -rf "$tools_dir"' EXIT
          curl --fail --silent --show-error --location --max-time 120 \
            https://github.com/tlaplus/tlaplus/releases/download/v1.7.4/tla2tools.jar \
            --output "$tools_dir/tla2tools.jar"
          TLA2TOOLS="$tools_dir/tla2tools.jar" bash verification/proofs/tlaplus/check.sh