S7: general capability qualification fixtures #338
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: Foundation verification | |
| on: | |
| push: | |
| branches: [main] | |
| pull_request: | |
| workflow_dispatch: | |
| inputs: | |
| proof_impact_base: | |
| description: Immutable base commit for proof-impact comparison | |
| required: true | |
| type: string | |
| permissions: | |
| contents: read | |
| concurrency: | |
| group: foundation-${{ github.workflow }}-${{ github.ref }} | |
| cancel-in-progress: true | |
| env: | |
| CARGO_BUILD_JOBS: "2" | |
| RUST_VERSION: 1.97.1 | |
| VERUS_VERSION: 0.2026.08.09.92f466f | |
| VERUS_LINUX_SHA256: 2f5a41c553f424aacdd732339e9d125563716a0b003c27730f75d6f81a282cef | |
| PERITUS_PROOF_IMPACT_BASE: ${{ github.event.pull_request.base.sha || github.event.before || inputs.proof_impact_base }} | |
| jobs: | |
| bootstrap: | |
| name: Verify pre-Cargo policy | |
| runs-on: ubuntu-24.04 | |
| timeout-minutes: 5 | |
| steps: | |
| - name: Check out repository | |
| uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| with: | |
| fetch-depth: 0 | |
| - name: Verify reviewed pre-Cargo policy | |
| shell: bash | |
| run: git diff --no-ext-diff --no-textconv --exit-code 6ca5f56d2ab12e93f155d684b33f4a86c2f877b8 -- .cargo/config.toml .gitattributes | |
| policy: | |
| name: Foundation policy | |
| needs: bootstrap | |
| runs-on: ubuntu-24.04 | |
| timeout-minutes: 10 | |
| steps: | |
| - name: Check out repository | |
| uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| with: | |
| fetch-depth: 0 | |
| - name: Install pinned Rust | |
| uses: dtolnay/rust-toolchain@6c977a6ca4077a0ceb28ffbe03f59d46e9ac8772 # v1 | |
| with: | |
| toolchain: ${{ env.RUST_VERSION }} | |
| - name: Enforce workspace policy | |
| run: cargo run --locked --package xtask -- all | |
| rust-format: | |
| name: Rust format source | |
| needs: bootstrap | |
| runs-on: ubuntu-24.04 | |
| timeout-minutes: 10 | |
| steps: | |
| - name: Check out repository | |
| uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| with: | |
| fetch-depth: 0 | |
| - name: Install pinned Rust | |
| uses: dtolnay/rust-toolchain@6c977a6ca4077a0ceb28ffbe03f59d46e9ac8772 # v1 | |
| with: | |
| toolchain: ${{ env.RUST_VERSION }} | |
| components: rustfmt | |
| - name: Check formatting | |
| run: cargo run --locked --package xtask -- format-check | |
| rust: | |
| name: Foundation Rust ${{ matrix.operation }} ${{ matrix.shard }} (${{ matrix.os }}) | |
| needs: bootstrap | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| os: [ubuntu-24.04, macos-15, windows-2025] | |
| operation: [build, test, doc-test, clippy, docs] | |
| shard: [foundation-state, runtime-tools, model-orchestration, app-runner, app-shell, testing, edge] | |
| runs-on: ${{ matrix.os }} | |
| timeout-minutes: 10 | |
| steps: | |
| - name: Check out repository | |
| uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| with: | |
| fetch-depth: 0 | |
| - name: Install pinned Rust | |
| uses: dtolnay/rust-toolchain@6c977a6ca4077a0ceb28ffbe03f59d46e9ac8772 # v1 | |
| with: | |
| toolchain: ${{ env.RUST_VERSION }} | |
| components: clippy,rustfmt | |
| - name: Run reviewed package shard | |
| run: cargo run --locked --target-dir target/xtask-bootstrap --package xtask -- ci-shard ${{ matrix.operation }} ${{ matrix.shard }} | |
| supply-chain: | |
| name: Licenses and dependency policy | |
| needs: bootstrap | |
| runs-on: ubuntu-24.04 | |
| timeout-minutes: 10 | |
| steps: | |
| - name: Check out repository | |
| uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| with: | |
| fetch-depth: 0 | |
| - name: Install pinned Rust | |
| uses: dtolnay/rust-toolchain@6c977a6ca4077a0ceb28ffbe03f59d46e9ac8772 # v1 | |
| with: | |
| toolchain: ${{ env.RUST_VERSION }} | |
| - name: Install pinned cargo-deny | |
| run: cargo install cargo-deny --version 0.20.2 --locked | |
| - name: Check advisories, licenses, bans, and sources | |
| run: cargo deny --locked check | |
| verus-policy: | |
| name: Foundation Verus policy | |
| needs: bootstrap | |
| runs-on: ubuntu-24.04 | |
| timeout-minutes: 10 | |
| steps: | |
| - name: Check out repository | |
| uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| with: | |
| fetch-depth: 0 | |
| - name: Install pinned Rust | |
| uses: dtolnay/rust-toolchain@6c977a6ca4077a0ceb28ffbe03f59d46e9ac8772 # v1 | |
| with: | |
| toolchain: ${{ env.RUST_VERSION }} | |
| - name: Install digest-checked Verus archive | |
| shell: bash | |
| run: | | |
| set -euo pipefail | |
| archive="$RUNNER_TEMP/verus.zip" | |
| install_root="$RUNNER_TEMP/peritus-verus" | |
| curl --fail --location --retry 3 \ | |
| --output "$archive" \ | |
| "https://github.com/verus-lang/verus/releases/download/release/$VERUS_VERSION/verus-$VERUS_VERSION-x86-linux.zip" | |
| printf '%s %s\n' "$VERUS_LINUX_SHA256" "$archive" | sha256sum --check --strict | |
| mkdir -p "$install_root" | |
| unzip -q "$archive" -d "$install_root" | |
| printf '%s\n' "$install_root/verus-x86-linux" >> "$GITHUB_PATH" | |
| - name: Probe every pinned tool component | |
| run: cargo run --locked --package xtask -- toolchain-check | |
| - name: Enforce ordinary-Rust formal API contracts | |
| run: cargo run --locked --package xtask -- ordinary-api-check | |
| verus: | |
| name: Foundation Verus ${{ matrix.operation }} ${{ matrix.shard }} | |
| needs: bootstrap | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| operation: [verus-verify, verus-verify-strict, verus-build, verus-build-strict] | |
| shard: [foundation-state, runtime-tools, model-orchestration, app-runner, app-shell, edge] | |
| runs-on: ubuntu-24.04 | |
| timeout-minutes: 10 | |
| steps: | |
| - name: Check out repository | |
| uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| with: | |
| fetch-depth: 0 | |
| - name: Install pinned Rust | |
| uses: dtolnay/rust-toolchain@6c977a6ca4077a0ceb28ffbe03f59d46e9ac8772 # v1 | |
| with: | |
| toolchain: ${{ env.RUST_VERSION }} | |
| - name: Install digest-checked Verus archive | |
| shell: bash | |
| run: | | |
| set -euo pipefail | |
| archive="$RUNNER_TEMP/verus.zip" | |
| install_root="$RUNNER_TEMP/peritus-verus" | |
| curl --fail --location --retry 3 \ | |
| --output "$archive" \ | |
| "https://github.com/verus-lang/verus/releases/download/release/$VERUS_VERSION/verus-$VERUS_VERSION-x86-linux.zip" | |
| printf '%s %s\n' "$VERUS_LINUX_SHA256" "$archive" | sha256sum --check --strict | |
| mkdir -p "$install_root" | |
| unzip -q "$archive" -d "$install_root" | |
| printf '%s\n' "$install_root/verus-x86-linux" >> "$GITHUB_PATH" | |
| - name: Run reviewed Verus package shard | |
| run: cargo run --locked --package xtask -- ci-shard ${{ matrix.operation }} ${{ matrix.shard }} |