CI #2950
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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" |