ci.yml

name: CI

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

# Cancel an in-flight CI run if a newer commit lands on the same ref.
# This dedupes user-push storms (rapid commits to a PR or main).
concurrency:
  group: ci-${{ github.workflow }}-${{ github.ref }}
  cancel-in-progress: true

env:
  CARGO_TERM_COLOR: always
  CARGO_INCREMENTAL: 0
  # `RUSTFLAGS: -D warnings` is applied per-step in the `rust` job below
  # rather than globally — the napi-rs binding crate has macro-generated
  # FFI items that trip pedantic-tier lints that don't apply to FFI
  # surfaces.

# Skip CI on PR sync events from the release-plz bot. Rationale:
#   - User pushes commit to main → CI runs on push (verifies the change).
#   - release-plz auto-updates its release PR with version bumps + changelog
#     entries on top of that commit → would re-trigger CI on pull_request
#     synchronize, but the only diff vs the just-tested main is mechanical
#     (Cargo.toml version, CHANGELOG.md additions) — testing it is redundant.
#   - After PR merge, push of "chore: release vX.Y.Z" to main runs CI again
#     (verifies the merged release state before release-plz publishes).
# Trade-off: if release-plz ever produces a broken Cargo.toml/CHANGELOG (e.g.
# malformed semver), we'd catch it post-merge instead of pre-merge. Acceptable
# since release-plz output is mechanical and the post-merge run still gates
# the publish step in release.yml.
#
# Applied as a per-job `if:` because GitHub Actions doesn't support workflow-
# level conditional triggering by author. The expression below excludes ONLY
# bot-authored PR-sync events; everything else (user push, user PR, etc.)
# runs normally.

jobs:
  # ---------------------------------------------------------------------
  # Rust: check + test + clippy + fmt + cargo-deny on the pinned 1.95
  # toolchain (workspace `rust-toolchain.toml`). Excludes binding crates
  # from `cargo test`/`cargo build` via workspace `default-members` —
  # they need their own toolchains (napi-rs, maturin, wasm-pack) and
  # land separately in the binding-specific jobs below.
  # ---------------------------------------------------------------------
  rust:
    name: Rust ${{ matrix.toolchain }}
    if: "${{ (github.event_name != 'pull_request' || github.actor != 'graphrefly-write-content[bot]') && (github.event_name != 'push' || !startsWith(github.event.head_commit.message, 'chore: release')) }}"
    runs-on: ubuntu-latest
    strategy:
      fail-fast: false
      matrix:
        toolchain: ["1.95"]
    steps:
      - uses: actions/checkout@v5

      - name: Install Rust toolchain
        uses: dtolnay/rust-toolchain@stable
        with:
          toolchain: ${{ matrix.toolchain }}
          components: rustfmt, clippy

      - name: Cache cargo registry + target
        uses: Swatinem/rust-cache@v2
        with:
          shared-key: rust-${{ matrix.toolchain }}

      - name: Cargo fmt --check
        run: cargo fmt --all -- --check

      - name: Cargo check (default-members)
        run: cargo check
        env:
          RUSTFLAGS: "-D warnings"

      - name: Cargo clippy (default-members, all targets, pedantic-tier)
        run: cargo clippy --all-targets -- -D warnings

      - name: Cargo test (default-members)
        run: cargo test --all-targets
        env:
          RUSTFLAGS: "-D warnings"

      - name: Cargo doc (no deps; catches broken intra-doc links)
        run: cargo doc --no-deps
        env:
          # `-D warnings` keeps real doc errors fatal (unparseable doc, missing
          # docs on must-document items, etc.) but allows the three noisy
          # doc-link lint families that pre-1.0 internal modules legitimately
          # trigger:
          #   - private_intra_doc_links: links from public docs to private
          #     items (informative for maintainers, fine for pre-1.0).
          #   - broken_intra_doc_links: typos / unresolved paths in doc
          #     comments. Should be cleaned up but isn't blocking.
          #   - redundant_explicit_links: explicit target same as label.
          # Tightening these to deny is a separate doc-quality slice (track
          # in `docs/porting-deferred.md` if/when prioritized).
          RUSTDOCFLAGS: "-D warnings -A rustdoc::private_intra_doc_links -A rustdoc::broken_intra_doc_links -A rustdoc::redundant_explicit_links"

  # ---------------------------------------------------------------------
  # Supply-chain audit via cargo-deny — license allowlist, advisory
  # database, version-unification warnings. Pinned action version so
  # `cargo install cargo-deny` doesn't recompile from source on every
  # CI run.
  # ---------------------------------------------------------------------
  deny:
    name: cargo deny (supply-chain audit)
    if: "${{ (github.event_name != 'pull_request' || github.actor != 'graphrefly-write-content[bot]') && (github.event_name != 'push' || !startsWith(github.event.head_commit.message, 'chore: release')) }}"
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v5
      - uses: EmbarkStudios/cargo-deny-action@v2
        with:
          command: check
          arguments: --all-features

  # ---------------------------------------------------------------------
  # napi-rs JavaScript binding — builds + lints. Doesn't run tests
  # (the binding's tests are JS-side and live in graphrefly-ts's
  # bench harness). The build verifies the cdylib link works.
  # ---------------------------------------------------------------------
  bindings-js:
    name: napi-rs binding (cdylib build + clippy)
    if: "${{ (github.event_name != 'pull_request' || github.actor != 'graphrefly-write-content[bot]') && (github.event_name != 'push' || !startsWith(github.event.head_commit.message, 'chore: release')) }}"
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v5

      - name: Install Rust toolchain
        uses: dtolnay/rust-toolchain@stable
        with:
          toolchain: "1.95"
          components: clippy

      - uses: actions/setup-node@v5
        with:
          node-version: "24"

      - name: Cache cargo
        uses: Swatinem/rust-cache@v2
        with:
          shared-key: bindings-js

      - name: Build napi-rs binding (lib + cdylib)
        run: cargo build -p graphrefly-bindings-js --features tracing

      # Clippy here is informational — napi-rs macro-generated code +
      # FFI-exported `pub fn` items trip clippy::pedantic warnings that
      # don't apply to FFI surfaces. Build success is the bar; clippy
      # output is captured for review.
      - name: Clippy on bindings-js (informational)
        run: cargo clippy -p graphrefly-bindings-js --features tracing
        continue-on-error: true

  # ---------------------------------------------------------------------
  # Cross-platform napi build matrix (Phase E rustImpl activation slice,
  # D075). Builds the `.node` artifact for each target triple and uploads
  # as a workflow artifact. NOT published to npm — that's a separate
  # release-engineering slice. Downstream parity-tests in graphrefly-ts
  # download the host artifact for activation testing.
  #
  # Matrix mirrors `crates/graphrefly-bindings-js/package.json`'s
  # `napi.targets`. linux-arm64 + win-arm64 are emitted but not yet
  # tested in parity (host runner constraint); when GitHub Actions
  # offers ARM runners more broadly we'll wire those into parity too.
  # ---------------------------------------------------------------------
  napi-build-matrix:
    name: napi build (${{ matrix.target }})
    if: "${{ (github.event_name != 'pull_request' || github.actor != 'graphrefly-write-content[bot]') && (github.event_name != 'push' || !startsWith(github.event.head_commit.message, 'chore: release')) }}"
    needs: bindings-js
    strategy:
      fail-fast: false
      matrix:
        include:
          # x86_64-apple-darwin dropped 2026-05-09 — Apple stopped selling
          # Intel Macs in 2023, install base shrinking, and macos-13 runner
          # pool was queueing for minutes per build. Re-add later if user
          # demand surfaces (could cross-compile from macos-14 to avoid the
          # macos-13 deprecated-pool problem).
          - target: aarch64-apple-darwin
            runner: macos-14
            artifact: graphrefly-native.darwin-arm64.node
          - target: x86_64-unknown-linux-gnu
            runner: ubuntu-latest
            artifact: graphrefly-native.linux-x64-gnu.node
          - target: aarch64-unknown-linux-gnu
            runner: ubuntu-latest
            artifact: graphrefly-native.linux-arm64-gnu.node
            cross: true
          - target: x86_64-pc-windows-msvc
            runner: windows-latest
            artifact: graphrefly-native.win32-x64-msvc.node
    runs-on: ${{ matrix.runner }}
    steps:
      - uses: actions/checkout@v5

      - name: Install Rust toolchain
        uses: dtolnay/rust-toolchain@stable
        with:
          toolchain: "1.95"
          targets: ${{ matrix.target }}

      - uses: actions/setup-node@v5
        with:
          node-version: "24"

      - name: Install pnpm
        uses: pnpm/action-setup@v5
        with:
          version: "10"

      - name: Cache cargo
        uses: Swatinem/rust-cache@v2
        with:
          shared-key: napi-${{ matrix.target }}

      - name: Install cross (linux-arm64 only)
        if: matrix.cross == true
        run: cargo install cross --git https://github.com/cross-rs/cross --locked

      - name: Install @napi-rs/cli + workspace deps
        working-directory: crates/graphrefly-bindings-js
        run: |
          pnpm install --no-frozen-lockfile

      - name: Build napi binding (${{ matrix.target }})
        working-directory: crates/graphrefly-bindings-js
        run: |
          if [ "${{ matrix.cross }}" = "true" ]; then
            pnpm exec napi build --platform --release --target ${{ matrix.target }} --features standard --use-cross
          else
            pnpm exec napi build --platform --release --target ${{ matrix.target }} --features standard
          fi
        shell: bash

      - name: Upload artifact
        uses: actions/upload-artifact@v4
        with:
          name: napi-${{ matrix.target }}
          path: crates/graphrefly-bindings-js/${{ matrix.artifact }}
          if-no-files-found: error
          retention-days: 7

  # ---------------------------------------------------------------------
  # TLA+ model checks — runs the canonical handle-protocol scenarios
  # from `~/src/graphrefly-ts/docs/research/`. The Rust port refines
  # the same wave_protocol invariants; any drift between the Rust
  # impl and the spec MUST surface here too.
  #
  # The MC harnesses live in graphrefly-ts. CI fetches them via raw
  # GitHub URLs so this workflow doesn't need a sibling-repo checkout.
  # When TS's MC files change, this CI picks them up on next run.
  #
  # Each TLC run uses ~10s of CPU on a small state space (the MCs are
  # tuned for fast verification — diamond + rewire scenarios).
  # ---------------------------------------------------------------------
  tlc:
    name: TLA+ model check (wave_protocol scenarios)
    if: "${{ (github.event_name != 'pull_request' || github.actor != 'graphrefly-write-content[bot]') && (github.event_name != 'push' || !startsWith(github.event.head_commit.message, 'chore: release')) }}"
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v5

      - name: Set up Java (TLC requires JRE 11+)
        uses: actions/setup-java@v4
        with:
          distribution: temurin
          java-version: "21"

      - name: Download TLA+ tools
        run: |
          curl -fL --retry 3 -o /tmp/tla2tools.jar \
            https://github.com/tlaplus/tlaplus/releases/download/v1.8.0/tla2tools.jar
          test -s /tmp/tla2tools.jar

      - name: Fetch MC harnesses from graphrefly-ts (handle-protocol + wave-protocol-rewire)
        # NOTE: pinned via the `TLA_REF` env var. `main` is the Rust port's
        # default tracking branch — it picks up canonical-spec amendments
        # immediately. Pin to a release SHA / tag once graphrefly-ts cuts
        # versioned releases (post-v1.0). Tracked in
        # `docs/porting-deferred.md` under "CI hardening".
        env:
          TLA_REF: main
        shell: bash -euo pipefail {0}
        run: |
          mkdir -p /tmp/tla
          # Two source repos:
          #   - graphrefly-ts/docs/research/ — handle_protocol + wave_protocol_rewire MC harnesses
          #   - graphrefly/formal/           — base wave_protocol.tla that handle_protocol EXTENDS
          BASE_TS="https://raw.githubusercontent.com/graphrefly/graphrefly-ts/${TLA_REF}/docs/research"
          BASE_SPEC="https://raw.githubusercontent.com/graphrefly/graphrefly/${TLA_REF}/formal"
          # Note: handle_protocol.tla uses underscore — TLA+ requires the
          # filename to match the MODULE name exactly (`MODULE handle_protocol`).
          # An earlier hyphenated `handle-protocol.tla` filename was renamed
          # in graphrefly-ts for this reason.
          fetch() {
            # `--retry-all-errors` retries on 404 too — covers the case where
            # raw.githubusercontent.com's CDN edge hasn't propagated a fresh
            # push yet. Without it, `--retry` skips 404. `--retry-delay 10`
            # spaces retries to let CDN catch up.
            local url="$1" out="$2"
            curl -fL --retry 5 --retry-all-errors --retry-delay 10 \
              -o "$out" "$url"
            test -s "$out"
          }
          # From graphrefly-ts (handle-protocol refinement + rewire harness
          # + Phase I partitioned-protocol harness).
          for f in handle_protocol.tla handle_protocol_MC.tla handle_protocol_MC.cfg \
                   wave_protocol_rewire.tla wave_protocol_rewire_MC.tla \
                   wave_protocol_rewire_MC.cfg \
                   wave_protocol_partitioned.tla wave_protocol_partitioned_MC.tla \
                   wave_protocol_partitioned_MC.cfg; do
            fetch "$BASE_TS/$f" "/tmp/tla/$f"
          done
          # From graphrefly (spec repo) — base modules that the above EXTEND.
          for f in wave_protocol.tla; do
            fetch "$BASE_SPEC/$f" "/tmp/tla/$f"
          done

      - name: TLC — handle_protocol_MC (diamond + handle-protocol refinement)
        working-directory: /tmp/tla
        # `set -euo pipefail` ensures a failed `java` invocation (OOM,
        # classpath error, etc.) propagates through `tee` instead of being
        # masked by `tee`'s exit code. The explicit `grep` checks cover
        # TLC's logical failures (invariant violations, "Error:" lines).
        shell: bash -euo pipefail {0}
        run: |
          java -XX:+UseParallelGC -jar /tmp/tla2tools.jar \
            -tool -workers auto -config handle_protocol_MC.cfg handle_protocol_MC.tla \
            | tee handle.log
          # TLC reports "Model checking completed" on success; "Error:" or
          # "Invariant ... is violated" on failure.
          grep -q "Model checking completed" handle.log
          ! grep -q "is violated" handle.log
          ! grep -qi "^error:" handle.log

      - name: TLC — wave_protocol_rewire_MC (set_deps substrate)
        working-directory: /tmp/tla
        shell: bash -euo pipefail {0}
        run: |
          java -XX:+UseParallelGC -jar /tmp/tla2tools.jar \
            -tool -workers auto -config wave_protocol_rewire_MC.cfg wave_protocol_rewire_MC.tla \
            | tee rewire.log
          grep -q "Model checking completed" rewire.log
          ! grep -q "is violated" rewire.log
          ! grep -qi "^error:" rewire.log

      - name: TLC — wave_protocol_partitioned_MC (Phase I — D3 closure)
        # Per-partition wave_owner protocol verification (Slice Y1+Y2,
        # 2026-05-09). Encodes Q6 invariants from
        # `archive/docs/SESSION-rust-port-d3-per-subgraph-parallelism.md`:
        # cross-partition deadlock-freedom, ascending-`SubgraphId`
        # acquisition ordering, `Subscription::Drop` cleanup cascade,
        # union/split discipline, mid-wave reentrancy rejection.
        working-directory: /tmp/tla
        shell: bash -euo pipefail {0}
        run: |
          java -XX:+UseParallelGC -jar /tmp/tla2tools.jar \
            -tool -workers auto -config wave_protocol_partitioned_MC.cfg wave_protocol_partitioned_MC.tla \
            | tee partitioned.log
          grep -q "Model checking completed" partitioned.log
          ! grep -q "is violated" partitioned.log
          ! grep -qi "^error:" partitioned.log