ci.yml

name: CI

on:
  push:
    branches: [main]
  pull_request:
  merge_group:
  schedule:
    - cron: '0 3 * * *'  # daily at 03:00 UTC to exercise full test matrix (SMT/Z3/CVC5)
  workflow_dispatch:

concurrency:
  group: ${{ github.workflow }}-${{ github.ref }}
  cancel-in-progress: ${{ github.ref != 'refs/heads/main' }}

permissions:
  contents: read

# ---------------------------------------------------------------------------
# Path filter: determine which groups of files changed so jobs can skip
# themselves when their inputs are untouched.
#
# A daily schedule trigger ensures the full test matrix (incl. SMT/Z3/CVC5
# native jobs) runs regularly even without pushes/PRs.
#
# Per-job CARGO_TARGET_DIR prevents cache key collisions.
# CARGO_INCREMENTAL=0 avoids wasting disk on incremental artifacts.
#
# Jobs run on free GitHub-hosted VMs (one machine per job). Heavy work
# (clippy, test, bench, codegen, cvc5, no-z3) is intentionally parallel
# after `changes`; do not re-serialize them "to save resources" unless
# returning to a shared self-hosted runner with limited RAM/disk.
#
# Filter groups:
#   rust           - any Rust crate or workspace file changed
#   codegen        - crates that affect code generation + demo files
#   tooling-only   - only CLI/LSP/server/fmt changed (not core pipeline)
#   editors-ts     - tree-sitter grammar
#   editors-vscode - VS Code extension
#   smt            - assura-smt crate (used to gate heavy CVC5 native jobs)
# ---------------------------------------------------------------------------
jobs:
  changes:
    runs-on: ubuntu-latest
    timeout-minutes: 2
    permissions:
      contents: read
      pull-requests: read
    outputs:
      rust:           ${{ steps.filter.outputs.rust }}
      codegen:        ${{ steps.filter.outputs.codegen }}
      tooling-only:   ${{ steps.filter.outputs.tooling-only }}
      editors-ts:     ${{ steps.filter.outputs.editors-ts }}
      editors-vscode: ${{ steps.filter.outputs.editors-vscode }}
      smt:            ${{ steps.filter.outputs.smt }}
      workflows:      ${{ steps.filter.outputs.workflows }}
    steps:
      - name: Harden runner
        uses: step-security/harden-runner@bf7454d06d71f1098171f2acdf0cd4708d7b5920 # v2.20.0
        with:
          egress-policy: audit
      - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7
      - uses: dorny/paths-filter@7b450fff21473bca461d4b92ce414b9d0420d706 # v4
        id: filter
        with:
          filters: |
            rust:
              - 'crates/**'
              - 'Cargo.toml'
              - 'Cargo.lock'
              - 'deny.toml'
              - 'scripts/**'
              - 'AGENTS.md'
              - '.github/workflows/ci.yml'
            codegen:
              - 'crates/assura-parser/**'
              - 'crates/assura-resolve/**'
              - 'crates/assura-types/**'
              - 'crates/assura-smt/**'
              - 'crates/assura-codegen/**'
              - 'crates/assura-config/**'
              - 'crates/assura-diagnostics/**'
              - 'demos/**'
              - 'Cargo.toml'
              - 'Cargo.lock'
            tooling-only:
              - 'crates/assura-cli/**'
              - 'crates/assura-lsp/**'
              - 'crates/assura-server/**'
              - 'crates/assura-fmt/**'
              - 'crates/assura-bench/**'
            editors-ts:
              - 'editors/tree-sitter-assura/**'
            editors-vscode:
              - 'editors/vscode/**'
            smt:
              - 'crates/assura-smt/**'
              - 'Cargo.toml'
              - 'Cargo.lock'
            workflows:
              - '.github/workflows/**'
              - '.github/actions/**'
              - '.github/zizmor.yml'

  # ── Fast lint (fmt, guards, cargo-deny; no workspace compile) ─────────────
  # Separate from clippy so the heavy compile does not wait on deny/fmt, and
  # so deny failures do not force a full re-clippy when only deny.toml changed.
  lint-fast:
    name: Fast lint
    needs: changes
    if: ${{ needs.changes.outputs.rust == 'true' || github.event_name == 'workflow_dispatch' || github.event_name == 'schedule' }}
    runs-on: ubuntu-latest
    timeout-minutes: 10
    steps:
      - name: Harden runner
        uses: step-security/harden-runner@bf7454d06d71f1098171f2acdf0cd4708d7b5920 # v2.20.0
        with:
          egress-policy: audit
      - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7
        with:
          persist-credentials: false

      - uses: ./.github/actions/setup-rust-ci
        with:
          shared-key: ci-lint-fast
          toolchain-components: rustfmt
          # Skip Z3/protobuf/OpenSSL: this job only runs fmt, guards, cargo-deny.
          install-system-deps: 'false'

      # guards.sh uses ripgrep; full system-deps install is unnecessary here.
      - name: Install ripgrep
        run: sudo apt-get install -y ripgrep
        env:
          DEBIAN_FRONTEND: noninteractive

      - name: Install cargo-deny
        uses: taiki-e/install-action@0c80bcf54d007ab0e714c95f3bcc43c387707535 # v2
        with:
          tool: cargo-deny
        env:
          HOME: ${{ runner.temp }}/install-action-home

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

      # Fast static greps: Verifier::new outside smt/pipeline, Type::Unknown ==,
      # missing ergonomics APIs, CHECKER_PIPELINE breadth. No compile required.
      - name: Static analysis guards
        if: ${{ !cancelled() }}
        run: bash scripts/guards.sh

      # Assert publish set/order (catches wrong expected graph in docs/scripts).
      # Full cargo package verify lives in the cargo-package job.
      - name: Check crates.io publish plan
        if: ${{ !cancelled() }}
        run: bash scripts/check-publish-plan.sh

      - name: Check dependencies
        if: ${{ !cancelled() }}
        run: cargo deny check

  # ── Clippy (parallel with test / lint-fast / heavy jobs) ──────────────────
  clippy:
    needs: changes
    if: ${{ needs.changes.outputs.rust == 'true' || github.event_name == 'workflow_dispatch' || github.event_name == 'schedule' }}
    runs-on: ubuntu-latest
    timeout-minutes: 15
    env:
      CARGO_TARGET_DIR: target/ci-clippy
      CARGO_INCREMENTAL: '0'
    steps:
      - name: Harden runner
        uses: step-security/harden-runner@bf7454d06d71f1098171f2acdf0cd4708d7b5920 # v2.20.0
        with:
          egress-policy: audit
      - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7
        with:
          persist-credentials: false

      - uses: ./.github/actions/setup-rust-ci
        with:
          shared-key: ci-clippy
          toolchain-components: clippy

      - name: Clippy
        run: cargo clippy --workspace --locked -- -D warnings

  # ── Workflow linting (actionlint + zizmor) ────────────────────────────────
  workflow-sanity:
    name: Workflow sanity
    needs: changes
    if: ${{ needs.changes.outputs.workflows == 'true' || github.event_name == 'workflow_dispatch' || github.event_name == 'schedule' }}
    runs-on: ubuntu-latest
    timeout-minutes: 5
    steps:
      - name: Harden runner
        uses: step-security/harden-runner@bf7454d06d71f1098171f2acdf0cd4708d7b5920 # v2.20.0
        with:
          egress-policy: audit
      - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7
        with:
          persist-credentials: false

      - name: Install linters
        run: |
          go install github.com/rhysd/actionlint/cmd/actionlint@v1.7.7
          echo "$(go env GOPATH)/bin" >> "$GITHUB_PATH"
          python3 -m pip install --user "zizmor==1.25.2"
          echo "$HOME/.local/bin" >> "$GITHUB_PATH"

      - name: Run actionlint
        run: actionlint -color

      - name: Run zizmor
        run: zizmor --config .github/zizmor.yml .github/workflows/*.yml

  # ── Tests (parallel with clippy) ──────────────────────────────────────────
  test:
    needs: changes
    if: ${{ needs.changes.outputs.rust == 'true' || github.event_name == 'workflow_dispatch' || github.event_name == 'schedule' }}
    runs-on: ubuntu-latest
    timeout-minutes: 25
    env:
      CARGO_TARGET_DIR: target/ci-test
      CARGO_INCREMENTAL: '0'
    steps:
      - name: Harden runner
        uses: step-security/harden-runner@bf7454d06d71f1098171f2acdf0cd4708d7b5920 # v2.20.0
        with:
          egress-policy: audit
      - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7
        with:
          persist-credentials: false

      - uses: ./.github/actions/setup-rust-ci
        with:
          shared-key: ci-test


      - name: Install cargo-nextest
        uses: taiki-e/install-action@0c80bcf54d007ab0e714c95f3bcc43c387707535 # nextest
        env:
          HOME: ${{ runner.temp }}/install-action-home

      - name: Test (nextest)
        run: cargo nextest run --workspace --locked



  # ── Pipeline benchmarks (parallel; free hosted VMs, no self-host throttle) ─
  benchmark:
    name: Pipeline benchmarks
    needs: changes
    if: ${{ needs.changes.outputs.codegen == 'true' || needs.changes.outputs.tooling-only == 'true' || github.event_name == 'workflow_dispatch' || github.event_name == 'schedule' }}
    runs-on: ubuntu-latest
    timeout-minutes: 15
    env:
      CARGO_TARGET_DIR: target/ci-bench
      CARGO_INCREMENTAL: '0'
    steps:
      - name: Harden runner
        uses: step-security/harden-runner@bf7454d06d71f1098171f2acdf0cd4708d7b5920 # v2.20.0
        with:
          egress-policy: audit
      - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7
        with:
          persist-credentials: false

      - uses: ./.github/actions/setup-rust-ci
        with:
          shared-key: ci-bench


      - name: Run pipeline benchmarks (smoke + compile check only)
        # Run only full_pipeline bench in CI (smoke to ensure it compiles/runs).
        # Minimum valid Criterion sample-size is 10. Use quiet + noplot for speed. No thresholds.
        run: cargo bench -p assura-bench --locked --bench pipeline full_pipeline -- --sample-size 10 --quiet --noplot

      - name: Upload benchmark output
        if: ${{ !cancelled() }}
        uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7
        with:
          name: assura-bench-${{ github.sha }}
          path: target/ci-bench/criterion/**
          if-no-files-found: ignore



  # ── Generated code compiles (parallel with test on free hosted runners) ──
  codegen-validation:
    name: Generated code compiles
    needs: changes
    if: ${{ needs.changes.outputs.codegen == 'true' || github.event_name == 'workflow_dispatch' || github.event_name == 'schedule' }}
    runs-on: ubuntu-latest
    timeout-minutes: 25
    env:
      CARGO_TARGET_DIR: target/ci-codegen
      CARGO_INCREMENTAL: '0'
    steps:
      - name: Harden runner
        uses: step-security/harden-runner@bf7454d06d71f1098171f2acdf0cd4708d7b5920 # v2.20.0
        with:
          egress-policy: audit
      - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7
        with:
          persist-credentials: false

      - uses: ./.github/actions/setup-rust-ci
        with:
          shared-key: ci-codegen


      - name: Build compiler
        run: cargo build --bin assura --locked

      - name: E2E check all demos (parse + resolve + typecheck + verify)
        run: |
          for demo in demos/*.assura; do
            # Audit demos have intentional counterexamples (real CVE models); skip them
            case "$demo" in *-audit*|*audit-*) echo "=== Skipping audit demo $demo ==="; continue;; esac
            echo "=== Checking $demo ==="
            cargo run --locked --bin assura -- check "$demo"
          done

      - name: Getting-started smoke (check + write-ir + bin + cargo test)
        if: ${{ !cancelled() }}
        run: bash scripts/smoke-getting-started.sh

      - name: Validate generated code for demos
        if: ${{ !cancelled() }}
        run: |
          for demo in demos/*.assura; do
            case "$demo" in *-audit*|*audit-*) continue;; esac
            echo "=== Building $demo ==="
            cargo run --locked --bin assura -- build --no-check "$demo"
            # build writes to <input-parent>/generated/ (e.g. demos/generated/)
            gen_dir="$(dirname "$demo")/generated"
            echo "=== Checking generated Rust for $demo ==="
            (cd "$gen_dir" && cargo check)
            rm -rf "$gen_dir"
          done



  # ── No-Z3 fallback check (~30s on ubuntu) ───────────────────────────────
  no-z3:
    needs: changes
    if: ${{ needs.changes.outputs.rust == 'true' || github.event_name == 'workflow_dispatch' || github.event_name == 'schedule' }}
    runs-on: ubuntu-latest
    timeout-minutes: 10
    steps:
      - name: Harden runner
        uses: step-security/harden-runner@bf7454d06d71f1098171f2acdf0cd4708d7b5920 # v2.20.0
        with:
          egress-policy: audit
      - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7
        with:
          persist-credentials: false
      - uses: ./.github/actions/setup-rust-ci
        with:
          shared-key: ci-no-z3
          install-system-deps: 'false'


      - name: Build without Z3 (graceful fallback)
        run: cargo check -p assura-smt --no-default-features --locked

  # ── CVC5 native integration tests (parallel with test) ──────────────────
  cvc5:
    name: CVC5 native tests
    needs: changes
    if: ${{ needs.changes.outputs.smt == 'true' || github.event_name == 'workflow_dispatch' || github.event_name == 'schedule' }}
    runs-on: ubuntu-latest
    timeout-minutes: 25
    env:
      CARGO_TARGET_DIR: target/ci-cvc5
      CARGO_INCREMENTAL: '0'
    steps:
      - name: Harden runner
        uses: step-security/harden-runner@bf7454d06d71f1098171f2acdf0cd4708d7b5920 # v2.20.0
        with:
          egress-policy: audit
      - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7
        with:
          persist-credentials: false

      - uses: ./.github/actions/setup-rust-ci
        with:
          shared-key: ci-cvc5


      - name: Install CVC5 prebuilt library
        run: |
          if [ "$(uname)" = "Darwin" ]; then
            ARCH=$(uname -m)
            curl -sL "https://github.com/cvc5/cvc5/releases/latest/download/cvc5-macOS-${ARCH}-static.zip" -o /tmp/cvc5.zip
            unzip -o /tmp/cvc5.zip -d /tmp/cvc5-install
            echo "CVC5_LIB_DIR=/tmp/cvc5-install/cvc5-macOS-${ARCH}-static/lib" >> "$GITHUB_ENV"
            echo "CVC5_INCLUDE_DIR=/tmp/cvc5-install/cvc5-macOS-${ARCH}-static/include" >> "$GITHUB_ENV"
          else
            curl -sL "https://github.com/cvc5/cvc5/releases/latest/download/cvc5-Linux-x86_64-static.zip" -o /tmp/cvc5.zip
            unzip -o /tmp/cvc5.zip -d /tmp/cvc5-install
            echo "CVC5_LIB_DIR=/tmp/cvc5-install/cvc5-Linux-x86_64-static/lib" >> "$GITHUB_ENV"
            echo "CVC5_INCLUDE_DIR=/tmp/cvc5-install/cvc5-Linux-x86_64-static/include" >> "$GITHUB_ENV"
          fi

      - name: Clippy with CVC5 native
        run: cargo clippy -p assura-smt --features cvc5-verify --locked -- -D warnings

      - name: Test assura-smt with CVC5 native
        if: ${{ !cancelled() }}
        run: cargo test -p assura-smt --features cvc5-verify --locked

      - name: Verify portfolio solver with CVC5
        if: ${{ !cancelled() }}
        run: |
          cargo build --bin assura --features cvc5-verify --locked
          cargo run --locked --bin assura --features cvc5-verify -- check --solver cvc5 demos/libwebp-huffman.assura



  # ── Tree-sitter grammar tests ───────────────────────────────────────────
  tree-sitter:
    name: Tree-sitter grammar tests
    needs: changes
    if: ${{ needs.changes.outputs.editors-ts == 'true' || github.event_name == 'workflow_dispatch' || github.event_name == 'schedule' }}
    runs-on: ubuntu-latest
    timeout-minutes: 10
    steps:
      - name: Harden runner
        uses: step-security/harden-runner@bf7454d06d71f1098171f2acdf0cd4708d7b5920 # v2.20.0
        with:
          egress-policy: audit
      - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7
        with:
          persist-credentials: false

      - name: Setup Node.js
        uses: actions/setup-node@820762786026740c76f36085b0efc47a31fe5020 # v6
        with:
          node-version: "20"

      - name: Install dependencies
        working-directory: editors/tree-sitter-assura
        run: npm ci

      - name: Generate parser
        working-directory: editors/tree-sitter-assura
        run: npx tree-sitter generate

      - name: Run tree-sitter tests
        working-directory: editors/tree-sitter-assura
        run: npx tree-sitter test

  # ── VS Code extension compiles ──────────────────────────────────────────
  vscode-extension:
    name: VS Code extension compiles
    needs: changes
    if: ${{ needs.changes.outputs.editors-vscode == 'true' || github.event_name == 'workflow_dispatch' || github.event_name == 'schedule' }}
    runs-on: ubuntu-latest
    timeout-minutes: 10
    steps:
      - name: Harden runner
        uses: step-security/harden-runner@bf7454d06d71f1098171f2acdf0cd4708d7b5920 # v2.20.0
        with:
          egress-policy: audit
      - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7
        with:
          persist-credentials: false

      - name: Setup Node.js
        uses: actions/setup-node@820762786026740c76f36085b0efc47a31fe5020 # v6
        with:
          node-version: "20"

      - name: Install dependencies
        working-directory: editors/vscode
        run: npm ci

      - name: Compile TypeScript
        working-directory: editors/vscode
        run: npx tsc -p ./

  # ── cargo package all publishable crates (crates.io preflight, #814) ──
  # Workspace cargo test/clippy do not catch include_str! paths that only
  # resolve inside the monorepo. cargo package --locked verifies each tarball.
  cargo-package:
    name: Cargo package (publishable)
    needs: changes
    if: ${{ needs.changes.outputs.rust == 'true' || github.event_name == 'workflow_dispatch' || github.event_name == 'schedule' }}
    runs-on: ubuntu-latest
    timeout-minutes: 45
    env:
      CARGO_TARGET_DIR: target/ci-package
      CARGO_INCREMENTAL: '0'
    steps:
      - name: Harden runner
        uses: step-security/harden-runner@bf7454d06d71f1098171f2acdf0cd4708d7b5920 # v2.20.0
        with:
          egress-policy: audit
      - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7
        with:
          persist-credentials: false

      - uses: ./.github/actions/setup-rust-ci
        with:
          shared-key: ci-cargo-package

      - name: cargo package all publishable crates
        run: bash scripts/check-cargo-package.sh

  # ── Gate job (single required status check for branch protection) ────
  ci:
    if: always()
    needs: [lint-fast, clippy, test, benchmark, codegen-validation, no-z3, cvc5, tree-sitter, vscode-extension, workflow-sanity, cargo-package]
    runs-on: ubuntu-latest
    timeout-minutes: 2
    steps:
      - name: Harden runner
        uses: step-security/harden-runner@bf7454d06d71f1098171f2acdf0cd4708d7b5920 # v2.20.0
        with:
          egress-policy: audit
      - name: Check job results
        run: |
          # Fail if any needed job failed (skipped is OK for path-filtered jobs)
          if [[ "${{ contains(needs.*.result, 'failure') }}" == "true" ]]; then
            echo "One or more CI jobs failed"
            exit 1
          fi
          if [[ "${{ contains(needs.*.result, 'cancelled') }}" == "true" ]]; then
            echo "One or more CI jobs were cancelled"
            exit 1
          fi
          echo "All CI jobs passed or were skipped"