diff --git a/.github/filters/ci.yml b/.github/filters/ci.yml deleted file mode 100644 index 32741ac..0000000 --- a/.github/filters/ci.yml +++ /dev/null @@ -1,66 +0,0 @@ -native: - - '.github/workflows/ci.yml' - - 'src/**' - - 'tests/**' - - 'examples/**' - - 'Cargo.{toml,lock}' - - '.cargo/**' - - 'mise.{toml,lock}' - - 'xtask/Cargo.toml' - - 'xtask/src/{main,cli,tasks}.rs' - - 'proofs/{lean/vectors,quint/traces,prolog/vectors}/**' -memory: - - 'src/{sys,handles,resource,transaction,child,command,plan,options,mitigation,failure_tests}.rs' - - 'tests/**' - - 'xtask/src/verifier.rs' - - 'Cargo.{toml,lock}' -api: - - '.github/workflows/ci.yml' - - 'src/**' - - 'Cargo.{toml,lock}' - - 'public-api/**' - - 'xtask/src/tasks.rs' - - 'mise.{toml,lock}' -package: - - '.github/workflows/ci.yml' - - 'mise.{toml,lock}' - - 'src/**' - - 'tests/**' - - 'examples/**' - - 'docs/**' - - 'Cargo.{toml,lock}' - - 'README.md' - - 'CHANGELOG.md' - - 'REUSE.toml' - - 'LICENSE*' - - 'xtask/src/tasks.rs' -kani: - - 'src/domain/**' - - 'src/mitigation.rs' - - 'Cargo.toml' - - 'xtask/src/proofs/{kani,tools,mod}.rs' -lean: - - 'src/domain/command_line_rules.rs' - - 'proofs/lean/**' - - 'xtask/src/proofs/{lean,tools,mod}.rs' -verus: - - 'src/domain/command_line_rules.rs' - - 'proofs/{verus,lean}/**' - - 'xtask/src/proofs/{verus,tools,mod}.rs' -tla: - - 'src/{child,transaction}.rs' - - 'proofs/tla/**' - - 'xtask/src/proofs/{tla,tools,mod}.rs' -quint: - - 'src/{child,transaction,command}.rs' - - 'tests/lifecycle/**' - - 'proofs/quint/**' - - 'xtask/src/proofs/{quint,tools,mod}.rs' -alloy: - - 'src/{handles,resource,transaction}.rs' - - 'proofs/alloy/**' - - 'xtask/src/proofs/{alloy,tools,mod}.rs' -prolog: - - 'src/{sys,command}.rs' - - 'proofs/prolog/**' - - 'xtask/src/proofs/{prolog,tools,mod}.rs' diff --git a/.github/renovate.json b/.github/renovate.json index 8aa240b..b366fc7 100644 --- a/.github/renovate.json +++ b/.github/renovate.json @@ -5,7 +5,7 @@ { "description": "Rust 1.84 is the workspace MSRV and moves only with an ADR (ADR 0018).", "matchDepNames": ["rust"], - "matchFileNames": [".github/workflows/ci.yml"], + "matchFileNames": [".github/workflows/ci.yml", ".github/workflows/release.yml"], "matchCurrentValue": "/^1\\.84(?:\\.\\d+)?$/", "enabled": false }, @@ -14,6 +14,12 @@ "matchManagers": ["cargo"], "matchDepNames": ["sha2"], "allowedVersions": "<0.11" + }, + { + "description": "yaml-rust2 0.12 requires Rust 1.85, above the workspace MSRV.", + "matchManagers": ["cargo"], + "matchDepNames": ["yaml-rust2"], + "allowedVersions": "<0.12" } ] } diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index fe6e556..b932cd2 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -8,11 +8,11 @@ permissions: contents: read env: - MISE_GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} + MISE_GITHUB_TOKEN: ${{ github.token }} MISE_AUTO_INSTALL: "false" concurrency: - group: ${{ github.workflow }}-${{ github.ref }} + group: ci-${{ github.ref }} cancel-in-progress: true jobs: @@ -20,128 +20,20 @@ jobs: name: Fast repository checks runs-on: ubuntu-24.04 timeout-minutes: 15 - permissions: - contents: read - pull-requests: read - outputs: - native: ${{ steps.changes.outputs.native }} - memory: ${{ steps.changes.outputs.memory }} - api: ${{ steps.changes.outputs.api }} - package: ${{ steps.changes.outputs.package }} - proofs: ${{ steps.layers.outputs.proofs }} steps: - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 with: - fetch-depth: 0 persist-credentials: false - - uses: dorny/paths-filter@ceb8a2b8f2d89434be7ff52d3de7ec3738c5cc9d # v4.0.3 - id: changes - with: - base: ${{ github.event.merge_group.base_sha || github.event.repository.default_branch }} - filters: .github/filters/ci.yml - - name: Select proof layers - id: layers - env: - CHANGES: ${{ steps.changes.outputs.changes }} - run: | - proofs=$(jq -ce '[.[] | select(IN("kani", "lean", "verus", "tla", "quint", "alloy", "prolog"))]' <<< "$CHANGES") - echo "proofs=$proofs" >> "$GITHUB_OUTPUT" - uses: jdx/mise-action@fc42bcc7ddbf51124c30f95a877a0c5168a3bfde with: version: v2026.10.17 cache: true - uses: Swatinem/rust-cache@d1527c8f67ef9af357290475d4af4b0fab8f12e0 # v2.9.3 - - run: mise x -- just fmt - - run: mise x -- just clippy - - run: mise x -- just gates - - run: mise x -- just test - - run: mise x -- just linux-empty - - run: mise x -- just supply-chain - - run: mise x -- uv run --no-project --with 'reuse[charset-normalizer]==6.2.0' cargo xtask reuse - - run: mise x -- just typos - - run: mise x -- actionlint - - test: - name: Windows / Rust ${{ matrix.rust }} - needs: [quality] - if: needs.quality.outputs.native == 'true' - strategy: - fail-fast: false - matrix: - rust: ["1.99.1", "1.84.1"] - runs-on: windows-2025 - timeout-minutes: 15 - steps: - - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 - with: - persist-credentials: false - - uses: dtolnay/rust-toolchain@683b588c487a69d01f6c6ddf40f036ff682cc2c8 # v1 - with: - toolchain: ${{ matrix.rust }} - components: ${{ matrix.rust != '1.84.1' && 'clippy' || '' }} - - uses: Swatinem/rust-cache@d1527c8f67ef9af357290475d4af4b0fab8f12e0 # v2.9.3 - with: - key: ${{ matrix.rust }} - - name: Lint the native Windows implementation - if: matrix.rust != '1.84.1' - run: cargo clippy --workspace --all-targets --locked -- -D warnings - - run: cargo xtask test + - run: mise x -- uv run --no-project --with 'reuse[charset-normalizer]==6.2.0' just check - i686-smoke: - name: Windows i686 execution smoke - needs: [quality] - if: needs.quality.outputs.native == 'true' - runs-on: windows-2025 - timeout-minutes: 15 - steps: - - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 - with: - persist-credentials: false - - uses: dtolnay/rust-toolchain@683b588c487a69d01f6c6ddf40f036ff682cc2c8 # v1 - with: - toolchain: "1.99.1" - targets: i686-pc-windows-msvc - - uses: Swatinem/rust-cache@d1527c8f67ef9af357290475d4af4b0fab8f12e0 # v2.9.3 - - run: >- - cargo test --locked --target i686-pc-windows-msvc --test windows_spawn - pseudoconsole_regular_stdio_stays_off_parent_pipes -- --exact - - arm64: - name: Windows 11 ARM64 - needs: [quality] - if: needs.quality.outputs.native == 'true' - runs-on: windows-11-arm - timeout-minutes: 20 - steps: - - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 - with: - persist-credentials: false - - uses: dtolnay/rust-toolchain@683b588c487a69d01f6c6ddf40f036ff682cc2c8 # v1 - with: - toolchain: "1.99.1" - - uses: Swatinem/rust-cache@d1527c8f67ef9af357290475d4af4b0fab8f12e0 # v2.9.3 - - run: cargo xtask test - - verifier: - name: Application Verifier - needs: [quality] - if: needs.quality.outputs.memory == 'true' - runs-on: windows-latest - timeout-minutes: 30 - steps: - - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 - with: - persist-credentials: false - - uses: dtolnay/rust-toolchain@683b588c487a69d01f6c6ddf40f036ff682cc2c8 # v1 - with: - toolchain: "1.99.1" - - uses: Swatinem/rust-cache@d1527c8f67ef9af357290475d4af4b0fab8f12e0 # v2.9.3 - - run: cargo xtask verifier - - api: - name: Windows public API - needs: [quality] - if: needs.quality.outputs.api == 'true' + windows-fast: + name: Windows x64 compile and spawn smoke + needs: quality runs-on: windows-2025 timeout-minutes: 15 steps: @@ -153,73 +45,15 @@ jobs: version: v2026.10.17 install_args: rust just cache: true - - uses: taiki-e/install-action@a4d3f3f761dcd95cce1b72cb61cb6d1963438177 # v2.87.30 - with: - tool: cargo-public-api@0.52.0 - - run: rustup toolchain install (Get-Content public-api/rust-toolchain -Raw).Trim() --profile minimal - - run: mise x -- just public-api - - proofs: - name: Proofs / ${{ matrix.layer }} - needs: [quality] - if: needs.quality.outputs.proofs != '[]' - strategy: - fail-fast: false - matrix: - layer: ${{ fromJSON(needs.quality.outputs.proofs) }} - runs-on: ubuntu-24.04 - timeout-minutes: 60 - steps: - - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 - with: - persist-credentials: false - - uses: dtolnay/rust-toolchain@683b588c487a69d01f6c6ddf40f036ff682cc2c8 # v1 - with: - toolchain: "1.99.1" - uses: Swatinem/rust-cache@d1527c8f67ef9af357290475d4af4b0fab8f12e0 # v2.9.3 - with: - key: ${{ matrix.layer }} - - name: Install Kani 0.68.0 - if: matrix.layer == 'kani' - run: | - curl --fail --location --silent --show-error --output kani.tar.gz \ - https://github.com/model-checking/kani/releases/download/kani-0.68.0/kani-0.68.0-x86_64-unknown-linux-gnu.tar.gz - echo "32e2b484d73ede0bbf64a2cf0879c4259422497d8aec4ee67d448de9ae7843d3 kani.tar.gz" | sha256sum --check - cargo install --locked kani-verifier --version 0.68.0 - cargo kani setup --use-local-bundle kani.tar.gz - - name: Install elan 4.2.4 - if: matrix.layer == 'lean' - run: | - curl --fail --location --silent --show-error --output elan.tar.gz \ - https://github.com/leanprover/elan/releases/download/v4.2.4/elan-x86_64-unknown-linux-gnu.tar.gz - echo "42b94d4244e8353142c456ec0e4ca6528fd898a6c604d4059f494e706e431f63 elan.tar.gz" | sha256sum --check - tar -xzf elan.tar.gz - ./elan-init -y --no-modify-path --default-toolchain none - echo "$HOME/.elan/bin" >> "$GITHUB_PATH" - - uses: actions/setup-java@b843ebf9b913146b38da2eaa7aeddf76074ae1ad # v6.1.0 - if: matrix.layer == 'tla' || matrix.layer == 'quint' || matrix.layer == 'alloy' - with: - distribution: temurin - java-version: "21" - - uses: actions/setup-node@949feb2413d6458794dcd2491c4babbbce0c15c1 # v7.1.0 - if: matrix.layer == 'quint' - with: - node-version: "24" - - name: Install SWI-Prolog - if: matrix.layer == 'prolog' - run: | - sudo apt-get update - sudo apt-get install --yes --no-install-recommends swi-prolog-nox - - env: - LAYER: ${{ matrix.layer }} - run: cargo xtask proofs "$LAYER" + - run: mise x -- just windows-smoke - package: - name: Package contents and build - needs: [quality] - if: needs.quality.outputs.package == 'true' - runs-on: windows-2025 - timeout-minutes: 15 + required: + name: required + if: always() + needs: [quality, windows-fast] + runs-on: ubuntu-24.04 + timeout-minutes: 5 steps: - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 with: @@ -227,40 +61,13 @@ jobs: - uses: jdx/mise-action@fc42bcc7ddbf51124c30f95a877a0c5168a3bfde with: version: v2026.10.17 - install_args: rust python uv + install_args: jq cache: true - - uses: Swatinem/rust-cache@d1527c8f67ef9af357290475d4af4b0fab8f12e0 # v2.9.3 - - run: mise x -- cargo xtask doc - - run: mise x -- cargo test --doc --locked - - run: mise x -- uv run --no-project --with 'reuse[charset-normalizer]==6.2.0' cargo xtask package-check - - required: - name: required - if: always() - needs: [quality, test, i686-smoke, arm64, verifier, api, proofs, package] - runs-on: ubuntu-24.04 - timeout-minutes: 5 - permissions: {} - steps: - - name: Require every selected check to succeed + - name: Require the ordinary checks to succeed env: RESULTS: ${{ toJSON(needs) }} - run: | - jq -e ' - def expected($selected): if $selected then "success" else "skipped" end; - .quality.outputs as $s | - ($s.proofs | fromjson) as $layers | - (keys | sort) == (["quality", "test", "i686-smoke", "arm64", "verifier", "api", "proofs", "package"] | sort) and - ([$s.native, $s.memory, $s.api, $s.package] | all(. == "true" or . == "false")) and - ($layers | type == "array") and - ($layers | all(IN("kani", "lean", "verus", "tla", "quint", "alloy", "prolog"))) and - (($layers | length) == ($layers | unique | length)) and - .quality.result == "success" and - (.test.result == expected($s.native == "true")) and - (."i686-smoke".result == expected($s.native == "true")) and - (.arm64.result == expected($s.native == "true")) and - (.verifier.result == expected($s.memory == "true")) and - (.api.result == expected($s.api == "true")) and - (.proofs.result == expected(($layers | length) > 0)) and - (.package.result == expected($s.package == "true")) - ' <<< "$RESULTS" + CONTRACT: | + type == "object" and + (keys | sort) == ["quality", "windows-fast"] and + all(.[]; type == "object" and .result == "success") + run: jq -e "$CONTRACT" <<< "$RESULTS" diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index c6d2ec7..a4a1fb5 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -5,7 +5,7 @@ # Publishes the version a maintainer's signed `vX.Y.Z` tag names. # -# * The tag rulesets let only the maintainer create a `v*` tag, and `candidate` refuses one that is not annotated and verified as signed. +# * The tag rulesets let only the maintainer create a `v*` tag, and `resolve` refuses one that is not annotated and verified as signed. # This file runs as the tagged commit has it, so those checks are defence in depth; the creation rule and the approval are the gates. # * `publish` deploys to the `crates-io` environment, which waits for the maintainer's approval. # crates.io's trusted publisher admits only that environment of this workflow, so nothing else can mint a publish token. @@ -18,33 +18,34 @@ name: Release permissions: {} +env: + RUSTUP_TOOLCHAIN: stable + concurrency: group: release-${{ github.ref }} cancel-in-progress: false jobs: - candidate: - name: Verify the tag and attest the release candidate + resolve: + name: Validate the tag and resolve the release revision if: github.repository == 'P4suta/windows-spawn' runs-on: windows-latest - timeout-minutes: 45 + timeout-minutes: 15 permissions: - artifact-metadata: write - attestations: write contents: read - id-token: write + outputs: + revision: ${{ steps.resolve.outputs.revision }} steps: - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 with: fetch-depth: 0 persist-credentials: false - - uses: dtolnay/rust-toolchain@683b588c487a69d01f6c6ddf40f036ff682cc2c8 # v1 - with: - toolchain: stable - - uses: taiki-e/install-action@a4d3f3f761dcd95cce1b72cb61cb6d1963438177 # v2.87.30 + - run: rustup toolchain install stable --profile minimal + - uses: jdx/mise-action@fc42bcc7ddbf51124c30f95a877a0c5168a3bfde with: - tool: cargo-cyclonedx@0.5.9 - - run: python -m pip install "reuse[charset-normalizer]==6.2.0" + version: v2026.10.17 + install_args: jq + cache: false - name: Require an annotated tag whose signature GitHub verified shell: bash env: @@ -64,6 +65,359 @@ jobs: fi - name: Verify the tag, its commit on main, and the Cargo version run: cargo xtask verify-release-tag "$env:GITHUB_REF_NAME" + - name: Export the verified revision + id: resolve + shell: pwsh + run: | + $revision = git rev-parse HEAD + if ($LASTEXITCODE -ne 0 -or $revision -cnotmatch '\A[0-9a-f]{40}\z') { + throw 'release revision must be a complete commit ID' + } + "revision=$revision" >> $env:GITHUB_OUTPUT + + qualify: + name: Qualify the release revision + if: always() + needs: [quality, test, i686-smoke, arm64, verifier, api, proofs] + runs-on: ubuntu-24.04 + timeout-minutes: 5 + permissions: + contents: read + steps: + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + with: + ref: ${{ needs.quality.outputs.revision }} + persist-credentials: false + - name: Require the release revision + env: + EXPECTED_REVISION: ${{ needs.quality.outputs.revision }} + run: | + set -euo pipefail + [[ "$EXPECTED_REVISION" =~ ^[0-9a-f]{40}$ ]] + test "$(git rev-parse HEAD)" = "$EXPECTED_REVISION" + - uses: jdx/mise-action@fc42bcc7ddbf51124c30f95a877a0c5168a3bfde + with: + version: v2026.10.17 + install_args: jq + cache: false + - name: Require complete release qualification + env: + RESULTS: ${{ toJSON(needs) }} + RELEASE_REVISION: ${{ needs.quality.outputs.revision }} + CONTRACT: | + type == "object" and + ($revision | test("\\A[0-9a-f]{40}\\z")) and + (keys | sort) == (["quality", "test", "i686-smoke", "arm64", "verifier", "api", "proofs"] | sort) and + .quality.outputs.revision == $revision and + (.quality.outputs.proofs | fromjson) == ["kani", "lean", "verus", "tla", "quint", "alloy", "prolog"] and + all(.[]; type == "object" and .result == "success") + run: jq -e --arg revision "$RELEASE_REVISION" "$CONTRACT" <<< "$RESULTS" + + quality: + name: Release repository checks + needs: resolve + runs-on: ubuntu-24.04 + timeout-minutes: 15 + permissions: + contents: read + env: + MISE_GITHUB_TOKEN: ${{ github.token }} + MISE_AUTO_INSTALL: "false" + RUSTUP_TOOLCHAIN: "1.99.1" + outputs: + revision: ${{ steps.selection.outputs.revision }} + proofs: ${{ steps.selection.outputs.proofs }} + steps: + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + with: + ref: ${{ needs.resolve.outputs.revision }} + persist-credentials: false + - name: Require the release revision + env: + EXPECTED_REVISION: ${{ needs.resolve.outputs.revision }} + run: | + set -euo pipefail + [[ "$EXPECTED_REVISION" =~ ^[0-9a-f]{40}$ ]] + test "$(git rev-parse HEAD)" = "$EXPECTED_REVISION" + - uses: jdx/mise-action@fc42bcc7ddbf51124c30f95a877a0c5168a3bfde + with: + version: v2026.10.17 + cache: false + - name: Select release qualification + id: selection + env: + RELEASE_REVISION: ${{ needs.resolve.outputs.revision }} + EVENT_NAME: ${{ github.event_name }} + EVENT_REF: ${{ github.ref }} + CONTRACT: | + if ($revision | test("\\A[0-9a-f]{40}\\z")) and $event == "push" and ($ref | test("\\Arefs/tags/v[0-9]+\\.[0-9]+\\.[0-9]+\\z")) then + {proofs: ["kani", "lean", "verus", "tla", "quint", "alloy", "prolog"], revision: $revision} + else + error("invalid release revision or event") + end + run: | + set -euo pipefail + selected=$(jq -n -c -e --arg revision "$RELEASE_REVISION" --arg event "$EVENT_NAME" --arg ref "$EVENT_REF" "$CONTRACT") + jq -r '"proofs=\(.proofs | tojson)\nrevision=\(.revision)"' <<< "$selected" >> "$GITHUB_OUTPUT" + - run: mise x -- uv run --no-project --with 'reuse[charset-normalizer]==6.2.0' just check + + test: + name: Release Windows / Rust ${{ matrix.rust }} + needs: [resolve, quality] + strategy: + fail-fast: false + matrix: + rust: ["1.99.1", "1.84.1"] + runs-on: windows-2025 + timeout-minutes: 30 + permissions: + contents: read + env: + RUSTUP_TOOLCHAIN: ${{ matrix.rust }} + steps: + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + with: + ref: ${{ needs.resolve.outputs.revision }} + persist-credentials: false + - name: Require the release revision + shell: bash + env: + EXPECTED_REVISION: ${{ needs.resolve.outputs.revision }} + run: | + set -euo pipefail + [[ "$EXPECTED_REVISION" =~ ^[0-9a-f]{40}$ ]] + test "$(git rev-parse HEAD)" = "$EXPECTED_REVISION" + - run: rustup toolchain install "$env:RUSTUP_TOOLCHAIN" --profile minimal + - if: matrix.rust != '1.84.1' + run: rustup component add clippy --toolchain "$env:RUSTUP_TOOLCHAIN" + - uses: jdx/mise-action@fc42bcc7ddbf51124c30f95a877a0c5168a3bfde + with: + version: v2026.10.17 + install_args: jq + cache: false + - uses: jdx/mise-action@fc42bcc7ddbf51124c30f95a877a0c5168a3bfde + if: matrix.rust != '1.84.1' + with: + version: v2026.10.17 + install_args: python uv + cache: false + - name: Lint the native Windows implementation + if: matrix.rust != '1.84.1' + run: cargo "+$env:RUSTUP_TOOLCHAIN" clippy --workspace --all-targets --locked -- -D warnings + - run: cargo "+$env:RUSTUP_TOOLCHAIN" xtask test + - name: Check documentation and package contents + if: matrix.rust != '1.84.1' + run: | + mise x -- cargo xtask doc + if ($LASTEXITCODE -ne 0) { exit $LASTEXITCODE } + mise x -- uv run --no-project --with 'reuse[charset-normalizer]==6.2.0' cargo xtask package-check + + i686-smoke: + name: Release Windows i686 execution smoke + needs: [resolve, quality] + runs-on: windows-2025 + timeout-minutes: 15 + permissions: + contents: read + env: + RUSTUP_TOOLCHAIN: "1.99.1" + steps: + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + with: + ref: ${{ needs.resolve.outputs.revision }} + persist-credentials: false + - name: Require the release revision + shell: bash + env: + EXPECTED_REVISION: ${{ needs.resolve.outputs.revision }} + run: | + set -euo pipefail + [[ "$EXPECTED_REVISION" =~ ^[0-9a-f]{40}$ ]] + test "$(git rev-parse HEAD)" = "$EXPECTED_REVISION" + - run: rustup toolchain install 1.99.1 --profile minimal --target i686-pc-windows-msvc + - run: >- + cargo +1.99.1 test --locked --target i686-pc-windows-msvc --test windows_spawn + pseudoconsole_regular_stdio_stays_off_parent_pipes -- --exact + + arm64: + name: Release Windows 11 ARM64 + needs: [resolve, quality] + runs-on: windows-11-arm + timeout-minutes: 20 + permissions: + contents: read + env: + RUSTUP_TOOLCHAIN: "1.99.1" + steps: + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + with: + ref: ${{ needs.resolve.outputs.revision }} + persist-credentials: false + - name: Require the release revision + shell: bash + env: + EXPECTED_REVISION: ${{ needs.resolve.outputs.revision }} + run: | + set -euo pipefail + [[ "$EXPECTED_REVISION" =~ ^[0-9a-f]{40}$ ]] + test "$(git rev-parse HEAD)" = "$EXPECTED_REVISION" + - run: rustup toolchain install 1.99.1 --profile minimal + - uses: jdx/mise-action@fc42bcc7ddbf51124c30f95a877a0c5168a3bfde + with: + version: v2026.10.17 + install_args: jq + cache: false + - run: cargo +1.99.1 xtask test + + verifier: + name: Release Application Verifier + needs: [resolve, quality] + runs-on: windows-latest + timeout-minutes: 30 + permissions: + contents: read + env: + RUSTUP_TOOLCHAIN: "1.99.1" + steps: + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + with: + ref: ${{ needs.resolve.outputs.revision }} + persist-credentials: false + - name: Require the release revision + shell: bash + env: + EXPECTED_REVISION: ${{ needs.resolve.outputs.revision }} + run: | + set -euo pipefail + [[ "$EXPECTED_REVISION" =~ ^[0-9a-f]{40}$ ]] + test "$(git rev-parse HEAD)" = "$EXPECTED_REVISION" + - run: rustup toolchain install 1.99.1 --profile minimal + - run: cargo +1.99.1 xtask verifier + + api: + name: Release Windows public API + needs: [resolve, quality] + runs-on: windows-2025 + timeout-minutes: 15 + permissions: + contents: read + env: + RUSTUP_TOOLCHAIN: "1.99.1" + steps: + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + with: + ref: ${{ needs.resolve.outputs.revision }} + persist-credentials: false + - name: Require the release revision + shell: bash + env: + EXPECTED_REVISION: ${{ needs.resolve.outputs.revision }} + run: | + set -euo pipefail + [[ "$EXPECTED_REVISION" =~ ^[0-9a-f]{40}$ ]] + test "$(git rev-parse HEAD)" = "$EXPECTED_REVISION" + - uses: jdx/mise-action@fc42bcc7ddbf51124c30f95a877a0c5168a3bfde + with: + version: v2026.10.17 + install_args: rust just + cache: false + - uses: taiki-e/install-action@a4d3f3f761dcd95cce1b72cb61cb6d1963438177 # v2.87.30 + with: + tool: cargo-public-api@0.52.0 + - run: rustup toolchain install (Get-Content public-api/rust-toolchain -Raw).Trim() --profile minimal + - run: mise x -- just public-api + + proofs: + name: Release proofs / ${{ matrix.layer }} + needs: [resolve, quality] + strategy: + fail-fast: false + matrix: + layer: ${{ fromJSON(needs.quality.outputs.proofs) }} + runs-on: ubuntu-24.04 + timeout-minutes: 60 + permissions: + contents: read + env: + RUSTUP_TOOLCHAIN: "1.99.1" + steps: + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + with: + ref: ${{ needs.resolve.outputs.revision }} + persist-credentials: false + - name: Require the release revision + env: + EXPECTED_REVISION: ${{ needs.resolve.outputs.revision }} + run: | + set -euo pipefail + [[ "$EXPECTED_REVISION" =~ ^[0-9a-f]{40}$ ]] + test "$(git rev-parse HEAD)" = "$EXPECTED_REVISION" + - run: rustup toolchain install 1.99.1 --profile minimal + - name: Install Kani 0.68.0 + if: matrix.layer == 'kani' + run: | + curl --fail --location --silent --show-error --output kani.tar.gz \ + https://github.com/model-checking/kani/releases/download/kani-0.68.0/kani-0.68.0-x86_64-unknown-linux-gnu.tar.gz + echo "32e2b484d73ede0bbf64a2cf0879c4259422497d8aec4ee67d448de9ae7843d3 kani.tar.gz" | sha256sum --check + cargo install --locked kani-verifier --version 0.68.0 + cargo kani setup --use-local-bundle kani.tar.gz + - name: Install elan 4.2.4 + if: matrix.layer == 'lean' + run: | + curl --fail --location --silent --show-error --output elan.tar.gz \ + https://github.com/leanprover/elan/releases/download/v4.2.4/elan-x86_64-unknown-linux-gnu.tar.gz + echo "42b94d4244e8353142c456ec0e4ca6528fd898a6c604d4059f494e706e431f63 elan.tar.gz" | sha256sum --check + tar -xzf elan.tar.gz + ./elan-init -y --no-modify-path --default-toolchain none + echo "$HOME/.elan/bin" >> "$GITHUB_PATH" + - uses: actions/setup-java@b843ebf9b913146b38da2eaa7aeddf76074ae1ad # v6.1.0 + if: matrix.layer == 'tla' || matrix.layer == 'quint' || matrix.layer == 'alloy' + with: + distribution: temurin + java-version: "21" + - uses: actions/setup-node@949feb2413d6458794dcd2491c4babbbce0c15c1 # v7.1.0 + if: matrix.layer == 'quint' + with: + node-version: "24" + package-manager-cache: false + - name: Install SWI-Prolog + if: matrix.layer == 'prolog' + run: | + sudo apt-get update + sudo apt-get install --yes --no-install-recommends swi-prolog-nox + - env: + LAYER: ${{ matrix.layer }} + run: cargo +1.99.1 xtask proofs "$LAYER" + + candidate: + name: Attest the qualified release candidate + needs: [resolve, qualify] + runs-on: windows-latest + timeout-minutes: 45 + permissions: + artifact-metadata: write # Store the candidate's attestation metadata. + attestations: write # Attach provenance and SBOM attestations to the candidate. + contents: read + id-token: write # Identify the workflow to the attestation service. + steps: + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + with: + ref: ${{ needs.resolve.outputs.revision }} + fetch-depth: 0 + persist-credentials: false + - name: Require the qualified revision + shell: bash + env: + EXPECTED_REVISION: ${{ needs.resolve.outputs.revision }} + run: | + set -euo pipefail + [[ "$EXPECTED_REVISION" =~ ^[0-9a-f]{40}$ ]] + test "$(git rev-parse HEAD)" = "$EXPECTED_REVISION" + - run: rustup toolchain install stable --profile minimal + - uses: taiki-e/install-action@a4d3f3f761dcd95cce1b72cb61cb6d1963438177 # v2.87.30 + with: + tool: cargo-cyclonedx@0.5.9 + - run: python -m pip install "reuse[charset-normalizer]==6.2.0" - name: Build and verify the release candidate id: candidate run: cargo xtask release-candidate --github-output @@ -96,14 +450,12 @@ jobs: url: https://crates.io/crates/windows-spawn permissions: contents: read - id-token: write + id-token: write # Authenticate this environment through crates.io trusted publishing. steps: - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 with: persist-credentials: false - - uses: dtolnay/rust-toolchain@683b588c487a69d01f6c6ddf40f036ff682cc2c8 # v1 - with: - toolchain: stable + - run: rustup toolchain install stable --profile minimal - uses: actions/download-artifact@9000827ccba6bdab643e8b6fd33ac0654aef8333 # v8.0.2 with: name: release-candidate @@ -152,14 +504,12 @@ jobs: runs-on: windows-latest timeout-minutes: 30 permissions: - contents: write + contents: write # Create the draft release and publish its complete asset set. steps: - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 with: persist-credentials: false - - uses: dtolnay/rust-toolchain@683b588c487a69d01f6c6ddf40f036ff682cc2c8 # v1 - with: - toolchain: stable + - run: rustup toolchain install stable --profile minimal - uses: actions/download-artifact@9000827ccba6bdab643e8b6fd33ac0654aef8333 # v8.0.2 with: name: release-candidate diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 484f73e..2014671 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -12,16 +12,19 @@ A change to ownership, handle inheritance, Job lifetime, ConPTY, mitigation, quo ## Development -Tests require Windows 10 version 1809 or later. +Native tests require Windows 10 version 1809 or later. The crate supports Rust 1.84 and later. -With the tool versions CI uses installed, run: +With the pinned tools installed, run the ordinary host checks: ```powershell -just ci -just coverage +mise x -- uv run --no-project --with 'reuse[charset-normalizer]==6.2.0' just check ``` -Also run: +The command includes strict library Clippy and the native smoke test on Windows. +`just windows-smoke` exposes those Windows checks for a focused investigation. +`just ci` remains a broader local suite for deliberate verification. +Coverage supports a specific investigation rather than every change. +Also check the diff and secrets: ```powershell actionlint @@ -61,23 +64,29 @@ cargo +nightly fuzz run environment-block -- -max_total_time=600 -max_len=16384 ``` `WINDOWS_SPAWN_RANDOM_SCALE` multiplies the number of random command lines and environments for a local investigation. -Hosted checks keep bounded native stress tests, careful, `Application Verifier`, proof layers, and the ordinary platform tests. -See [targeted assurance campaigns](docs/adr/targeted-assurance-campaigns.md) for the hosted verification policy. +Ordinary hosted checks run the Linux repository gate and Windows x64 smoke check on every pull request and merge group. +The signed-tag release workflow qualifies the exact commit with the full native, MSRV, architecture, API, package, and proof gates before building its candidate. +See [release-only heavy checks](docs/adr/release-only-heavy-checks.md) for the cadence and [CI selection](docs/ci.md) for commands and evidence boundaries. ## Expectations -- Keep the documented ownership and cleanup behavior, including on errors. -- Give every `unsafe` block a specific safety justification. -- Write only doc comments and `// SAFETY:` comments; the reason for a change goes in its commit message (ADR 0013). -- Write a lint exception as `#[expect(lint, reason = "…")]` on the one item it concerns; `just gates` refuses every `allow` and checks the other repository laws (ADR 0018). -- Add deterministic tests for behavior changes; tests wait for events, never for time (ADR 0010). -- Change the public API snapshot only with an API change, and state its compatibility impact. -- Update the crate docs, ADRs, or security boundary when a contract changes. -- Keep dependencies few and within the MSRV. +Keep the documented ownership and cleanup behavior, including on errors. +Give every `unsafe` block a specific safety justification. +Write only doc comments and `// SAFETY:` comments. +The reason for a change goes in its commit message, as [ADR 0013](docs/adr/0013-repository-laws-are-enforced-mechanically.md) requires. -Required checks and review threads must be resolved before merge. +Write a lint exception as `#[expect(lint, reason = "…")]` on the one item it concerns. +`just gates` refuses every `allow` and checks the other repository laws in [ADR 0018](docs/adr/0018-lint-exceptions-expire-and-the-msrv-is-rust-1-84.md). +Add deterministic tests for behavior changes. +Tests wait for events, never for time, as [ADR 0010](docs/adr/0010-time-decides-nothing.md) requires. + +Change the public API snapshot only with an API change, and state its compatibility impact. +Update the crate docs, ADRs, or security boundary when a contract changes. +Keep dependencies few and within the MSRV. + +Pass required checks and resolve review threads before merge. Pull requests are squash-merged into `main`. ## Check selection -See [CI selection](docs/ci.md) for the always-running gate, affected native and proof contracts, and local setup. +See [CI selection](docs/ci.md) for the ordinary gate, release qualification, and local setup. diff --git a/Cargo.lock b/Cargo.lock index 9139ae8..a231f4d 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -2,6 +2,12 @@ # It is not intended for manual editing. version = 4 +[[package]] +name = "arraydeque" +version = "0.5.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7d902e3d592a523def97af8f317b08ce16b7ab854c1985a0c671e6f15cebc236" + [[package]] name = "block-buffer" version = "0.10.4" @@ -46,6 +52,12 @@ dependencies = [ "crypto-common", ] +[[package]] +name = "foldhash" +version = "0.2.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "77ce24cb58228fbb8aa041425bb1050850ac19177686ea6e0f41a70416f56fdb" + [[package]] name = "generic-array" version = "0.14.7" @@ -56,6 +68,24 @@ dependencies = [ "version_check", ] +[[package]] +name = "hashbrown" +version = "0.16.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "841d1cc9bed7f9236f321df977030373f4a4163ae1a7dbfe1a51a2c1a51d9100" +dependencies = [ + "foldhash", +] + +[[package]] +name = "hashlink" +version = "0.11.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "824e001ac4f3012dd16a264bec811403a67ca9deb6c102fc5049b32c4574b35f" +dependencies = [ + "hashbrown", +] + [[package]] name = "itoa" version = "1.0.18" @@ -210,6 +240,17 @@ dependencies = [ "serde_json", "sha2", "windows-spawn", + "yaml-rust2", +] + +[[package]] +name = "yaml-rust2" +version = "0.11.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b36710ce3a279cfce8465dbab826f161675a262950b922cb2c3663852dfe9eb0" +dependencies = [ + "arraydeque", + "hashlink", ] [[package]] diff --git a/deny.toml b/deny.toml index 7ffbb89..04b7693 100644 --- a/deny.toml +++ b/deny.toml @@ -18,7 +18,7 @@ yanked = "deny" version = 2 allow = ["Apache-2.0", "MIT"] confidence-threshold = 1.0 -exceptions = [] +exceptions = [{ name = "foldhash", version = "=0.2.0", allow = ["Zlib"] }] include-build = true include-dev = true unused-allowed-license = "deny" diff --git a/docs/adr/release-only-heavy-checks.md b/docs/adr/release-only-heavy-checks.md new file mode 100644 index 0000000..e7c32a8 --- /dev/null +++ b/docs/adr/release-only-heavy-checks.md @@ -0,0 +1,73 @@ +--- +date: 2026-10-26 +status: proposed +--- + +# Release-only heavy checks + +## Status + +Proposed. +This partly supersedes the hosted cadence and path selection in [select checks by changed contract](select-checks-by-changed-contract.md). +The native contracts and proof obligations from the earlier decisions continue to apply. + +## Context + +Path selection avoids some unrelated verification, but workflow maintenance still selects native matrices and every proof layer. +Repeating those checks on each pull request makes a runner-label or workflow change trigger release-scale verification. +The native Windows boundary still needs an ordinary check because Linux exposes no Windows API. +The release must bind complete native and formal evidence to the same source that produces its candidate. + +## Decision + +Run the existing Linux repository checks and a Windows x64 smoke check on every pull request and merge group. +The Windows check uses strict library Clippy and `args_environment_cwd_and_wait_cache_work`. +The smoke test checks process creation, exit code 37, and repeated wait results after configuring arguments, environment, and working directory. +Its assertions establish that bounded process lifecycle rather than the full native contract. + +Run the full native suite on Rust 1.99.1 and 1.84.1, the i686 regression, and ARM64 tests at release qualification. +The same qualification requires the native `appverif.exe` checks, the public API snapshot, documentation, package checks, and all seven proof layers. +The current-Rust native job runs documentation, package, and license metadata checks together. +The native test command already runs Windows doctests. +Keep each proof layer's complete inventory, implementation correspondence checks, and negative controls. +The [proof guide](../../proofs/README.md) preserves the distinction between bounded code checks, models, refinement checks, and native observations. + +Resolve the annotated release tag only after checking its signature, GitHub's verification result, commit on main, and Cargo version. +Require every qualification checkout's `HEAD` to match the resolver's full 40-character commit SHA. +The release workflow runs Linux quality and all six heavy roles on the resolved source. +The full native job covers the ordinary Windows smoke test and its compilation checks, so release qualification omits the separate smoke job. +The qualification summary requires successful results from exactly those seven roles and the complete seven-layer proof inventory. +Require successful qualification before building the release candidate. +Preserve the existing candidate, publication, and draft GitHub Release boundaries. +Missing, failed, cancelled, or skipped evidence must stop the release. +The ordinary workflow contains only Linux quality, Windows smoke verification, and `required`. +Its summary requires successful results from exactly the two verification jobs. +Move the heavy job definitions into the release workflow without duplicating them or adding a reusable or manual campaign entry point. + +The workflow tests parse the production YAML and execute its jq contracts. +Keep `yaml-rust2` at 0.11.1 because versions 0.12 and 0.13 require Rust 1.85 while the workspace supports Rust 1.84. +The dependency update rule excludes those incompatible versions and protects the release workflow's MSRV declaration. +The parser's transitive `foldhash` 0.2.0 dependency uses the Zlib license. +Accept that exact dependency in `deny.toml` while keeping the general `Apache-2.0` and `MIT` policy and checking development dependencies. + +Keep `just check` as the ordinary host command, including the Windows smoke check on Windows. +Keep `just windows-smoke` for the native job and focused local checks, and keep `just ci` as a broader explicit local suite. +Coverage, broad stress, allocation poisoning, fuzzing, and mutation remain tools for a specific investigation. +Add no scheduled campaign. +Changes to a verified decision still update its proof, model, or vectors in the same change. + +Keeping path-selected heavy jobs on pull requests would preserve the repeated release-scale cost for workflow maintenance. +Deleting those jobs would lose evidence for supported native contracts. +Leaving them to unrelated manual runs would fail to bind their results to the released commit. + +## Consequences + +Every change retains Linux verification and a native Windows signal. +The release waits for the full platform and proof inventory on one source commit. +Defects outside the ordinary smoke check may emerge during focused local verification or release qualification. +Contributors must choose focused tests when changing the affected native or modeled contract. + +The smoke test doesn't prove argument, environment, or working-directory round trips. +The proof layers keep the limits stated in their existing models and implementation links. +Source-contract tests can check job dependencies, source binding, and aggregation, but native and hosted adapters still need execution evidence. +An unrun qualification or publication stage supplies no passing result. diff --git a/docs/adr/select-checks-by-changed-contract.md b/docs/adr/select-checks-by-changed-contract.md index aeeb53c..2195d8b 100644 --- a/docs/adr/select-checks-by-changed-contract.md +++ b/docs/adr/select-checks-by-changed-contract.md @@ -9,18 +9,20 @@ status: accepted Accepted. This partly supersedes [targeted assurance campaigns](targeted-assurance-campaigns.md). +The proposed [release-only heavy checks](release-only-heavy-checks.md) decision partly supersedes the hosted cadence and path selection below. +The native contracts, proof inventories, negative controls, and strict aggregation remain required. ## Context -Every pull request currently repeats two Windows generations, two Rust versions, all seven proof layers, stress, allocation poisoning, Application Verifier, coverage, and reproducible release candidates. -Documentation and tooling changes do not alter every native or modeled contract. +Before path selection, every pull request repeated two Windows generations, two Rust versions, all seven proof layers, stress, allocation poisoning, native `appverif.exe` checks, coverage, and reproducible release candidates. +Documentation and tooling changes don't alter every native or modeled contract. Push verification repeats the pull request checks, while scheduled CodeQL scans repeat unchanged source. ## Decision -Run the deterministic Linux gate on every pull request and merge group, and select extra checks using [contract filters](../../.github/filters/ci.yml). -Keep native Rust 1.84.1 and current-toolchain execution, 32-bit execution, ARM64 execution, API snapshots, Application Verifier, packaging, and the individual proof layers for their affected inputs. -Aggregate exact expected job results and reject missing, invalid, failed, cancelled, or unexpectedly skipped work. +Run the deterministic Linux gate on every pull request and merge group, and select extra checks using `.github/filters/ci.yml`. +Keep native Rust 1.84.1 and current-toolchain execution, 32-bit execution, ARM64 execution, API snapshots, native `appverif.exe` checks, packaging, and the individual proof layers for their affected inputs. +Require the exact expected job results and reject missing, invalid, failed, or cancelled work, and skips that selection doesn't permit. Keep complete proof inventories and their negative controls inside each selected layer. Keep broad stress, coverage, and allocation poisoning as local investigation tools. @@ -34,7 +36,8 @@ Requiring private machines would make a contributor's merge verdict depend on un ## Consequences -Contributors retain the same project commands and supported native contracts. -Changes to contract boundaries must update their filters and verify both selection and the strict aggregate. -The OS, GitHub event, and external tool adapters still require native or hosted verification; selection checks do not prove Win32 behavior. +Contributors keep the same project commands and supported native contracts. +Changes to contract boundaries must update their filters and verify both selection and the strict summary. +The OS, GitHub event, and external tool adapters still require native or hosted verification. +Selection checks don't prove Win32 behavior. Reassess removed instrumentation when a concrete defect or new boundary needs it. diff --git a/docs/ci.md b/docs/ci.md index d7a9de8..4c170bd 100644 --- a/docs/ci.md +++ b/docs/ci.md @@ -1,34 +1,63 @@ # CI selection `CI` runs on pull requests and merge groups. -One Ubuntu 24.04 job always runs formatting, Clippy, repository laws, unit and integration tests available on Linux, the empty non-Windows API check, dependency policy, REUSE, typos, and actionlint. +Every change runs the Linux repository checks and a Windows x64 smoke check. +The Linux job runs formatting, Clippy, repository laws, supported unit and integration tests, the empty non-Windows API check, dependency policy, license metadata checks, Typos, and Actionlint. `mise.toml` pins its tools. The pinned mise action verifies each platform's binary with the release's signed checksums. -Windows-only doctests run with the native Windows tests; Linux still executes all supported unit and integration targets. -[The path filters](../.github/filters/ci.yml) select additional contracts. +The Windows job runs strict library Clippy and the existing [`args_environment_cwd_and_wait_cache_work` test](../tests/windows_spawn.rs). +The test configures arguments, an environment value, and a working directory before spawning a child. +Its assertions check exit code 37 and the same result from repeated waits. +The full native suite supplies broader Windows verification at release qualification. -| Contract | Selected verification | -| --- | --- | -| Native source, tests, build inputs, or replay vectors | Windows Clippy, x64 tests on Rust 1.84.1 and 1.99.1, i686 ConPTY regression, native ARM64 tests | -| Native ownership or memory boundary | Windows Application Verifier, including its misuse controls | -| Library API or snapshot toolchain | Windows public API snapshot | -| Package contents, documentation, or packaging command | Windows documentation, doctests, and package contents and build check | -| A decision core or proof input | Only the corresponding Kani, Lean, Verus, TLA+, Quint, Alloy, or Prolog layer | +The `required` job requires both ordinary jobs to succeed. +Its dependency set contains exactly those two jobs. +Missing results, cancellation, failure, and skips refuse the gate. -The `required` job accepts only a successful fast job and the exact expected success or skip for every selected contract. -Missing results, malformed flags, unknown or duplicate proof layers, cancellation, failure, and skipping a selected job refuse the gate. -Proof commands retain their complete expected inventories, source links, and negative controls. -Changing selection or workflow configuration requires checking those filters and the aggregate, without repeating unrelated proof models. +## Local checks -Run commands through `mise x -- just COMMAND` locally. -`just ci` remains the complete ordinary local suite on Windows. -Install Rust 1.84 with rustup for `just msrv`, the three Windows MSVC targets for `just cross-targets`, and the toolchain in `public-api/rust-toolchain` plus cargo-public-api 0.52.0 for `just public-api`. -`just reuse` needs the pinned REUSE environment: `mise x -- uv run --no-project --with 'reuse[charset-normalizer]==6.2.0' cargo xtask reuse`. -Windows execution requires Windows; Application Verifier additionally requires its SDK tool and administrative rights. +Run the ordinary checks with the pinned Python environment: + +```powershell +mise x -- uv run --no-project --with 'reuse[charset-normalizer]==6.2.0' just check +``` + +`just check` runs the repository checks available on the host and includes the native smoke check on Windows. +`just windows-smoke` runs the Windows job's checks for a focused native investigation. +`just ci` remains a broader local suite for deliberate verification. +Use `mise x -- just COMMAND` for other project recipes. +Install Rust 1.84 with rustup for `just msrv` and the three Windows Microsoft Visual C++ targets for `just cross-targets`. +`just public-api` needs the toolchain in `public-api/rust-toolchain` and cargo-public-api 0.52.0. +`just reuse` needs the pinned Python environment: `mise x -- uv run --no-project --with 'reuse[charset-normalizer]==6.2.0' cargo xtask reuse`. +Native execution requires Windows. +`just verifier` also needs the Windows SDK tool `appverif.exe` and administrative rights. + +## Release qualification + +The [release workflow](../.github/workflows/release.yml) validates the annotated tag, GitHub's signature-verification result, the commit's ancestry on main, and the Cargo version. +Its resolver emits the full 40-character commit SHA. +Every qualification checkout verifies that `HEAD` matches that SHA. +The release runs Linux quality and six heavy qualification roles. +The full native job includes the ordinary Windows smoke test and its compilation checks. +The `qualify` job requires successful results from exactly those seven roles and the complete seven-layer proof inventory. +Missing results, invalid proof-layer data, unknown or duplicate layers, cancellation, failure, and skips refuse qualification. +The candidate waits for both the resolver and qualification, then checks out the resolver's commit. +The existing publication and draft-release stages follow the candidate. + +Full qualification runs native tests on Rust 1.99.1 and 1.84.1, the i686 regression, ARM64 tests, the native verifier, and the public API snapshot. +The current-Rust native job also checks documentation, package contents and build, and license metadata through its pinned environment. +The native test command includes its Windows doctests. +All seven proof layers run: Kani, Lean, Verus, `TLA+`, Quint, Alloy, and Prolog. +Each layer keeps its complete expected inventory, source correspondence checks, and negative controls. +The [proof guide](../proofs/README.md) states each model's scope and connection to the implementation. + +Each candidate must supply evidence from every required gate. +Source-contract checks can't establish Windows behavior, model refinement, or GitHub's hosted permissions and event handling. +The [release-only heavy-check decision](adr/release-only-heavy-checks.md) records the cadence and its tradeoffs. Coverage, allocation poisoning, broad cleanup stress, fuzzing, and mutation support a specific local investigation. They have no recurring hosted campaign. -The protected release workflow retains reproducible candidates and publication evidence. -Rust 1.84 compatibility remains explicit; sha2 stays below 0.11 while that workspace contract applies. +Rust 1.84 compatibility remains explicit. +sha2 stays below 0.11 while that workspace contract applies. The public API nightly has one declaration shared by installation and snapshot generation, which Renovate tracks as a Rust toolchain file. diff --git a/justfile b/justfile index 332e6dc..3ca23f6 100644 --- a/justfile +++ b/justfile @@ -3,6 +3,12 @@ set windows-shell := ["powershell.exe", "-NoLogo", "-NoProfile", "-ExecutionPoli default: @just --list +check: + cargo xtask check + +windows-smoke: + cargo xtask windows-smoke + fmt: cargo xtask fmt @@ -52,7 +58,7 @@ mutation: cargo xtask mutation proofs *layers: - cargo xtask proofs {{layers}} + cargo xtask proofs {{ layers }} proof-traces: cargo xtask proof-traces diff --git a/mise.lock b/mise.lock index 308d58c..b198c33 100644 --- a/mise.lock +++ b/mise.lock @@ -89,6 +89,41 @@ checksum = "sha256:975a22143262fd27476d19ee00c7af67978426e40e1dee94eed6bbade1cf8 url = "https://github.com/EmbarkStudios/cargo-deny/releases/download/0.20.2/cargo-deny-0.20.2-x86_64-pc-windows-msvc.tar.gz" url_api = "https://api.github.com/repos/EmbarkStudios/cargo-deny/releases/assets/471599057" +[[tools.jq]] +version = "1.8.2" +backend = "aqua:jqlang/jq" +specifiers = ["1.8.2"] + +[tools.jq."platforms.linux-arm64"] +checksum = "sha256:8b85c817833814ddca00a144c33705546355afccf0cf39b188f3cdb48b852309" +url = "https://github.com/jqlang/jq/releases/download/jq-1.8.2/jq-linux-arm64" +url_api = "https://api.github.com/repos/jqlang/jq/releases/assets/453012756" +provenance = "github-attestations" + +[tools.jq."platforms.linux-x64"] +checksum = "sha256:b1c22172dd303f3be49e935aa56aa48a8b7a46e0bc838b4997d3bb451495870f" +url = "https://github.com/jqlang/jq/releases/download/jq-1.8.2/jq-linux-amd64" +url_api = "https://api.github.com/repos/jqlang/jq/releases/assets/453012752" +provenance = "github-attestations" + +[tools.jq."platforms.macos-arm64"] +checksum = "sha256:2d75340ba57a4b4b4c8708a21c2dc8e958a48aaa8bba13b27f77f6e4c0eca07e" +url = "https://github.com/jqlang/jq/releases/download/jq-1.8.2/jq-macos-arm64" +url_api = "https://api.github.com/repos/jqlang/jq/releases/assets/453012783" +provenance = "github-attestations" + +[tools.jq."platforms.windows-arm64"] +checksum = "sha256:a6fc67fedaf9128a3309a1e2ebb8b986aeccf70122ee46d2cb4849e423f0c627" +url = "https://github.com/jqlang/jq/releases/download/jq-1.8.2/jq-windows-amd64.exe" +url_api = "https://api.github.com/repos/jqlang/jq/releases/assets/453012788" +provenance = "github-attestations" + +[tools.jq."platforms.windows-x64"] +checksum = "sha256:a6fc67fedaf9128a3309a1e2ebb8b986aeccf70122ee46d2cb4849e423f0c627" +url = "https://github.com/jqlang/jq/releases/download/jq-1.8.2/jq-windows-amd64.exe" +url_api = "https://api.github.com/repos/jqlang/jq/releases/assets/453012788" +provenance = "github-attestations" + [[tools.just]] version = "1.59.0" backend = "aqua:casey/just" diff --git a/mise.toml b/mise.toml index 2bd13b3..02cb28f 100644 --- a/mise.toml +++ b/mise.toml @@ -6,3 +6,4 @@ typos = "1.51.1" cargo-deny = "0.20.2" python = "3.15.1" uv = "0.13.5" +jq = "1.8.2" diff --git a/xtask/Cargo.toml b/xtask/Cargo.toml index 7111299..71c3cde 100644 --- a/xtask/Cargo.toml +++ b/xtask/Cargo.toml @@ -11,8 +11,11 @@ semver = "1.0.28" serde_json = "1.0.151" sha2 = "0.10.9" +[dev-dependencies] +yaml-rust2 = { version = "=0.11.1", default-features = false } + [target.'cfg(windows)'.dependencies] -windows-spawn = { path = ".." } +windows-spawn = { path = "..", version = "0.1.0" } [lints] workspace = true diff --git a/xtask/src/cli.rs b/xtask/src/cli.rs index a26fdb9..d301094 100644 --- a/xtask/src/cli.rs +++ b/xtask/src/cli.rs @@ -2,6 +2,8 @@ use std::path::PathBuf; #[derive(Clone, Copy, Debug, Eq, PartialEq)] pub(crate) enum SimpleTask { + Check, + WindowsSmoke, Fmt, Clippy, Gates, @@ -84,6 +86,8 @@ pub(crate) fn parse(arguments: impl IntoIterator) -> Result = arguments.collect(); match command.as_str() { + "check" => no_arguments(&rest, Task::Simple(SimpleTask::Check)), + "windows-smoke" => no_arguments(&rest, Task::Simple(SimpleTask::WindowsSmoke)), "fmt" => no_arguments(&rest, Task::Simple(SimpleTask::Fmt)), "clippy" => no_arguments(&rest, Task::Simple(SimpleTask::Clippy)), "gates" => no_arguments(&rest, Task::Simple(SimpleTask::Gates)), @@ -239,6 +243,22 @@ mod tests { values.iter().map(ToString::to_string).collect() } + #[test] + fn local_fast_commands_accept_only_their_exact_entrypoints() { + for (command, expected) in [ + ("check", SimpleTask::Check), + ("windows-smoke", SimpleTask::WindowsSmoke), + ] { + assert_eq!(parse(strings(&[command])).unwrap(), Task::Simple(expected)); + for argument in ["extra", "--allow-dirty", "--", "--skip-tests"] { + assert!( + parse(strings(&[command, argument])).is_err(), + "{command} {argument}" + ); + } + } + } + #[test] fn parses_flags_and_forwarded_mutation_arguments() { assert_eq!( diff --git a/xtask/src/tasks.rs b/xtask/src/tasks.rs index 1b965d7..d142a21 100644 --- a/xtask/src/tasks.rs +++ b/xtask/src/tasks.rs @@ -80,6 +80,33 @@ impl From for TaskError { } const PACKAGE_NAME: &str = "windows-spawn"; +const WINDOWS_SMOKE_TEST: &str = "args_environment_cwd_and_wait_cache_work"; +const CLIPPY_ARGUMENTS: &[&str] = &[ + "clippy", + "--workspace", + "--all-targets", + "--locked", + "--", + "-D", + "warnings", +]; +const WORKSPACE_TEST_ARGUMENTS: &[&str] = &[ + "test", + "--workspace", + "--all-targets", + "--locked", + "--", + "--test-threads=1", +]; +const LINUX_EMPTY_ARGUMENTS: &[&str] = &[ + "check", + "--package", + PACKAGE_NAME, + "--all-targets", + "--locked", + "--target", + "x86_64-unknown-linux-gnu", +]; const PUBLIC_API_TOOLCHAIN: &str = include_str!("../../public-api/rust-toolchain"); /// The target whose API the snapshot records, named so that every host renders the same snapshot. const PUBLIC_API_TARGET: &str = "x86_64-pc-windows-msvc"; @@ -133,6 +160,7 @@ fn print_help() { println!( "\ Repository tasks: + cargo xtask check|windows-smoke cargo xtask fmt|clippy|gates|test|doc|msrv|cross-targets|linux-empty cargo xtask supply-chain|reuse|typos|coverage|ci cargo xtask public-api [--update] @@ -150,29 +178,13 @@ Repository tasks: fn run_simple(root: &Path, task: SimpleTask) -> Result<()> { match task { + SimpleTask::Check => run_check(root), + SimpleTask::WindowsSmoke => run_windows_smoke(root), SimpleTask::Fmt => run_cargo(root, &["fmt", "--all", "--", "--check"]), - SimpleTask::Clippy => run_cargo( - root, - &[ - "clippy", - "--workspace", - "--all-targets", - "--locked", - "--", - "-D", - "warnings", - ], - ), + SimpleTask::Clippy => run_cargo(root, CLIPPY_ARGUMENTS), SimpleTask::Test => { let mut targets = cargo(root); - with_vectors(&mut targets).args([ - "test", - "--workspace", - "--all-targets", - "--locked", - "--", - "--test-threads=1", - ]); + with_vectors(&mut targets).args(WORKSPACE_TEST_ARGUMENTS); run(&mut targets)?; if !cfg!(windows) { return Ok(()); @@ -213,21 +225,11 @@ fn run_simple(root: &Path, task: SimpleTask) -> Result<()> { } Ok(()) } - SimpleTask::LinuxEmpty => run_cargo( + SimpleTask::LinuxEmpty => run_cargo(root, LINUX_EMPTY_ARGUMENTS), + SimpleTask::SupplyChain => run_cargo( root, - &[ - "check", - "--package", - PACKAGE_NAME, - "--all-targets", - "--locked", - "--target", - "x86_64-unknown-linux-gnu", - ], + &["deny", "--workspace", "--all-features", "--locked", "check"], ), - SimpleTask::SupplyChain => { - run_cargo(root, &["deny", "--all-features", "--locked", "check"]) - } SimpleTask::Reuse => run_program(root, "python", &["-m", "reuse", "lint"]), SimpleTask::Typos => run_program(root, "typos", &[]), SimpleTask::Coverage => coverage(root), @@ -236,6 +238,93 @@ fn run_simple(root: &Path, task: SimpleTask) -> Result<()> { } } +fn run_check(root: &Path) -> Result<()> { + if !cfg!(any(windows, target_os = "linux")) { + return fail("check requires a native Windows or Linux host"); + } + let target = ordinary_target(root); + run_simple(root, SimpleTask::Fmt)?; + run(ordinary_cargo(root, &target).args(CLIPPY_ARGUMENTS))?; + run_simple(root, SimpleTask::Gates)?; + if cfg!(windows) { + run(ordinary_cargo(root, &target).args(["test", "--package", "xtask", "--locked"]))?; + run_windows_smoke_test(root, &target)?; + } else { + let mut tests = ordinary_cargo(root, &target); + with_vectors(&mut tests).args(WORKSPACE_TEST_ARGUMENTS); + run(&mut tests)?; + run(ordinary_cargo(root, &target).args(LINUX_EMPTY_ARGUMENTS))?; + } + for check in [ + SimpleTask::SupplyChain, + SimpleTask::Reuse, + SimpleTask::Typos, + ] { + run_simple(root, check)?; + } + run_program(root, "actionlint", &[]) +} + +fn run_windows_smoke(root: &Path) -> Result<()> { + if !cfg!(windows) { + return fail("windows-smoke requires a native Windows host"); + } + let target = ordinary_target(root); + run(ordinary_cargo(root, &target).args([ + "clippy", + "--package", + PACKAGE_NAME, + "--lib", + "--locked", + "--", + "-D", + "warnings", + ]))?; + run_windows_smoke_test(root, &target) +} + +fn run_windows_smoke_test(root: &Path, target: &Path) -> Result<()> { + let mut listing = windows_smoke_command(root, target); + listing.args(["--list", "--format", "terse"]); + require_windows_smoke_selection(&capture(&mut listing)?)?; + run(&mut windows_smoke_command(root, target)) +} + +fn require_windows_smoke_selection(listing: &str) -> Result<()> { + if listing.trim() == format!("{WINDOWS_SMOKE_TEST}: test") { + Ok(()) + } else { + fail("expected exactly one Windows smoke test in the terse test inventory") + } +} + +fn windows_smoke_command(root: &Path, target: &Path) -> Command { + let mut command = ordinary_cargo(root, target); + command.args([ + "test", + "--locked", + "--test", + "windows_spawn", + WINDOWS_SMOKE_TEST, + "--", + "--exact", + "--test-threads=1", + ]); + command +} + +fn ordinary_target(root: &Path) -> PathBuf { + let selected = + env::var_os("CARGO_TARGET_DIR").map_or_else(|| root.join("target"), PathBuf::from); + root.join(selected).join("ordinary-checks") +} + +fn ordinary_cargo(root: &Path, target: &Path) -> Command { + let mut command = cargo(root); + command.env("CARGO_TARGET_DIR", target); + command +} + fn run_gates(root: &Path) -> Result<()> { let findings = gates::check(root)?; for finding in &findings { @@ -1005,6 +1094,58 @@ mod tests { use super::*; use serde_json::json; + #[test] + fn windows_smoke_selection_requires_the_single_exact_test() { + let expected = format!("{WINDOWS_SMOKE_TEST}: test"); + assert!(require_windows_smoke_selection(&expected).is_ok()); + assert!(require_windows_smoke_selection(&format!("{expected}\r\n")).is_ok()); + for listing in [ + String::new(), + "0 tests, 0 benchmarks".to_owned(), + "different_test: test".to_owned(), + format!("{WINDOWS_SMOKE_TEST}: benchmark"), + format!("{expected}\n{expected}"), + format!("{expected}\nanother_test: test"), + ] { + let error = require_windows_smoke_selection(&listing).unwrap_err(); + assert!(error.to_string().contains("exactly one Windows smoke test")); + } + } + + #[test] + fn windows_smoke_command_keeps_its_exact_test_and_child_target() { + let root = repository_root().unwrap(); + let target = root.join("target/ordinary-checks"); + let command = windows_smoke_command(&root, &target); + let arguments: Vec<_> = command.get_args().collect(); + assert_eq!( + arguments, + [ + "test", + "--locked", + "--test", + "windows_spawn", + WINDOWS_SMOKE_TEST, + "--", + "--exact", + "--test-threads=1", + ] + .map(OsStr::new) + ); + assert_eq!(command.get_current_dir(), Some(root.as_path())); + assert!(command.get_envs().any(|(name, value)| { + name == "CARGO_TARGET_DIR" && value == Some(target.as_os_str()) + })); + } + + #[cfg(not(windows))] + #[test] + fn windows_smoke_rejects_non_windows_before_starting_cargo() { + let missing = env::temp_dir().join("windows-spawn-missing-smoke-root"); + let error = run_windows_smoke(&missing).unwrap_err(); + assert!(error.to_string().contains("native Windows host")); + } + #[test] fn selects_only_the_root_manifest_package() { let root = repository_root().unwrap(); diff --git a/xtask/tests/ci_workflow.rs b/xtask/tests/ci_workflow.rs new file mode 100644 index 0000000..98e7a78 --- /dev/null +++ b/xtask/tests/ci_workflow.rs @@ -0,0 +1,951 @@ +// SPDX-FileCopyrightText: 2026 Yasunobu Sakashita +// SPDX-License-Identifier: MIT OR Apache-2.0 + +//! Evaluates the actual workflow contracts and their release-source bindings. + +use std::fmt; +use std::io::{BufRead as _, BufReader, Write as _}; +use std::path::{Path, PathBuf}; +use std::process::{Child, Command, Output, Stdio}; +use std::sync::atomic::{AtomicU64, Ordering}; + +use serde_json::{json, Value}; +use yaml_rust2::{Yaml, YamlLoader}; + +#[derive(Debug)] +enum CheckError { + Io(std::io::Error), + Yaml(yaml_rust2::ScanError), + Json(serde_json::Error), + Contract(String), +} + +impl fmt::Display for CheckError { + fn fmt(&self, formatter: &mut fmt::Formatter<'_>) -> fmt::Result { + match self { + Self::Io(error) => error.fmt(formatter), + Self::Yaml(error) => error.fmt(formatter), + Self::Json(error) => error.fmt(formatter), + Self::Contract(message) => formatter.write_str(message), + } + } +} + +impl std::error::Error for CheckError { + fn source(&self) -> Option<&(dyn std::error::Error + 'static)> { + match self { + Self::Io(error) => Some(error), + Self::Yaml(error) => Some(error), + Self::Json(error) => Some(error), + Self::Contract(_) => None, + } + } +} + +impl From for CheckError { + fn from(error: std::io::Error) -> Self { + Self::Io(error) + } +} + +impl From for CheckError { + fn from(error: yaml_rust2::ScanError) -> Self { + Self::Yaml(error) + } +} + +impl From for CheckError { + fn from(error: serde_json::Error) -> Self { + Self::Json(error) + } +} + +impl From<&str> for CheckError { + fn from(message: &str) -> Self { + Self::Contract(message.into()) + } +} + +impl From for CheckError { + fn from(message: String) -> Self { + Self::Contract(message) + } +} + +type Result = std::result::Result; + +const CI: &str = ".github/workflows/ci.yml"; +const RELEASE: &str = ".github/workflows/release.yml"; +const LAYERS: [&str; 7] = ["kani", "lean", "verus", "tla", "quint", "alloy", "prolog"]; +const JOBS: [&str; 7] = [ + "quality", + "test", + "i686-smoke", + "arm64", + "verifier", + "api", + "proofs", +]; +const RELEASE_REF: &str = "${{ needs.resolve.outputs.revision }}"; +const REVISION: &str = "0123456789abcdef0123456789abcdef01234567"; + +fn root() -> PathBuf { + Path::new(env!("CARGO_MANIFEST_DIR")).join("..") +} + +fn yaml(path: &str) -> Result { + parse(&std::fs::read_to_string(root().join(path))?) +} + +fn parse(source: &str) -> Result { + let mut documents = YamlLoader::load_from_str(source)?.into_iter(); + let document = documents.next().ok_or("missing YAML document")?; + require( + documents.next().is_none(), + "one workflow document is required", + )?; + Ok(document) +} + +fn require(condition: bool, message: &str) -> Result { + if condition { + Ok(()) + } else { + Err(message.into()) + } +} + +fn field<'a>(node: &'a Yaml, key: &str) -> Result<&'a Yaml> { + node.as_hash() + .and_then(|mapping| mapping.get(&Yaml::String(key.into()))) + .ok_or_else(|| format!("missing YAML field {key}").into()) +} + +fn text(node: &Yaml) -> Result<&str> { + node.as_str().ok_or_else(|| "expected YAML string".into()) +} + +fn array(node: &Yaml) -> Result<&[Yaml]> { + node.as_vec() + .map(Vec::as_slice) + .ok_or_else(|| "expected YAML sequence".into()) +} + +fn job<'a>(workflow: &'a Yaml, name: &str) -> Result<&'a Yaml> { + field(field(workflow, "jobs")?, name) +} + +fn steps(job: &Yaml) -> Result<&[Yaml]> { + array(field(job, "steps")?) +} + +fn step<'a>(job: &'a Yaml, id: &str) -> Result<&'a Yaml> { + steps(job)? + .iter() + .find(|step| { + field(step, "id") + .and_then(text) + .is_ok_and(|actual| actual == id) + }) + .ok_or_else(|| format!("missing production step {id}").into()) +} + +fn contract_step(job: &Yaml) -> Result<&Yaml> { + let step = steps(job)? + .iter() + .find(|step| { + field(step, "env") + .and_then(|env| field(env, "CONTRACT")) + .is_ok() + }) + .ok_or("missing production contract")?; + require( + text(field(step, "run")?)?.contains("\"$CONTRACT\""), + "the actual shell must execute the contract", + )?; + Ok(step) +} + +fn contract(job: &Yaml) -> Result<&str> { + text(field(field(contract_step(job)?, "env")?, "CONTRACT")?) +} + +fn names(node: &Yaml) -> Result> { + if let Some(name) = node.as_str() { + Ok(vec![name]) + } else { + array(node)?.iter().map(text).collect() + } +} + +fn needs(job: &Yaml) -> Result> { + names(field(job, "needs")?) +} + +fn summary_input(release: bool) -> Value { + let mut results = serde_json::Map::new(); + for name in if release { + JOBS.as_slice() + } else { + &["quality", "windows-fast"] + } { + let _previous = results.insert((*name).into(), json!({"result":"success"})); + } + if release { + let _previous = results.insert( + "quality".into(), + json!({"result":"success", "outputs": { + "revision": REVISION, "proofs": json!(LAYERS).to_string() + }}), + ); + } + Value::Object(results) +} + +fn summary(needs: &Value, release: bool) -> Result { + summary_revision(needs, release, REVISION) +} + +fn summary_revision(needs: &Value, release: bool, revision: &str) -> Result { + let workflow = yaml(if release { RELEASE } else { CI })?; + let required = job(&workflow, if release { "qualify" } else { "required" })?; + let input = serde_json::to_vec(needs)?; + let mut child = Command::new("jq") + .args(["-e", "--arg", "revision", revision, contract(required)?]) + .stdin(Stdio::piped()) + .stdout(Stdio::piped()) + .stderr(Stdio::piped()) + .spawn()?; + write_summary_input(&mut child, &input)?; + Ok(child.wait_with_output()?) +} + +fn write_summary_input(child: &mut Child, input: &[u8]) -> Result { + with_summary_input(child, |child| { + child + .stdin + .take() + .ok_or("missing jq stdin")? + .write_all(input)?; + Ok(()) + }) +} + +fn with_summary_input(child: &mut Child, write: impl FnOnce(&mut Child) -> Result) -> Result { + match write(child) { + Ok(()) => Ok(()), + Err(primary) => { + cleanup_summary_child(child, &primary); + Err(primary) + } + } +} + +fn cleanup_summary_child(child: &mut Child, primary: &CheckError) { + if let Err(error) = child.kill() { + eprintln!("could not terminate jq after summary input error ({primary}): {error}"); + } + if let Err(error) = child.wait() { + eprintln!("could not reap jq after summary input error ({primary}): {error}"); + } +} + +fn waiting_summary_child() -> Result { + let mut child = Command::new("jq") + .args(["-n", "--unbuffered", "\"ready\", input"]) + .stdin(Stdio::piped()) + .stdout(Stdio::piped()) + .stderr(Stdio::piped()) + .spawn()?; + let ready = (|| -> Result { + let stdout = child.stdout.take().ok_or("missing fixture stdout")?; + let mut line = String::new(); + BufReader::new(stdout).read_line(&mut line)?; + require(line.trim() == "\"ready\"", "jq fixture must become ready") + })(); + if let Err(primary) = ready { + cleanup_summary_child(&mut child, &primary); + return Err(primary); + } + Ok(child) +} + +#[test] +fn summary_input_write_failure_reaps_live_child() -> Result { + let mut child = waiting_summary_child()?; + let result = with_summary_input(&mut child, |_child| { + Err(CheckError::Io(std::io::Error::new( + std::io::ErrorKind::BrokenPipe, + "injected summary write failure", + ))) + }); + let status = child.try_wait(); + if !matches!(status, Ok(Some(_))) { + cleanup_summary_child(&mut child, &CheckError::from("fixture cleanup")); + } + assert!(matches!(result, Err(CheckError::Io(ref error)) + if error.kind() == std::io::ErrorKind::BrokenPipe + && error.to_string() == "injected summary write failure")); + assert!( + status?.is_some(), + "the failed summary write must terminate and reap its live child" + ); + Ok(()) +} + +#[test] +fn summary_input_missing_stdin_reaps_live_child() -> Result { + let mut child = waiting_summary_child()?; + let held_input = child.stdin.take(); + let result = write_summary_input(&mut child, b"{}"); + let status = child.try_wait(); + if !matches!(status, Ok(Some(_))) { + cleanup_summary_child(&mut child, &CheckError::from("fixture cleanup")); + } + drop(held_input); + assert!( + matches!(result, Err(CheckError::Contract(ref message)) if message == "missing jq stdin") + ); + assert!( + status?.is_some(), + "missing summary stdin must terminate and reap its live child" + ); + Ok(()) +} + +#[test] +fn ordinary_ci_edit_does_not_select_heavy_windows_jobs() -> Result { + let workflow = yaml(CI)?; + let mut selected = 0_usize; + for (name, variants) in [ + ("test", 2), + ("i686-smoke", 1), + ("arm64", 1), + ("api", 1), + ("package", 1), + ] { + if job(&workflow, name).is_ok() { + selected = selected.checked_add(variants).ok_or("job count overflow")?; + } + } + assert_eq!( + selected, 0, + "an ordinary CI edit retains {selected} heavy Windows variants in the PR workflow" + ); + assert!( + !root().join(".github/filters/ci.yml").exists(), + "ordinary selection must not retain path filters" + ); + let jobs = field(&workflow, "jobs")? + .as_hash() + .ok_or("jobs must be a mapping")?; + let mut job_names = jobs.keys().map(text).collect::>>()?; + job_names.sort_unstable(); + assert_eq!(job_names, ["quality", "required", "windows-fast"]); + let events = field(&workflow, "on")? + .as_hash() + .ok_or("events must be a mapping")?; + let mut event_names = events.keys().map(text).collect::>>()?; + event_names.sort_unstable(); + assert_eq!(event_names, ["merge_group", "pull_request"]); + for name in ["quality", "windows-fast"] { + assert!( + field(job(&workflow, name)?, "if").is_err(), + "{name} remains mandatory" + ); + } + Ok(()) +} + +#[test] +fn actual_summary_programs_cover_every_terminal_result() -> Result { + for (release, count) in [(false, 16), (true, 16384)] { + let workflow = yaml(if release { RELEASE } else { CI })?; + let production = contract(job( + &workflow, + if release { "qualify" } else { "required" }, + )?)?; + let inventory = if release { + json!(JOBS) + } else { + json!(["quality", "windows-fast"]) + }; + let program = format!( + r#" + def production: {production}; + {inventory} as $names | + def cases: + range(0; {count}) as $encoded | + [range(0; ($names | length)) | ["success", "failure", "cancelled", "skipped"] + [(($encoded / pow(4; .) | floor) % 4)]] as $results | + (reduce range(0; ($names | length)) as $i ({{}}; .[$names[$i]] = {{result: $results[$i]}})) | + (if {release} then .quality.outputs = {{revision: $revision, proofs: (["kani","lean","verus","tla","quint","alloy","prolog"] | tojson)}} else . end) as $input | + if ($input | production) == ($results | all(. == "success")) + then 1 else error("production summary accepted an incorrect terminal result") end; + reduce cases as $case (0; . + $case) == {count} + "# + ); + let output = Command::new("jq") + .args(["-en", "--arg", "revision", REVISION, &program]) + .output()?; + assert!(output.status.success(), "{output:?}"); + assert_eq!( + serde_json::from_slice::(&output.stdout)?, + json!(true) + ); + } + Ok(()) +} + +#[test] +fn summaries_reject_missing_unknown_unfinished_and_malformed_results() -> Result { + for release in [false, true] { + let healthy = summary_input(release); + assert!(summary(&healthy, release)?.status.success()); + for name in if release { + JOBS.as_slice() + } else { + &["quality", "windows-fast"] + } { + let mut missing = healthy.clone(); + let _removed = missing + .as_object_mut() + .ok_or("needs must be an object")? + .remove(*name); + assert!( + !summary(&missing, release)?.status.success(), + "missing {name}" + ); + for result in [ + json!(null), + json!("queued"), + json!("in_progress"), + json!("unknown"), + json!(true), + ] { + let mut invalid = healthy.clone(); + *invalid + .pointer_mut(&format!("/{name}/result")) + .ok_or("result field")? = result; + assert!( + !summary(&invalid, release)?.status.success(), + "invalid {name}: {invalid}" + ); + } + } + let mut unknown = healthy.clone(); + let _previous = unknown + .as_object_mut() + .ok_or("needs must be an object")? + .insert("unexpected".into(), json!({"result":"success"})); + assert!(!summary(&unknown, release)?.status.success()); + for value in [json!(null), json!([]), json!("invalid"), json!({})] { + assert!(!summary(&value, release)?.status.success()); + } + } + Ok(()) +} + +fn bash() -> Result { + if cfg!(windows) { + Ok( + PathBuf::from(std::env::var_os("ProgramFiles").ok_or("missing ProgramFiles")?) + .join("Git/bin/bash.exe"), + ) + } else { + Ok(PathBuf::from("bash")) + } +} + +fn release_selection() -> Result { + Ok(step(job(&yaml(RELEASE)?, "quality")?, "selection")?.clone()) +} + +fn select_release(revision: &str, event: &str, reference: &str) -> Result { + let selection = release_selection()?; + Ok(Command::new("jq") + .args([ + "-n", "-c", "-e", "--arg", "revision", revision, "--arg", "event", event, "--arg", + "ref", reference, + ]) + .arg(text(field(field(&selection, "env")?, "CONTRACT")?)?) + .output()?) +} + +fn selection_shell( + revision: Option<&str>, + event: &str, + reference: &str, +) -> Result<(Output, String)> { + static NEXT: AtomicU64 = AtomicU64::new(0); + let directory = std::env::temp_dir().join(format!( + "windows-spawn-ci-{}-{}", + std::process::id(), + NEXT.fetch_add(1, Ordering::Relaxed) + )); + std::fs::create_dir(&directory)?; + let path = directory.join("outputs"); + let selection = release_selection()?; + let mut command = Command::new(bash()?); + command + .args(["-c", text(field(&selection, "run")?)?]) + .env_remove("RELEASE_REVISION") + .env("EVENT_NAME", event) + .env("EVENT_REF", reference) + .env("GITHUB_OUTPUT", &path) + .env( + "CONTRACT", + text(field(field(&selection, "env")?, "CONTRACT")?)?, + ); + if let Some(revision) = revision { + command.env("RELEASE_REVISION", revision); + } + let output = command.output(); + let contents = match std::fs::read_to_string(&path) { + Ok(contents) => { + std::fs::remove_file(&path)?; + Ok(contents) + } + Err(error) if error.kind() == std::io::ErrorKind::NotFound => Ok(String::new()), + Err(error) => Err(error), + }; + std::fs::remove_dir(directory)?; + Ok((output?, contents?)) +} + +#[test] +fn release_selector_accepts_only_complete_revision_and_version_tag_event_shape() -> Result { + let output = select_release(REVISION, "push", "refs/tags/v1.2.3")?; + assert!(output.status.success(), "{output:?}"); + assert_eq!( + serde_json::from_slice::(&output.stdout)?, + json!({"revision":REVISION,"proofs":LAYERS}) + ); + let selection = release_selection()?; + let env = field(&selection, "env")?; + assert_eq!(text(field(env, "RELEASE_REVISION")?)?, RELEASE_REF); + assert_eq!(text(field(env, "EVENT_NAME")?)?, "${{ github.event_name }}"); + assert_eq!(text(field(env, "EVENT_REF")?)?, "${{ github.ref }}"); + for revision in [ + String::new(), + "a".repeat(39), + "a".repeat(41), + "A".repeat(40), + "main".into(), + format!("{REVISION}\n"), + ] { + assert!( + !select_release(&revision, "push", "refs/tags/v1.2.3")? + .status + .success(), + "invalid revision {revision:?}" + ); + } + for (event, reference) in [ + ("pull_request", "refs/tags/v1.2.3"), + ("merge_group", "refs/tags/v1.2.3"), + ("workflow_call", "refs/tags/v1.2.3"), + ("workflow_dispatch", "refs/tags/v1.2.3"), + ("push", "refs/heads/main"), + ("push", "refs/tags/v1.2"), + ("push", "refs/tags/v1.2.3-rc.1"), + ("push", "refs/tags/v1.2.3\n"), + ] { + assert!( + !select_release(REVISION, event, reference)?.status.success(), + "invalid release event {event}/{reference:?}" + ); + } + Ok(()) +} + +#[test] +fn actual_release_selector_shell_fails_closed_and_renders_exact_outputs() -> Result { + let (valid_output, valid_contents) = + selection_shell(Some(REVISION), "push", "refs/tags/v1.2.3")?; + assert!(valid_output.status.success(), "{valid_output:?}"); + let expected = format!("proofs={}\nrevision={REVISION}\n", json!(LAYERS)); + assert_eq!( + valid_contents.lines().collect::>(), + expected.lines().collect::>() + ); + for revision in [None, Some(""), Some("main")] { + let (output, contents) = selection_shell(revision, "push", "refs/tags/v1.2.3")?; + assert!( + !output.status.success(), + "invalid revision {revision:?}: {output:?}" + ); + assert!( + contents.is_empty(), + "invalid revision emitted outputs: {contents}" + ); + assert!( + !String::from_utf8_lossy(&output.stderr).contains("command not found"), + "the actual jq engine must run" + ); + } + Ok(()) +} + +#[test] +fn qualification_rejects_missing_mismatched_or_malformed_release_identity() -> Result { + let healthy = summary_input(true); + for revision in [ + String::new(), + "main".into(), + "a".repeat(39), + "A".repeat(40), + format!("{REVISION}\n"), + ] { + assert!( + !summary_revision(&healthy, true, &revision)? + .status + .success(), + "invalid revision argument {revision:?}" + ); + let mut matching = healthy.clone(); + *matching + .pointer_mut("/quality/outputs/revision") + .ok_or("revision fixture")? = json!(revision); + assert!( + !summary_revision(&matching, true, &revision)? + .status + .success(), + "invalid matching revision {revision:?}" + ); + } + for (path, value) in [ + ("/quality/outputs/revision", json!(null)), + ("/quality/outputs/revision", json!("a".repeat(40))), + ("/quality/outputs/proofs", json!(null)), + ("/quality/outputs/proofs", json!("invalid")), + ("/quality/outputs/proofs", json!("{}")), + ("/quality/outputs/proofs", json!("[]")), + ("/quality/outputs/proofs", json!("[\"kani\",\"kani\"]")), + ("/quality/outputs/proofs", json!("[\"unknown\"]")), + ] { + let mut invalid = healthy.clone(); + *invalid + .pointer_mut(path) + .ok_or("missing identity fixture field")? = value; + assert!( + !summary(&invalid, true)?.status.success(), + "invalid identity {invalid}" + ); + } + Ok(()) +} + +#[test] +fn actual_summary_shells_reject_skipped_or_missing_mandatory_work() -> Result { + for release in [false, true] { + let workflow = yaml(if release { RELEASE } else { CI })?; + let required = job(&workflow, if release { "qualify" } else { "required" })?; + let step = contract_step(required)?; + for results in [summary_input(release), json!({})] { + let output = Command::new(bash()?) + .args(["-c", text(field(step, "run")?)?]) + .env("RESULTS", results.to_string()) + .env("RELEASE_REVISION", REVISION) + .env("CONTRACT", contract(required)?) + .output()?; + assert_eq!( + output.status.success(), + results == summary_input(release), + "{output:?}" + ); + assert!( + !String::from_utf8_lossy(&output.stderr).contains("command not found"), + "the actual jq engine must run" + ); + } + } + Ok(()) +} + +fn checkout(job: &Yaml) -> Result<&Yaml> { + steps(job)? + .iter() + .find(|step| { + field(step, "uses") + .and_then(text) + .is_ok_and(|uses| uses.starts_with("actions/checkout@")) + }) + .ok_or_else(|| "missing checkout".into()) +} + +fn validate_revision(job: &Yaml, reference: &str) -> Result { + require( + text(field(field(checkout(job)?, "with")?, "ref")?)? == reference, + "checkout must use the resolved revision", + )?; + require( + steps(job)?.iter().any(|step| { + field(step, "run").and_then(text).is_ok_and(|script| { + script.contains("git rev-parse HEAD") + && script.contains("EXPECTED_REVISION") + && script.contains("[0-9a-f]{40}") + }) && field(step, "env") + .and_then(|env| field(env, "EXPECTED_REVISION")) + .and_then(text) + .is_ok_and(|value| value == reference) + }), + "checkout must verify actual HEAD against the resolved revision", + ) +} + +#[test] +fn actual_release_head_guard_rejects_empty_mismatched_and_newline_revisions() -> Result { + let release = yaml(RELEASE)?; + let quality = job(&release, "quality")?; + let guard = steps(quality)? + .iter() + .find(|step| { + field(step, "env") + .and_then(|env| field(env, "EXPECTED_REVISION")) + .is_ok() + }) + .ok_or("missing actual revision guard")?; + let script = text(field(guard, "run")?)?; + let actual = Command::new("git") + .args(["rev-parse", "HEAD"]) + .current_dir(root()) + .output()?; + assert!(actual.status.success(), "{actual:?}"); + let head = String::from_utf8_lossy(&actual.stdout).trim().to_owned(); + let check = |revision: &str| -> Result { + Ok(Command::new(bash()?) + .args(["-c", script]) + .env("EXPECTED_REVISION", revision) + .current_dir(root()) + .output()?) + }; + assert!( + check(&head)?.status.success(), + "the actual checked-out HEAD must pass" + ); + for invalid in [ + String::new(), + "a".repeat(40), + head.to_ascii_uppercase(), + format!("{head}\n"), + ] { + let output = check(&invalid)?; + assert!( + !output.status.success(), + "invalid expected HEAD {invalid:?}" + ); + assert!( + !String::from_utf8_lossy(&output.stderr).contains("command not found"), + "the actual git engine must run" + ); + } + Ok(()) +} + +fn validate_release(release: &Yaml) -> Result { + let events = field(release, "on")?.as_hash().ok_or("release events")?; + require( + events.len() == 1 && field(field(release, "on")?, "push").is_ok(), + "release qualification is tag-push only", + )?; + require( + names(field(field(field(release, "on")?, "push")?, "tags")?)? == ["v[0-9]+.[0-9]+.[0-9]+"], + "release qualification uses version tags", + )?; + let resolve = job(release, "resolve")?; + require( + text(field(field(resolve, "outputs")?, "revision")?)? + == "${{ steps.resolve.outputs.revision }}", + "resolver publishes the checked revision", + )?; + let resolver = text(field(step(resolve, "resolve")?, "run")?)?; + require( + resolver.contains("git rev-parse HEAD") + && resolver.contains("[0-9a-f]{40}") + && resolver.contains("GITHUB_OUTPUT"), + "resolver emits a complete commit ID", + )?; + let scripts = steps(resolve)? + .iter() + .filter_map(|step| field(step, "run").and_then(text).ok()) + .collect::>() + .join("\n"); + require( + scripts.contains(".object.type") + && scripts.contains(".verification.verified") + && scripts.contains("cargo xtask verify-release-tag"), + "verified annotated-tag, main, and version guards precede qualification", + )?; + for name in JOBS { + let job = job(release, name)?; + require( + needs(job)?.contains(&"resolve"), + "qualification depends on the checked resolver", + )?; + validate_revision(job, RELEASE_REF)?; + } + let repository_checks = job(release, "quality")?; + for output in ["revision", "proofs"] { + require( + text(field(field(repository_checks, "outputs")?, output)?)? + == format!("${{{{ steps.selection.outputs.{output} }}}}"), + "quality publishes the actual selector outputs", + )?; + } + require( + text(field( + field(field(job(release, "proofs")?, "strategy")?, "matrix")?, + "layer", + )?)? == "${{ fromJSON(needs.quality.outputs.proofs) }}", + "release matrix must execute the selected exact proof inventory", + )?; + let qualify = job(release, "qualify")?; + let qualified_revision = "${{ needs.quality.outputs.revision }}"; + validate_revision(qualify, qualified_revision)?; + require( + text(field( + field(contract_step(qualify)?, "env")?, + "RELEASE_REVISION", + )?)? == qualified_revision, + "summary checks the selected release revision", + )?; + let mut actual = needs(qualify)?; + actual.sort_unstable(); + let mut expected = JOBS; + expected.sort_unstable(); + require( + actual == expected, + "qualification summary requires the exact seven jobs", + )?; + require( + text(field(qualify, "if")?)? == "always()", + "qualification summary must report failures", + )?; + let candidate = job(release, "candidate")?; + let mut dependencies = needs(candidate)?; + dependencies.sort_unstable(); + require( + dependencies == ["qualify", "resolve"], + "candidate requires resolver and qualification", + )?; + validate_revision(candidate, RELEASE_REF)?; + require( + needs(job(release, "publish")?)?.contains(&"candidate"), + "publication depends on candidate", + )?; + require( + needs(job(release, "github-release")?)?.contains(&"publish"), + "GitHub release follows crate publication", + ) +} + +fn replace_yaml(node: &mut Yaml, path: &[&str], replacement: Yaml) -> Result { + let (first, rest) = path.split_first().ok_or("empty YAML mutation path")?; + let value = node + .as_mut_hash() + .and_then(|mapping| mapping.get_mut(&Yaml::String((*first).into()))) + .ok_or("missing YAML mutation field")?; + if rest.is_empty() { + *value = replacement; + Ok(()) + } else { + replace_yaml(value, rest, replacement) + } +} + +#[test] +fn release_inventory_and_candidate_chain_reject_broken_bindings() -> Result { + let release = yaml(RELEASE)?; + validate_release(&release)?; + for (path, replacement) in [ + ( + vec!["jobs", "quality", "needs"], + Yaml::String("candidate".into()), + ), + ( + vec!["jobs", "candidate", "needs"], + Yaml::Array(vec![Yaml::String("resolve".into())]), + ), + ( + vec!["jobs", "publish", "needs"], + Yaml::String("resolve".into()), + ), + ( + vec!["jobs", "github-release", "needs"], + Yaml::String("candidate".into()), + ), + ( + vec!["jobs", "resolve", "outputs", "revision"], + Yaml::String("${{ github.sha }}".into()), + ), + ( + vec!["jobs", "proofs", "strategy", "matrix", "layer"], + Yaml::Array(vec![ + Yaml::String("kani".into()), + Yaml::String("kani".into()), + ]), + ), + ] { + let mut broken = release.clone(); + replace_yaml(&mut broken, &path, replacement)?; + assert!( + validate_release(&broken).is_err(), + "accepted broken release path {path:?}" + ); + } + let mut broken = release; + let jobs = broken + .as_mut_hash() + .and_then(|mapping| mapping.get_mut(&Yaml::String("jobs".into()))) + .and_then(Yaml::as_mut_hash) + .ok_or("jobs")?; + let candidate = jobs + .get_mut(&Yaml::String("candidate".into())) + .ok_or("candidate")?; + let steps = candidate + .as_mut_hash() + .and_then(|mapping| mapping.get_mut(&Yaml::String("steps".into()))) + .and_then(Yaml::as_mut_vec) + .ok_or("candidate steps")?; + let checkout = steps + .iter_mut() + .find(|step| { + field(step, "uses") + .and_then(text) + .is_ok_and(|value| value.starts_with("actions/checkout@")) + }) + .ok_or("candidate checkout")?; + replace_yaml(checkout, &["with", "ref"], Yaml::String("main".into()))?; + assert!( + validate_release(&broken).is_err(), + "candidate must reject a moving checkout ref" + ); + Ok(()) +} + +#[test] +fn mandatory_summary_inventory_matches_the_actual_needs() -> Result { + let workflow = yaml(CI)?; + let required = job(&workflow, "required")?; + let mut actual = needs(required)?; + actual.sort_unstable(); + assert_eq!(actual, ["quality", "windows-fast"]); + assert_eq!(text(field(required, "if")?)?, "always()"); + let windows = job(&workflow, "windows-fast")?; + assert!(steps(windows)?.iter().any(|step| field(step, "run") + .and_then(text) + .is_ok_and(|script| script.contains("just windows-smoke")))); + Ok(()) +} + +#[test] +fn yaml_adapter_preserves_on_and_rejects_duplicate_or_multiple_documents() -> Result { + let workflow = parse("on:\n pull_request:\njobs: {}\n")?; + assert!(field(field(&workflow, "on")?, "pull_request").is_ok()); + assert!(parse("on: {}\non: {}\n").is_err()); + assert!(parse("jobs:\n quality: {}\n quality: {}\n").is_err()); + assert!(parse("---\njobs: {}\n---\njobs: {}\n").is_err()); + assert!(parse("jobs: [broken\n").is_err()); + Ok(()) +}